diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3c6a4422152044f42fc2ed91ccf6b1a74045053c..388ee7c906ea7f98fe2da7d036454ffd93a9ae05 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -72,6 +72,12 @@ add_executable(hybrid-sog main.cpp
   ModelCheckerTh.h
   MCHybridSOG.cpp
   MCHybridSOG.h
+  HybridKripke.cpp
+  HybridKripke.h
+  HybridKripkeIterator.cpp
+  HybridKripkeIterator.h
+  HybridKripkeState.cpp
+  HybridKripkeState.h
   )
 
 target_link_libraries(hybrid-sog
diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index 34f75adb7d0f3a7f460f40ff209e82f7da5536cf..62ff0155b9bd882d730611ba019169d543bb1cdb 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -10,21 +10,21 @@
 #include "HybridKripke.h"
 #include <map>
 using namespace spot;
-SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder): spot::kripke(dict_ptr),m_builder(builder)
+HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder): spot::kripke(dict_ptr),m_builder(builder)
 {
-    SogKripkeIteratorTh::m_builder=builder;
-    SogKripkeStateTh::m_builder=builder;
-    SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
-    SogKripkeIteratorTh::m_deadlock.setLDDValue(1);
-    SogKripkeIteratorTh::m_deadlock.setVisited();
-    SogKripkeIteratorTh::m_deadlock.setCompletedSucc();
-    SogKripkeIteratorTh::m_div.setLDDValue(0);
-    SogKripkeIteratorTh::m_div.setVisited();
-    SogKripkeIteratorTh::m_div.setCompletedSucc();
-    SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));
+    HybridKripkeIterator::m_builder=builder;
+    HybridKripkeIterator::m_builder=builder;
+    HybridKripkeIterator::m_dict_ptr=&dict_ptr;
+    HybridKripkeIterator::m_deadlock.setLDDValue(1);
+    HybridKripkeIterator::m_deadlock.setVisited();
+    HybridKripkeIterator::m_deadlock.setCompletedSucc();
+    HybridKripkeIterator::m_div.setLDDValue(0);
+    HybridKripkeIterator::m_div.setVisited();
+    HybridKripkeIterator::m_div.setCompletedSucc();
+    HybridKripkeIterator::m_div.Successors.push_back(pair<LDDState*,int>(&HybridKripkeIterator::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) {
+HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):HybridKripke(dict_ptr,builder) {
 
     for (auto it=l_transap.begin();it!=l_transap.end();it++) {
         register_ap(*it);
@@ -35,35 +35,35 @@ SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *bu
 }
 
 
-state* SogKripkeTh::get_init_state() const {
+state* HybridKripke::get_init_state() const {
    LDDState *ss=m_builder->getInitialMetaState();   
-    return new SogKripkeStateTh(ss);//new SpotSogState();
+    return new HybridKripkeState(ss);//new SpotSogState();
 
 }
 // Allows to print state label representing its id
-std::string SogKripkeTh::format_state(const spot::state* s) const
+std::string HybridKripke::format_state(const spot::state* s) const
   {
     //cout<<__func__<<endl;
-    auto ss = static_cast<const SogKripkeStateTh*>(s);
+    auto ss = static_cast<const HybridKripkeState*>(s);
     std::ostringstream out;
     out << "( " << ss->getLDDState()->getLDDValue() <<  ")";
    // cout << " ( " << ss->getLDDState()->getLDDValue() <<  ")";
     return out.str();
   }
 
-SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
+HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
    
-    auto ss = static_cast<const SogKripkeStateTh*>(s);
+    auto ss = static_cast<const HybridKripkeState*>(s);
     LDDState *aggregate=ss->getLDDState();
     bdd cond = state_condition(ss);
     if (iter_cache_)
     {
-      auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
+      auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
       iter_cache_ = nullptr;    // empty the cache
       it->recycle(aggregate, cond);
       return it;
     }
-  return new SogKripkeIteratorTh(aggregate,cond);
+  return new HybridKripkeIterator(aggregate,cond);
 
     
     
@@ -74,10 +74,10 @@ SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
     return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));*/
 }
 
