diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp index f86562dd1b76d8b8e22742d72c6f293fec09749c..2cc68c683c278d8b004d05906dac268ad451a95c 100644 --- a/src/SogKripke.cpp +++ b/src/SogKripke.cpp @@ -14,24 +14,15 @@ SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(d { SogKripkeIterator::m_graph=sog; SogKripkeIterator::m_dict_ptr=&dict_ptr; -/*spot::bdd_dict *p=dict_ptr.get(); -cout<<"Taille du dictionnaire :"<<p->var_map.size()<<endl; +} -map<spot::formula,int>::iterator i=(p->var_map).begin(); +SogKripke::SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap):SogKripke(dict_ptr,sog) { + for (auto it=l_transap.begin();it!=l_transap.end();it++) { + register_ap(*it); + } +} -while (i!=(p->var_map).end()) { - cout<<" test :"<<(*i).first.ap_name()<<endl; -std::ostringstream stream; - stream << (*i).first; - std::string str = stream.str(); - cout<<" formule 1: "<<str<<endl; - cout<<" formule 2: "<<str<<endl; - i++; -}*/ -//spot::bdd_format_formula(dict_ptr,"test"); -//map<bdd,spot::ltl::formula>.iterator it=p->vf_map.begin(); -} state* SogKripke::get_init_state() const { //cout<<"Initial state given...\n"; return new SogKripkeState(m_sog->getInitialState());//new SpotSogState(); @@ -57,17 +48,18 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const { return new SogKripkeIterator(ss->getLDDState(),b);//,b);//s state_condition(ss)); } - /* MDD state_condition(const spot::state* s) const override +bdd SogKripke::state_condition(const spot::state* s) const { - auto ss = static_cast<const SogKripkeState*>(s); + /*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)) - return res; - }*/ + return res;*/ + return bddtrue; + } SogKripke::~SogKripke() diff --git a/src/SogKripke.h b/src/SogKripke.h index a0cf52d2da10e5bc2b82efe658b60d4173aae2b0..a2bac013e9a200f25b471fa02d7315871ef35667 100644 --- a/src/SogKripke.h +++ b/src/SogKripke.h @@ -9,11 +9,12 @@ 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); virtual ~SogKripke(); spot::state* get_init_state() const; SogKripkeIterator* succ_iter(const spot::state* s) const override; std::string format_state(const spot::state* s) const override; - // MDD state_condition(const spot::state* s) const override; + bdd state_condition(const spot::state* s) const override; protected: diff --git a/src/SogTwa.cpp b/src/SogTwa.cpp index f65c22bdbc86a208d8f33dceac399456038352b5..42ea5c24844880c8460b9f2ecdeb06f5d1743c43 100644 --- a/src/SogTwa.cpp +++ b/src/SogTwa.cpp @@ -14,23 +14,13 @@ SogTwa::SogTwa(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): twa(dict_ptr),m_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; - -map<spot::formula,int>::iterator i=(p->var_map).begin(); - -while (i!=(p->var_map).end()) { - cout<<" test :"<<(*i).first.ap_name()<<endl; -std::ostringstream stream; - stream << (*i).first; - std::string str = stream.str(); - cout<<" formule 1: "<<str<<endl; - cout<<" formule 2: "<<str<<endl; - i++; -}*/ -//spot::bdd_format_formula(dict_ptr,"test"); -//map<bdd,spot::ltl::formula>.iterator it=p->vf_map.begin(); +} + +SogTwa::SogTwa(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap):SogTwa(dict_ptr,sog) { + for (auto it=l_transap.begin();it!=l_transap.end();it++) { + register_ap(*it); + } } state* SogTwa::get_init_state() const { //cout<<"Initial state given...\n"; diff --git a/src/SogTwa.h b/src/SogTwa.h index 05a0033be06f80f3173735657b7e12ada80f95ce..5a39479ed0d8a71ebec8141115bb36ce3f343128 100644 --- a/src/SogTwa.h +++ b/src/SogTwa.h @@ -7,6 +7,7 @@ class SogTwa : public spot::twa { public: SogTwa(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog); + SogTwa(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap); virtual ~SogTwa(); spot::state* get_init_state() const; SpotSogIterator* succ_iter(const spot::state* s) const override; diff --git a/src/main.cpp b/src/main.cpp index 4645d56af360016a2f3741cee419e1bb517e5f6f..5ce1d93b10df2543246ecf98fb47624e868320f0 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -176,6 +176,7 @@ int main(int argc, char** argv) { cout<<"Building automata for not(formula)\n"; auto d = spot::make_bdd_dict(); + // d->register_ap("jbhkj"); spot::twa_graph_ptr af = spot::translator(d).run(not_f); cout<<"Formula automata built.\n"; cout<<"Want to save the graph in a dot file ?"; @@ -188,7 +189,7 @@ int main(int argc, char** argv) spot::print_dot(file, af); file.close(); } - auto k = std::make_shared<SogTwa>(d,DR.getGraph()); + auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP()); cout<<"SOG translated to SPOT succeeded.."<<endl; cout<<"Want to save the graph in a dot file ?"; cin>>c;