From 4142afbae8be2152b0345dac00043d5186eb2c68 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Wed, 29 May 2019 11:53:54 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/SogKripkeIteratorOTF.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeOTF.cpp=20=09mod?=
=?UTF-8?q?ifi=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/ModelCheckLace.cpp | 2 ++
src/SogKripkeIteratorOTF.cpp | 4 ++--
src/SogKripkeOTF.cpp | 1 +
src/main.cpp | 22 +++++-----------------
4 files changed, 10 insertions(+), 19 deletions(-)
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 62fbe66..dd7e34c 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -213,6 +213,7 @@ LDDState * ModelCheckLace::buildInitialMetaState()
void ModelCheckLace::buildSucc(LDDState *agregate)
{
+
if (!agregate->isVisited()) {
// It's first time to visit agregate, then we have to build its successors
agregate->setVisited();
@@ -260,6 +261,7 @@ void ModelCheckLace::buildSucc(LDDState *agregate)
}
+
}
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
index c0a9245..2790ac5 100644
--- a/src/SogKripkeIteratorOTF.cpp
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -21,7 +21,7 @@ SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_
}
bool SogKripkeIteratorOTF::first() {
- //cout<<"entering "<<__func__<<endl;
+ // cout<<"entering "<<__func__<<endl;
m_current_edge=0;
//cout<<"exciting "<<__func__<<endl;
return m_lsucc.size()!=0;
@@ -43,7 +43,7 @@ bool SogKripkeIteratorOTF::done() const {
SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
{
- //out<<"enter/excit "<<__func__<<endl;
+ //cout<<"enter/excit "<<__func__<<endl;
return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
}
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index f9b3451..5267d34 100644
--- a/src/SogKripkeOTF.cpp
+++ b/src/SogKripkeOTF.cpp
@@ -15,6 +15,7 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder)
SogKripkeIteratorOTF::m_builder=builder;
SogKripkeStateOTF::m_builder=builder;
SogKripkeIteratorOTF::m_dict_ptr=&dict_ptr;
+ //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) {
diff --git a/src/main.cpp b/src/main.cpp
index 4d9e172..7dc13f6 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -148,33 +148,21 @@ int main(int argc, char** argv)
// Initialize SOG builder
ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
cout<<"Created"<<endl;
- spot::twa_graph_ptr k =
- spot::make_twa_graph(std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
- spot::twa::prop_set::all(), true);
+ auto k =
+ std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ;
// Performing on the fly Modelchecking
cout<<"Performing on the fly Modelchecking"<<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,"ka");
- file.close();
- }
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.
+ std::cout << "formula is violated by the following run:\n"<<*run<<endl;
+ /*run->highlight(5); // 5 is a color number.
fstream file;
file.open("violated.dot",fstream::out);
cout<<"Property is violated!"<<endl;
cout<<"Check the dot file."<<endl;
spot::print_dot(file, k, ".kA");
- file.close();
+ file.close();*/
}
else
std::cout << "formula is verified\n";
--
GitLab