From c9915e41ba9d59cbbc29bfb80ba08f0a703f44b0 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Tue, 31 Mar 2020 16:05:25 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/CommonSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/CommonSOG.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/LDDGraph.cpp=20=09modifi=C3=A9=C2=A0:=20=20?=
=?UTF-8?q?=20=20=20=20=20=20=20src/ModelCheckBaseMT.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/ModelCheckerTh.cpp=20=09m?=
=?UTF-8?q?odifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeTh.cp?=
=?UTF-8?q?p?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
CMakeLists.txt | 2 +-
src/CommonSOG.cpp | 2 +-
src/CommonSOG.h | 2 +-
src/LDDGraph.cpp | 1 +
src/ModelCheckBaseMT.cpp | 4 ++--
src/ModelCheckerTh.cpp | 18 +++++++++---------
src/SogKripkeTh.cpp | 2 +-
7 files changed, 16 insertions(+), 15 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 668dedc..f11cb07 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -6,7 +6,7 @@ project(pmc-sog C CXX)
# compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -g3")
endif()
# add pn parser
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 498a6d4..8200ca6 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -226,4 +226,4 @@ string CommonSOG::getPlace(int pos)
{
return m_graph->getPlace(pos);
}
-
+static LDDGraph *CommonSOG::m_graph;
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index e94a93e..39a3d47 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -29,7 +29,7 @@ class CommonSOG
protected:
NewNet* m_net;
int m_nbPlaces = 0;
- LDDGraph *m_graph;
+ static LDDGraph *m_graph;
vector<TransSylvan> m_tb_relation;
MDD m_initialMarking;
map<string, uint16_t> m_transitionName;
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index b8e89d2..eaba61f 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -12,6 +12,7 @@ LDDGraph::~LDDGraph()
void LDDGraph::setInitialState(LDDState *c)
{
m_currentstate=m_initialstate=c;
+ //
}
diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp
index 4a854fa..69af203 100644
--- a/src/ModelCheckBaseMT.cpp
+++ b/src/ModelCheckBaseMT.cpp
@@ -14,8 +14,8 @@ ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R,int nbThread)
}
void ModelCheckBaseMT::loadNet()
{
- preConfigure();
- m_graph=new LDDGraph(this);
+ m_graph=new LDDGraph(this);
+ preConfigure();
m_graph->setTransition(m_transitionName);
m_graph->setPlace(m_placeName);
}
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 67b02dc..05efa1e 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -86,8 +86,7 @@ void ModelCheckerTh::preConfigure() {
}
LDDState* ModelCheckerTh::getInitialMetaState() {
- while (!m_finish_initial)
- ;
+ while (!m_finish_initial) ;
LDDState *initial_metastate = m_graph->getInitialState();
if (!initial_metastate->isVisited()) {
initial_metastate->setVisited();
@@ -112,18 +111,20 @@ void* ModelCheckerTh::Compute_successors() {
pthread_mutex_unlock(&m_mutex);
Set fire;
int min_charge = 0;
+
if (id_thread == 0) {
LDDState *c = new LDDState;
MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
ldd_refs_push(Complete_meta_state);
MDD canonised_initial = Complete_meta_state; //Canonize(Complete_meta_state,0);
- ldd_refs_push(canonised_initial);
+ /*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));
+ c->setDeadLock(false);//Set_Bloc(Complete_meta_state));
+ c->setDiv(false);//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_charge[0] = 1;
@@ -154,10 +155,9 @@ void* ModelCheckerTh::Compute_successors() {
}
MDD Complete_meta_state = Accessible_epsilon(get_successor(e.first.second, t));
-
ldd_refs_push(Complete_meta_state);
MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0);
- ldd_refs_push(reduced_meta);
+ /*ldd_refs_push(reduced_meta);*/
if (id_thread == 0) {
pthread_mutex_lock(&m_gc_mutex);
@@ -188,8 +188,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));
+ reached_class->setDiv(false);//Set_Div(Complete_meta_state));
+ reached_class->setDeadLock(false);//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/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index 9cb4ccc..d410ea5 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -78,7 +78,7 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
{
auto ss = static_cast<const SogKripkeStateTh*>(s);
- vector<uint16_t> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
+ vector<uint16_t> marked_place = ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
bdd result=bddtrue;
--
GitLab