From b1d45e9dff876ecb53b8f8967acc3e8136f8454b Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Mon, 23 Mar 2020 16:06:45 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/CommonSOG.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/DistributedSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20?=
=?UTF-8?q?=20=20=20=20=20=20=20src/HybridKripkeState.h=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/HybridSOG.cpp=20=09modifi?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/MCHybridSOG.cpp=20?=
=?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/ModelCheck?=
=?UTF-8?q?BaseMT.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20s?=
=?UTF-8?q?rc/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20=20src/ModelCheckerTh.cpp=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/main.cpp=20=09modifi=C3=A9=C2=A0:?=
=?UTF-8?q?=20=20=20=20=20=20=20=20=20src/threadSOG.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/CommonSOG.h | 2 +-
src/DistributedSOG.cpp | 10 +++++-----
src/HybridKripkeState.h | 4 ++--
src/HybridSOG.cpp | 6 +++---
src/MCHybridSOG.cpp | 2 +-
src/ModelCheckBaseMT.cpp | 4 ++--
src/ModelCheckLace.cpp | 26 +++++++++++++-------------
src/ModelCheckerTh.cpp | 26 +++++++++++++-------------
src/main.cpp | 10 +++++-----
src/threadSOG.cpp | 8 ++++----
10 files changed, 49 insertions(+), 49 deletions(-)
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 0de9bed..e94a93e 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -27,7 +27,7 @@ class CommonSOG
string getTransition(int pos);
string getPlace(int pos);
protected:
- NewNet m_net;
+ NewNet* m_net;
int m_nbPlaces = 0;
LDDGraph *m_graph;
vector<TransSylvan> m_tb_relation;
diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 8284488..eeaf6cf 100644
--- a/src/DistributedSOG.cpp
+++ b/src/DistributedSOG.cpp
@@ -38,7 +38,7 @@ DistributedSOG::DistributedSOG(const NewNet &R,bool init)
sylvan_init_package();
sylvan_init_ldd();
// sylvan_gc_enable();
- m_net=R;
+ m_net=&R;
m_init=init;
@@ -109,7 +109,7 @@ DistributedSOG::DistributedSOG(const NewNet &R,bool init)
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////////////////////////////// Version distribu�e en utilisant les LDD - MPI/////////////////////////////////////////////////////////
+//////////////////////////////////////////////////// Version distribu�e en utilisant les LDD - MPI/////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -175,7 +175,7 @@ void *DistributedSOG::doCompute()
while (Terminated==false)
{
- // cout<<"Nouvelle it�ration"<<endl;
+ // cout<<"Nouvelle it�ration"<<endl;
/****************************************** debut boucle pile ********************************************/
if (!m_st.empty())
{
@@ -343,7 +343,7 @@ void *DistributedSOG::doCompute()
}
}
- /****************************************** debut reception de nombre de msg envoy� ********************************************/
+ /****************************************** debut reception de nombre de msg envoy� ********************************************/
if(m_st.empty())
{
@@ -462,7 +462,7 @@ void DistributedSOG::read_state_message()
}
else delete Agregate;
MPI_Iprobe(MPI_ANY_SOURCE,TAG_STATE,MPI_COMM_WORLD,&flag,&status); // exist a msg to receiv?
- //cout<<"Fin Boucle r�ception state "<<task_id<<endl;
+ //cout<<"Fin Boucle r�ception state "<<task_id<<endl;
}
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index ec7bfa3..cd5afa9 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -4,8 +4,8 @@
#include <mpi.h>
#include "LDDState.h"
#include "ModelCheckBaseMT.h"
-#define TAG_ASK_STATE 9
-#define TAG_ACK_STATE 10
+constexpr auto TAG_ASK_STATE = 9;
+constexpr auto TAG_ACK_STATE = 10;
#define TAG_ASK_SUCC 4
#define TAG_ACK_SUCC 11
#define TAG_NOTCOMPLETED 20
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index 4d60c90..4e9a73d 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -64,7 +64,7 @@ HybridSOG::HybridSOG(const NewNet &R,bool init)
sylvan_init_package();
sylvan_init_ldd();
sylvan_gc_enable();
- m_net=R;
+ m_net=&R;
m_init=init;
m_nbPlaces=R.places.size();
@@ -144,7 +144,7 @@ HybridSOG::HybridSOG(const NewNet &R,bool init)
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////////////////////////////// Version distribu�e en utilisant les LDD - MPI/////////////////////////////////////////////////////////
+//////////////////////////////////////////////////// Version distribu�e en utilisant les LDD - MPI/////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -447,7 +447,7 @@ void *HybridSOG::doCompute()
}
- /******************************* Construction des aggregats � partir de pile de messages ************************************/
+ /******************************* Construction des aggregats � partir de pile de messages ************************************/
if (!m_msg[id_thread].empty())
{
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 35e8816..ab2a151 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -40,7 +40,7 @@ MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world,bool init)
sylvan_init_package();
sylvan_init_ldd();
sylvan_gc_enable();
- m_net=R;
+ m_net=&R;
m_init=init;
m_nbPlaces=R.places.size();
diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp
index c9e7a49..4a854fa 100644
--- a/src/ModelCheckBaseMT.cpp
+++ b/src/ModelCheckBaseMT.cpp
@@ -9,8 +9,8 @@ using namespace sylvan;
ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R,int nbThread)
{
m_nb_thread=nbThread;
- m_net=R;
- m_nbPlaces=m_net.places.size();
+ m_net=&R;
+ m_nbPlaces=m_net->places.size();
}
void ModelCheckBaseMT::loadNet()
{
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index cb4c3f8..7ef1b3a 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -43,27 +43,27 @@ void ModelCheckLace::preConfigure() {
int i;
vector<Place>::const_iterator it_places;
- transitions=m_net.transitions;
- m_observable=m_net.Observable;
- m_place_proposition=m_net.m_formula_place;
- m_nonObservable=m_net.NonObservable;
+ transitions=m_net->transitions;
+ m_observable=m_net->Observable;
+ m_place_proposition=m_net->m_formula_place;
+ m_nonObservable=m_net->NonObservable;
- m_transitionName=m_net.transitionName;
- m_placeName=m_net.m_placePosName;
+ m_transitionName=m_net->transitionName;
+ m_placeName=m_net->m_placePosName;
- InterfaceTrans=m_net.InterfaceTrans;
+ InterfaceTrans=m_net->InterfaceTrans;
cout<<"Nombre de places : "<<m_nbPlaces<<endl;
- cout<<"Derniere place : "<<m_net.places[m_nbPlaces-1].name<<endl;
+ cout<<"Derniere place : "<<m_net->places[m_nbPlaces-1].name<<endl;
- uint32_t * liste_marques=new uint32_t[m_net.places.size()];
- for(i=0,it_places=m_net.places.begin(); it_places!=m_net.places.end(); i++,it_places++)
+ uint32_t * liste_marques=new uint32_t[m_net->places.size()];
+ for(i=0,it_places=m_net->places.begin(); it_places!=m_net->places.end(); i++,it_places++)
{
liste_marques[i] =it_places->marking;
}
- m_initialMarking=lddmc_cube(liste_marques,m_net.places.size());
+ m_initialMarking=lddmc_cube(liste_marques,m_net->places.size());
delete []liste_marques;
lddmc_refs_push(m_initialMarking);
@@ -73,8 +73,8 @@ void ModelCheckLace::preConfigure() {
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc= new uint32_t [m_nbPlaces];
// Transition relation
- for(auto t=m_net.transitions.begin();
- t!=m_net.transitions.end(); t++)
+ for(auto t=m_net->transitions.begin();
+ t!=m_net->transitions.end(); t++)
{
// Initialisation
for(i=0; i<m_nbPlaces; i++)
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 0666d72..67b02dc 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -24,31 +24,31 @@ void ModelCheckerTh::preConfigure() {
init_gc_seq();
- //_______________
- transitions = m_net.transitions;
- m_observable = m_net.Observable;
- m_place_proposition = m_net.m_formula_place;
- m_nonObservable = m_net.NonObservable;
- m_transitionName = m_net.transitionName;
- m_placeName = m_net.m_placePosName;
+ transitions = m_net->transitions;
+ m_observable = m_net->Observable;
+ m_place_proposition = m_net->m_formula_place;
+ m_nonObservable = m_net->NonObservable;
- InterfaceTrans = m_net.InterfaceTrans;
+ m_transitionName = m_net->transitionName;
+ m_placeName = m_net->m_placePosName;
+
+ InterfaceTrans = m_net->InterfaceTrans;
cout << "Nombre de places : " << m_nbPlaces << endl;
- cout << "Derniere place : " << m_net.places[m_nbPlaces - 1].name << endl;
+ cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
- uint32_t *liste_marques = new uint32_t[m_net.places.size()];
- for (i = 0, it_places = m_net.places.begin(); it_places != m_net.places.end(); i++, it_places++) {
+ uint32_t *liste_marques = new uint32_t[m_net->places.size()];
+ for (i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++) {
liste_marques[i] = it_places->marking;
}
- m_initialMarking = lddmc_cube(liste_marques, m_net.places.size());
+ m_initialMarking = lddmc_cube(liste_marques, m_net->places.size());
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc = new uint32_t[m_nbPlaces];
// Transition relation
- for (vector<Transition>::const_iterator t = m_net.transitions.begin(); t != m_net.transitions.end(); t++) {
+ for (vector<Transition>::const_iterator t = m_net->transitions.begin(); t != m_net->transitions.end(); t++) {
// Initialisation
for (i = 0; i < m_nbPlaces; i++) {
prec[i] = 0;
diff --git a/src/main.cpp b/src/main.cpp
index 2e5c6d9..0f773ef 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -150,8 +150,8 @@ int main(int argc, char **argv) {
auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
cout << "Performing on the fly Modelchecking" << endl;
if (strcmp(algorithm, "")) {
- cout << "Couvreur99 algorithm..." << endl;
- shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
+ cout << "Spot emptiness check algorithm : "<<algorithm<< endl;
+ shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(k,af);
//spot::couvreur99_check_shy check = spot::couvreur99_check_shy(product);
/****************************/
const char *err;
@@ -162,8 +162,8 @@ int main(int argc, char **argv) {
cerr << "Spot unknown emptiness algorithm" << endl;
exit(2);
}
- spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
auto startTime = std::chrono::steady_clock::now();
+ spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
bool res = (echptr->check() == 0);
auto finalTime = std::chrono::steady_clock::now();
displayTime(startTime, finalTime);
@@ -332,10 +332,10 @@ int main(int argc, char **argv) {
}
else
cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
+ auto startTime = std::chrono::high_resolution_clock::now();
spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
- auto startTime = std::chrono::steady_clock::now();
bool res = (echptr->check() == 0);
- auto finalTime = std::chrono::steady_clock::now();
+ auto finalTime = std::chrono::high_resolution_clock::now();
displayTime(startTime, finalTime);
displayCheckResult(res);
/*spot::couvreur99_check check = spot::couvreur99_check(product);
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index b6cf5bc..b6fa858 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -46,7 +46,7 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
/*sylvan_gc_hook_pregc(TASK(gc_start));
sylvan_gc_hook_postgc(TASK(gc_end));
sylvan_gc_enable();*/
- m_net=R;
+ m_net=&R;
m_init=init;
int i;
@@ -146,7 +146,7 @@ threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
-//**************************************************** Version s�quentielle en utilisant les LDD********************************************************************
+//**************************************************** Version s�quentielle en utilisant les LDD********************************************************************
void threadSOG::computeSeqSOG(LDDGraph &g)
{
// m_graph=&g;
@@ -436,7 +436,7 @@ void * threadSOG::doCompute()
}
while (isNotTerminated());
- //cout<<"Thread :"<<id_thread<<" has performed "<<nb_it<<" it�rations avec "<<nb_failed<<" �checs"<<endl;
+ //cout<<"Thread :"<<id_thread<<" has performed "<<nb_it<<" it�rations avec "<<nb_failed<<" �checs"<<endl;
//cout<<"Max succ :"<<max_succ<<endl;
}
@@ -601,7 +601,7 @@ void * threadSOG::doComputeCanonized()
}
while (isNotTerminated());
- //cout<<"Thread :"<<id_thread<<" has performed "<<nb_it<<" it�rations avec "<<nb_failed<<" �checs"<<endl;
+ //cout<<"Thread :"<<id_thread<<" has performed "<<nb_it<<" it�rations avec "<<nb_failed<<" �checs"<<endl;
//cout<<"Max succ :"<<max_succ<<endl;
}
--
GitLab