From fdd0c896cb4e88ee571856b71b3af2a8270f11f3 Mon Sep 17 00:00:00 2001
From: chihebabid <chiheb.abid@fst.utm.tn>
Date: Sun, 3 Jul 2022 17:19:33 +0100
Subject: [PATCH] Fix NDFS initialization
---
src/algorithm/CNDFS.cpp | 22 +++++++++-------------
src/algorithm/CNDFS.h | 15 +++++++--------
2 files changed, 16 insertions(+), 21 deletions(-)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index f05c86b..6786df6 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -22,6 +22,7 @@ using namespace std;
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh)
{
+ getInitialState();
spawnThreads();
}
@@ -43,22 +44,17 @@ void CNDFS::spawnThreads() {
}
void CNDFS::threadHandler(void *context) {
- _state* state = ((CNDFS *) context)->getInitialState();
- ((CNDFS *) context)->dfsBlue(state);
+ ((CNDFS *) context)->dfsBlue(((CNDFS *) context)->mInitStatePtr);
}
//get initial state of the product automata
-_state* CNDFS::getInitialState(){
- mMutex.lock();
- _state * initStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
- initStatePtr->left = mMcl->getInitialMetaState();
- initStatePtr->right = mAa->get_init_state();
- initStatePtr->new_successors = static_cast<vector<pair<_state *, int>>>(NULL);
- initStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
- initStatePtr->isConstructed = true;
- mMutex.unlock();
-// sharedPool.push_back(make_pair(initStatePtr->left,initStatePtr->right));
- return initStatePtr;
+void CNDFS::getInitialState(){
+ mInitStatePtr = new _state; //static_cast<_state *>(malloc(sizeof(_state)));
+ mInitStatePtr->left = mMcl->getInitialMetaState();
+ mInitStatePtr->right = mAa->get_init_state();
+ //mInitStatePtr->new_successors = nullptr;
+ mInitStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
+ mInitStatePtr->isConstructed = true;
}
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 5859d35..f4b189c 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -20,28 +20,28 @@ struct myState{
LDDState *left;
const spot::twa_graph_state* right;
vector<pair<struct myState*, int>> new_successors;
- atomic_bool isAcceptance {false};
- atomic_bool isConstructed {false};
+ atomic<bool> isAcceptance {false};
+ atomic<bool> isConstructed {false};
bool cyan {false};
- atomic_bool blue {false};
- atomic_bool red {false};
+ atomic<bool> blue {false};
+ atomic<bool> red {false};
};
typedef struct myState _state; // @alias
class CNDFS {
-
private:
static constexpr uint8_t MAX_THREADS=64;
ModelCheckBaseMT * mMcl;
spot::twa_graph_ptr mAa;
uint16_t mNbTh;
atomic<uint8_t> mIdThread;
- static void threadHandler(void *context);
std::thread* mlThread[MAX_THREADS];
mutex mMutex;
condition_variable cv;
void spawnThreads();
-
+ _state * mInitStatePtr;
+ void getInitialState();
+ static void threadHandler(void *context);
public:
// typedef myState _state;
@@ -53,7 +53,6 @@ public:
virtual ~CNDFS();
void computeSuccessors(_state *state);
void dfsBlue(_state *state);
- _state* getInitialState();
void dfsRed(_state* state, deque<_state*> mydeque);
void WaitForTestCompleted(_state* state);
atomic_bool awaitCondition(_state* state,deque<_state*> mydeque);
--
GitLab