diff --git a/src/SogKripke.h b/src/SogKripke.h
index 6dae6cfb1dd5705312580575c0777e8c053a9e15..b6fc776b246cd2fe754c2476ae4eaffc81b0f3da 100644
--- a/src/SogKripke.h
+++ b/src/SogKripke.h
@@ -1,6 +1,7 @@
 #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;
 
diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..20565dcf9ac12be92ea11fd53e1447ca95780b20 100644
--- a/src/SogKripkeIterator.cpp
+++ b/src/SogKripkeIterator.cpp
@@ -0,0 +1,68 @@
+#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;
diff --git a/src/SogKripkeIterator.h b/src/SogKripkeIterator.h
index eed35492ab0ff8ef472b0600d619d3b9edf7cb5d..33fdf33a5b260b6446a74d3e55ee3c78cd26e615 100644
--- a/src/SogKripkeIterator.h
+++ b/src/SogKripkeIterator.h
@@ -1,6 +1,33 @@
 #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
diff --git a/src/SogKripkeState.cpp b/src/SogKripkeState.cpp
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..8d471cc0fae3acf2e119050d4b5f9ee74786f02d 100644
--- a/src/SogKripkeState.cpp
+++ b/src/SogKripkeState.cpp
@@ -0,0 +1,8 @@
+#include "LDDState.h"
+#include "SogKripkeState.h"
+
+
+SogKripkeState::~SogKripkeState()
+{
+    //dtor
+}
diff --git a/src/SogKripkeState.h b/src/SogKripkeState.h
index 57c6dbe7648b8273d0b9f945c28b5a08302d594f..089692b2ad4b7fbb325ac05b4dae4cc5b0369efb 100644
--- a/src/SogKripkeState.h
+++ b/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
diff --git a/src/main.cpp b/src/main.cpp
index bcba3af558ced24720697c63058845cc458141b8..4645d56af360016a2f3741cee419e1bb517e5f6f 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -23,6 +23,7 @@
 #include <spot/tl/apcollect.hh>
 #include "NewNet.h"
 #include "SogTwa.h"
+#include "SogKripke.h"