diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp index 8ca3114fbe84ef951d22f668db67ba40b54a6802..ae14cc890331e05cadfb29dea2a5f5d4ed8cbba0 100644 --- a/src/HybridSOG.cpp +++ b/src/HybridSOG.cpp @@ -78,6 +78,7 @@ HybridSOG::HybridSOG(const NewNet &R, int BOUND,bool init) m_nonObservable=R.NonObservable; m_place_proposition=R.m_formula_place; m_transitionName=R.transitionName; + m_placeName=R.m_placePosName; InterfaceTrans=R.InterfaceTrans; m_nbPlaces=R.places.size(); diff --git a/src/LDDState.cpp b/src/LDDState.cpp index f81f1a3848ee6a860e167e19352109c9d735da43..feced7a72c97669549344c84b391014930b7f11e 100644 --- a/src/LDDState.cpp +++ b/src/LDDState.cpp @@ -39,7 +39,8 @@ vector<int> LDDState::getMarkedPlaces() { int depth=0; while (mdd>lddmc_true) { - mddnode_t node=GETNODE(m_lddstate); + //printf("mddd : %d \n",mdd); + mddnode_t node=GETNODE(mdd); if (mddnode_getvalue(node)==1) { result.push_back(depth); } diff --git a/src/NewNet.h b/src/NewNet.h index a1f269f189d33e4cc478bc08e61e9a0bf8a254e3..a4f2536e1e05bee21ef6376a17e9e9c9d694c4cd 100644 --- a/src/NewNet.h +++ b/src/NewNet.h @@ -106,9 +106,10 @@ class NewNet : public RdPMonteur { int nbTransition() const { return transitions.size(); }; set<string>& getListTransitionAP() {return m_ltransitionAP;} set<string>& getListPlaceAP() {return m_lplaceAP;} + map<int,string> m_placePosName; private: map<int,string> m_transitionPosName; - map<int,string> m_placePosName; + set<string> m_ltransitionAP; set<string> m_lplaceAP; diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp index 6182a15b67538538e39c95e6c5898c3235fe93f3..439b3e738b155c0cec8be420fbd73ebcaa2e759d 100644 --- a/src/SogKripke.cpp +++ b/src/SogKripke.cpp @@ -43,22 +43,21 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const { auto ss = static_cast<const SogKripkeState*>(s); ////////////////////////////////////////////// - // Must be changed - // State condition ???? - /////////////////////// - bdd b=bddtrue; - return new SogKripkeIterator(ss->getLDDState(),b);//,b);//s state_condition(ss)); + + return new SogKripkeIterator(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss)); } 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(); - spot::formula f=spot::formula::ap("jhkh"); - //dict_->var_map.find(f); + + 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<<endl; spot::formula f=spot::formula::ap(name); result&=bdd_ithvar((dict_->var_map.find(f))->second); } diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp index 047dd30a33f7a67cc2d6bb4b56789c6a262412e5..a281b20c05b64112fca0e054787d4a192f9a6596 100644 --- a/src/threadSOG.cpp +++ b/src/threadSOG.cpp @@ -63,6 +63,7 @@ threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool m_nonObservable=R.NonObservable; m_transitionName=R.transitionName; + m_placeName=R.m_placePosName; cout<<"Toutes les Transitions:"<<endl; map<string,int>::iterator it2=m_transitionName.begin(); @@ -624,7 +625,7 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised) int rc; m_graph=&g; m_graph->setTransition(m_transitionName); - + m_graph->setPlace(m_placeName); m_id_thread=0; pthread_mutex_init(&m_mutex, NULL); @@ -777,6 +778,7 @@ void threadSOG::computeSOGLace(LDDGraph &g) Set fire; m_graph=&g; m_graph->setTransition(m_transitionName); + m_graph->setPlace(m_placeName); m_nbmetastate=0; m_MaxIntBdd=0; @@ -965,7 +967,7 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g) Set fire; m_graph=&g; m_graph->setTransition(m_transitionName); - + m_graph->setPlace(m_placeName); m_nbmetastate=0; m_MaxIntBdd=0;