diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index 4d5c0713e07d9f10975e2de20cc61e87a27cf60c..db484e9f9e0eb2c6559296b8d23c6518db0f3631 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -36,6 +36,7 @@ std::string SogKripke::format_state(const spot::state* s) const
     auto ss = static_cast<const SogKripkeState*>(s);
     std::ostringstream out;
     out << "( " << ss->getLDDState()->getLDDValue() <<  ")";
+    cout << "( " << ss->getLDDState()->getLDDValue() <<  ")";
     return out.str();
   }
 
@@ -49,17 +50,18 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
 
 bdd SogKripke::state_condition(const spot::state* s) const
   {
-   cout<<"yessss "<<endl;
+
     auto ss = static_cast<const SogKripkeState*>(s);
     vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
 
-    cout<<"function name :"<<__func__<<endl;
+
     bdd result=bddtrue;
     for (auto it=marked_place.begin();it!=marked_place.end();it++) {
     string name=m_sog->getPlace(*it);
-    cout<<"Place name marked : "<<*it<<"  "<<name<<endl;
+    //cout<<"Place name marked : "<<"  "<<name<<endl;
     spot::formula f=spot::formula::ap(name);
-    result&=bdd_ithvar((dict_->var_map.find(f))->second);
+    result=bdd_ithvar((dict_->var_map.find(f))->second);
+    cout<<"verified ldd : "<<ss->getLDDState()->getLDDValue()<<"Place name marked : "<<name<<endl;
     }
 
   return result;
diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp
index 9b2b6797b9a1288d8ab95ce66ab7a937191eb7d9..c60d0eae8afbb37110737ca69ec03629016b203e 100644
--- a/src/SogKripkeIterator.cpp
+++ b/src/SogKripkeIterator.cpp
@@ -51,14 +51,15 @@ bdd SogKripkeIterator::cond()  const {
     spot::formula f=spot::formula::ap(name);
     bdd   result=bdd_ithvar((p->var_map.find(f))->second);
 
-    //cout<<"Iterator "<<__func__<<"  "<<m_current_edge<<"\n";
-    return result;
+    //cout<<"Iterator "<<__func__<<"  "<<m_current_edge<<"\n";*/
+    //return result;
+    return result & spot::kripke_succ_iterator::cond();
 }
 
-spot::acc_cond::mark_t SogKripkeIterator::acc() const {
+/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
   //cout<<"Iterator acc()\n";
-  return 1U;
-}
+  return 0U;
+}*/
 SogKripkeIterator::~SogKripkeIterator()
 {
     //dtor
diff --git a/src/SogKripkeIterator.h b/src/SogKripkeIterator.h
index 435c240e64f51eb771de13221b2d94a05ce3795f..7793c1133e509a082a97d89694c46b9f2ed6d4fc 100644
--- a/src/SogKripkeIterator.h
+++ b/src/SogKripkeIterator.h
@@ -16,9 +16,8 @@ class SogKripkeIterator : public spot::kripke_succ_iterator
         bool next() override;
         bool done() const override;
         SogKripkeState* dst() const override;
-
         bdd cond() const override final;
-        spot::acc_cond::mark_t acc() const override final;
+      /*  spot::acc_cond::mark_t acc() const override final;*/
 
     protected:
 
diff --git a/src/main.cpp b/src/main.cpp
index 7378758bbba56dce7472c6b21c7f33158b354e78..6b4c00478087e92225ae7e2f08b3a31d3711ff4b 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -189,20 +189,34 @@ int main(int argc, char** argv)
                     spot::print_dot(file, af);
                     file.close();
                 }
-                auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
+                //auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
+
+                spot::twa_graph_ptr k =
+    spot::make_twa_graph(std::make_shared<SogKripke>(d,DR.getGraph(),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, k);
+                    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;
+                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.
+                    fstream file;
+                    file.open("violated.dot",fstream::out);
+                    cout<<"xxxxxxxxxxxxxxxxxx"<<endl;
+                    spot::print_dot(file, k, ".kA");
+                    file.close();
+                    }
                 else
                     std::cout << "formula is verified\n";
             }