From ffc832c4246ec20b686a85f10d47b010c8ec4120 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Wed, 27 Jan 2021 17:18:07 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20CMakeLists.txt=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
=?UTF-8?q?=20=20src/HybridKripkeState.h=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/ModelCheckThReq.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeIteratorTh.cpp?=
=?UTF-8?q?=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/main.cp?=
=?UTF-8?q?p?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
CMakeLists.txt | 2 +-
src/HybridKripkeState.h | 31 ++++++++++++++++---------------
src/ModelCheckThReq.cpp | 1 +
src/SogKripkeIteratorTh.cpp | 9 ++++++---
src/main.cpp | 1 -
5 files changed, 24 insertions(+), 20 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4e43304..5ae4704 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 14641f8..b3151a8 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 2e87f52..43e5358 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 e48c97f..54c76d1 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 842624a..4aa400d 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -1,4 +1,3 @@
-// version 0.1
#include <time.h>
#include <chrono>
#include <iostream>
--
GitLab