diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp index 426e2b7c14df415c3ff5b66f00ddad3986aa323f..c5e2ba0ad63f06e868a6a633013737d57176cc35 100644 --- a/src/LDDGraph.cpp +++ b/src/LDDGraph.cpp @@ -212,6 +212,12 @@ LDDState *LDDGraph::getLDDStateById(unsigned int id) { } string LDDGraph::getTransition(int pos) { + //return m_transition->at(pos); + /* map<string,int>::iterator it=m_transition->begin(); + int i=0; + while (i<pos) {it++;i++;} + return it->first;*/ + cout<<"********** Pos "<<pos<<endl; map<string,int>::iterator it=m_transition->begin(); while(it != m_transition->end()) { @@ -219,7 +225,7 @@ string LDDGraph::getTransition(int pos) { return it->first; it++; } - return ""; + return it->first; } void LDDGraph::setTransition(map<string,int>& list_transitions) { diff --git a/src/SogTwa.cpp b/src/SogTwa.cpp index 7927e1519aa8e6104172c311c3b30c36a234a8ff..f65c22bdbc86a208d8f33dceac399456038352b5 100644 --- a/src/SogTwa.cpp +++ b/src/SogTwa.cpp @@ -13,6 +13,7 @@ using namespace spot; SogTwa::SogTwa(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): twa(dict_ptr),m_sog(sog) { SpotSogIterator::m_graph=sog; + SpotSogIterator::m_dict_ptr=&dict_ptr; /*spot::bdd_dict *p=dict_ptr.get(); cout<<"Taille du dictionnaire :"<<p->var_map.size()<<endl; diff --git a/src/SpotSogIterator.cpp b/src/SpotSogIterator.cpp index 83e3376838ab2c4c6841db21fdb6913293e7f496..fc0a42ed81446d2e64c9ea7a651e4248f58564ab 100644 --- a/src/SpotSogIterator.cpp +++ b/src/SpotSogIterator.cpp @@ -35,9 +35,14 @@ SpotSogState* SpotSogIterator::dst() const bdd SpotSogIterator::cond() const { bdd a=bddtrue;//1; string name=m_graph->getTransition(m_lddstate->getSuccessors()->at(m_current_edge).second); - cout<<"Transition name "<<name<<endl; + cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl; + + spot::bdd_dict *p=m_dict_ptr->get(); + spot::formula f=spot::formula::ap(name); + bdd result=bdd_ithvar((p->var_map.find(f))->second); + //cout<<"Iterator cond()"<<m_current_edge<<"\n"; - return a; + return result; } spot::acc_cond::mark_t SpotSogIterator::acc() const { @@ -50,3 +55,4 @@ SpotSogIterator::~SpotSogIterator() } static LDDGraph * SpotSogIterator::m_graph; +static spot::bdd_dict_ptr* SpotSogIterator::m_dict_ptr; diff --git a/src/SpotSogIterator.h b/src/SpotSogIterator.h index fb425008cae8392a567b3dde8880ccf6f87aca7c..6580ea20400ab25033fef54ce6ffe7ece44f1349 100644 --- a/src/SpotSogIterator.h +++ b/src/SpotSogIterator.h @@ -7,6 +7,7 @@ class SpotSogIterator : public spot::twa_succ_iterator { public: static LDDGraph * m_graph; + static spot::bdd_dict_ptr* m_dict_ptr; SpotSogIterator(const LDDState *lddstate); virtual ~SpotSogIterator(); bool first() override; diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp index 2785c1ffbe05b2678330129b35a3b5292783dfad..17f8baf7ee326c580e9561d4faba64916a66c34b 100644 --- a/src/threadSOG.cpp +++ b/src/threadSOG.cpp @@ -81,10 +81,22 @@ threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool ini //_______________ transitions=R.transitions; Observable=R.Observable; + NonObservable=R.NonObservable; Formula_Trans=R.Formula_Trans; transitionName=R.transitionName; + cout<<"Toutes les Transitions:"<<endl; + map<string,int>::iterator it2=transitionName.begin(); + for (;it2!=transitionName.end();it2++) { + cout<<(*it2).first<<" : "<<(*it2).second<<endl;} + + + + cout<<"Transitions observables :"<<endl; + Set::iterator it=Observable.begin(); + for (;it!=Observable.end();it++) {cout<<*it<<" ";} + cout<<endl; InterfaceTrans=R.InterfaceTrans; m_nbPlaces=R.places.size(); cout<<"Nombre de places : "<<m_nbPlaces<<endl; @@ -1089,6 +1101,7 @@ TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>* if(succ!=lddmc_false) { res.insert(*i); + } } @@ -1169,6 +1182,7 @@ void threadSOG::computeSOGLace(LDDGraph &g) while(iter!=e.second.end()) { int t = *iter; + cout<<"Transition order1: "<<*iter<<endl; //e.second.erase(t); SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&NonObservable,&m_tb_relation); onb_it++;iter++; @@ -1176,8 +1190,11 @@ void threadSOG::computeSOGLace(LDDGraph &g) for (unsigned int i=0; i<onb_it; i++) { - int t = *e.second.end(); - e.second.erase(t); + Set::iterator it = e.second.end(); + it--; + int t=*it; + cout<<"Transition order2: "<<t<<endl; + e.second.erase(it); MDD Complete_meta_state=SYNC(Accessible_epsilon_lace); reached_class=new LDDState; reached_class->m_lddstate=Complete_meta_state; @@ -1371,6 +1388,7 @@ cout<<"\n=========================================\n"; for (unsigned int i=0; i<onb_it; i++) { int t = *e.second.end(); + e.second.erase(t); MDD Complete_meta_state=SYNC(Accessible_epsilon_lace); lddmc_refs_push(Complete_meta_state);