-bdd SogKripkeTh::state_condition(const spot::state* s) const
+bdd HybridKripke::state_condition(const spot::state* s) const
   {
 
-    auto ss = static_cast<const SogKripkeStateTh*>(s);
+    auto ss = static_cast<const HybridKripkeState*>(s);
     vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
 
 
@@ -99,7 +99,7 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
   }
 
 
-SogKripkeTh::~SogKripkeTh()
+HybridKripke::~HybridKripke()
 {
     //dtor
 }
diff --git a/src/HybridKripke.h b/src/HybridKripke.h
index 152457d6b62a16f470e70350c100a3c4a6010e09..b9f718120d032c82d5caac5a78d0a3848657c6b3 100644
--- a/src/HybridKripke.h
+++ b/src/HybridKripke.h
@@ -7,14 +7,14 @@
 #include <NewNet.h>
 
 
-class SogKripkeTh: public spot::kripke {
+class HybridKripke: public spot::kripke {
     public:
 
-        SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder);
-        SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap);
-        virtual ~SogKripkeTh();
+        HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder);
+        HybridKripke(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap);
+        virtual ~HybridKripke();
         spot::state* get_init_state() const override;
-        SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
+        HybridKripkeIterator* succ_iter(const spot::state* s) const override;
         std::string format_state(const spot::state* s) const override;
         bdd state_condition(const spot::state* s) const override;
 
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index 0c0deb06c6ed2b08971d7f209dbf4c73f56ff364..69a4079f5c2783cc64b979145c2c4423d2c5e5b3 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -4,7 +4,7 @@
 #include "HybridKripkeIterator.h"
 
 
-SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
+HybridKripkeIterator::HybridKripkeIterator(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
 {
     for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
         m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
@@ -17,7 +17,7 @@ SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_ld
     }
 
 }
