modifié : src/ModelCheckLace.cpp

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

src/ModelCheckLace.cpp

@@ -117,12 +117,12 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
 
 string ModelCheckLace::getTransition(int pos)
 {
-    m_graph->getTransition(pos);
+    return m_graph->getTransition(pos);
 }
 
 string ModelCheckLace::getPlace(int pos)
 {
-    m_graph->getPlace(pos);
+    return m_graph->getPlace(pos);
 }
 
 TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation)
@@ -169,6 +169,7 @@ TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, t
 
 LDDState * ModelCheckLace::buildInitialMetaState()
 {
+
     LDDState *c=new LDDState;
     LDDState *reached_class;
     LACE_ME;
@@ -204,6 +205,7 @@ LDDState * ModelCheckLace::buildInitialMetaState()
         c->Successors.insert(c->Successors.begin(),LDDEdge(reached_class,t));
         reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(c,t));
     }
+
     return c;
 }
 

src/SogKripkeIterator.cpp

@@ -44,6 +44,7 @@ SogKripkeState* SogKripkeIterator::dst() const
 
 bdd SogKripkeIterator::cond()  const {
     if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+
     string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
     //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
 

src/SogKripkeIteratorOTF.cpp

@@ -6,7 +6,7 @@
 
 SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
 {
-    //vector<pair<LDDState*, int>>
+
     m_lddstate->setDiv(true);
     for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
         m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
@@ -17,43 +17,52 @@ SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_
     if (lddstate->isDiv()) {
         m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
     }
+
 }
 bool SogKripkeIteratorOTF::first() {
   //  m_sog->getLDDStateById(m_id)->Successors().
     //return m_sog->get_successor()
-
+    cout<<"entering "<<__func__<<endl;
     m_current_edge=0;
+    cout<<"exciting "<<__func__<<endl;
     return m_lsucc.size()!=0;
+
 }
 
 bool SogKripkeIteratorOTF::next() {
-
+    cout<<"entering "<<__func__<<endl;
     m_current_edge++;
     return m_current_edge<m_lsucc.size();
+
 }
 
 bool SogKripkeIteratorOTF::done() const {
-
+cout<<"entring /excit"<<__func__<<endl;
     return m_current_edge==m_lsucc.size();
+
 }
 
 SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
   {
+    cout<<"enter/excit "<<__func__<<endl;
     return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
   }
 
 bdd SogKripkeIteratorOTF::cond()  const {
+    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";*/
-    //return result;
-    return result;
+    cout<<"exciting "<<__func__<<endl;
+    return result & spot::kripke_succ_iterator::cond();
 }
 
 /*spot::acc_cond::mark_t SogKripkeIterator::acc() const {

src/SogKripkeOTF.cpp

@@ -18,30 +18,34 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder)
 }
 
 SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeOTF(dict_ptr,builder) {
+
     for (auto it=l_transap.begin();it!=l_transap.end();it++) {
         register_ap(*it);
     }
     for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
         register_ap(*it);
+
 }
 
 
 state* SogKripkeOTF::get_init_state() const {
-    //cout<<"Initial state given...\n";
+    cout<<__func__<<endl;
     return new SogKripkeStateOTF(m_builder->buildInitialMetaState());//new SpotSogState();
 
 }
 // Allows to print state label representing its id
 std::string SogKripkeOTF::format_state(const spot::state* s) const
   {
+    cout<<__func__<<endl;
     auto ss = static_cast<const SogKripkeStateOTF*>(s);
     std::ostringstream out;
     out << "( " << ss->getLDDState()->getLDDValue() <<  ")";
-    cout << "( " << ss->getLDDState()->getLDDValue() <<  ")";
+    cout << " ( " << ss->getLDDState()->getLDDValue() <<  ")";
     return out.str();
   }
 
 SogKripkeIteratorOTF* SogKripkeOTF::succ_iter(const spot::state* s) const {
+   cout<<__func__<<endl;
 
     auto ss = static_cast<const SogKripkeStateOTF*>(s);
    //////////////////////////////////////////////
@@ -69,6 +73,7 @@ bdd SogKripkeOTF::state_condition(const spot::state* s) const
     spot::formula f=spot::formula::ap(name);
     result&=!bdd_ithvar((dict_->var_map.find(f))->second);
     }
+
   return result;
   }
 

src/SpotSogIterator.cpp

@@ -7,6 +7,7 @@
 SpotSogIterator::SpotSogIterator(const LDDState* lddstate):m_lddstate(lddstate)
 {
     //vector<pair<LDDState*, int>>
+
     m_lddstate->setDiv(true);
     for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
         m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));

src/main.cpp

@@ -147,10 +147,13 @@ 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);
         // Performing on the fly Modelchecking
+        cout<<"Performing on the fly Modelchecking"<<endl;
+        exit(0);
     }
     else if (n_tasks==1)
     {