diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 69c18446b14cada3a2352621be64bd0d36397643..f05c86bb2aafe9cb0e7900a26ccda201d432a373 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -19,9 +19,6 @@
#include "misc/stacksafe.h"
using namespace std;
-deque <int> mm;
-//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)
{
@@ -51,21 +48,24 @@ void CNDFS::threadHandler(void *context) {
}
//get initial state of the product automata
-CNDFS::_state* CNDFS::getInitialState(){
+_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;
}
//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, bool cyan){
+_state* CNDFS::buildState(LDDState* left, spot::state* right, bool acc, bool constructed, bool cyan){
bool _cyan{false};
+ mMutex.lock();
_state * buildStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
_cyan = cyan;
buildStatePtr->left = left;
@@ -74,10 +74,11 @@ CNDFS::_state* CNDFS::buildState(LDDState* left, spot::state* right, vector<pair
buildStatePtr->isAcceptance = acc;
buildStatePtr->isConstructed = constructed;
buildStatePtr->cyan= _cyan;
+ mMutex.unlock();
return buildStatePtr;
}
-std::ostream & operator<<(std::ostream & Str, CNDFS::_state* state) {
+std::ostream & operator<<(std::ostream & Str,_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;
int i = 0;
for (auto ii : state->new_successors)
@@ -89,7 +90,7 @@ std::ostream & operator<<(std::ostream & Str, CNDFS::_state* state) {
}
//all visited accepting nodes (non seed, non red) should be red
-atomic_bool CNDFS::awaitCondition(_state* state,deque<CNDFS::_state*> localDeque)
+atomic_bool CNDFS::awaitCondition(_state* state,deque<_state*> localDeque)
{
vector<bool> localList ;
for (auto qu: localDeque)
@@ -111,7 +112,7 @@ atomic_bool CNDFS::awaitCondition(_state* state,deque<CNDFS::_state*> localDeque
// while ( awaitCondition(state) == false) ;
//}
-void CNDFS::dfsRed(_state* state,deque<CNDFS::_state*> localDeque)
+void CNDFS::dfsRed(_state* state,deque<_state*> localDeque)
{
cout << "dfsRed" << endl;
localDeque.push_back(state);
@@ -144,8 +145,7 @@ void CNDFS::computeSuccessors(_state *state)
transitionNames.push(f);
cv.notify_one();
}
-
- //iterate over the successors of an aggregate
+ //iterate over the successors of a current aggregate
for (int i = 0; i < sog_current_state->Successors.size(); i++)
{
int transition = sog_current_state->Successors.at(i).second; // je récupère le numéro du transition
@@ -166,30 +166,30 @@ void CNDFS::computeSuccessors(_state *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
+ {
+ //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)
{
- // cout << "matched bdd " << matched << endl;
- //new terminal state without successors
- // 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);
//make a copy that we can iterate
- SafeDequeue<myCouple> tempSharedPool = sharedPool;
+// SafeDequeue<myCouple> tempSharedPool = sharedPool;
+ SafeDequeue<_state*> tempSharedPool = sharedPoolTemp;
while (!tempSharedPool.empty())
{
-// mMutex.lock();
- if ((tempSharedPool.front().first == sog_current_state->Successors.at(i).first) &&
- (tempSharedPool.front().second == const_cast<spot::state *>(ii->dst())))
+ 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 == sog_current_state->Successors.at(i).first) && (tempSharedPool.front()->right == const_cast<spot::state *>(ii->dst())))
{
- nd->cyan = true;
- state->new_successors.push_back(make_pair(nd, transition));
- // state->new_successors.push_back(make_pair(pool,transition));
+// 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
+ _state *nd = buildState(sog_current_state->Successors.at(i).first,
+ const_cast<spot::state *>(ii->dst()),
+ mAa->state_is_accepting(ii->dst()), true, false);
state->new_successors.push_back(make_pair(nd, transition));
}
// mMutex.unlock();
@@ -211,14 +211,15 @@ int i = 1;
//Perform the dfsBlue
void CNDFS::dfsBlue(_state *state) {
-// myStack.push(2);
- thread_local deque<CNDFS::_state*> localDeque;
+ deque<_state*> localDeque;
uint16_t idThread = mIdThread++;
cout<< "appel recursif " << i << endl;
i++;
state->cyan = true;
- sharedPool.push(myCouple (state->left,state->right));
+// sharedPool.push(myCouple (state->left,state->right));
+ sharedPoolTemp.push(state);
cv.notify_one();
+// new_successor.push(coupleSuccessor(state,2));
computeSuccessors(state);
cout << " \n current state " << state << endl;
// cout << "nbr of successors of the current state "<< state->new_successors.size() << " with thread "<< idThread<< endl;
@@ -245,8 +246,9 @@ void CNDFS::dfsBlue(_state *state) {
// 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, localDeque)) cv.wait(lk);
+// cv.wait(lk,[this] {return !awaitCondition(state, localDeque)});
+ lk.unlock();
// notify once we have unlocked - this is important to avoid a pessimization.
awaitCondition(state,localDeque)=true;
cv.notify_all();
@@ -258,7 +260,6 @@ void CNDFS::dfsBlue(_state *state) {
cout << "no cycle detected" << endl;
}
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 6030e4c429db5917d556b2855065ff5c9d72ac1c..5859d352c686050cd6849017ad3c2dd7c8005c8a 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -13,6 +13,20 @@
#include <condition_variable>
#include "misc/SafeDequeue.h"
+using namespace std ;
+typedef pair<struct myState*, int> coupleSuccessor;
+
+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};
+ bool cyan {false};
+ atomic_bool blue {false};
+ atomic_bool red {false};
+};
+typedef struct myState _state; // @alias
class CNDFS {
@@ -29,31 +43,22 @@ private:
void spawnThreads();
public:
- typedef struct _state{
- LDDState *left;
- const spot::twa_graph_state* right;
- vector<pair<_state*, int>> new_successors ;
-// SafeDequeue<coupleSucc> new_successors ;
- atomic_bool isAcceptance {false};
- atomic_bool isConstructed {false};
- bool cyan {false};
- atomic_bool blue {false};
- atomic_bool red {false};
- } _state;
- SafeDequeue<myCouple> sharedPool;
- SafeDequeue<spot::formula> transitionNames;
+// typedef myState _state;
+ SafeDequeue<struct myState*> sharedPoolTemp;
+// SafeDequeue<myCouple> sharedPool;
+ SafeDequeue<spot::formula> transitionNames;
+ SafeDequeue<coupleSuccessor> new_successor;
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, deque<CNDFS::_state*> mydeque);
+ void dfsRed(_state* state, deque<_state*> mydeque);
void WaitForTestCompleted(_state* state);
- atomic_bool awaitCondition(_state* state,deque<CNDFS::_state*> mydeque);
- _state* buildState(LDDState* left, spot::state* right, vector<pair<_state *, int>> succ, bool acc, bool constructed,bool cyan);
+ atomic_bool awaitCondition(_state* state,deque<_state*> mydeque);
+ _state* buildState(LDDState* left, spot::state* right, bool acc, bool constructed,bool cyan);
static spot::bdd_dict_ptr* m_dict_ptr;
};
-
#endif //PMC_SOG_CNDFS_H
diff --git a/src/misc/SafeDequeue.cpp b/src/misc/SafeDequeue.cpp
index 559f76b9e20fbe5002602e598b612c020321f79f..8834583aa3d5f2652a36bd2d467fa0b2c0e02267 100644
--- a/src/misc/SafeDequeue.cpp
+++ b/src/misc/SafeDequeue.cpp
@@ -47,6 +47,7 @@ void SafeDequeue<T>::push ( T new_value )
}
+
template<typename T>
bool SafeDequeue<T>::try_pop ( T& value )
{
@@ -60,8 +61,6 @@ bool SafeDequeue<T>::try_pop ( T& value )
}
-
-
template<typename T>
bool SafeDequeue<T>::empty() const
{
@@ -105,6 +104,7 @@ template class SafeDequeue<Pair>;
typedef pair<string *, unsigned int> MSG;
template class SafeDequeue<MSG>;
template class SafeDequeue<couple_th>;
-template class SafeDequeue<myCouple>;
-template class SafeDequeue<coupleSucc>;
+
+template class SafeDequeue<coupleSuccessor>;
template class SafeDequeue<spot::formula>;
+template class SafeDequeue<struct myState*>;
diff --git a/src/misc/SafeDequeue.h b/src/misc/SafeDequeue.h
index 10d3e5f3f281711cc95df6b110aa10abb4e0b407..eea1e20259de5137d5ddf8387958cc9f8701333d 100644
--- a/src/misc/SafeDequeue.h
+++ b/src/misc/SafeDequeue.h
@@ -20,18 +20,20 @@
#define SAFEDEQUEUE_H
#include <memory>
#include "LDDState.h"
+#include "algorithm/CNDFS.h"
#include <queue>
#include <mutex>
#include <functional>
#include <condition_variable>
#include <spot/twa/twagraph.hh>
-#include "algorithm/CNDFS.h";
-typedef pair<LDDState *, MDD> couple;
-typedef pair<LDDState*,const spot::twa_graph_state*> myCouple;
+//class CNDFS;
+typedef pair<LDDState*, MDD> couple;
typedef pair<couple, Set> Pair;
-typedef pair<LDDState *, int> couple_th;
-typedef pair<_state*, int> coupleSucc;
+typedef pair<LDDState*, int> couple_th;
+
+typedef pair<struct myState*, int> coupleSuccessor;
+
struct empty_queue: std::exception {
~empty_queue() {};
const char* what() const noexcept {return "";}