modifié : src/LDDState.cpp

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

src/LDDState.cpp

@@ -55,5 +55,26 @@ vector<int> LDDState::getMarkedPlaces(set<int>& lplacesAP) {
     return result;
 }
 
+vector<int> LDDState::getUnmarkedPlaces(set<int>& lplacesAP) {
+    vector<int> result;
+    MDD mdd=m_lddstate;
+
+    int depth=0;
+    while (mdd>lddmc_true)
+    {
+        //printf("mddd : %d \n",mdd);
+        mddnode_t node=GETNODE(mdd);
+        if (lplacesAP.find(depth)!=lplacesAP.end())
+        if (mddnode_getvalue(node)==0) {
+            result.push_back(depth);
+            cout<<"depth "<<depth<<endl;
+        }
+
+        mdd=mddnode_getdown(node);
+        depth++;
+
+    }
+    return result;
+}
 
 

src/LDDState.h

@@ -38,6 +38,7 @@ class LDDState {
   void setDeadLock(bool de) {m_blocage=de;}
   bool isDeadLock() {return m_blocage;}
   vector<int> getMarkedPlaces(set<int>& lplacesAP);
+  vector<int> getUnmarkedPlaces(set<int>& lplacesAP);
 
  protected:
  private:

src/SogKripke.cpp

@@ -56,14 +56,18 @@ bdd SogKripke::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);
-    //cout<<"Place name marked : "<<"  "<<name<<endl;
     spot::formula f=spot::formula::ap(name);
-    result=bdd_ithvar((dict_->var_map.find(f))->second);
-    cout<<"verified ldd : "<<ss->getLDDState()->getLDDValue()<<"Place name marked : "<<name<<endl;
+    result&=bdd_ithvar((dict_->var_map.find(f))->second);
+    }
+    vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
+    for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
+    string name=m_sog->getPlace(*it);
+    spot::formula f=spot::formula::ap(name);
+    result&=!bdd_ithvar((dict_->var_map.find(f))->second);
     }
-
   return result;
   }