diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index a8a433d20b09404d36fc8036833a8c12c333b402..e610b328f90984733fbb50309ff94d349831e9e9 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -18,9 +18,10 @@
using namespace std;
thread_local bool _cyan{false};
-thread_local deque<CNDFS::_state*> mydeque ;
+thread_local deque<CNDFS::_state*> mydeque;
thread_local list<bool> mytempList ;
vector<pair<LDDState*,const spot::twa_graph_state*>> sharedPool;
+//vector<CNDFS::_state*> sharedPool;
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh)
{
@@ -86,7 +87,7 @@ std::ostream & operator<<(std::ostream & Str, CNDFS::_state* state) {
return Str;
}
-//algo line 22 test
+//all visited accepting nodes (non seed, non red) should be red
atomic_bool CNDFS::awaitCondition(_state* state)
{
for (auto qu: mydeque)
@@ -119,8 +120,9 @@ void CNDFS::dfsRed(_state* state)
if (p.first->cyan)
{
cout << "cycle detected" << endl;
- exit(1);
+ exit(0);
}
+ // unvisited and not red state
if ((find(mydeque.begin(), mydeque.end(), state) != mydeque.end()) && ! p.first->red )
dfsRed(p.first);
}
@@ -176,7 +178,8 @@ void CNDFS::computeSuccessors(_state *state)
{
// cout << "matched bdd " << matched << endl;
//new terminal state without successors
- _state* nd = buildState(sog_current_state->Successors.at(i).first,
+// state_is_accepting() should only be called on automata with state-based acceptance
+ _state* nd = buildState(sog_current_state->Successors.at(i).first,
const_cast<spot::state *>(ii->dst()), static_cast<vector<pair<_state *, int>>>(NULL), mAa->state_is_accepting(ii->dst()), true, false);
for (auto pool:sharedPool)
{
@@ -184,7 +187,11 @@ void CNDFS::computeSuccessors(_state *state)
{
nd->cyan=true;
state->new_successors.push_back(make_pair(nd,transition));
- } else state->new_successors.push_back(make_pair(nd,transition));
+// state->new_successors.push_back(make_pair(pool,transition));
+ } else
+ {
+ state->new_successors.push_back(make_pair(nd,transition));
+ }
}
}
@@ -205,14 +212,15 @@ void CNDFS::dfsBlue(_state *state) {
cout<< "appel recursif " << i << endl ;
i++;
state->cyan = true;
+// sharedPool.push_back(state);
sharedPool.push_back(make_pair(state->left,state->right));
computeSuccessors(state);
-// cout << "state " << state << endl;
-// cout << "nbr of successors of the state "<< state->new_successors.size() << " with thread "<< idThread<< endl;
+ cout << "current state " << state << endl;
+ cout << "nbr of successors of the current state "<< state->new_successors.size() << " with thread "<< idThread<< endl;
for (auto p:state->new_successors)
{
// cout << "state " << p.first << endl;
- while ((p.first->cyan == false) && (p.first->blue == false))
+ while ((!p.first->cyan) && (!p.first->blue))
{
dfsBlue(p.first);
}
@@ -220,18 +228,31 @@ void CNDFS::dfsBlue(_state *state) {
state->blue = true;
if (state->isAcceptance)
{
- cout << "hello redDFS " << endl;
- dfsRed(state);
- WaitForTestCompleted(state);
- std::lock_guard<std::mutex> lk(*mMutex);
- cv.notify_all();
- for (auto qu: mydeque)
+ cout << "Acceptance state detected " << endl;
+ if (state->left->isDeadLock() || state->left->isDiv())
{
- qu->red = true;
+ cout << "cycle detected: an aggregate with deal_lock or live_lock" << endl;
+ exit(0);
+ } else
+ {
+ dfsRed(state); //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
+ std::unique_lock<std::mutex> lk(*mMutex);
+ // WaitForTestCompleted(state);
+ while (!awaitCondition(state)) cv.wait(lk);
+ // notify once we have unlocked - this is important to avoid a pessimization.
+ awaitCondition(state)=true;
+ cv.notify_all();
+ for (auto qu: mydeque) // prune other dfsRed
+ {
+ qu->red = true;
+ }
}
+ cout << "no cycle detected" << endl;
}
state->cyan = false;
- cout << state << endl;
+// cout << state << endl;
}
spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 206b5c860d808b42b1fcb331d54e488a9a9d3266..f9bbbaa6d626517ac23edb6b869f2b14a7df2192 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -27,7 +27,7 @@ private:
public:
typedef struct _state{
- LDDState * left;
+ LDDState *left;
const spot::twa_graph_state* right;
vector<pair<_state*, int>> new_successors ;
atomic_bool isAcceptance {false};
diff --git a/src/main.cpp b/src/main.cpp
index 881e643d5f431cb22f7812318599e20d26bbb807..f2447b05818f02fcb3152cea93003795fa9add66 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -523,13 +523,9 @@ int main(int argc, char **argv)
// TODO: Implement here Ghofrane's algorithms
if (algorithm == "UFSCC" || algorithm == "CNDFS")
{
-
std::cout<<"------------CNDFS-------------"<<std::endl;
-
- CNDFS cndfs(mcl,af,2);
-
+ CNDFS cndfs(mcl,af,1); // If I increase the number of threads, a segmentation fault appears.
return(0);
-
}
else // run on the fly sequential model-checking
{