diff --git a/CMakeLists.txt b/CMakeLists.txt index 4e43304d03f78980f1d78d37bf55145712fa284c..5ae470481402bebe1ca1e72038ed2b452ef73f3c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -3,7 +3,7 @@ cmake_minimum_required(VERSION 3.8 FATAL_ERROR) # project name and language project(pmc-sog C CXX) -project(pmc-sog VERSION 0.4.1) +project(pmc-sog VERSION 0.4.2) configure_file(PMCSOGConfig.h.in src/PMCSOGConfig.h) diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h index 14641f8bc3378b1194fde6be66152e4ac1247aee..b3151a8d4bf838964e7c475e70f3e7c648151c5f 100644 --- a/src/HybridKripkeState.h +++ b/src/HybridKripkeState.h @@ -95,6 +95,21 @@ public: uint32_t nb_succ; memcpy(&nb_succ,inmsg,4); indice=4; + m_succ.reserve(nb_succ+2); + if (m_deadlock) { + succ_t el; + el.id[0]='d'; + el.pcontainer=0; + el._virtual=true; + el.transition=-1; + m_succ.push_back(el); + } + if (m_div) { + succ_t el=e; + el._virtual=false; + el.transition=-1; + m_succ.push_back(el); + } succ_t succ_elt; //printf("List of successors of %.16s\n",m_id); for (uint32_t i=0;i<nb_succ;i++) { @@ -108,23 +123,9 @@ public: indice+=2; succ_elt._virtual=false; m_succ.push_back(succ_elt); - // delete succ_elt; } - if (m_deadlock) { - succ_t el; - el.id[0]='d'; - el.pcontainer=0; - el._virtual=true; - el.transition=-1; - m_succ.push_back(el); - } - if (m_div) { - succ_t el=e; - el._virtual=false; - el.transition=-1; - m_succ.push_back(el); - } + } diff --git a/src/ModelCheckThReq.cpp b/src/ModelCheckThReq.cpp index 2e87f52296ea142955e50f41f4138a39664da27e..43e53580693036118ebf0d1de74299d47933e1f2 100644 --- a/src/ModelCheckThReq.cpp +++ b/src/ModelCheckThReq.cpp @@ -135,6 +135,7 @@ LDDState *ModelCheckThReq::getInitialMetaState() { c->setDiv(Set_Div(initial_meta_state)); c->setDeadLock(Set_Bloc(initial_meta_state)); if (!fire.empty()) { + for (auto it = fire.begin(); it != fire.end(); it++) m_common_stack.push(couple_th(c, *it)); std::unique_lock<std::mutex> lk(m_mutexBuildCompleted); diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp index e48c97f5281f2dfd6d944bea4d2bd12bc08bcd37..54c76d16d73bcc403925c268a8888230675638aa 100644 --- a/src/SogKripkeIteratorTh.cpp +++ b/src/SogKripkeIteratorTh.cpp @@ -6,9 +6,7 @@ SogKripkeIteratorTh::SogKripkeIteratorTh ( LDDState* lddstate, bdd cnd ) :m_lddstate ( lddstate ), kripke_succ_iterator ( cnd ) { - for ( int i=0; i<m_lddstate->getSuccessors()->size(); i++ ) { - m_lsucc.push_back ( m_lddstate->getSuccessors()->at ( i ) ); - } + m_lsucc.reserve(m_lddstate->getSuccessors()->size()+ 2); if ( lddstate->isDeadLock() ) { m_lsucc.push_back ( pair<LDDState*,int> ( &m_deadlock,-1 ) ); } @@ -16,6 +14,11 @@ SogKripkeIteratorTh::SogKripkeIteratorTh ( LDDState* lddstate, bdd cnd ) :m_ldds m_lsucc.push_back ( pair<LDDState*,int> ( (LDDState*)lddstate,-1 ) ); } + for ( int i=0; i<m_lddstate->getSuccessors()->size(); i++ ) { + m_lsucc.push_back ( m_lddstate->getSuccessors()->at ( i ) ); + } + + } bool SogKripkeIteratorTh::first() { diff --git a/src/main.cpp b/src/main.cpp index 842624afab5845280b961252ec25da8a7ded4037..4aa400d4fa62bdcf1c2316a98693c29e8907a649 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -1,4 +1,3 @@ -// version 0.1 #include <time.h> #include <chrono> #include <iostream>