modifié : src/HybridSOG.cpp

	modifié :         src/LDDState.cpp
	modifié :         src/NewNet.h
	modifié :         src/SogKripke.cpp
	modifié :         src/threadSOG.cpp

src/HybridSOG.cpp

@@ -78,6 +78,7 @@ HybridSOG::HybridSOG(const NewNet &R, int BOUND,bool init)
     m_nonObservable=R.NonObservable;
     m_place_proposition=R.m_formula_place;
     m_transitionName=R.transitionName;
+    m_placeName=R.m_placePosName;
     InterfaceTrans=R.InterfaceTrans;
 
     m_nbPlaces=R.places.size();

src/LDDState.cpp

@@ -39,7 +39,8 @@ vector<int> LDDState::getMarkedPlaces() {
     int depth=0;
     while (mdd>lddmc_true)
     {
-        mddnode_t node=GETNODE(m_lddstate);
+        //printf("mddd : %d \n",mdd);
+        mddnode_t node=GETNODE(mdd);
         if (mddnode_getvalue(node)==1) {
             result.push_back(depth);
         }

src/NewNet.h

@@ -106,9 +106,10 @@ class NewNet : public RdPMonteur {
   int nbTransition() const { return transitions.size(); };
   set<string>& getListTransitionAP() {return m_ltransitionAP;}
   set<string>& getListPlaceAP() {return m_lplaceAP;}
+  map<int,string> m_placePosName;
   private:
   map<int,string> m_transitionPosName;
-  map<int,string> m_placePosName;
+
 
   set<string> m_ltransitionAP;
   set<string> m_lplaceAP;

src/SogKripke.cpp

@@ -43,22 +43,21 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
 
     auto ss = static_cast<const SogKripkeState*>(s);
    //////////////////////////////////////////////
-    // Must be changed
-    // State condition ????
-    ///////////////////////
-    bdd b=bddtrue;
-    return new SogKripkeIterator(ss->getLDDState(),b);//,b);//s state_condition(ss));
+
+    return new SogKripkeIterator(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
 }
 
 bdd SogKripke::state_condition(const spot::state* s) const
   {
+   cout<<"yessss "<<endl;
     auto ss = static_cast<const SogKripkeState*>(s);
     vector<int> marked_place=ss->getLDDState()->getMarkedPlaces();
-    spot::formula f=spot::formula::ap("jhkh");
-    //dict_->var_map.find(f);
+
+    cout<<"function name :"<<__func__<<endl;
     bdd result=bddtrue;
     for (auto it=marked_place.begin();it!=marked_place.end();it++) {
     string name=m_sog->getPlace(*it);
+    cout<<"Place name marked : "<<*it<<endl;
     spot::formula f=spot::formula::ap(name);
     result&=bdd_ithvar((dict_->var_map.find(f))->second);
     }

src/threadSOG.cpp

@@ -63,6 +63,7 @@ threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool
     m_nonObservable=R.NonObservable;
 
     m_transitionName=R.transitionName;
+    m_placeName=R.m_placePosName;
 
     cout<<"Toutes les Transitions:"<<endl;
     map<string,int>::iterator it2=m_transitionName.begin();
@@ -624,7 +625,7 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised)
     int rc;
     m_graph=&g;
     m_graph->setTransition(m_transitionName);
-
+    m_graph->setPlace(m_placeName);
     m_id_thread=0;
 
     pthread_mutex_init(&m_mutex, NULL);
@@ -777,6 +778,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
     Set fire;
     m_graph=&g;
     m_graph->setTransition(m_transitionName);
+    m_graph->setPlace(m_placeName);
     m_nbmetastate=0;
     m_MaxIntBdd=0;
 
@@ -965,7 +967,7 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
     Set fire;
     m_graph=&g;
     m_graph->setTransition(m_transitionName);
-
+    m_graph->setPlace(m_placeName);
 
     m_nbmetastate=0;
     m_MaxIntBdd=0;