diff --git a/CMakeLists.txt b/CMakeLists.txt index 668dedcaa5902124ee1a4422ca68e42ac6c5b65e..f11cb076b140cfc115a6725bff79905019e9de7b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -6,7 +6,7 @@ project(pmc-sog C CXX) # compiler flags if(CMAKE_COMPILER_IS_GNUCC) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -g3") endif() # add pn parser diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp index 498a6d400c268c974848be3e3eb3c19229292171..8200ca6ca70812e98c740bb8eb981076c3b217c2 100644 --- a/src/CommonSOG.cpp +++ b/src/CommonSOG.cpp @@ -226,4 +226,4 @@ string CommonSOG::getPlace(int pos) { return m_graph->getPlace(pos); } - +static LDDGraph *CommonSOG::m_graph; diff --git a/src/CommonSOG.h b/src/CommonSOG.h index e94a93ebe2061896287b0d124b326f7c5bdc92e8..39a3d47671c86346a446aa6bd2e49b7a42beae5b 100644 --- a/src/CommonSOG.h +++ b/src/CommonSOG.h @@ -29,7 +29,7 @@ class CommonSOG protected: NewNet* m_net; int m_nbPlaces = 0; - LDDGraph *m_graph; + static LDDGraph *m_graph; vector<TransSylvan> m_tb_relation; MDD m_initialMarking; map<string, uint16_t> m_transitionName; diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp index b8e89d2bae4a0594f5f90743344ab3011a2b328f..eaba61f91f4271dfe4c626036c38da531aac1f10 100644 --- a/src/LDDGraph.cpp +++ b/src/LDDGraph.cpp @@ -12,6 +12,7 @@ LDDGraph::~LDDGraph() void LDDGraph::setInitialState(LDDState *c) { m_currentstate=m_initialstate=c; + // } diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp index 4a854fa86da2bf962420de5f0c5bcdc945a55ee0..69af2039d3b6be2e1be3ad14caff030f45e46e66 100644 --- a/src/ModelCheckBaseMT.cpp +++ b/src/ModelCheckBaseMT.cpp @@ -14,8 +14,8 @@ ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R,int nbThread) } void ModelCheckBaseMT::loadNet() { - preConfigure(); - m_graph=new LDDGraph(this); + m_graph=new LDDGraph(this); + preConfigure(); m_graph->setTransition(m_transitionName); m_graph->setPlace(m_placeName); } diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp index 67b02dcd065e1aead7f0dbff30083ca4974be577..05efa1e88039a21216664cbff255664ce44d234b 100644 --- a/src/ModelCheckerTh.cpp +++ b/src/ModelCheckerTh.cpp @@ -86,8 +86,7 @@ void ModelCheckerTh::preConfigure() { } LDDState* ModelCheckerTh::getInitialMetaState() { - while (!m_finish_initial) - ; + while (!m_finish_initial) ; LDDState *initial_metastate = m_graph->getInitialState(); if (!initial_metastate->isVisited()) { initial_metastate->setVisited(); @@ -112,18 +111,20 @@ void* ModelCheckerTh::Compute_successors() { pthread_mutex_unlock(&m_mutex); Set fire; int min_charge = 0; + if (id_thread == 0) { LDDState *c = new LDDState; MDD Complete_meta_state(Accessible_epsilon(m_initialMarking)); ldd_refs_push(Complete_meta_state); MDD canonised_initial = Complete_meta_state; //Canonize(Complete_meta_state,0); - ldd_refs_push(canonised_initial); + /*ldd_refs_push(canonised_initial);*/ fire = firable_obs(Complete_meta_state); c->m_lddstate = canonised_initial; - c->setDeadLock(Set_Bloc(Complete_meta_state)); - c->setDiv(Set_Div(Complete_meta_state)); + c->setDeadLock(false);//Set_Bloc(Complete_meta_state)); + c->setDiv(false);//Set_Div(Complete_meta_state)); m_st[0].push(Pair(couple(c, Complete_meta_state), fire)); + m_graph->setInitialState(c); m_graph->insert(c); m_charge[0] = 1; @@ -154,10 +155,9 @@ void* ModelCheckerTh::Compute_successors() { } MDD Complete_meta_state = Accessible_epsilon(get_successor(e.first.second, t)); - ldd_refs_push(Complete_meta_state); MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0); - ldd_refs_push(reduced_meta); + /*ldd_refs_push(reduced_meta);*/ if (id_thread == 0) { pthread_mutex_lock(&m_gc_mutex); @@ -188,8 +188,8 @@ void* ModelCheckerTh::Compute_successors() { m_graph->addArc(); m_graph->insert(reached_class); - reached_class->setDiv(Set_Div(Complete_meta_state)); - reached_class->setDeadLock(Set_Bloc(Complete_meta_state)); + reached_class->setDiv(false);//Set_Div(Complete_meta_state)); + reached_class->setDeadLock(false);//Set_Bloc(Complete_meta_state)); pthread_mutex_unlock(&m_graph_mutex); e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(reached_class, t)); diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp index 9cb4ccc9487232c2f22c8330ccc70cf8a8bc300e..d410ea5a49c9b769f4d3d378066e6fefac464b17 100644 --- a/src/SogKripkeTh.cpp +++ b/src/SogKripkeTh.cpp @@ -78,7 +78,7 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const { auto ss = static_cast<const SogKripkeStateTh*>(s); - vector<uint16_t> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition()); + vector<uint16_t> marked_place = ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition()); bdd result=bddtrue;