diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 55925ec7565590f222c4af507489bda1dbb8346c..091f3c90e5df3fe833f3a4e34042ebab6dbe989c 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -155,6 +155,10 @@ void ModelCheckerTh::buildSucc(LDDState *agregate)
         pthread_spin_lock(&m_spin_stack[m_min_charge]);
         m_st[m_min_charge].push(agregate);
         pthread_spin_unlock(&m_spin_stack[m_min_charge]);
+        if(!isNotTerminated())
+        {
+             ComputeTh_Succ();
+        }
 
     }
 }
diff --git a/src/main.cpp b/src/main.cpp
index 619058a9290e7f24bf1b6970b59929ab35e16673..98b741311e9c6e0d67754e86c881e00ecf435aba 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -151,7 +151,19 @@ int main(int argc, char** argv)
         ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
         cout<<"Created"<<endl;
         auto k =
-            std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());                                 ;
+            std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
+                            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, k,"ka");
+                    file.close();
+                }                                ;
         // Performing on the fly Modelchecking
         cout<<"Performing on the fly Modelchecking"<<endl;
 
@@ -194,8 +206,20 @@ int main(int argc, char** argv)
         ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th);
         cout<<"Created"<<endl;
         auto k =
-            std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());                                 ;
+            std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
         // Performing on the fly Modelchecking
+        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, k,"ka");
+                    file.close();
+                }
         cout<<"Performing on the fly Modelchecking"<<endl;
 
         if (auto run = k->intersecting_run(af))