diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 1da8b063be0818890bfc52ae1d70d232c90d3cf8..02f933f399a18f126876a41b40a7f332da115b5b 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -7,18 +7,17 @@
 
 using namespace sylvan;
 
-ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
+ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread):ModelCheckBaseMT(R,BOUND,nbThread)  {
+}
+void ModelCheckerTh::preConfigure()
 {
-    m_nb_thread=nbThread;
+   
     lace_init(1, 0);
     lace_startup(0, NULL, NULL);
 
     sylvan_set_limits(2LL<<30, 16, 3);
     sylvan_init_package();
     sylvan_init_ldd();
-//    LACE_ME;
-    m_net=R;
-
 
     int  i;
     vector<Place>::const_iterator it_places;
@@ -28,13 +27,13 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
 
 
     //_______________
-    transitions=R.transitions;
-    m_observable=R.Observable;
-    m_place_proposition=R.m_formula_place;
-    m_nonObservable=R.NonObservable;
+    transitions=m_net.transitions;
+    m_observable=m_net.Observable;
+    m_place_proposition=m_net.m_formula_place;
+    m_nonObservable=m_net.NonObservable;
 
-    m_transitionName=R.transitionName;
-    m_placeName=R.m_placePosName;
+    m_transitionName=m_net.transitionName;
+    m_placeName=m_net.m_placePosName;
 
    /* cout<<"Toutes les Transitions:"<<endl;
     map<string,int>::iterator it2=m_transitionName.begin();
@@ -44,24 +43,24 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
     }*/
 
 
-    InterfaceTrans=R.InterfaceTrans;
-    m_nbPlaces=R.places.size();
+    InterfaceTrans=m_net.InterfaceTrans;
+   
     cout<<"Nombre de places : "<<m_nbPlaces<<endl;
-    cout<<"Derniere place : "<<R.places[m_nbPlaces-1].name<<endl;
+    cout<<"Derniere place : "<<m_net.places[m_nbPlaces-1].name<<endl;
 
-    uint32_t * liste_marques=new uint32_t[R.places.size()];
-    for(i=0,it_places=R.places.begin(); it_places!=R.places.end(); i++,it_places++)
+    uint32_t * liste_marques=new uint32_t[m_net.places.size()];
+    for(i=0,it_places=m_net.places.begin(); it_places!=m_net.places.end(); i++,it_places++)
     {
         liste_marques[i] =it_places->marking;
     }
 
-    m_initialMarking=lddmc_cube(liste_marques,R.places.size());
+    m_initialMarking=lddmc_cube(liste_marques,m_net.places.size());
 
     uint32_t *prec = new uint32_t[m_nbPlaces];
     uint32_t *postc= new uint32_t [m_nbPlaces];
     // Transition relation
-    for(vector<Transition>::const_iterator t=R.transitions.begin();
-            t!=R.transitions.end(); t++)
+    for(vector<Transition>::const_iterator t=m_net.transitions.begin();
+            t!=m_net.transitions.end(); t++)
     {
         // Initialisation
         for(i=0; i<m_nbPlaces; i++)
@@ -99,9 +98,7 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
     }
     delete [] prec;
     delete [] postc;
-    m_graph=new LDDGraph(this);
-    m_graph->setTransition(m_transitionName);
-    m_graph->setPlace(m_placeName);
+   
 }
 
 
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index a27296dba07ecc495b00c8ff344e2458e3f6cea9..4619d242b9a1fca312e628e4a9ed4dfb9683a21c 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -1,10 +1,10 @@
 #ifndef MODELCHECKERTH_H
 #define MODELCHECKERTH_H
-#include "CommonSOG.h"
+#include "ModelCheckBaseMT.h"
 typedef pair<LDDState *, int> couple_th;
 typedef stack<pair<LDDState *,int>> pile_t;
 
-class ModelCheckerTh : public CommonSOG
+class ModelCheckerTh : public ModelCheckBaseMT
 {
 public:
     ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
@@ -15,7 +15,7 @@ public:
     void *Compute_successors();
     void ComputeTh_Succ();
 private:
-    int m_nb_thread;
+    void preConfigure();
 
     pile_t m_st[128];
     int m_id_thread;
diff --git a/src/main.cpp b/src/main.cpp
index cc3535a9a9af76b9c0fcd94fd613108ef97ae06e..89895cf15d6c232ee447332165378da9694e7ca3 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -184,10 +184,10 @@ int main(int argc, char** argv)
     }
     else if (n_tasks==1 && !strcmp(argv[1],"otfP"))
     {
-     cout<<"Multi-threaded on the fly Model checking (Pthread)..."<<endl;
+        cout<<"Multi-threaded on the fly Model checking (Pthread)..."<<endl;
         cout<<"Building automata for not(formula)\n";
         auto d = spot::make_bdd_dict();
-        // d->register_ap("jbhkj");
+        
         spot::twa_graph_ptr af = spot::translator(d).run(not_f);
         cout<<"Formula automata built.\n";
         cout<<"Want to save the graph in a dot file ?";
@@ -204,10 +204,7 @@ int main(int argc, char** argv)
         }
         // Initialize SOG builder
         ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th);
-
-
-
-
+        mcl->loadNet();
         auto k =
             std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());                                             ;