diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3a31882230faef5bb8842329f107e46380b6a26d..2bdab4d35a1fa68f0da3c7452d51013a905337ae 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -73,32 +73,33 @@ add_executable(pmc-sog main.cpp
SogKripkeIteratorTh.cpp
SogKripkeIteratorTh.h
- misc/stacksafe.cpp
- misc/stacksafe.h
- misc/SafeDequeue.cpp
- misc/SafeDequeue.h
- Hybrid/HybridKripke.cpp
- Hybrid/HybridKripke.h
- Hybrid/HybridKripkeIterator.cpp
- Hybrid/HybridKripkeIterator.h
- Hybrid/HybridKripkeState.cpp
- Hybrid/HybridKripkeState.h
- SylvanWrapper.cpp
- SylvanWrapper.h
- SylvanCacheWrapper.cpp SylvanCacheWrapper.h
- MCMultiCore/ModelCheckerCPPThread.cpp MCMultiCore/ModelCheckerCPPThread.h
- MCMultiCore/ModelCheckerTh.cpp MCMultiCore/ModelCheckerTh.h
- MCMultiCore/MCThReqPor.cpp MCMultiCore/MCThReqPor.h
- MCMultiCore/MCCPPThPor.cpp MCMultiCore/MCCPPThPor.h
- threadSOG.cpp threadSOG.h
- HybridSOG.cpp HybridSOG.h
- Hybrid/MCHybrid/MCHybridSOG.cpp Hybrid/MCHybrid/MCHybridSOG.h
- MCMultiCore/ModelCheckThReq.cpp MCMultiCore/ModelCheckThReq.h
- Hybrid/MCHybridReq/MCHybridSOGReq.cpp
- Hybrid/MCHybridReq/MCHybridSOGReq.h
- Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp
- Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h
- misc/md5_hash.h Hybrid/MCHybridPOR/MCHybridSOGPOR.cpp Hybrid/MCHybridPOR/MCHybridSOGPOR.h)
+
+ Hybrid/HybridKripke.cpp
+ Hybrid/HybridKripke.h
+ Hybrid/HybridKripkeIterator.cpp
+ Hybrid/HybridKripkeIterator.h
+ Hybrid/HybridKripkeState.cpp
+ Hybrid/HybridKripkeState.h
+ misc/SafeDequeue.cpp
+ misc/SafeDequeue.h
+ misc/stacksafe.cpp
+ misc/stacksafe.h
+ SylvanWrapper.cpp
+ SylvanWrapper.h
+ SylvanCacheWrapper.cpp SylvanCacheWrapper.h
+ MCMultiCore/ModelCheckerCPPThread.cpp MCMultiCore/ModelCheckerCPPThread.h
+ MCMultiCore/ModelCheckerTh.cpp MCMultiCore/ModelCheckerTh.h
+ MCMultiCore/MCThReqPor.cpp MCMultiCore/MCThReqPor.h
+ MCMultiCore/MCCPPThPor.cpp MCMultiCore/MCCPPThPor.h
+ threadSOG.cpp threadSOG.h
+ HybridSOG.cpp HybridSOG.h
+ Hybrid/MCHybrid/MCHybridSOG.cpp Hybrid/MCHybrid/MCHybridSOG.h
+ MCMultiCore/ModelCheckThReq.cpp MCMultiCore/ModelCheckThReq.h
+ Hybrid/MCHybridReq/MCHybridSOGReq.cpp
+ Hybrid/MCHybridReq/MCHybridSOGReq.h
+ Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp
+ Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h
+ misc/md5_hash.h Hybrid/MCHybridPOR/MCHybridSOGPOR.cpp Hybrid/MCHybridPOR/MCHybridSOGPOR.h)
target_include_directories(pmc-sog PUBLIC "${PROJECT_BINARY_DIR}/src")
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index e610b328f90984733fbb50309ff94d349831e9e9..69c18446b14cada3a2352621be64bd0d36397643 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -15,12 +15,12 @@
#include <deque>
#include <atomic>
#include <condition_variable>
-using namespace std;
+#include "misc/SafeDequeue.h"
+#include "misc/stacksafe.h"
-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;
+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)
@@ -65,6 +65,7 @@ CNDFS::_state* CNDFS::getInitialState(){
//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){
+ bool _cyan{false};
_state * buildStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
_cyan = cyan;
buildStatePtr->left = left;
@@ -81,40 +82,39 @@ std::ostream & operator<<(std::ostream & Str, CNDFS::_state* state) {
int i = 0;
for (auto ii : state->new_successors)
{
- cout << "succ num " << i << ii.first << endl;
+ cout << "succ num " << i << ii.first << " with transition " << ii.second<< endl;
i++;
}
return Str;
}
//all visited accepting nodes (non seed, non red) should be red
-atomic_bool CNDFS::awaitCondition(_state* state)
+atomic_bool CNDFS::awaitCondition(_state* state,deque<CNDFS::_state*> localDeque)
{
- for (auto qu: mydeque)
+ vector<bool> localList ;
+ for (auto qu: localDeque)
{
if ((qu->isAcceptance) && (qu!=state))
- mytempList.push_back(qu->red); // add all the red values
+ localList.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; }))
+ if (all_of(localList.begin(),localList.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::WaitForTestCompleted(_state* state) {
+// while ( awaitCondition(state) == false) ;
+//}
-void CNDFS::dfsRed(_state* state)
+void CNDFS::dfsRed(_state* state,deque<CNDFS::_state*> localDeque)
{
cout << "dfsRed" << endl;
- mydeque.push_back(state);
+ localDeque.push_back(state);
computeSuccessors(state);
for (auto p:state->new_successors) {
if (p.first->cyan)
@@ -123,8 +123,8 @@ void CNDFS::dfsRed(_state* state)
exit(0);
}
// unvisited and not red state
- if ((find(mydeque.begin(), mydeque.end(), state) != mydeque.end()) && ! p.first->red )
- dfsRed(p.first);
+ if ((find(localDeque.begin(), localDeque.end(), state) != localDeque.end()) && ! p.first->red )
+ dfsRed(p.first, localDeque);
}
}
@@ -135,93 +135,99 @@ void CNDFS::computeSuccessors(_state *state)
const spot::twa_graph_state* ba_current_state = state->right;
while (!sog_current_state);
while (!sog_current_state->isCompletedSucc());
+ auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
//fetch the state's atomic proposition
for (auto vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
{
string name = string(mMcl->getPlace(vv));
auto f = spot::formula::ap(name);
- transitionNames.push_back(f);
+ transitionNames.push(f);
+ cv.notify_one();
}
-// 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;
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
- 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;
+ transitionNames.push(f); // push state'S AP to edge'S AP
+ cv.notify_one();
+// cout << " AP in state ";
+// for (auto tn: transitionNames) {
+// cout << tn << " ";
// }
-
- for (auto it = transitionNames.begin(); it != transitionNames.end(); ++it)
+ //make a copy that we can iterate
+ SafeDequeue<spot::formula> tempTransitionNames = transitionNames;
+ while (!tempTransitionNames.empty())
{
- 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;
- //iterate over the successors of a BA state
- spot::twa_succ_iterator* ii = mAa->succ_iter(ba_current_state);
- if (ii->first())
- do
- {
- bdd matched = ii->cond()&result;
- if (matched!=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);
- for (auto pool:sharedPool)
+ //iterate over the successors of a BA state
+ spot::twa_succ_iterator *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)
+ {
+ // 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;
+ while (!tempSharedPool.empty())
{
- 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));
-// state->new_successors.push_back(make_pair(pool,transition));
- } else
- {
- state->new_successors.push_back(make_pair(nd,transition));
- }
+// mMutex.lock();
+ if ((tempSharedPool.front().first == sog_current_state->Successors.at(i).first) &&
+ (tempSharedPool.front().second == 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));
+ } else
+ {
+ state->new_successors.push_back(make_pair(nd, transition));
+ }
+// mMutex.unlock();
+ tempSharedPool.try_pop(tempSharedPool.front());
}
+ }
}
}
- while (ii->next());
- mAa->release_iter(ii);
-// cout << *it << " is a common transaction!" << endl;
- }
-// else cout << *it << " isn't a common transaction" << endl;
+ while (ii->next());
+ mAa->release_iter(ii);
+ tempTransitionNames.try_pop(tempTransitionNames.front());
}
- transitionNames.pop_back();
+ transitionNames.try_pop(transitionNames.front());
}
}
+
int i = 1;
+
//Perform the dfsBlue
void CNDFS::dfsBlue(_state *state) {
+// myStack.push(2);
+ thread_local deque<CNDFS::_state*> localDeque;
uint16_t idThread = mIdThread++;
- cout<< "appel recursif " << i << endl ;
+ cout<< "appel recursif " << i << endl;
i++;
state->cyan = true;
-// sharedPool.push_back(state);
- sharedPool.push_back(make_pair(state->left,state->right));
+ sharedPool.push(myCouple (state->left,state->right));
+ cv.notify_one();
computeSuccessors(state);
- cout << "current state " << state << endl;
- cout << "nbr of successors of the current state "<< state->new_successors.size() << " with thread "<< idThread<< endl;
+ cout << " \n 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) && (!p.first->blue))
{
+ transitionNames.try_pop(transitionNames.front());
dfsBlue(p.first);
}
}
@@ -235,16 +241,16 @@ void CNDFS::dfsBlue(_state *state) {
exit(0);
} else
{
- dfsRed(state); //looking for an accepting cycle
+ dfsRed(state, localDeque); //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);
+ std::unique_lock<std::mutex> lk(mMutex);
// WaitForTestCompleted(state);
- while (!awaitCondition(state)) cv.wait(lk);
+ while (!awaitCondition(state, localDeque)) cv.wait(lk);
// notify once we have unlocked - this is important to avoid a pessimization.
- awaitCondition(state)=true;
+ awaitCondition(state,localDeque)=true;
cv.notify_all();
- for (auto qu: mydeque) // prune other dfsRed
+ for (auto qu: localDeque) // prune other dfsRed
{
qu->red = true;
}
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index f9bbbaa6d626517ac23edb6b869f2b14a7df2192..6030e4c429db5917d556b2855065ff5c9d72ac1c 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -6,10 +6,13 @@
#include "../ModelCheckBaseMT.h"
#include <spot/tl/apcollect.hh>
#include <cstdint>
-#include <thread>
+#include <spot/twa/twagraph.hh>
#include <atomic>
+#include <thread>
+#include <mutex>
#include <condition_variable>
-#include <spot/twa/twagraph.hh>
+#include "misc/SafeDequeue.h"
+
class CNDFS {
@@ -21,7 +24,7 @@ private:
atomic<uint8_t> mIdThread;
static void threadHandler(void *context);
std::thread* mlThread[MAX_THREADS];
- mutex *mMutex;
+ mutex mMutex;
condition_variable cv;
void spawnThreads();
@@ -30,6 +33,7 @@ public:
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};
@@ -37,17 +41,16 @@ public:
atomic_bool red {false};
} _state;
-
- list<spot::formula> transitionNames;
-
+ SafeDequeue<myCouple> sharedPool;
+ SafeDequeue<spot::formula> transitionNames;
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 dfsRed(_state* state, deque<CNDFS::_state*> mydeque);
void WaitForTestCompleted(_state* state);
- atomic_bool awaitCondition(_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);
static spot::bdd_dict_ptr* m_dict_ptr;
};
diff --git a/src/main.cpp b/src/main.cpp
index f2447b05818f02fcb3152cea93003795fa9add66..685f2a6fb0e411f39cd7130669cfd0fa2b558b91 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -524,7 +524,7 @@ int main(int argc, char **argv)
if (algorithm == "UFSCC" || algorithm == "CNDFS")
{
std::cout<<"------------CNDFS-------------"<<std::endl;
- CNDFS cndfs(mcl,af,1); // If I increase the number of threads, a segmentation fault appears.
+ CNDFS cndfs(mcl,af,2); // If I increase the number of threads, a segmentation fault appears.
return(0);
}
else // run on the fly sequential model-checking
diff --git a/src/misc/SafeDequeue.cpp b/src/misc/SafeDequeue.cpp
index fdcb4655d56b2083db1317a36fdbb79c977d9f18..559f76b9e20fbe5002602e598b612c020321f79f 100644
--- a/src/misc/SafeDequeue.cpp
+++ b/src/misc/SafeDequeue.cpp
@@ -69,8 +69,42 @@ bool SafeDequeue<T>::empty() const
return data_queue.empty();
}
+template <typename T>
+T& SafeDequeue<T>::front()
+{
+ std::unique_lock<std::mutex> lk(mut);
+ while (data_queue.empty())
+ {
+ data_cond.wait(lk);
+ }
+ return data_queue.front();
+}
+
+template <typename T>
+T& SafeDequeue<T>::back()
+{
+ std::unique_lock<std::mutex> lk(mut);
+ while (data_queue.empty())
+ {
+ data_cond.wait(lk);
+ }
+ return data_queue.back();
+}
+
+template <typename T>
+int SafeDequeue<T>::size()
+{
+ std::unique_lock<std::mutex> lk(mut);
+ int size = data_queue.size();
+ lk.unlock();
+ return size;
+}
+
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<spot::formula>;
diff --git a/src/misc/SafeDequeue.h b/src/misc/SafeDequeue.h
index d2ffdd42689250a6ec3f3d14b081c262af91046d..10d3e5f3f281711cc95df6b110aa10abb4e0b407 100644
--- a/src/misc/SafeDequeue.h
+++ b/src/misc/SafeDequeue.h
@@ -24,10 +24,14 @@
#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;
typedef pair<couple, Set> Pair;
typedef pair<LDDState *, int> couple_th;
+typedef pair<_state*, int> coupleSucc;
struct empty_queue: std::exception {
~empty_queue() {};
const char* what() const noexcept {return "";}
@@ -64,6 +68,9 @@ class SafeDequeue {
void push ( T new_value );
bool try_pop ( T& value );
bool empty() const;
+ T& front();
+ T& back();
+ int size();
};
#endif // SAFEDEQUEUE_H