modifié : src/SogKripkeIteratorTh.cpp

	modifié :         src/SogKripkeIteratorTh.h
	modifié :         src/SogKripkeTh.cpp

src/SogKripkeIteratorTh.cpp

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

src/SogKripkeIteratorTh.h

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

src/SogKripkeTh.cpp

@@ -15,7 +15,9 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder)
     SogKripkeIteratorTh::m_builder=builder;
     SogKripkeStateTh::m_builder=builder;
     SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
-    
+    SogKripkeIteratorTh::m_deadlock.setLDDValue(1);
+    SogKripkeIteratorTh::m_div.setLDDValue(0);
+    SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));
 }
 
 SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {