From 521068bb0cbd3cc8e25ecb2e83506d53f4d98fd0 Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Sat, 4 May 2019 00:05:03 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/SogKripke.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?= =?UTF-8?q?=20=20=20src/SogKripkeIterator.cpp=20=09modifi=C3=A9=C2=A0:=20?= =?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeIterator.h=20=09modifi?= =?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/main.cpp?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/SogKripke.cpp | 10 ++++++---- src/SogKripkeIterator.cpp | 11 ++++++----- src/SogKripkeIterator.h | 3 +-- src/main.cpp | 22 ++++++++++++++++++---- 4 files changed, 31 insertions(+), 15 deletions(-) diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp index 4d5c071..db484e9 100644 --- a/src/SogKripke.cpp +++ b/src/SogKripke.cpp @@ -36,6 +36,7 @@ std::string SogKripke::format_state(const spot::state* s) const auto ss = static_cast<const SogKripkeState*>(s); std::ostringstream out; out << "( " << ss->getLDDState()->getLDDValue() << ")"; + cout << "( " << ss->getLDDState()->getLDDValue() << ")"; return out.str(); } @@ -49,17 +50,18 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const { 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(m_sog->getConstructor()->getPlaceProposition()); - 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<<" "<<name<<endl; + //cout<<"Place name marked : "<<" "<<name<<endl; spot::formula f=spot::formula::ap(name); - result&=bdd_ithvar((dict_->var_map.find(f))->second); + result=bdd_ithvar((dict_->var_map.find(f))->second); + cout<<"verified ldd : "<<ss->getLDDState()->getLDDValue()<<"Place name marked : "<<name<<endl; } return result; diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp index 9b2b679..c60d0ea 100644 --- a/src/SogKripkeIterator.cpp +++ b/src/SogKripkeIterator.cpp @@ -51,14 +51,15 @@ bdd SogKripkeIterator::cond() const { spot::formula f=spot::formula::ap(name); bdd result=bdd_ithvar((p->var_map.find(f))->second); - //cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n"; - return result; + //cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n";*/ + //return result; + return result & spot::kripke_succ_iterator::cond(); } -spot::acc_cond::mark_t SogKripkeIterator::acc() const { +/*spot::acc_cond::mark_t SogKripkeIterator::acc() const { //cout<<"Iterator acc()\n"; - return 1U; -} + return 0U; +}*/ SogKripkeIterator::~SogKripkeIterator() { //dtor diff --git a/src/SogKripkeIterator.h b/src/SogKripkeIterator.h index 435c240..7793c11 100644 --- a/src/SogKripkeIterator.h +++ b/src/SogKripkeIterator.h @@ -16,9 +16,8 @@ class SogKripkeIterator : public spot::kripke_succ_iterator bool next() override; bool done() const override; SogKripkeState* dst() const override; - bdd cond() const override final; - spot::acc_cond::mark_t acc() const override final; + /* spot::acc_cond::mark_t acc() const override final;*/ protected: diff --git a/src/main.cpp b/src/main.cpp index 7378758..6b4c004 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -189,20 +189,34 @@ int main(int argc, char** argv) spot::print_dot(file, af); file.close(); } - auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()); + //auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()); + + spot::twa_graph_ptr k = + spot::make_twa_graph(std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP()), + spot::twa::prop_set::all(), true); + + cout<<"SOG translated to SPOT succeeded.."<<endl; cout<<"Want to save the graph in a dot file ?"; cin>>c; if (c=='y') { fstream file; + string st(argv[3]); st+=".dot"; file.open(st.c_str(),fstream::out); - spot::print_dot(file, k); + spot::print_dot(file, k,"ka"); file.close(); } - if (auto run = k->intersecting_run(af)) - std::cout << "formula is violated by the following run:\n" << *run; + if (auto run = k->intersecting_run(af)) { + /*std::cout << "formula is violated by the following run:\n" << *run;*/ + run->highlight(5); // 5 is a color number. + fstream file; + file.open("violated.dot",fstream::out); + cout<<"xxxxxxxxxxxxxxxxxx"<<endl; + spot::print_dot(file, k, ".kA"); + file.close(); + } else std::cout << "formula is verified\n"; } -- GitLab