diff --git a/src/CommonSOG.h b/src/CommonSOG.h index 8ff04f23577a3cda6a6689f4da05130090b3a513..a6c165719f7c47a3d2414e15e507f604ff76f5b7 100644 --- a/src/CommonSOG.h +++ b/src/CommonSOG.h @@ -25,6 +25,7 @@ class CommonSOG vector<TransSylvan> m_tb_relation; LDDState m_M0; map<string, int> m_transitionName; + map<int,string> m_placeName; Set m_observable; Set m_nonObservable; Set InterfaceTrans; diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp index 13a89d31b4646fda81c3f422c23739b11eebd0ed..ddfe47367991fcd209557b80cdf8cd0c1f59a131 100644 --- a/src/LDDGraph.cpp +++ b/src/LDDGraph.cpp @@ -197,9 +197,16 @@ string LDDGraph::getTransition(int pos) { return it->first; } +string LDDGraph::getPlace(int pos) { + return m_places->find(pos)->second; +} + void LDDGraph::setTransition(map<string,int>& list_transitions) { m_transition=&list_transitions; } +void LDDGraph::setPlace(map<int,string>& list_places) { + m_places=&list_places; +} //void LDDGraph::setTransition(vector<string> list) diff --git a/src/LDDGraph.h b/src/LDDGraph.h index bf174ef4a2a2d8782d543e039560b3ae41387533..9bb00fa8856afa14625b0832a78dd83be4227ee7 100755 --- a/src/LDDGraph.h +++ b/src/LDDGraph.h @@ -18,6 +18,7 @@ class LDDGraph public: string getTransition(int pos); string getPlace(int pos); + void setPlace(map<int,string>& list_places); void setTransition(map<string,int>& list_transitions); MetaLDDNodes m_GONodes; LDDState *getLDDStateById(unsigned int id); diff --git a/src/NewNet.cpp b/src/NewNet.cpp index 67939da0dab0318108bca53bb2c1a049b68af389..66bf51c694fe6485d2400d022cc95af717bd4290 100644 --- a/src/NewNet.cpp +++ b/src/NewNet.cpp @@ -187,7 +187,7 @@ void NewNet::setListObservable(const set<string> & list_t) if (pi!=placeName.end()) cout<<"Place was found!"<<endl; m_formula_place.insert(pi->second); - + m_lplaceAP.insert(*i); // Adding adjacent transitions of a place as observable transitions Place p=places.at(pi->second); for (auto iter=p.post.begin(); iter!=p.post.end(); iter++) diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp index 2cc68c683c278d8b004d05906dac268ad451a95c..6182a15b67538538e39c95e6c5898c3235fe93f3 100644 --- a/src/SogKripke.cpp +++ b/src/SogKripke.cpp @@ -16,10 +16,12 @@ SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(d SogKripkeIterator::m_dict_ptr=&dict_ptr; } -SogKripke::SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap):SogKripke(dict_ptr,sog) { +SogKripke::SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap):SogKripke(dict_ptr,sog) { 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); } @@ -50,15 +52,18 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const { bdd SogKripke::state_condition(const spot::state* s) const { - /*auto ss = static_cast<const SogKripkeState*>(s); - - MDD res = lddmc_true; - std::map<int, int>::const_iterator it; - for (it = place_prop.begin(); it != place_prop.end(); ++it) - if (m_sog->is_marked(it->first, m)) + 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); + bdd result=bddtrue; + for (auto it=marked_place.begin();it!=marked_place.end();it++) { + string name=m_sog->getPlace(*it); + spot::formula f=spot::formula::ap(name); + result&=bdd_ithvar((dict_->var_map.find(f))->second); + } - return res;*/ - return bddtrue; + return result; } diff --git a/src/SogKripke.h b/src/SogKripke.h index a2bac013e9a200f25b471fa02d7315871ef35667..d4b13c849a53ba1be2a84fa620ee7f5f36fd55e1 100644 --- a/src/SogKripke.h +++ b/src/SogKripke.h @@ -9,7 +9,7 @@ class SogKripke: public spot::kripke { SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog); - SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap); + SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap); virtual ~SogKripke(); spot::state* get_init_state() const; SogKripkeIterator* succ_iter(const spot::state* s) const override; diff --git a/src/main.cpp b/src/main.cpp index 5ce1d93b10df2543246ecf98fb47624e868320f0..9fdac55de51ea1b160478caa9031b54131337c87 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -189,7 +189,7 @@ int main(int argc, char** argv) spot::print_dot(file, af); file.close(); } - auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP()); + auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()); cout<<"SOG translated to SPOT succeeded.."<<endl; cout<<"Want to save the graph in a dot file ?"; cin>>c; diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp index 14e820acf5778a913c51b74e35a6fdef2ddb917b..047dd30a33f7a67cc2d6bb4b56789c6a262412e5 100644 --- a/src/threadSOG.cpp +++ b/src/threadSOG.cpp @@ -624,6 +624,7 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised) int rc; m_graph=&g; m_graph->setTransition(m_transitionName); + m_id_thread=0; pthread_mutex_init(&m_mutex, NULL);