modifié : src/ModelCheckLace.cpp

	modifié :         src/SogKripkeIteratorOTF.cpp
	modifié :         src/SogKripkeOTF.cpp
	modifié :         src/main.cpp

src/ModelCheckLace.cpp

@@ -170,15 +170,16 @@ TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, t
 LDDState * ModelCheckLace::buildInitialMetaState()
 {
 
-    LDDState *c=new LDDState;
+    LDDState *initalAggregate=new LDDState;
     LDDState *reached_class;
     LACE_ME;
     MDD initial_meta_state(CALL(Aggregate_epsilon_lace,m_initalMarking,&m_nonObservable,&m_tb_relation));
     Set fire=fire_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
 
     // c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this);
-    m_graph->setInitialState(c);
-    m_graph->insert(c);
+    initalAggregate->m_lddstate=initial_meta_state;
+    m_graph->setInitialState(initalAggregate);
+    m_graph->insert(initalAggregate);
     // Compute successors
     unsigned int onb_it=0;
     Set::const_iterator iter=fire.begin();
@@ -202,11 +203,11 @@ LDDState * ModelCheckLace::buildInitialMetaState()
         reached_class->m_lddstate=Complete_meta_state;
         m_graph->addArc();
         m_graph->insert(reached_class);
-        c->Successors.insert(c->Successors.begin(),LDDEdge(reached_class,t));
-        reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(c,t));
+        initalAggregate->Successors.insert(initalAggregate->Successors.begin(),LDDEdge(reached_class,t));
+        reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(initalAggregate,t));
     }
 
-    return c;
+    return initalAggregate;
 }
 
 void ModelCheckLace::buildSucc(LDDState *agregate)

src/SogKripkeIteratorOTF.cpp

@@ -30,38 +30,37 @@ bool SogKripkeIteratorOTF::first() {
 }
 
 bool SogKripkeIteratorOTF::next() {
-    cout<<"entering "<<__func__<<endl;
+    //cout<<"entering "<<__func__<<endl;
     m_current_edge++;
     return m_current_edge<m_lsucc.size();
 
 }
 
 bool SogKripkeIteratorOTF::done() const {
-cout<<"entring /excit"<<__func__<<endl;
+    //cout<<"entring /excit"<<__func__<<endl;
     return m_current_edge==m_lsucc.size();
 
 }
 
 SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
   {
-    cout<<"enter/excit "<<__func__<<endl;
+    //out<<"enter/excit "<<__func__<<endl;
     return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
   }
 
 bdd SogKripkeIteratorOTF::cond()  const {
-    cout<<"entering "<<__func__<<endl;
+    //cout<<"entering "<<__func__<<endl;
     if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
-    cout<<"step 0"<<endl;
+
     string name=m_builder->getTransition(m_lsucc.at(m_current_edge).second);
     //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
-    cout<<"step 1 "<<name<<endl;
+
     spot::bdd_dict *p=m_dict_ptr->get();
-    cout<<"step 2"<<endl;
     spot::formula f=spot::formula::ap(name);
     bdd   result=bdd_ithvar((p->var_map.find(f))->second);
 
     //cout<<"Iterator "<<__func__<<"  "<<m_current_edge<<"\n";*/
-    cout<<"exciting "<<__func__<<endl;
+    //cout<<"exciting "<<__func__<<endl;
     return result & spot::kripke_succ_iterator::cond();
 }
 

src/SogKripkeOTF.cpp

@@ -29,7 +29,7 @@ SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *bu
 
 
 state* SogKripkeOTF::get_init_state() const {
-    cout<<__func__<<endl;
+   // cout<<__func__<<endl;
     return new SogKripkeStateOTF(m_builder->buildInitialMetaState());//new SpotSogState();
 
 }

src/main.cpp

@@ -171,13 +171,14 @@ int main(int argc, char** argv)
             run->highlight(5); // 5 is a color number.
             fstream file;
             file.open("violated.dot",fstream::out);
-            cout<<"xxxxxviolatedxxxxxxx"<<endl;
+            cout<<"Property is violated!"<<endl;
+            cout<<"Check the dot file."<<endl;
             spot::print_dot(file, k, ".kA");
             file.close();
         }
         else
             std::cout << "formula is verified\n";
-        //  exit(0);
+
     }
     else if (n_tasks==1)
     {