diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index 08f95b4f339dd588f3035532e2d92fd9d7447145..3f2ed91af0de40d56cf3f35debe5268a81b01620 100644
--- a/src/LDDState.cpp
+++ b/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;
+}
 
 
diff --git a/src/LDDState.h b/src/LDDState.h
index 072580291bb3b0088fca9f7811e5103274585939..7f444c69a45f3db24092850f922aa2cd9c9262ee 100755
--- a/src/LDDState.h
+++ b/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:
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index db484e9f9e0eb2c6559296b8d23c6518db0f3631..d2dffaa205d2f30cef05ca44a214f5a847a44e01 100644
--- a/src/SogKripke.cpp
+++ b/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;
   }