modifié : src/LDDState.h

	modifié :         src/ModelCheckerTh.cpp
	modifié :         src/SogKripkeIteratorOTF.cpp
	modifié :         src/SogKripkeIteratorOTF.h
	modifié :         src/SogKripkeIteratorTh.cpp
	modifié :         src/SogKripkeIteratorTh.h
	modifié :         src/SogKripkeOTF.cpp

src/LDDState.h

@@ -24,10 +24,10 @@ class LDDState {
   pair<LDDState*, int> LastEdge;
   void setLDDValue(MDD m);
   MDD getLDDValue();
-  MDD m_lddstate;
+  MDD m_lddstate=0;
   unsigned char m_SHA2[81];
   unsigned char* getSHAValue();
-  bool m_boucle;
+  bool m_boucle=false;
   bool m_blocage;
 
 

src/ModelCheckerTh.cpp

@@ -245,5 +245,4 @@ ModelCheckerTh::~ModelCheckerTh() {
      {
          pthread_join(m_list_thread[i], NULL);
      }
-     cout<<"Destructor "<<endl;
 }

src/SogKripkeIteratorOTF.cpp

@@ -74,3 +74,4 @@ SogKripkeIteratorOTF::~SogKripkeIteratorOTF()
 
 static ModelCheckLace * SogKripkeIteratorOTF::m_builder;
 static spot::bdd_dict_ptr* SogKripkeIteratorOTF::m_dict_ptr;
+static LDDState SogKripkeIteratorOTF::m_deadlock;

src/SogKripkeIteratorOTF.h

@@ -7,7 +7,7 @@
 class SogKripkeIteratorOTF : public spot::kripke_succ_iterator
 {
 public:
-
+    static LDDState m_deadlock;
     static ModelCheckLace * m_builder;
     static spot::bdd_dict_ptr* m_dict_ptr;
   //  sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);

src/SogKripkeIteratorTh.cpp

@@ -7,13 +7,14 @@
 SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
 {
 
-    m_lddstate->setDiv(true);
+    //m_lddstate->setDiv(true);
+    //if (m_lddstate->getLDDValue()) m_lddstate->setDeadLock(true);
     for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
         m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
     }
-   /* if (lddstate->isDeadLock()) {
-        m_lsucc.push_back(pair(,-1));
-    }*/
+   if (lddstate->isDeadLock()) {
+     m_lsucc.push_back(pair<LDDState*,int>(&m_deadlock,-1));
+    }
     if (lddstate->isDiv()) {
         m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
     }
@@ -58,8 +59,6 @@ bdd SogKripkeIteratorTh::cond()  const {
     spot::formula f=spot::formula::ap(name);
     bdd   result=bdd_ithvar((p->var_map.find(f))->second);
 
-    //cout<<"Iterator "<<__func__<<"  "<<m_current_edge<<"\n";*/
-    //cout<<"exciting "<<__func__<<endl;
     return result & spot::kripke_succ_iterator::cond();
 }
 
@@ -74,3 +73,4 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
 
 static ModelCheckerTh * SogKripkeIteratorTh::m_builder;
 static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
+static LDDState SogKripkeIteratorTh::m_deadlock;

src/SogKripkeIteratorTh.h

@@ -7,7 +7,7 @@
 class SogKripkeIteratorTh : public spot::kripke_succ_iterator
 {
 public:
-
+    static LDDState m_deadlock;
     static ModelCheckerTh * m_builder;
     static spot::bdd_dict_ptr* m_dict_ptr;
   //  sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);

src/SogKripkeOTF.cpp

@@ -15,6 +15,7 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder)
     SogKripkeIteratorOTF::m_builder=builder;
     SogKripkeStateOTF::m_builder=builder;
     SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
+
     //cout<<__func__<<endl;
 }