modifié : src/ModelCheckLace.h

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

src/ModelCheckLace.h

@@ -4,7 +4,7 @@
 class ModelCheckLace : public CommonSOG {
 public:
         ModelCheckLace(const NewNet &R, int BOUND,int nbThread);
-        LDDState & buildInitialMetaState();
+        LDDState * buildInitialMetaState();
         string getTransition(int pos);
 private:
     int m_nb_thread;

src/SogKripkeOTF.cpp

@@ -27,7 +27,7 @@ SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *bu
 
 state* SogKripkeOTF::get_init_state() const {
     //cout<<"Initial state given...\n";
-    return new SogKripkeStateOTF(m_sog->getInitialState());//new SpotSogState();
+    return new SogKripkeStateOTF(m_builder->buildInitialMetaState());//new SpotSogState();
 
 }
 // Allows to print state label representing its id
@@ -52,7 +52,7 @@ bdd SogKripkeOTF::state_condition(const spot::state* s) const
   {
 
     auto ss = static_cast<const SogKripkeStateOTF*>(s);
-    vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
+    vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
 
 
     bdd result=bddtrue;

src/SogKripkeOTF.h

@@ -10,7 +10,7 @@
 class SogKripkeOTF: public spot::kripke {
     public:
 
-        //SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
+        SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder);
         SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder,set<string> &l_transap,set<string> &l_placeap);
         virtual ~SogKripkeOTF();
         spot::state* get_init_state() const;