modifié : src/SogKripke.h

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

src/SogKripke.h

 #ifndef SOGKRIPKE_H_INCLUDED
 #define SOGKRIPKE_H_INCLUDED
-
+#include "LDDGraph.h"
+#include "SogKripkeIterator.h"
 class SogKripke : public spot::kripke
 {
     public:
@@ -10,7 +11,7 @@ class SogKripke : public spot::kripke
         SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
         virtual ~SogKripke();
         spot::state* get_init_state() const;
-        SpotSogIterator* succ_iter(const spot::state* s) const override;
+        SogKripkeIterator* succ_iter(const spot::state* s) const override;
         std::string format_state(const spot::state* s) const override;
         MDD state_condition(const spot::state* s) const override;
 

src/SogKripkeIterator.cpp

+#include <spot/twa/twa.hh>
+#include "LDDGraph.h"
+#include "SogKripkeState.h"
+#include "SogKripkeIterator.h"
+
+
+SogKripkeIterator::SogKripkeIterator(const LDDState* lddstate):m_lddstate(lddstate)
+{
+    //vector<pair<LDDState*, int>>
+    m_lddstate->setDiv(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->isDiv()) {
+        m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
+    }
+}
+bool SogKripkeIterator::first() {
+  //  m_sog->getLDDStateById(m_id)->Successors().
+    //return m_sog->get_successor()
+
+    m_current_edge=0;
+    return m_lsucc.size()!=0;
+}
+
+bool SogKripkeIterator::next() {
+
+    m_current_edge++;
+    return m_current_edge<m_lsucc.size();
+}
+
+bool SogKripkeIterator::done() const {
+
+    return m_current_edge==m_lsucc.size();
+}
+
+SpotSogState* SogKripkeIterator::dst() const
+  {
+    return new SpotSogState(m_lsucc.at(m_current_edge).first);
+  }
+
+bdd SogKripkeIterator::cond()  const {
+    if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+    string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
+    //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
+
+    spot::bdd_dict *p=m_dict_ptr->get();
+    spot::formula f=spot::formula::ap(name);
+    bdd   result=bdd_ithvar((p->var_map.find(f))->second);
+
+    //cout<<"Iterator "<<__func__<<"  "<<m_current_edge<<"\n";
+    return result;
+}
+
+spot::acc_cond::mark_t SogKripkeIterator::acc() const {
+  //cout<<"Iterator acc()\n";
+  return 1U;
+}
+SogKripkeIterator::~SogKripkeIterator()
+{
+    //dtor
+}
+
+static LDDGraph * SogKripkeIterator::m_graph;
+static spot::bdd_dict_ptr* SogKripkeIterator::m_dict_ptr;

src/SogKripkeIterator.h

 #ifndef SOGKRIPKEITERATOR_H_INCLUDED
 #define SOGKRIPKEITERATOR_H_INCLUDED
+#include "SogKripkeState.h"
+#include "LDDGraph.h"
+// Iterator for a SOG graph
+class SogKripkeIterator : public spot::twa_succ_iterator
+{
+    public:
 
+        static LDDGraph * m_graph;
+        static spot::bdd_dict_ptr* m_dict_ptr;
+        SogKripkeIterator(const LDDState *lddstate);
+        virtual ~SogKripkeIterator();
+        bool first() override;
+        bool next() override;
+        bool done() const override;
+        SogKripkeState* dst() const override;
+
+        bdd cond() const override final;
+        spot::acc_cond::mark_t acc() const override final;
+
+    protected:
+
+    private:
+        // Associated SOG graph
+
+        LDDState * m_lddstate;
+        vector<pair<LDDState*, int>> m_lsucc;
+        unsigned int m_current_edge=0;
+};
 
 
 #endif // SOGKRIPKEITERATOR_H_INCLUDED

src/SogKripkeState.cpp

+#include "LDDState.h"
+#include "SogKripkeState.h"
+
+
+SogKripkeState::~SogKripkeState()
+{
+    //dtor
+}

src/SogKripkeState.h

@@ -2,5 +2,40 @@
 #define SOGKRIPKESTATE_H_INCLUDED
 
 
+#include "LDDState.h"
+class SogKripkeState : public spot::state
+{
+public:
+    SogKripkeState(LDDState *st):m_state(st) {};
+    virtual ~SogKripkeState();
+
+    SogKripkeState* clone() const override
+    {
+        return new SogKripkeState(m_state);
+    }
+    size_t hash() const override
+    {
+        return m_state->getLDDValue();
+    }
+
+    int compare(const spot::state* other) const override
+    {
+        auto o = static_cast<const SogKripkeState*>(other);
+        size_t oh = o->hash();
+        size_t h = hash();
+        if (h < oh)
+            return -1;
+        else
+            return h > oh;
+    }
+    LDDState* getLDDState() {
+        return m_state;
+    }
+protected:
+
+private:
+    LDDState *m_state;
+};
+
 
 #endif // SOGKRIPKESTATE_H_INCLUDED

src/main.cpp

@@ -23,6 +23,7 @@
 #include <spot/tl/apcollect.hh>
 #include "NewNet.h"
 #include "SogTwa.h"
+#include "SogKripke.h"