diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6e83dc31f4d6db034da5bff69b6e89e5019573ed..ba2bdb001c42b5da2db217c4618a57b434498b5c 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -75,3 +75,4 @@ 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 1443e6b5c37df39e9be393d2d08bf40841221365..e0cc32b599ddde6a3b9b041bb688f0301add255e 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -22,6 +22,8 @@
using namespace std;
+int i=0;
+
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
mNbTh(nbTh) {
dict_ba = mAa->get_dict();
@@ -100,6 +102,8 @@ void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread)
// cout << "dfsRed" << endl;
Rp.push_back(state);
// computeSuccessors(state);
+ std::mt19937 g(rd());
+ std::shuffle(state->new_successors.begin(), state->new_successors.end(), g);
for (const auto &succ: state->new_successors) {
// cout << "dfs red 1 " << succ.first->cyan[idThread]<< endl;
if (succ.first->cyan[idThread]) {
@@ -107,14 +111,16 @@ void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread)
exit(0);
}
// unvisited and not red state
- if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && !succ.first->red)
+ if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && !succ.first->red){
dfsRed(succ.first, Rp, idThread);
+ }
+
}
}
/*
* Check whether a product state exists or not
- */
+*/
myState_t *CNDFS::isStateBuilt(LDDState *sogState, spot::twa_graph_state *spotState) {
auto compare = [sogState, spotState](myState_t *state) {
return (state->left == sogState && state->right == spotState);
@@ -125,6 +131,7 @@ myState_t *CNDFS::isStateBuilt(LDDState *sogState, spot::twa_graph_state *spotSt
//compute new successors of a product state
void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
+
if (state->succState == SuccState::done) return;
std::unique_lock lk(mMutexStatus);
if (state->succState == SuccState::doing) {
@@ -144,13 +151,6 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
auto ap_state = spot::formula::ap(name);
if (dict_ba->var_map.find(ap_state) != dict_ba->var_map.end()) {
ap_sog.push_back(ap_state);
- for( auto n: dict_ba->var_map)
- {
- if (n.first != ap_state)
- {
- ap_sog.push_back(spot::formula::Not(n.first));
- }
- }
}
}
//iterate over the successors of a current aggregate
@@ -161,9 +161,13 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
if (dict_ba->var_map.find(ap_edge) != dict_ba->var_map.end()) {
ap_sog.push_back(ap_edge);
}
-
- spot::formula pa_sog_result = spot::formula::And(ap_sog);
-// cout << "formula sog: " << pa_sog_result << endl;
+ for( auto &n: dict_ba->var_map)
+ {
+ if (std::find(ap_sog.begin(), ap_sog.end(), n.first) == ap_sog.end()) {
+ ap_sog.push_back(spot::formula::Not(n.first));
+ }
+ }
+ auto pa_sog_result = spot::formula::And(ap_sog);
//iterate over the successors of a BA state
auto ii = mAa->succ_iter(ba_current_state);
if (ii->first())
diff --git a/src/algorithm/CndfsV2.cpp b/src/algorithm/CndfsV2.cpp
index b2916febd4692bf855dfefd1eb64f4eb8bf3c9fb..60bdf27b19afd44a1a7c562969d3bb791e17b7d6 100644
--- a/src/algorithm/CndfsV2.cpp
+++ b/src/algorithm/CndfsV2.cpp
@@ -99,7 +99,6 @@ myState_t *CndfsV2::buildState(myState_t *state, pair<spot::formula, int > tr) {
buildStatePtr->right = getSuccessorFromBA(state->right,tr);
buildStatePtr->isAcceptance = mAa->state_is_accepting(buildStatePtr->right);
buildStatePtr->isConstructed = true;
-
return buildStatePtr;
}
@@ -109,6 +108,8 @@ void CndfsV2::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread
// cout << "dfsRed" << endl;
Rp.push_back(state);
// computeSuccessors(state);
+ std::mt19937 g(rd());
+ std::shuffle(state->new_successors.begin(), state->new_successors.end(), g);
for (const auto &succ: state->new_successors) {
// cout << "dfs red 1 " << succ.first->cyan[idThread]<< endl;
if (succ.first->cyan[idThread]) {
@@ -155,13 +156,6 @@ void CndfsV2::fireable(myState_t *state, vector<spot::formula> ap_sog, uint8_t
auto ap_state = spot::formula::ap(name);
if (dict_ba->var_map.find(ap_state) != dict_ba->var_map.end()) {
ap_sog.push_back(ap_state);
- for( auto n: dict_ba->var_map)
- {
- if (n.first != ap_state)
- {
- ap_sog.push_back(spot::formula::Not(n.first));
- }
- }
}
}
//iterate over the successors of a current aggregate
@@ -172,7 +166,12 @@ void CndfsV2::fireable(myState_t *state, vector<spot::formula> ap_sog, uint8_t
if (dict_ba->var_map.find(ap_edge) != dict_ba->var_map.end()) {
ap_sog.push_back(ap_edge);
}
-
+ for( auto n: dict_ba->var_map)
+ {
+ if (std::find(ap_sog.begin(), ap_sog.end(), n.first) == ap_sog.end()) {
+ ap_sog.push_back(spot::formula::Not(n.first));
+ }
+ }
spot::formula pa_sog_result = spot::formula::And(ap_sog);
// cout << "formula sog: " << pa_sog_result << endl;
//iterate over the successors of a BA state
diff --git a/src/main.cpp b/src/main.cpp
index ba18f34e2b6e8eaee463e6e14695854dd6ba70b7..82c37bfac3a5b77cbb24e6426c969b4afb2f8833 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -528,7 +528,15 @@ int main(int argc, char **argv)
if (algorithm == "CndfsV1")
{
cout<<"------------MC-CNDFS-VERSION1-------------"<<endl;
- CNDFS cndfs(mcl,af,2); // If I increase the number of threads, a segmentation fault appears.
+ //start time
+// std::chrono::steady_clock::time_point startTime, finalTime;
+// startTime = std::chrono::steady_clock::now();
+ CNDFS cndfs(mcl,af,2);
+// finalTime = std::chrono::steady_clock::now();
+// displayTime(startTime, finalTime);
+
+ //finish time
+ //diff
return(0);
}
else if (algorithm == "CndfsV2")// run on the fly sequential model-checking
@@ -545,7 +553,9 @@ int main(int argc, char **argv)
}else
{
auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
+ //temps depart
runOnTheFlyMC(algorithm, k, af);
+ //temps fin
}
// stop model checker process