diff --git a/.kdev4/mc-sog.kdev4 b/.kdev4/mc-sog.kdev4
new file mode 100644
index 0000000000000000000000000000000000000000..2ed6747ac4718c05600e5c5dcea9128766bcfd65
--- /dev/null
+++ b/.kdev4/mc-sog.kdev4
@@ -0,0 +1,19 @@
+[Buildset]
+BuildItems=@Variant(\x00\x00\x00\t\x00\x00\x00\x00\x01\x00\x00\x00\x0b\x00\x00\x00\x00\x01\x00\x00\x00\x0c\x00m\x00c\x00-\x00s\x00o\x00g)
+
+[CMake]
+Build Directory Count=1
+Current Build Directory Index-Host System=0
+
+[CMake][CMake Build Directory 0]
+Build Directory Path=/home/chiheb/ProjectCPP/mc-sog/build
+Build Type=Debug
+CMake Binary=/usr/bin/cmake
+CMake Executable=/usr/bin/cmake
+Environment Profile=
+Extra Arguments=
+Install Directory=
+Runtime=Host System
+
+[Project]
+VersionControlSupport=kdevgit
diff --git a/mc-sog.kdev4 b/mc-sog.kdev4
new file mode 100644
index 0000000000000000000000000000000000000000..686e1e7d72cbf16f20d35fcb812660e3a6b7afe9
--- /dev/null
+++ b/mc-sog.kdev4
@@ -0,0 +1,4 @@
+[Project]
+CreatedFrom=CMakeLists.txt
+Manager=KDevCMakeManager
+Name=mc-sog
diff --git a/src/NewNet.h b/src/NewNet.h
index a4f2536e1e05bee21ef6376a17e9e9c9d694c4cd..10107a044d95ba59d98744209c254420af8b0a50 100644
--- a/src/NewNet.h
+++ b/src/NewNet.h
@@ -10,8 +10,8 @@
 #include <set>
 #include <string>
 #include <vector>
-#include "RdPMonteur.hpp"
-typedef set<int> Set;
+#include "RdPMonteur.hpp"   
+typedef set<int> Set;  
 class Node {
  public:
   Node(){};
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index f28f3244245afe7be1a8b60664279c07a660bde7..3bde48f2d8c66b66d40318512085e16cffdc3125 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -71,6 +71,6 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
     //dtor
 }
 
-static ModelCheckerTh * SogKripkeIteratorTh::m_builder;
+static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
 static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
 static LDDState SogKripkeIteratorTh::m_deadlock;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
index 1a8adc86648666cca49e43359220a0faee2c8e4a..774cbd5f9826003ddfd89a7e47981195962688c5 100644
--- a/src/SogKripkeIteratorTh.h
+++ b/src/SogKripkeIteratorTh.h
@@ -1,14 +1,14 @@
 #ifndef SOGKRIPKEITERATORTH_H_INCLUDED
 #define SOGKRIPKEITERATORTH_H_INCLUDED
 #include "SogKripkeStateTh.h"
-#include "ModelCheckerTh.h"
+#include "ModelCheckBaseMT.h"
 #include <spot/kripke/kripke.hh>
 // Iterator for a SOG graph
 class SogKripkeIteratorTh : public spot::kripke_succ_iterator
 {
 public:
     static LDDState m_deadlock;
-    static ModelCheckerTh * m_builder;
+    static ModelCheckBaseMT * m_builder;
     static spot::bdd_dict_ptr* m_dict_ptr;
   //  sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
     SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd);
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index f0dbf22d2a93d0894fa132a80abc27d1a51a7bef..4f2e563b1b6e609633bf212649c488a3093b7e03 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -10,7 +10,7 @@
 #include "SogKripkeTh.h"
 #include <map>
 using namespace spot;
-SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckerTh *builder): spot::kripke(dict_ptr),m_builder(builder)
+SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder): spot::kripke(dict_ptr),m_builder(builder)
 {
     SogKripkeIteratorTh::m_builder=builder;
     SogKripkeStateTh::m_builder=builder;
@@ -18,7 +18,7 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckerTh *builder):
     
 }
 
-SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
+SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
 
     for (auto it=l_transap.begin();it!=l_transap.end();it++) {
         register_ap(*it);
diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h
index 4f4a114286a9b024fefcb7f5b697f9344b7e6b06..81d27eb07d33c23094447c14b669176e1c44c8d6 100644
--- a/src/SogKripkeTh.h
+++ b/src/SogKripkeTh.h
@@ -10,8 +10,8 @@
 class SogKripkeTh: public spot::kripke {
     public:
 
-        SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder);
-        SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap);
+        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();
         spot::state* get_init_state() const;
         SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
diff --git a/src/main.cpp b/src/main.cpp
index 89895cf15d6c232ee447332165378da9694e7ca3..985756446af247bfdf81caf0b241f9936012f656 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -151,7 +151,7 @@ int main(int argc, char** argv)
         ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
         mcl->loadNet();        
         auto k =
-            std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
+            std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
                             cout<<"Want to save the graph in a dot file ?";
                 cin>>c;
                 if (c=='y')