From 720974b5c8d63f446ddafaf62a76624da2309083 Mon Sep 17 00:00:00 2001
From: ouni <ouni@lipn.univ-paris13.fr>
Date: Wed, 29 May 2019 01:57:54 +0200
Subject: [PATCH] src
---
src/main.cpp | 30 +++++++++++++++++++++++++++---
1 file changed, 27 insertions(+), 3 deletions(-)
diff --git a/src/main.cpp b/src/main.cpp
index 3d07fc7..e67360c 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -149,11 +149,35 @@ int main(int argc, char** argv)
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);
+ spot::make_twa_graph(std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
+ spot::twa::prop_set::all(), true);
// Performing on the fly Modelchecking
cout<<"Performing on the fly Modelchecking"<<endl;
- exit(0);
+ 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.
+ fstream file;
+ file.open("violated.dot",fstream::out);
+ cout<<"xxxxxviolatedxxxxxxx"<<endl;
+ spot::print_dot(file, k, ".kA");
+ file.close();
+ }
+ else
+ std::cout << "formula is verified\n";
+ // exit(0);
}
else if (n_tasks==1)
{
--
GitLab