diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 62fbe66ce1bd7060998085f1e884f0ee7f625eac..dd7e34c6230033be8288d29d749b2a9e0e21825c 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -213,6 +213,7 @@ LDDState * ModelCheckLace::buildInitialMetaState()
 
 void ModelCheckLace::buildSucc(LDDState *agregate)
 {
+
    if (!agregate->isVisited()) {
    // It's first time to visit agregate, then we have to build its successors
         agregate->setVisited();
@@ -260,6 +261,7 @@ void ModelCheckLace::buildSucc(LDDState *agregate)
 
 
    }
+
 }
 
 
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
index c0a924535baa1b46b0ca5261a45447907794acbe..2790ac5845d539460dc6c95314d7a4de2a07c560 100644
--- a/src/SogKripkeIteratorOTF.cpp
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -21,7 +21,7 @@ SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_
 }
 bool SogKripkeIteratorOTF::first() {
 
-    //cout<<"entering "<<__func__<<endl;
+   // cout<<"entering "<<__func__<<endl;
     m_current_edge=0;
     //cout<<"exciting "<<__func__<<endl;
     return m_lsucc.size()!=0;
@@ -43,7 +43,7 @@ bool SogKripkeIteratorOTF::done() const {
 
 SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
   {
-    //out<<"enter/excit "<<__func__<<endl;
+    //cout<<"enter/excit "<<__func__<<endl;
     return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
   }
 
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index f9b345182696112b28275f7fff9f915214df3488..5267d342aba80171e18e0fda3f9eb4f569393009 100644
--- a/src/SogKripkeOTF.cpp
+++ b/src/SogKripkeOTF.cpp
@@ -15,6 +15,7 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder)
     SogKripkeIteratorOTF::m_builder=builder;
     SogKripkeStateOTF::m_builder=builder;
     SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
+    //cout<<__func__<<endl;
 }
 
 SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeOTF(dict_ptr,builder) {
diff --git a/src/main.cpp b/src/main.cpp
index 4d9e1723a44ccfab1c5b25c384bea2a85617807b..7dc13f6a179ad529ac7db51526e408f595587324 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -148,33 +148,21 @@ int main(int argc, char** argv)
         // Initialize SOG builder
         ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
         cout<<"Created"<<endl;
-        spot::twa_graph_ptr k =
-            spot::make_twa_graph(std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
-                                 spot::twa::prop_set::all(), true);
+        auto k =
+            std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());                                 ;
         // Performing on the fly Modelchecking
         cout<<"Performing on the fly Modelchecking"<<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, k,"ka");
-            file.close();
-        }
         if (auto run = k->intersecting_run(af))
         {
-            /*std::cout << "formula is violated by the following run:\n" << *run;*/
-            run->highlight(5); // 5 is a color number.
+            std::cout << "formula is violated by the following run:\n"<<*run<<endl;
+            /*run->highlight(5); // 5 is a color number.
             fstream file;
             file.open("violated.dot",fstream::out);
             cout<<"Property is violated!"<<endl;
             cout<<"Check the dot file."<<endl;
             spot::print_dot(file, k, ".kA");
-            file.close();
+            file.close();*/
         }
         else
             std::cout << "formula is verified\n";