modifié : src/SogKripke.cpp

	modifié :         src/SogKripkeIterator.cpp
	modifié :         src/SogKripkeIterator.h
	modifié :         src/SogKripkeState.cpp

src/SogKripke.cpp

@@ -49,8 +49,12 @@ std::string SogKripke::format_state(const spot::state* s) const
 SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
 
     auto ss = static_cast<const SogKripkeState*>(s);
-    bdd b=bddfalse;
-    return new SogKripkeIterator(ss->getLDDState());//,b);//s state_condition(ss));
+   //////////////////////////////////////////////
+    // Must be changed
+    // State condition ????
+    ///////////////////////
+    bdd b=bddtrue;
+    return new SogKripkeIterator(ss->getLDDState(),b);//,b);//s state_condition(ss));
 }
 
   /* MDD state_condition(const spot::state* s) const override

src/SogKripkeIterator.cpp

-#include <spot/twa/twa.hh>
+#include <spot/kripke/kripke.hh>
 #include "LDDGraph.h"
 #include "SogKripkeState.h"
 #include "SogKripkeIterator.h"
 
 
-SogKripkeIterator::SogKripkeIterator(const LDDState* lddstate):m_lddstate(lddstate)
+SogKripkeIterator::SogKripkeIterator(const LDDState* lddstate, bdd cond):kripke_succ_iterator(cond),m_lddstate(lddstate)
 {
     //vector<pair<LDDState*, int>>
     m_lddstate->setDiv(true);

src/SogKripkeIterator.h

@@ -2,14 +2,15 @@
 #define SOGKRIPKEITERATOR_H_INCLUDED
 #include "SogKripkeState.h"
 #include "LDDGraph.h"
+#include <spot/kripke/kripke.hh>
 // Iterator for a SOG graph
-class SogKripkeIterator : public spot::twa_succ_iterator
+class SogKripkeIterator : public spot::kripke_succ_iterator
 {
     public:
 
         static LDDGraph * m_graph;
         static spot::bdd_dict_ptr* m_dict_ptr;
-        SogKripkeIterator(const LDDState *lddstate);
+        SogKripkeIterator(const LDDState *lddstate,bdd cond);
         virtual ~SogKripkeIterator();
         bool first() override;
         bool next() override;

src/SogKripkeState.cpp

-#include <spot/twa/twa.hh>
+#include <spot/kripke/kripke.hh>
 #include "LDDState.h"
 #include "SogKripkeState.h"