diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4269e84c020b2dd3dde63db9cabfe0a3466f0ba6..6e83dc31f4d6db034da5bff69b6e89e5019573ed 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -70,6 +70,8 @@ add_subdirectory(src)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -pthread")
+
+
# add tests
# enable_testing()
# add_subdirectory(tests)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 480bbded240b4b2b783b2bf5d35175050c36c456..778ebd477e5743374223f73ad1cc6e342118bb75 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -12,9 +12,13 @@
#include <spot/twa/twa.hh>
#include <bddx.h>
#include <cstddef>
+#include <deque>
+#include <condition_variable>
using namespace std;
+thread_local deque<CNDFS::_state*> mydeque ;
+thread_local list<bool> mytempList ;
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh)
{
@@ -54,6 +58,7 @@ CNDFS::_state* CNDFS::getInitialState(){
return initStatePtr;
}
+
//this function is to build a state with list of successor initially null
CNDFS::_state* CNDFS::buildState(LDDState* left, spot::state* right, vector<pair<_state *, int>> succ, bool acc, bool constructed){
_state * buildStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
@@ -65,6 +70,50 @@ CNDFS::_state* CNDFS::buildState(LDDState* left, spot::state* right, vector<pair
return buildStatePtr;
}
+std::ostream & operator<<(std::ostream & Str, CNDFS::_state* state) {
+ Str << "({ Sog state= " << state->left << ", BA state= " << state->right << ", acceptance= " << state->isAcceptance << ", constructed= " << state->isConstructed << ", cyan= " << state->cyan << ", red= " << state->red << ", blue= " << state->blue <<" }" << endl;
+ return Str;
+}
+
+//algo line 22 test
+atomic_bool CNDFS::awaitCondition(_state* state)
+{
+ for (auto qu: mydeque)
+ {
+ if ((qu->isAcceptance) && (qu!=state))
+ mytempList.push_back(qu->red); // add all the red values
+// return(qu->red == true);
+ }
+ //test if all elements are true
+ if (all_of(mytempList.begin(),mytempList.end(),[] (bool cond) {return cond ==true; }))
+ {
+ return true;
+ }
+ return false;
+}
+
+
+//block all threads while awaitCondition is false
+void CNDFS::WaitForTestCompleted(_state* state) {
+ while ( awaitCondition(state) == false) ;
+}
+
+
+void CNDFS::dfsRed(_state* state)
+{
+ cout << "dfsRed" << endl;
+ mydeque.push_back(state);
+ computeSuccessors(state);
+ for (auto p:state->new_successors) {
+ if (p.first->cyan)
+ {
+ cout << "cycle detected" << endl;
+ exit(1);
+ }
+ if ((find(mydeque.begin(), mydeque.end(), state) != mydeque.end()) && ! p.first->red )
+ dfsRed(p.first);
+ }
+}
//compute new successors of a product state
void CNDFS::computeSuccessors(_state *state)
@@ -96,10 +145,10 @@ void CNDFS::computeSuccessors(_state *state)
transitionNames.push_back(f); // push state'S AP to edge'S AP
auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
//cout << p->bdd_map.size() << endl;
- for (auto v: p->var_map)
- {
- cout << v.first << "-----" << v.second << endl;
- }
+// for (auto v: p->var_map)
+// {
+// cout << v.first << "-----" << v.second << endl;
+// }
for (auto it = transitionNames.begin(); it != transitionNames.end(); ++it)
{
@@ -117,42 +166,56 @@ void CNDFS::computeSuccessors(_state *state)
{
cout << "matched bdd " << matched << endl;
//new terminal state without successors
+// std::lock_guard<std::mutex> lg(*mMutex);
_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);
- //add the successor found to the vestor of successor of the current state
+ cout << "new succ state " << nd ;
+ //add the successor found to the successor's vector of the current state
state->new_successors.push_back(make_pair(nd,transition));
- cout << *it << " is a common transaction!" << endl; // p->var_map.find ( f )->second => donne la bdd
}
}
while (ii->next());
mAa->release_iter(ii);
+ cout << *it << " is a common transaction!" << endl;
} else cout << *it << " isn't a common transaction" << endl;
}
transitionNames.pop_back();
}
-
}
//Compute the synchronized product
void CNDFS::dfsBlue(_state *state) {
uint16_t idThread = mIdThread++;
-
- cout << state->isConstructed << endl;
+ cout << state;
+ state->cyan = true;
+// cout << "first state " << "({ " << state->right << ", " << state->left << ", " << state->isAcceptance << ", " << state->isConstructed << ", " << state->cyan << ", " << state->red << ", " << state->blue <<" }" << endl;
computeSuccessors(state);
- for (auto p:state->new_successors) {
- std::cout << "list of successors of current state " << "({ " << p.first->right << ", " << p.first->left << ", " << p.first->isAcceptance << ", " << p.first->isConstructed << " }" << ", " << p.second << ") ";
- }
+ for (auto p:state->new_successors)
+ {
+ cout <<"STATE 1 " << state<< endl;
+ cout << "STATE 2 "<< p.first<< endl;
+ cout << " cyan " << p.first->cyan << endl;
+// cout << "list of successors of current state " << "({ " << p.first->right << ", " << p.first->left << ", " << p.first->isAcceptance << ", " << p.first->isConstructed << ", " << p.first->cyan << ", " << p.first->red << ", " << p.first->blue <<" }" << ", " << p.second << ") " << endl;
+ while((p.first->cyan == 0) && (p.first->blue == 0))
+ {
+ cout << " appel recursive 2 " << endl;
+ dfsBlue(p.first);
+ }
-// for (auto k = new_successors.begin(); k != new_successors.end(); ++k)
+ }
+ state->blue = true;
+// if (state->isAcceptance)
// {
-// sog_current_state= k->first.left;
-// ba_current_state= dynamic_cast<const spot::twa_graph_state *>(k->first.right);
-// //computeSuccessors(sog_current_state,ba_current_state);
-// if (! k->first.isConstructed)
-// dfsBlue();
+// dfsRed(state);
+// WaitForTestCompleted(state);
+// std::lock_guard<std::mutex> lk(*mMutex);
+// cv.notify_all();
+// for (auto qu: mydeque)
+// {
+// qu->red = true;
+// }
// }
-
-
+// state->cyan = false;
}
spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 0e44440c2a1b06ece9e74590e2d5a0d701b652ca..f51d7501a7a1c5543a7d5a5a623a622ac9ef99a7 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -1,15 +1,16 @@
//
// Created by ghofrane on 5/4/22.
//
-
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
#include "../ModelCheckBaseMT.h"
-//#include "../SogKripkeTh.h"
#include <spot/tl/apcollect.hh>
#include <cstdint>
#include <thread>
+#include <atomic>
+#include <condition_variable>
#include <spot/twa/twagraph.hh>
+
class CNDFS {
private:
@@ -20,7 +21,8 @@ private:
atomic<uint8_t> mIdThread;
static void threadHandler(void *context);
std::thread* mlThread[MAX_THREADS];
- std::mutex mMutex;
+ mutex *mMutex;
+ condition_variable cv;
void spawnThreads();
public:
@@ -30,16 +32,21 @@ public:
vector<pair<_state* , int>> new_successors ;
bool isAcceptance = false;
bool isConstructed = false;
+ inline static thread_local atomic_bool cyan = {false};
+ bool blue = false;
+ bool red = false;
} _state;
-// vector<pair<_state , int>> new_successors;
+
list<spot::formula> transitionNames;
- vector<bdd>temp;
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
void computeSuccessors(_state *state);
void dfsBlue(_state *state);
_state* getInitialState();
+ void dfsRed(_state* state);
+ void WaitForTestCompleted(_state* state);
+ atomic_bool awaitCondition(_state* state);
_state* buildState(LDDState* left, spot::state* right, vector<pair<_state *, int>> succ, bool acc, bool constructed);
static spot::bdd_dict_ptr* m_dict_ptr;
};