diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f4953cc3b80278b1043e7a2978f3cf5f81382792..3c737d71afcb6164c04b47f6414fd68c140867f2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -52,7 +52,12 @@ add_executable(hybrid-sog main.cpp
   SpotSogIterator.h
   SogTwa.cpp
   SogTwa.h
-
+  SogKripkeState.cpp
+  SogKripkeState.h
+  SogKripkeIterator.cpp
+  SogKripkeIterator.h
+  SogKripke.cpp
+  SogKripke.h
   )
 
 target_link_libraries(hybrid-sog
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index f46fa15f2f535f66b1baeb0eecf084633fd3be49..69a420d77f22e5cad90a886a9f68bf135a1dbdf5 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -1,19 +1,19 @@
 #include <spot/twaalgos/dot.hh>
 #include <spot/twaalgos/hoa.hh>
-#include <spot/twa/twa.hh>
+#include <spot/kripke/kripke.hh>
 #include <spot/twa/bdddict.hh>
 
 
-#include "SpotSogIterator.h"
-#include "SpotSogState.h"
+#include "SogKripkeIterator.h"
+#include "SogKripkeState.h"
 
 #include "SogKripke.h"
 #include <map>
 using namespace spot;
-SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): twa(dict_ptr),m_sog(sog)
+SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(dict_ptr),m_sog(sog)
 {
-    SpotSogIterator::m_graph=sog;
-    SpotSogIterator::m_dict_ptr=&dict_ptr;
+    SogKripkeIterator::m_graph=sog;
+    SogKripkeIterator::m_dict_ptr=&dict_ptr;
 /*spot::bdd_dict *p=dict_ptr.get();
 cout<<"Taille du dictionnaire :"<<p->var_map.size()<<endl;
 
@@ -34,28 +34,28 @@ std::ostringstream stream;
 }
 state* SogKripke::get_init_state() const {
     //cout<<"Initial state given...\n";
-    return new SpotSogState(m_sog->getInitialState());//new SpotSogState();
+    return new SogKripkeState(m_sog->getInitialState());//new SpotSogState();
 
 }
 // Allows to print state label representing its id
 std::string SogKripke::format_state(const spot::state* s) const
   {
-    auto ss = static_cast<const SpotSogState*>(s);
+    auto ss = static_cast<const SogKripkeState*>(s);
     std::ostringstream out;
     out << "( " << ss->getLDDState()->getLDDValue() <<  ")";
     return out.str();
   }
 
-SpotSogIterator* SogKripke::succ_iter(const spot::state* s) const {
+SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
 
-    auto ss = static_cast<const SpotSogState*>(s);
+    auto ss = static_cast<const SogKripkeState*>(s);
     bdd b=bddfalse;
-    return new SpotSogIterator(ss->getLDDState());//,b);//s state_condition(ss));
+    return new SogKripkeIterator(ss->getLDDState());//,b);//s state_condition(ss));
 }
 
-   MDD state_condition(const spot::state* s) const override
+  /* MDD state_condition(const spot::state* s) const override
   {
-    auto ss = static_cast<const SpotSogState*>(s);
+    auto ss = static_cast<const SogKripkeState*>(s);
 
   MDD res = lddmc_true;
   std::map<int, int>::const_iterator it;
@@ -63,7 +63,7 @@ SpotSogIterator* SogKripke::succ_iter(const spot::state* s) const {
     if (m_sog->is_marked(it->first, m))
 
   return res;
-  }
+  }*/
 
 
 SogKripke::~SogKripke()
diff --git a/src/SogKripke.h b/src/SogKripke.h
index b6fc776b246cd2fe754c2476ae4eaffc81b0f3da..a0cf52d2da10e5bc2b82efe658b60d4173aae2b0 100644
--- a/src/SogKripke.h
+++ b/src/SogKripke.h
@@ -2,8 +2,8 @@
 #define SOGKRIPKE_H_INCLUDED
 #include "LDDGraph.h"
 #include "SogKripkeIterator.h"
-class SogKripke : public spot::kripke
-{
+#include <spot/kripke/kripke.hh>
+class SogKripke: public spot::kripke {
     public:
 
 
@@ -13,7 +13,7 @@ class SogKripke : public spot::kripke
         spot::state* get_init_state() const;
         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;
+      //  MDD state_condition(const spot::state* s) const override;
 
 
     protected:
diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp
index 20565dcf9ac12be92ea11fd53e1447ca95780b20..949abe1b4de92194290ff4dd24eed20af615cb5b 100644
--- a/src/SogKripkeIterator.cpp
+++ b/src/SogKripkeIterator.cpp
@@ -37,9 +37,9 @@ bool SogKripkeIterator::done() const {
     return m_current_edge==m_lsucc.size();
 }
 
-SpotSogState* SogKripkeIterator::dst() const
+SogKripkeState* SogKripkeIterator::dst() const
   {
-    return new SpotSogState(m_lsucc.at(m_current_edge).first);
+    return new SogKripkeState(m_lsucc.at(m_current_edge).first);
   }
 
 bdd SogKripkeIterator::cond()  const {
diff --git a/src/SogKripkeState.cpp b/src/SogKripkeState.cpp
index 8d471cc0fae3acf2e119050d4b5f9ee74786f02d..d47cc4a4161ca353b3e086e064aad531e8b07542 100644
--- a/src/SogKripkeState.cpp
+++ b/src/SogKripkeState.cpp
@@ -1,3 +1,4 @@
+#include <spot/twa/twa.hh>
 #include "LDDState.h"
 #include "SogKripkeState.h"