modifié : src/ModelCheckLace.cpp

	modifié :         src/ModelCheckLace.h
	modifié :         src/SogKripkeOTF.cpp

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;
+}

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;

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);
     }