diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 73e186f1a5171a4e677b67f3f3855bdd2a2e7eda..c983e66022f572224c56b62a8ca6eb947414fd0e 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -11,17 +11,16 @@
#include <utility>
#include <spot/twa/twa.hh>
#include <bddx.h>
-#include <cstddef>
#include <deque>
#include <atomic>
#include <condition_variable>
-#include "misc/SafeDequeue.h"
+#include <algorithm>
#include "misc/stacksafe.h"
using namespace std;
-CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh)
-{
+CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
+ mNbTh(nbTh) {
getInitialState();
spawnThreads();
}
@@ -46,168 +45,151 @@ void CNDFS::spawnThreads() {
void CNDFS::threadHandler(void *context) {
((CNDFS *) context)->threadRun();
}
+
void CNDFS::threadRun() {
uint16_t idThread = mIdThread++;
- vector<myState_t*> Rp;
- dfsBlue(mInitStatePtr,Rp,idThread);
+ vector<myState_t *> Rp;
+ dfsBlue(mInitStatePtr, Rp, idThread);
}
-//get initial state of the product automata
-void CNDFS::getInitialState(){
- mInitStatePtr = new myState_t; //static_cast<_state *>(malloc(sizeof(_state)));
+/*
+ * Build initial state of the product automata
+ */
+void CNDFS::getInitialState() {
+ mInitStatePtr = new myState_t;
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;
+ mlBuiltStates.push_back(mInitStatePtr);
}
//this function is to build a state with list of successor initially null
-myState_t* CNDFS::buildState(LDDState* left, spot::state* right, bool acc, bool constructed, bool cyan){
- myState_t * buildStatePtr = new myState_t;
+myState_t *CNDFS::buildState(LDDState *left, spot::state *right, bool acc, bool constructed, bool cyan) {
+ myState_t *buildStatePtr = new myState_t;
buildStatePtr->left = left;
- buildStatePtr->right = dynamic_cast<const spot::twa_graph_state *>(right);
+ buildStatePtr->right = (spot::twa_graph_state *) right;
buildStatePtr->isAcceptance = acc;
buildStatePtr->isConstructed = constructed;
-
return buildStatePtr;
}
-std::ostream & operator<<(std::ostream & Str,myState_t* state) {
- Str << "({ Sog state= " << state->left << ", BA state= " << state->right << ", acceptance= " << state->isAcceptance << ", constructed= " << state->isConstructed << ", red= " << state->red << ", blue= " << state->blue << " }" << endl;
- int i = 0;
- for (const auto & ii : state->new_successors)
- {
- cout << "succ num " << i << ii.first << " with transition " << ii.second<< endl;
- i++;
- }
+std::ostream &operator<<(std::ostream &Str, myState_t *state) {
+ Str << "({ Sog state= " << state->left << ", BA state= " << state->right << ", acceptance= " << state->isAcceptance
+ << ", constructed= " << state->isConstructed << ", red= " << state->red << ", blue= " << state->blue << " }"
+ << endl;
+ int i = 0;
+ for (const auto &ii: state->new_successors) {
+ cout << "succ num " << i << ii.first << " with transition " << ii.second << endl;
+ i++;
+ }
return Str;
}
-
-
-//block all threads while awaitCondition is false
-//void CNDFS::WaitForTestCompleted(_state* state) {
-// while ( awaitCondition(state) == false) ;
-//}
-
-void CNDFS::dfsRed(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread)
-{
+void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread) {
cout << "dfsRed" << endl;
Rp.push_back(state);
computeSuccessors(state);
- for (const auto& succ:state->new_successors) {
- if (succ.first->cyan[idThread])
- {
- cout << "cycle detected" << endl;
- exit(0);
- }
- // unvisited and not red state
- if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && ! succ.first->red )
- dfsRed(succ.first, Rp,idThread);
+ for (const auto &succ: state->new_successors) {
+ if (succ.first->cyan[idThread]) {
+ cout << "cycle detected" << endl;
+ exit(0);
+ }
+ // unvisited and not red state
+ if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && !succ.first->red)
+ dfsRed(succ.first, Rp, idThread);
}
}
+/*
+ * Check whether a product state exists or not
+ */
+myState_t *CNDFS::isStateBuilt(LDDState *sogState, spot::twa_graph_state *spotState) {
+ auto compare = [sogState, spotState](myState_t *state) {
+ return (state->left == sogState && state->right == spotState);
+ };
+ auto result = find_if(begin(mlBuiltStates), end(mlBuiltStates), compare);
+ return result == end(mlBuiltStates) ? nullptr : *result;
+}
+
//compute new successors of a product state
-void CNDFS::computeSuccessors(myState_t *state)
-{
- auto sog_current_state = state->left;
- const spot::twa_graph_state* ba_current_state = state->right;
+void CNDFS::computeSuccessors(myState_t *state) {
+ if (state->succState == SuccState::built) return;
+ std::unique_lock lk(mMutexStatus);
+ if (state->succState == SuccState::beingbuilt) {
+ mMutexStatus.unlock();
+ mDataCondWait.wait(lk, [state] { return state->succState == SuccState::built; });
+ return;
+ }
+ state->succState = SuccState::beingbuilt;
+ lk.unlock();
+ auto sog_current_state = state->left;
+ const spot::twa_graph_state *ba_current_state = state->right;
while (!sog_current_state->isCompletedSucc());
auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
//fetch the state's atomic proposition
- for (const auto & vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
- {
- auto name = string(mMcl->getPlace(vv));
- auto f = spot::formula::ap(name);
- transitionNames.push(f);
+ /* for (const auto & vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
+ {
+ auto name = string(mMcl->getPlace(vv));
+ auto f = spot::formula::ap(name);
+ transitionNames.push(f);
- }
+ }*/
//iterate over the successors of a current aggregate
- for (const auto &elt : sog_current_state->Successors)
- {
+ for (const auto &elt: sog_current_state->Successors) {
auto transition = elt.second; // je récupère le numéro du transition
auto name = string(mMcl->getTransition(transition)); // récuprer le nom de la transition
auto f = spot::formula::ap(name);// récuperer la proposition atomique qui correspond à la transition
- transitionNames.push(f); // push state'S AP to edge'S AP
-
- SafeDequeue<spot::formula> tempTransitionNames = transitionNames;
- while (!tempTransitionNames.empty())
- {
- //iterate over the successors of a BA state
- auto ii = mAa->succ_iter(ba_current_state);
- if (ii->first())
- do {
- if (p->var_map.find(tempTransitionNames.front()) !=p->var_map.end())
- {
- //fetch the transition of BA that have the same AP as the SOG transition
- const bdd result = bdd_ithvar((p->var_map.find(tempTransitionNames.front()))->second);
- if ((ii->cond() & result) != bddfalse)
- {
- //make a copy that we can iterate
-// SafeDequeue<myCouple> tempSharedPool = sharedPool;
- SafeDequeue<myState_t*> tempSharedPool = mSharedPoolTemp;
- while (!tempSharedPool.empty())
- {
- std::lock_guard<std::mutex> guard(mMutex);
-// if ((tempSharedPool.front().first == sog_current_state->Successors.at(i).first) &&
-// (tempSharedPool.front().second == const_cast<spot::state *>(ii->dst())))
- if ((tempSharedPool.front()->left == elt.first) && (tempSharedPool.front()->right == const_cast<spot::state *>(ii->dst())))
- {
-// nd->cyan = true;
- state->new_successors.push_back(make_pair(tempSharedPool.front(), transition));
- } else
- {
- //new terminal state without successors
- //state_is_accepting() should only be called on automata with state-based acceptance
- myState_t *nd = buildState(elt.first,
- const_cast<spot::state *>(ii->dst()),
- mAa->state_is_accepting(ii->dst()), true, false);
- state->new_successors.push_back(make_pair(nd, transition));
- }
-//
-
- }
- }
+ //iterate over the successors of a BA state
+ auto ii = mAa->succ_iter(ba_current_state);
+ if (ii->first())
+ do {
+ if (p->var_map.find(f) != p->var_map.end()) {
+ //fetch the transition of BA that have the same AP as the SOG transition
+ const bdd result = bdd_ithvar((p->var_map.find(f))->second);
+ if ((ii->cond() & result) != bddfalse) {
+ std::unique_lock lk(mMutex);
+ auto result = isStateBuilt(elt.first, (spot::twa_graph_state *) ii->dst());
+ if (result) {
+ state->new_successors.push_back(make_pair(result, transition));
+ } else {
+ myState_t *nd = buildState(elt.first,
+ const_cast<spot::state *>(ii->dst()),
+ mAa->state_is_accepting(ii->dst()), true, false);
+ state->new_successors.push_back(make_pair(nd, transition));
}
}
- while (ii->next());
- mAa->release_iter(ii);
- tempTransitionNames.try_pop(tempTransitionNames.front());
- }
- transitionNames.try_pop(transitionNames.front());
+ }
+ } while (ii->next());
+ mAa->release_iter(ii);
}
+ state->succState = SuccState::built;
+ mDataCondWait.notify_all();
}
-
//Perform the dfsBlue
-void CNDFS::dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread) {
- state->cyan[idThread]=true;
- for (const auto & succ:state->new_successors)
- {
- if (!succ.first->blue && !succ.first->cyan[idThread])
- {
- dfsBlue(succ.first,Rp,idThread);
- }
+void CNDFS::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread) {
+ state->cyan[idThread] = true;
+ for (const auto &succ: state->new_successors) {
+ if (!succ.first->blue && !succ.first->cyan[idThread]) {
+ dfsBlue(succ.first, Rp, idThread);
+ }
}
state->blue = true;
- if (state->isAcceptance)
- {
+ if (state->isAcceptance) {
cout << "Acceptance state detected " << endl;
- if (state->left->isDeadLock() || state->left->isDiv())
- {
- cout << "cycle detected: an aggregate with deal_lock or live_lock" << endl;
+ if (state->left->isDeadLock() || state->left->isDiv()) {
+ cout << "cycle detected: an aggregate with deal_lock or live_lock" << endl;
exit(0);
- } else
- {
+ } else {
Rp.clear();
- dfsRed(state, Rp,idThread); //looking for an accepting cycle
- // the thread processed the current state waits for all visited accepting nodes (non seed, non red) to turn red
- // the late red coloring forces the other acceptance states to be processed in post-order by the other threads
+ dfsRed(state, Rp, idThread); //looking for an accepting cycle
+ // the thread processed the current state waits for all visited accepting nodes (non seed, non red) to turn red
+ // the late red coloring forces the other acceptance states to be processed in post-order by the other threads
bool cond;
do {
cond = true;
@@ -218,7 +200,7 @@ void CNDFS::dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread) {
}
} while (!cond);
- for (const auto& qu: Rp) // prune other dfsRed
+ for (const auto &qu: Rp) // prune other dfsRed
{
qu->red = true;
}
@@ -227,5 +209,6 @@ void CNDFS::dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread) {
}
state->cyan[idThread] = false;
}
+
spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 87369446ad6717881c4429f1ba8998f45d4090ac..c58e6ff4d397cc3d2e5f8a30ec1c2d1af3574ce3 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -3,6 +3,7 @@
//
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
+
#include "../ModelCheckBaseMT.h"
#include <spot/tl/apcollect.hh>
#include <cstdint>
@@ -13,49 +14,64 @@
#include <condition_variable>
#include "misc/SafeDequeue.h"
-using namespace std ;
-typedef pair<struct myState_t*, int> coupleSuccessor;
-static constexpr uint8_t MAX_THREADS=64;
+using namespace std;
+typedef pair<struct myState_t *, int> coupleSuccessor;
+static constexpr uint8_t MAX_THREADS = 64;
+
+enum class SuccState {notyet,beingbuilt,built};
struct myState_t {
LDDState *left;
- const spot::twa_graph_state* right;
- vector<pair<struct myState_t*, int>> new_successors;
+ const spot::twa_graph_state *right;
+ vector<pair<struct myState_t *, int>> new_successors;
bool isAcceptance {false};
bool isConstructed {false};
- array<bool,MAX_THREADS> cyan {false};
- atomic<bool> blue {false};
- atomic<bool> red {false};
+ array<bool, MAX_THREADS> cyan {false};
+ atomic<bool> blue{false};
+ atomic<bool> red{false};
+ SuccState succState {SuccState::notyet};
};
class CNDFS {
private:
-
- ModelCheckBaseMT * mMcl;
+ ModelCheckBaseMT *mMcl;
spot::twa_graph_ptr mAa;
uint16_t mNbTh;
atomic<uint8_t> mIdThread;
- std::thread* mlThread[MAX_THREADS];
- mutex mMutex;
+ std::thread *mlThread[MAX_THREADS];
+ mutex mMutex,mMutexStatus;
+ std::condition_variable mDataCondWait;
condition_variable cv;
- void spawnThreads();
- myState_t * mInitStatePtr;
- SafeDequeue<struct myState_t*> mSharedPoolTemp;
- static spot::bdd_dict_ptr* m_dict_ptr;
+ myState_t *mInitStatePtr;
+ vector<myState_t *> mlBuiltStates;
+ SafeDequeue<struct myState_t *> mSharedPoolTemp;
+ static spot::bdd_dict_ptr *m_dict_ptr;
+
void getInitialState();
+
+ void spawnThreads();
+
static void threadHandler(void *context);
+
void threadRun();
+
+ void computeSuccessors(myState_t *state);
+
+ myState_t *buildState(LDDState *left, spot::state *right, bool acc, bool constructed, bool cyan);
+ myState_t* isStateBuilt(LDDState *sogState,spot::twa_graph_state *spotState);
public:
-// SafeDequeue<myCouple> sharedPool;
- SafeDequeue<spot::formula> transitionNames;
- SafeDequeue<coupleSuccessor> new_successor;
- CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
+ CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh);
+
virtual ~CNDFS();
- void computeSuccessors(myState_t *state);
- void dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread);
- void dfsRed(myState_t* state, vector<myState_t*>& Rp,uint8_t idThread);
- void WaitForTestCompleted(myState_t* state);
- myState_t* buildState(LDDState* left, spot::state* right, bool acc, bool constructed,bool cyan);
+
+
+ void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
+
+ void dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
+
+
+
+
};