From 8a83ddf40bff014aa15b8f24670733207dbbd072 Mon Sep 17 00:00:00 2001 From: ouni <ouni@lipn.univ-paris13.fr> Date: Tue, 4 Jun 2019 15:21:50 +0200 Subject: [PATCH] src/ModelCheckerTh --- src/ModelCheckerTh.cpp | 4 ++++ src/main.cpp | 28 ++++++++++++++++++++++++++-- 2 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp index 55925ec..091f3c9 100644 --- a/src/ModelCheckerTh.cpp +++ b/src/ModelCheckerTh.cpp @@ -155,6 +155,10 @@ void ModelCheckerTh::buildSucc(LDDState *agregate) pthread_spin_lock(&m_spin_stack[m_min_charge]); m_st[m_min_charge].push(agregate); pthread_spin_unlock(&m_spin_stack[m_min_charge]); + if(!isNotTerminated()) + { + ComputeTh_Succ(); + } } } diff --git a/src/main.cpp b/src/main.cpp index 619058a..98b7413 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -151,7 +151,19 @@ int main(int argc, char** argv) ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th); cout<<"Created"<<endl; auto k = - std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ; + std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); + 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(); + } ; // Performing on the fly Modelchecking cout<<"Performing on the fly Modelchecking"<<endl; @@ -194,8 +206,20 @@ int main(int argc, char** argv) ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th); cout<<"Created"<<endl; auto k = - std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ; + std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); // Performing on the fly Modelchecking + 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(); + } cout<<"Performing on the fly Modelchecking"<<endl; if (auto run = k->intersecting_run(af)) -- GitLab