From de376356617aca872233ecd8579625742ddf90ed Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sun, 2 Jun 2019 23:46:49 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/SogKripkeOTF.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/SogKripkeOTF.cpp | 49 ++++++++++++++++++++++++--------------------
src/main.cpp | 3 ++-
2 files changed, 29 insertions(+), 23 deletions(-)
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index 5267d34..13037d5 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 7dc13f6..977117e 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();
}
--
GitLab