diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 7e76293f89fa9c8d089aefbbab482c7821f2bc08..bcffda8ee75fb3b382fd00617826886fb3c1e765 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -36,22 +36,14 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
     m_transitionName=R.transitionName;
     m_placeName=R.m_placePosName;
 
-    cout<<"Toutes les Transitions:"<<endl;
+   /* cout<<"Toutes les Transitions:"<<endl;
     map<string,int>::iterator it2=m_transitionName.begin();
     for (; it2!=m_transitionName.end(); it2++)
     {
         cout<<(*it2).first<<" : "<<(*it2).second<<endl;
-    }
-
+    }*/
 
 
-    cout<<"Transitions observables :"<<endl;
-    Set::iterator it=m_observable.begin();
-    for (; it!=m_observable.end(); it++)
-    {
-        cout<<*it<<"  ";
-    }
-    cout<<endl;
     InterfaceTrans=R.InterfaceTrans;
     m_nbPlaces=R.places.size();
     cout<<"Nombre de places : "<<m_nbPlaces<<endl;
@@ -65,10 +57,6 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
 
     m_initalMarking=lddmc_cube(liste_marques,R.places.size());
 
-
-
-
-
     uint32_t *prec = new uint32_t[m_nbPlaces];
     uint32_t *postc= new uint32_t [m_nbPlaces];
     // Transition relation
@@ -132,7 +120,6 @@ LDDState * ModelCheckerTh::buildInitialMetaState()
 {
     ComputeTh_Succ();
     LDDState *c=new LDDState;
-    cout<<"Initial marking : "<<m_initalMarking<<endl;
     MDD initial_meta_state=Accessible_epsilon(m_initalMarking);
     ldd_refs_push(initial_meta_state);
     c->m_lddstate=initial_meta_state;
@@ -171,11 +158,8 @@ void * ModelCheckerTh::Compute_successors()
     pthread_mutex_lock(&m_mutex);
     id_thread=m_id_thread++;
     pthread_mutex_unlock(&m_mutex);
-
     LDDState* reached_class=nullptr;
-    // size_t max_meta_state_size;
-    // int min_charge;
-    cout<<"Thread id : "<<id_thread<<endl;
+
     do
     {
         pthread_barrier_wait(&m_barrier_threads);
@@ -211,8 +195,7 @@ void * ModelCheckerTh::Compute_successors()
         }
         pthread_barrier_wait(&m_barrier_builder);
     }
-    while (1);
-
+    while (!m_finish);
 }
 
 
@@ -233,15 +216,13 @@ void ModelCheckerTh::ComputeTh_Succ()
     m_id_thread=0;
 
     pthread_mutex_init(&m_mutex, NULL);
-    pthread_mutex_init(&m_gc_mutex,NULL);
+    //pthread_mutex_init(&m_gc_mutex,NULL);
     pthread_mutex_init(&m_graph_mutex,NULL);
-    pthread_mutex_init(&m_supervise_gc_mutex,NULL);
-    m_gc=0;
+    //pthread_mutex_init(&m_supervise_gc_mutex,NULL);
+    pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);
+    pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread+1);
 
-    pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread);
-    pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread);
-
-    for (int i=0; i<m_nb_thread-1; i++)
+    for (int i=0; i<m_nb_thread; i++)
     {
         if ((rc = pthread_create(&m_list_thread[i], NULL,threadHandler,this)))
         {
@@ -256,3 +237,13 @@ void ModelCheckerTh::ComputeTh_Succ()
 
 
 }
+ModelCheckerTh::~ModelCheckerTh() {
+    m_finish=true;
+    pthread_barrier_wait(&m_barrier_threads);
+    pthread_barrier_wait(&m_barrier_builder);
+    for (int i = 0; i < m_nb_thread-1; i++)
+     {
+         pthread_join(m_list_thread[i], NULL);
+     }
+     cout<<"Destructor "<<endl;
+}
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index e92aea86b4177a50159370bc62e2b80bdb89a976..b271d6c85ae88fac79815425d1660b5c39e7e235 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -8,6 +8,7 @@ class ModelCheckerTh : public CommonSOG
 {
 public:
     ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
+    ~ModelCheckerTh();
     LDDState * buildInitialMetaState();
     string getTransition(int pos);
     string getPlace(int pos);
@@ -18,17 +19,16 @@ public:
 private:
     int m_nb_thread;
     MDD m_initalMarking;
-    int m_min_charge;
     pile_t m_st[128];
-    int m_charge[128];
     int m_id_thread;
     pthread_mutex_t m_mutex;
     pthread_mutex_t m_graph_mutex;
-    pthread_mutex_t m_gc_mutex;
-    pthread_mutex_t m_supervise_gc_mutex;
+    //pthread_mutex_t m_gc_mutex;
+    //pthread_mutex_t m_supervise_gc_mutex;
 
     pthread_barrier_t m_barrier_threads,m_barrier_builder;
-    unsigned int m_gc;
+    //unsigned int m_gc;
+    bool m_finish=false;
 
     pthread_mutex_t m_mutex_stack[128];
     pthread_t m_list_thread[128];
diff --git a/src/main.cpp b/src/main.cpp
index e1b435a661895884e16bf83b93fa00caf2dc6ca8..9c41fdb324ffac21943bf875b3ae09dda72b9d44 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -204,28 +204,8 @@ int main(int argc, char** argv)
         }
         // Initialize SOG builder
         ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th);
-        cout<<"Created"<<endl;
-        /********************************************************************/
-        spot::twa_graph_ptr kk =
-                    spot::make_twa_graph(std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
-                                         spot::twa::prop_set::all(), true);
 
 
-                cout<<"SOG translated to SPOT succeeded.."<<endl;
-                cout<<"Want to save the graph in a dot file ?";
-                cin>>c;
-                if (c=='y')
-                {
-                    fstream file;
-
-                    string st(argv[3]);
-                    st+=".dot";
-                    file.open(st.c_str(),fstream::out);
-                    spot::print_dot(file, kk,"ka");
-                    file.close();
-                }
-
-        /********************************************************************/
 
 
         auto k =
@@ -259,6 +239,7 @@ int main(int argc, char** argv)
         }
         else
             std::cout << "formula is verified\n";
+        delete mcl;
 
     }