From 57a3e5cd9506bef527be46ef29eafd84483fe9db Mon Sep 17 00:00:00 2001
From: Ghofrane Amaimi <ghofraneeamaimi@gmail.com>
Date: Thu, 21 Jul 2022 15:06:10 +0200
Subject: [PATCH] add the shuffle
---
src/algorithm/CNDFS.cpp | 27 ++++++++++++---------------
1 file changed, 12 insertions(+), 15 deletions(-)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index cfa92a4..efd7249 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -21,6 +21,8 @@
#include <spot/misc/minato.hh>
#include <spot/twaalgos/contains.hh>
#include <spot/tl/contain.hh>
+#include <random>
+#include <algorithm>
using namespace std;
@@ -98,13 +100,13 @@ std::ostream &operator<<(std::ostream &Str, myState_t *state) {
}
void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread) {
- cout << "dfsRed" << endl;
+// cout << "dfsRed" << endl;
Rp.push_back(state);
// computeSuccessors(state);
for (const auto &succ: state->new_successors) {
- cout << "dfs red 1 " << succ.first->cyan[idThread]<< endl;
+// cout << "dfs red 1 " << succ.first->cyan[idThread]<< endl;
if (succ.first->cyan[idThread]) {
- cout << "cycle detected" << endl;
+ cout << "cycle detected with the thread " << unsigned(idThread) << endl;
exit(0);
}
// unvisited and not red state
@@ -139,10 +141,6 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
const spot::twa_graph_state *ba_current_state = state->right;
while (!sog_current_state->isCompletedSucc());
auto p = mAa->get_dict();//avoir le dictionnaire bdd,proposition atomique
-// for( auto n: p->var_map)
-// {
-// cout << n.first <<endl;
-// }
//fetch the state's atomic proposition
for (const auto & vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
{
@@ -169,13 +167,13 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
}
spot::formula pa_sog_result = spot::formula::And(ap_sog);
- cout << "formula sog: " << pa_sog_result << endl;
+// cout << "formula sog: " << pa_sog_result << endl;
//iterate over the successors of a BA state
auto ii = mAa->succ_iter(ba_current_state);
if (ii->first())
do {
- auto pa_ba_result = spot::bdd_to_formula(ii->cond(), p);
- cout << "formula ba: " << pa_ba_result << endl;
+ auto pa_ba_result = spot::bdd_to_formula(ii->cond(), p); // from bdd to formula
+// cout << "formula ba: " << pa_ba_result << endl;
// std::cout << (spot::are_equivalent(pa_ba_result, pa_sog_result) ?
// "Equivalent\n" : "Not equivalent\n");
// std::cout << "match " << c.contained(pa_sog_result, pa_ba_result) << endl;
@@ -205,14 +203,13 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
mDataCondWait.notify_all();
}
-int i =0;
+std::random_device rd;
//Perform the dfsBlue
void CNDFS::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread, vector<spot::formula> ap_sog) {
- cout << "appel " << i << endl;
- i++;
state->cyan[idThread] = true;
computeSuccessors(state, ap_sog);
-// cout << "current state " << state << " cyan " << state->cyan[idThread]<< endl;
+ std::mt19937 g(rd());
+ std::shuffle(state->new_successors.begin(), state->new_successors.end(), g);
for (const auto &succ: state->new_successors) {
// cout << "cyan " << succ.first->cyan[idThread] << endl;
if (!succ.first->blue && !succ.first->cyan[idThread]) {
@@ -221,7 +218,7 @@ void CNDFS::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread,
}
state->blue = true;
if (state->isAcceptance) {
- cout << "Acceptance state detected " << endl;
+// cout << "Acceptance state detected " << endl;
if (state->left->isDeadLock() || state->left->isDiv()) {
cout << "cycle detected: an aggregate with deal_lock or live_lock" << endl;
exit(0);
--
GitLab