Skip to content
Snippets Groups Projects
Commit fdd0c896 authored by chihebabid's avatar chihebabid
Browse files

Fix NDFS initialization

parent 6fc23102
No related branches found
No related tags found
1 merge request!6Feature/ufscc emptiness check
Pipeline #5032 passed
......@@ -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;
}
......
......@@ -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);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment