diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 778ebd477e5743374223f73ad1cc6e342118bb75..a8a433d20b09404d36fc8036833a8c12c333b402 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -13,12 +13,14 @@
#include <bddx.h>
#include <cstddef>
#include <deque>
+#include <atomic>
#include <condition_variable>
using namespace std;
-
+thread_local bool _cyan{false};
thread_local deque<CNDFS::_state*> mydeque ;
thread_local list<bool> mytempList ;
+vector<pair<LDDState*,const spot::twa_graph_state*>> sharedPool;
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh)
{
@@ -55,23 +57,32 @@ CNDFS::_state* CNDFS::getInitialState(){
initStatePtr->new_successors = static_cast<vector<pair<_state *, int>>>(NULL);
initStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
initStatePtr->isConstructed = true;
+// sharedPool.push_back(make_pair(initStatePtr->left,initStatePtr->right));
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){
+CNDFS::_state* CNDFS::buildState(LDDState* left, spot::state* right, vector<pair<_state *, int>> succ, bool acc, bool constructed, bool cyan){
_state * buildStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
+ _cyan = cyan;
buildStatePtr->left = left;
buildStatePtr->right = dynamic_cast<const spot::twa_graph_state *>(right);
buildStatePtr->new_successors = static_cast<vector<pair<_state *, int>>>(NULL);
buildStatePtr->isAcceptance = acc;
buildStatePtr->isConstructed = constructed;
+ buildStatePtr->cyan= _cyan;
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;
+ 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;
+ int i = 0;
+ for (auto ii : state->new_successors)
+ {
+ cout << "succ num " << i << ii.first << endl;
+ i++;
+ }
return Str;
}
@@ -129,16 +140,15 @@ void CNDFS::computeSuccessors(_state *state)
auto f = spot::formula::ap(name);
transitionNames.push_back(f);
}
-
- for (auto tn: transitionNames)
- {
- cout << " \n AP in state " << tn << endl;
- }
+// for (auto tn: transitionNames)
+// {
+// cout << " \n AP in state " << tn << endl;
+// }
//iterate over the successors of an aggregate
for (int i = 0; i < sog_current_state->Successors.size(); i++)
{
- cout <<"------"<< " SOG's successor " << i << " ------" << endl;
+// cout <<"------"<< " SOG's successor " << i << " ------" << endl;
int transition = sog_current_state->Successors.at(i).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
@@ -155,7 +165,7 @@ void CNDFS::computeSuccessors(_state *state)
if (p->var_map.find(*it) != 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(*it))->second);
- cout << "dbb result " << result << endl;
+// cout << "dbb result " << result << endl;
//iterate over the successors of a BA state
spot::twa_succ_iterator* ii = mAa->succ_iter(ba_current_state);
if (ii->first())
@@ -164,58 +174,64 @@ void CNDFS::computeSuccessors(_state *state)
bdd matched = ii->cond()&result;
if (matched!=bddfalse)
{
- cout << "matched bdd " << matched << endl;
+// 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);
- 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));
+ _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)
+ {
+ if ((pool.first == sog_current_state->Successors.at(i).first) && (pool.second == const_cast<spot::state *>(ii->dst())) )
+ {
+ nd->cyan=true;
+ state->new_successors.push_back(make_pair(nd,transition));
+ } else state->new_successors.push_back(make_pair(nd,transition));
+
+ }
}
}
while (ii->next());
mAa->release_iter(ii);
- cout << *it << " is a common transaction!" << endl;
- } else cout << *it << " isn't a common transaction" << endl;
+// cout << *it << " is a common transaction!" << endl;
+ }
+// else cout << *it << " isn't a common transaction" << endl;
}
transitionNames.pop_back();
}
}
-
-//Compute the synchronized product
+int i = 1;
+//Perform the dfsBlue
void CNDFS::dfsBlue(_state *state) {
uint16_t idThread = mIdThread++;
- cout << state;
+ cout<< "appel recursif " << i << endl ;
+ i++;
state->cyan = true;
-// cout << "first state " << "({ " << state->right << ", " << state->left << ", " << state->isAcceptance << ", " << state->isConstructed << ", " << state->cyan << ", " << state->red << ", " << state->blue <<" }" << endl;
+ 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;
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 << "state " << p.first << endl;
+ while ((p.first->cyan == false) && (p.first->blue == false))
{
- cout << " appel recursive 2 " << endl;
dfsBlue(p.first);
}
-
}
state->blue = true;
-// if (state->isAcceptance)
-// {
-// dfsRed(state);
-// WaitForTestCompleted(state);
-// std::lock_guard<std::mutex> lk(*mMutex);
-// cv.notify_all();
-// for (auto qu: mydeque)
-// {
-// qu->red = true;
-// }
-// }
-// state->cyan = false;
+ 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)
+ {
+ qu->red = true;
+ }
+ }
+ state->cyan = false;
+ cout << state << endl;
}
spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index f51d7501a7a1c5543a7d5a5a623a622ac9ef99a7..206b5c860d808b42b1fcb331d54e488a9a9d3266 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -27,18 +27,19 @@ private:
public:
typedef struct _state{
- LDDState *left;
+ LDDState * left;
const spot::twa_graph_state* right;
- 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;
+ vector<pair<_state*, int>> new_successors ;
+ atomic_bool isAcceptance {false};
+ atomic_bool isConstructed {false};
+ bool cyan {false};
+ atomic_bool blue {false};
+ atomic_bool red {false};
} _state;
list<spot::formula> transitionNames;
+
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
void computeSuccessors(_state *state);
@@ -47,7 +48,7 @@ public:
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);
+ _state* buildState(LDDState* left, spot::state* right, vector<pair<_state *, int>> succ, bool acc, bool constructed,bool cyan);
static spot::bdd_dict_ptr* m_dict_ptr;
};
diff --git a/src/main.cpp b/src/main.cpp
index b94d3bd64675c00b8b55714a1534e8a1638e2e08..881e643d5f431cb22f7812318599e20d26bbb807 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -526,7 +526,7 @@ int main(int argc, char **argv)
std::cout<<"------------CNDFS-------------"<<std::endl;
- CNDFS cndfs(mcl,af,1);
+ CNDFS cndfs(mcl,af,2);
return(0);
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index dab83310167345d5b6424c64e7748243112334c8..1210e51ea3f3f680c8f7e67e7366926abf3bf9f4 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -50,7 +50,6 @@ threadSOG::threadSOG(const NewNet &R, int nbThread, bool uselace, bool init) {
cout << it2.first << " : " << it2.second << endl;
}
-
cout << "mObservable transitions:" << endl;
for (const auto &it: m_net->mObservable) {