diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp index b155c67f1c615de8d56d53c80dbf8f516f52b447..1e748b0e1599a063d1536d3e783635d407ccec2a 100644 --- a/src/ModelCheckerTh.cpp +++ b/src/ModelCheckerTh.cpp @@ -152,6 +152,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 84156d77178fa6996d6ab9f8df7bbd7d2dd09a9d..85b562ba87643ccfc4f3d89333015379f74cd6f3 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; @@ -217,8 +229,24 @@ int main(int argc, char** argv) auto k = +<<<<<<< HEAD std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ; +======= + std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); +>>>>>>> 8a83ddf40bff014aa15b8f24670733207dbbd072 // 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))