From 71c6ecac65ef63515b7409f66837d8a0f1b619f9 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Wed, 19 Jun 2019 16:14:30 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/ModelCheckerTh.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/ModelCheckerTh.cpp | 10 ++++++----
src/main.cpp | 4 ++--
2 files changed, 8 insertions(+), 6 deletions(-)
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 4fc0d3e..56a5895 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -139,17 +139,17 @@ void * ModelCheckerTh::Compute_successors()
MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
ldd_refs_push(Complete_meta_state);
- MDD canonised_initial=Canonize(Complete_meta_state,0);
+ MDD canonised_initial=Complete_meta_state;//Canonize(Complete_meta_state,0);
ldd_refs_push(canonised_initial);
fire=firable_obs(Complete_meta_state);
c->m_lddstate=canonised_initial;
-
+ c->setDeadLock(Set_Bloc(Complete_meta_state));
+ c->setDiv(Set_Div(Complete_meta_state));
m_st[0].push(Pair(couple(c,Complete_meta_state),fire));
m_graph->setInitialState(c);
m_graph->insert(c);
- //m_graph->nbMarking+=bdd_pathcount(c->m_lddstate);
m_charge[0]=1;
m_finish_initial=true;
@@ -193,7 +193,7 @@ void * ModelCheckerTh::Compute_successors()
ldd_refs_push(Complete_meta_state);
- MDD reduced_meta=Canonize(Complete_meta_state,0);
+ MDD reduced_meta=Complete_meta_state;//Canonize(Complete_meta_state,0);
ldd_refs_push(reduced_meta);
if (id_thread==0)
@@ -225,6 +225,8 @@ void * ModelCheckerTh::Compute_successors()
m_graph->addArc();
m_graph->insert(reached_class);
+ reached_class->setDiv(Set_Div(Complete_meta_state));
+ reached_class->setDeadLock(Set_Bloc(Complete_meta_state));
pthread_mutex_unlock(&m_graph_mutex);
e.first.first->Successors.insert(e.first.first->Successors.begin(),LDDEdge(reached_class,t));
diff --git a/src/main.cpp b/src/main.cpp
index bc75319..b174cec 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -157,7 +157,7 @@ int main(int argc, char** argv)
mcl->loadNet();
auto k =
std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
- /* cout<<"Want to save the graph in a dot file ?";
+ cout<<"Want to save the graph in a dot file ?";
cin>>c;
if (c=='y')
{
@@ -167,7 +167,7 @@ int main(int argc, char** argv)
file.open(st.c_str(),fstream::out);
spot::print_dot(file, k,"ka");
file.close();
- } */ ;
+ } ;
// Performing on the fly Modelchecking
cout<<"Performing on the fly Modelchecking"<<endl;
--
GitLab