From 5eeeba34441f58e07ed2c87d08566fa2e097391f Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Mon, 27 May 2019 00:07:51 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?= =?UTF-8?q?=20=20=20=20=20src/ModelCheckLace.h=20=09modifi=C3=A9=C2=A0:=20?= =?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeOTF.cpp?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/ModelCheckLace.cpp | 5 +++++ src/ModelCheckLace.h | 1 + src/SogKripkeOTF.cpp | 6 +++--- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index 1e73d55..69f72f8 100644 --- a/src/ModelCheckLace.cpp +++ b/src/ModelCheckLace.cpp @@ -120,3 +120,8 @@ string ModelCheckLace::getTransition(int pos) { string temp; return temp; } + +string ModelCheckLace::getPlace(int pos) { +string temp; +return temp; +} diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h index 216a361..40e7d4d 100644 --- a/src/ModelCheckLace.h +++ b/src/ModelCheckLace.h @@ -6,6 +6,7 @@ public: ModelCheckLace(const NewNet &R, int BOUND,int nbThread); LDDState * buildInitialMetaState(); string getTransition(int pos); + string getPlace(int pos); private: int m_nb_thread; MDD m_initalMarking; diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp index 77cb496..48584c6 100644 --- a/src/SogKripkeOTF.cpp +++ b/src/SogKripkeOTF.cpp @@ -58,13 +58,13 @@ bdd SogKripkeOTF::state_condition(const spot::state* s) const bdd result=bddtrue; // Marked places for (auto it=marked_place.begin();it!=marked_place.end();it++) { - string name=m_sog->getPlace(*it); + string name=m_builder->getPlace(*it); spot::formula f=spot::formula::ap(name); result&=bdd_ithvar((dict_->var_map.find(f))->second); } - vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_sog->getConstructor()->getPlaceProposition()); + vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_builder->getPlaceProposition()); for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) { - string name=m_sog->getPlace(*it); + string name=m_builder->getPlace(*it); spot::formula f=spot::formula::ap(name); result&=!bdd_ithvar((dict_->var_map.find(f))->second); } -- GitLab