From 6393f641864a4978982abd7c33d469ba2268cf85 Mon Sep 17 00:00:00 2001
From: Ghofrane Amaimi <ghofraneeamaimi@gmail.com>
Date: Thu, 21 Jul 2022 13:47:01 +0200
Subject: [PATCH] cycle detected without buddy
---
src/algorithm/CNDFS.cpp | 37 +++++++++++++++++++++++++------------
src/main.cpp | 2 +-
2 files changed, 26 insertions(+), 13 deletions(-)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 738483a..cfa92a4 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -17,6 +17,7 @@
#include <algorithm>
#include "misc/stacksafe.h"
#include <spot/twa/formula2bdd.hh>
+#include <spot/tl/formula.hh>
#include <spot/misc/minato.hh>
#include <spot/twaalgos/contains.hh>
#include <spot/tl/contain.hh>
@@ -101,6 +102,7 @@ void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread)
Rp.push_back(state);
// computeSuccessors(state);
for (const auto &succ: state->new_successors) {
+ cout << "dfs red 1 " << succ.first->cyan[idThread]<< endl;
if (succ.first->cyan[idThread]) {
cout << "cycle detected" << endl;
exit(0);
@@ -137,6 +139,10 @@ 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()))
{
@@ -144,6 +150,13 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
auto ap_state = spot::formula::ap(name);
if (p->var_map.find(ap_state) != p->var_map.end()) {
ap_sog.push_back(ap_state);
+ for( auto n: p->var_map)
+ {
+ if (n.first != ap_state)
+ {
+ ap_sog.push_back(spot::formula::Not(n.first));
+ }
+ }
}
}
//iterate over the successors of a current aggregate
@@ -154,20 +167,18 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
if (p->var_map.find(ap_edge) != p->var_map.end()) {
ap_sog.push_back(ap_edge);
}
+
spot::formula pa_sog_result = spot::formula::And(ap_sog);
- cout << "formula 1 " << 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 f = spot::bdd_to_formula(ii->cond(), p);
- cout << "formula 2 " << f << endl;
-// std::cout << (spot::are_equivalent(f, pa_sog_result) ?
+ auto pa_ba_result = spot::bdd_to_formula(ii->cond(), p);
+ 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(f, pa_sog_result) << endl;
-
-
+// std::cout << "match " << c.contained(pa_sog_result, pa_ba_result) << endl;
// auto form= p->var_map.find(bdd_var(ii->cond()))->second.id();
// cout << "here " << form << endl;
// if (p->var_map.find(pa_sog_result) != p->var_map.end()) { //extra text
@@ -175,7 +186,7 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
// //fetch the transition of BA that have the same AP as the SOG transition
// cout << "dbb "<< mAa->register_ap(pa_sog_result) << endl; //The BDD variable number assigned for this atomic proposition.
// const bdd result = bdd_ithvar((p->var_map.find(pa_sog_result))->second);
- if (c.contained(f, pa_sog_result)) {
+ if (c.contained(pa_sog_result, pa_ba_result) || c.contained(pa_ba_result, pa_sog_result)) {
std::unique_lock lk(mMutex);
auto result = isStateBuilt(elt.first, (spot::twa_graph_state *) ii->dst());
if (result) {
@@ -194,14 +205,16 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
mDataCondWait.notify_all();
}
-
+int i =0;
//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;
+// cout << "current state " << state << " cyan " << state->cyan[idThread]<< endl;
for (const auto &succ: state->new_successors) {
- cout << "cyan " << succ.first->cyan[idThread] << endl;
+// cout << "cyan " << succ.first->cyan[idThread] << endl;
if (!succ.first->blue && !succ.first->cyan[idThread]) {
dfsBlue(succ.first, Rp, idThread, ap_sog);
}
diff --git a/src/main.cpp b/src/main.cpp
index cc0fddc..a201e03 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -526,7 +526,7 @@ int main(int argc, char **argv)
if (algorithm == "UFSCC" || algorithm == "CNDFS")
{
std::cout<<"------------CNDFS-------------"<<std::endl;
- CNDFS cndfs(mcl,af,2); // If I increase the number of threads, a segmentation fault appears.
+ CNDFS cndfs(mcl,af,1); // If I increase the number of threads, a segmentation fault appears.
return(0);
}
else // run on the fly sequential model-checking
--
GitLab