diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp index 1e73d55aed98d2a9ea539de5bf4cf786831d29e4..69f72f8fdeac3b9d6d1b8934dfd6e2123163a7c5 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 216a361da9e427268e5b5b7955b0b0ede9141f53..40e7d4dd921269d085eec815cdf0c087633d8110 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 77cb496340461e479e46eb76dd0e41b98a8fc3a2..48584c67cc4b5743c23e861f8876dabc883b2a5c 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); }