diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 0de9bedf203c138c245038a9f5dd59193e86a5bf..e94a93ebe2061896287b0d124b326f7c5bdc92e8 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 8284488f3c6fa6acae8a88dafcb14eac78982518..eeaf6cfea16c728644bd8a91f420a26c13842344 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 ec7bfa30ba6aa56f48d5b847081bd4ab8edc5dff..cd5afa9496e16b47b5f2b76879cfff5eb4376b8f 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 4d60c90e8a4097760e4f4592b85dc30556f5720f..4e9a73d99f8aa5a032876ec33e776916ff41e62c 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 35e8816e370774c21baa9530ff70130a580d4e7d..ab2a151b4c9c0f34fcb1fa94665de846a45c9156 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 c9e7a49097597a6b5133a92ae1feca603f95ec93..4a854fa86da2bf962420de5f0c5bcdc945a55ee0 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 cb4c3f838fbe63a1747bb4db6e3f6461589d50ee..7ef1b3afb9d964e0598c1b7056771272bfc10cf9 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 0666d7297c1908193fea0b15e63194b03dfd3074..67b02dcd065e1aead7f0dbff30083ca4974be577 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 2e5c6d9d17a9f04bdfcf6739f92aec9356713e52..0f773efc82f9ba2c159f83413559b7dde77423bd 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 b6cf5bc8287217c8557d1a9427d21709f28e92a4..b6fa85817271201e2c097bf19515913dfba23221 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;
}