diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp index 5267d342aba80171e18e0fda3f9eb4f569393009..13037d583dff9c4ab330013a9537219e0ea36d74 100644 --- a/src/SogKripkeOTF.cpp +++ b/src/SogKripkeOTF.cpp @@ -18,44 +18,47 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder) //cout<<__func__<<endl; } -SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeOTF(dict_ptr,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++) { + 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++) + for (auto it=l_placeap.begin(); it!=l_placeap.end(); it++) register_ap(*it); } -state* SogKripkeOTF::get_init_state() const { - // cout<<__func__<<endl; +state* SogKripkeOTF::get_init_state() const +{ + // 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() << ")"; return out.str(); - } +} -SogKripkeIteratorOTF* SogKripkeOTF::succ_iter(const spot::state* s) const { - // cout<<__func__<<endl; +SogKripkeIteratorOTF* SogKripkeOTF::succ_iter(const spot::state* s) const +{ +// cout<<__func__<<endl; auto ss = static_cast<const SogKripkeStateOTF*>(s); - ////////////////////////////////////////////// + ////////////////////////////////////////////// return new SogKripkeIteratorOTF(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss)); } bdd SogKripkeOTF::state_condition(const spot::state* s) const - { +{ auto ss = static_cast<const SogKripkeStateOTF*>(s); vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition()); @@ -63,20 +66,22 @@ bdd SogKripkeOTF::state_condition(const spot::state* s) const bdd result=bddtrue; // Marked places - for (auto it=marked_place.begin();it!=marked_place.end();it++) { - string name=m_builder->getPlace(*it); - spot::formula f=spot::formula::ap(name); - result&=bdd_ithvar((dict_->var_map.find(f))->second); + for (auto it=marked_place.begin(); it!=marked_place.end(); it++) + { + string name=m_builder->getPlace(*it); + spot::formula f=spot::formula::ap(name); + result&=bdd_ithvar((dict_->var_map.find(f))->second); } vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_builder->getPlaceProposition()); - for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) { - string name=m_builder->getPlace(*it); - spot::formula f=spot::formula::ap(name); - result&=!bdd_ithvar((dict_->var_map.find(f))->second); + for (auto it=unmarked_place.begin(); it!=unmarked_place.end(); it++) + { + string name=m_builder->getPlace(*it); + spot::formula f=spot::formula::ap(name); + result&=!bdd_ithvar((dict_->var_map.find(f))->second); } - return result; - } + return result; +} SogKripkeOTF::~SogKripkeOTF() diff --git a/src/main.cpp b/src/main.cpp index 7dc13f6a179ad529ac7db51526e408f595587324..977117ee2f0412824972de1236bfff6cff44ca56 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -260,7 +260,8 @@ int main(int argc, char** argv) run->highlight(5); // 5 is a color number. fstream file; file.open("violated.dot",fstream::out); - cout<<"xxxxxxxxxxxxxxxxxx"<<endl; + cout<<"Property is violated"<<endl; + cout<<"Check the dot file to get a violation run"<<endl; spot::print_dot(file, k, ".kA"); file.close(); }