-bool SogKripkeIteratorTh::first() {
+bool HybridKripkeIterator::first() {
 
    // cout<<"entering "<<__func__<<endl;
     m_current_edge=0;
@@ -26,26 +26,26 @@ bool SogKripkeIteratorTh::first() {
 
 }
 
-bool SogKripkeIteratorTh::next() {
+bool HybridKripkeIterator::next() {
     //cout<<"entering "<<__func__<<"   "<<m_current_edge<<endl;
     m_current_edge++;
     return m_current_edge<m_lsucc.size();
 
 }
 
-bool SogKripkeIteratorTh::done() const {
+bool HybridKripkeIterator::done() const {
     //cout<<"entring /excit"<<__func__<<endl;
     return m_current_edge==m_lsucc.size();
 
 }
 
-SogKripkeStateTh* SogKripkeIteratorTh::dst() const
+HybridKripkeState* HybridKripkeIterator::dst() const
   {
     /*cout<<"Source "<<m_lddstate->getLDDValue()<<"Destination :"<<m_lsucc.at(m_current_edge).first->getLDDValue()<<" in "<<m_lsucc.size()<<" / "<<m_current_edge<<endl;*/
-    return new SogKripkeStateTh(m_lsucc.at(m_current_edge).first);
+    return new HybridKripkeState(m_lsucc.at(m_current_edge).first);
   }
 
-bdd SogKripkeIteratorTh::cond()  const {
+bdd HybridKripkeIterator::cond()  const {
     //cout<<"entering "<<__func__<<endl;
     if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
 
@@ -63,18 +63,18 @@ bdd SogKripkeIteratorTh::cond()  const {
   //cout<<"Iterator acc()\n";
   return 0U;
 }*/
-SogKripkeIteratorTh::~SogKripkeIteratorTh()
+HybridKripkeIterator::~HybridKripkeIterator()
 {
     //dtor
 }
 
-void SogKripkeIteratorTh::recycle(LDDState* aggregate, bdd cond)
+void HybridKripkeIterator::recycle(LDDState* aggregate, bdd cond)
 {
         m_lddstate=aggregate;
         spot::kripke_succ_iterator::recycle(cond);
 }
 
-static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
-static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
-static LDDState SogKripkeIteratorTh::m_deadlock;
-static LDDState SogKripkeIteratorTh::m_div;
+static ModelCheckBaseMT * HybridKripkeIterator::m_builder;
+static spot::bdd_dict_ptr* HybridKripkeIterator::m_dict_ptr;
+static LDDState HybridKripkeIterator::m_deadlock;
+static LDDState HybridKripkeIterator::m_div;
diff --git a/src/HybridKripkeIterator.h b/src/HybridKripkeIterator.h
index 8e906d2b1b1b8862cf3c099d6f715de6b0621316..a4e5d85fb6079254517d898ca4df6fd33f6bd45b 100644
--- a/src/HybridKripkeIterator.h
+++ b/src/HybridKripkeIterator.h
@@ -17,10 +17,10 @@ public:
     bool first() override;
     bool next() override;
     bool done() const override;
-    SogKripkeStateTh* dst() const override;
+    HybridKripkeState* dst() const override;
     bdd cond() const override final;
 
-    SogKripkeStateTh* current_state() const;
+    HybridKripkeState* current_state() const;
 
     void recycle(LDDState *aggregate, bdd cond);
 
diff --git a/src/HybridKripkeState.cpp b/src/HybridKripkeState.cpp
index 70712c959c9f31f743b067701b6265b9d27d7b66..31dd140aa3b194166fc6cac92b71ba4d525a6081 100644
--- a/src/HybridKripkeState.cpp
+++ b/src/HybridKripkeState.cpp
@@ -1,11 +1,11 @@
 #include <spot/kripke/kripke.hh>
 #include "LDDState.h"
-#include "SogKripkeStateTh.h"
+#include "HybridKripkeState.h"
 
 
-SogKripkeStateTh::~SogKripkeStateTh()
+HybridKripkeState::~HybridKripkeState()
 {
     //dtor
 }
 
-static ModelCheckBaseMT * SogKripkeStateTh::m_builder;
+static ModelCheckBaseMT * HybridKripkeState::m_builder;
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index f07ab07d4d426b77c3a061d64e6cd3e344de0742..212f0561349662cc8722c93e05c0d6a6387d50af 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -1,22 +1,22 @@
-#ifndef SOGKRIPKESTATETH_H_INCLUDED
-#define SOGKRIPKESTATETH_H_INCLUDED
+#ifndef HYBRIDKRIPKESTATETH_H_INCLUDED
+#define HYBRIDKRIPKESTATETH_H_INCLUDED
 
 
 #include "LDDState.h"
 #include "ModelCheckBaseMT.h"
 
-class SogKripkeStateTh : public spot::state
+class HybridKripkeState : public spot::state
 {
 public:
     static ModelCheckBaseMT * m_builder;
-    SogKripkeStateTh(LDDState *st):m_state(st) {
+    HybridKripkeState(LDDState *st):m_state(st) {
             m_builder->buildSucc(st);
     };
-    virtual ~SogKripkeStateTh();
+    virtual ~HybridKripkeState();
 
-    SogKripkeStateTh* clone() const override
+    HybridKripkeState* clone() const override
     {
-        return new SogKripkeStateTh(m_state);
+        return new HybridKripkeState(m_state);
     }
     size_t hash() const override
     {
@@ -25,7 +25,7 @@ public:
 
     int compare(const spot::state* other) const override
     {
-        auto o = static_cast<const SogKripkeStateTh*>(other);
+        auto o = static_cast<const HybridKripkeState*>(other);
         size_t oh = o->hash();
         size_t h = hash();
         //return (h!=oh);