From 3584e7b5a63c8cb7ba521b8ce1e58687dd6c569a Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sat, 15 Feb 2020 18:33:53 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/DistributedSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/DistributedSOG.h=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/HybridSOG.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/HybridSOG.h=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/MCHybridSO?=
=?UTF-8?q?G.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/Mode?=
=?UTF-8?q?lCheckBaseMT.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
=?UTF-8?q?=20=20src/ModelCheckBaseMT.h=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/ModelCheckLace.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/ModelCheckLace.h=20=09mod?=
=?UTF-8?q?ifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/ModelCheckerTh.c?=
=?UTF-8?q?pp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/Model?=
=?UTF-8?q?CheckerTh.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20?=
=?UTF-8?q?src/main.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/threadSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/threadSOG.h?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/DistributedSOG.cpp | 2 +-
src/DistributedSOG.h | 2 +-
src/HybridSOG.cpp | 2 +-
src/HybridSOG.h | 2 +-
src/MCHybridSOG.cpp | 2 +-
src/MCHybridSOG.h | 2 +-
src/ModelCheckBaseMT.cpp | 2 +-
src/ModelCheckBaseMT.h | 2 +-
src/ModelCheckLace.cpp | 2 +-
src/ModelCheckLace.h | 2 +-
src/ModelCheckerTh.cpp | 2 +-
src/ModelCheckerTh.h | 2 +-
src/main.cpp | 13 ++++++-------
src/threadSOG.cpp | 2 +-
src/threadSOG.h | 22 +++++++++++-----------
15 files changed, 30 insertions(+), 31 deletions(-)
diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 3c5a77c..8284488 100644
--- a/src/DistributedSOG.cpp
+++ b/src/DistributedSOG.cpp
@@ -25,7 +25,7 @@ using namespace sylvan;
/**************************************************/
-DistributedSOG::DistributedSOG(const NewNet &R, int BOUND,bool init)
+DistributedSOG::DistributedSOG(const NewNet &R,bool init)
{
diff --git a/src/DistributedSOG.h b/src/DistributedSOG.h
index d608110..16c4327 100644
--- a/src/DistributedSOG.h
+++ b/src/DistributedSOG.h
@@ -46,7 +46,7 @@ extern int n_tasks, task_id;
// typedef vector<Trans> vec_trans;
class DistributedSOG : public CommonSOG{
public:
- DistributedSOG(const NewNet &, int BOUND = 32, bool init = false);
+ DistributedSOG(const NewNet &, bool init = false);
void buildFromNet(int index);
void computeDSOG(LDDGraph &g);
void BuildInitialState(LDDState *m_state, MDD mdd);
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index 4da8513..4d60c90 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -50,7 +50,7 @@ using namespace sylvan;
} */
-HybridSOG::HybridSOG(const NewNet &R, int BOUND,bool init)
+HybridSOG::HybridSOG(const NewNet &R,bool init)
{
diff --git a/src/HybridSOG.h b/src/HybridSOG.h
index f480981..dab4baa 100644
--- a/src/HybridSOG.h
+++ b/src/HybridSOG.h
@@ -47,7 +47,7 @@ typedef stack<MSG> pile_msg;
class HybridSOG : public CommonSOG
{
public:
- HybridSOG(const NewNet &, int BOUND = 32, bool init = false);
+ HybridSOG(const NewNet &, bool init = false);
void buildFromNet(int index);
/// principal functions to construct the SOG
void computeDSOG(LDDGraph &g);
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index c0d31b8..e793f5d 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -25,7 +25,7 @@ using namespace sylvan;
#define TAG_ACK_SUCC 11
#define TAG_NOTCOMPLETED 20
-MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world, int BOUND,bool init)
+MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world,bool init)
{
m_comm_world=comm_world;
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index ae70af3..f41218b 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -48,7 +48,7 @@ typedef stack<MSG> pile_msg;
class MCHybridSOG : public CommonSOG
{
public:
- MCHybridSOG(const NewNet &,MPI_Comm &, int BOUND = 32, bool init = false);
+ MCHybridSOG(const NewNet &,MPI_Comm &, bool init = false);
void buildFromNet(int index);
/// principal functions to construct the SOG
void computeDSOG(LDDGraph &g);
diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp
index 4e8df68..c9e7a49 100644
--- a/src/ModelCheckBaseMT.cpp
+++ b/src/ModelCheckBaseMT.cpp
@@ -6,7 +6,7 @@
#include <sylvan_int.h>
using namespace sylvan;
-ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R, int BOUND,int nbThread)
+ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R,int nbThread)
{
m_nb_thread=nbThread;
m_net=R;
diff --git a/src/ModelCheckBaseMT.h b/src/ModelCheckBaseMT.h
index 0215fc2..d6dbd4c 100644
--- a/src/ModelCheckBaseMT.h
+++ b/src/ModelCheckBaseMT.h
@@ -3,7 +3,7 @@
#include "CommonSOG.h"
class ModelCheckBaseMT : public CommonSOG {
public:
- ModelCheckBaseMT(const NewNet &R, int BOUND,int nbThread);
+ ModelCheckBaseMT(const NewNet &R,int nbThread);
virtual LDDState * getInitialMetaState()=0;
virtual void buildSucc(LDDState *agregate)=0;
void loadNet();
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 740269a..01b157e 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -6,7 +6,7 @@
#include <sylvan_int.h>
using namespace sylvan;
-ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread):ModelCheckBaseMT(R,BOUND,nbThread)
+ModelCheckLace::ModelCheckLace(const NewNet &R,int nbThread):ModelCheckBaseMT(R,nbThread)
{
}
void
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index bd2e6f8..1b540b4 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -3,7 +3,7 @@
#include "ModelCheckBaseMT.h"
class ModelCheckLace : public ModelCheckBaseMT {
public:
- ModelCheckLace(const NewNet &R, int BOUND,int nbThread);
+ ModelCheckLace(const NewNet &R,int nbThread);
LDDState * getInitialMetaState() override;
void buildSucc(LDDState *agregate) override;
private:
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 9a4af03..ab91b12 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -7,7 +7,7 @@
using namespace sylvan;
-ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread):ModelCheckBaseMT(R,BOUND,nbThread) {
+ModelCheckerTh::ModelCheckerTh(const NewNet &R,int nbThread):ModelCheckBaseMT(R,nbThread) {
}
void ModelCheckerTh::preConfigure()
{
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index f03025c..c274d19 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -7,7 +7,7 @@ typedef stack<pair<LDDState *,int>> pile_t;
class ModelCheckerTh : public ModelCheckBaseMT
{
public:
- ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
+ ModelCheckerTh(const NewNet &R,int nbThread);
~ModelCheckerTh();
LDDState * getInitialMetaState();
void buildSucc(LDDState *agregate);
diff --git a/src/main.cpp b/src/main.cpp
index eca2813..f9ba315 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -97,7 +97,6 @@ int main(int argc, char** argv)
if (argc > 6)
strcpy(Int, argv[5]);
- int bound = atoi(argv[argc - 1])==0?32:atoi(argv[argc - 1]);
//if(argc>5)
nb_th = atoi(argv[2])==0 ? 1 : atoi(argv[2]);
@@ -151,9 +150,9 @@ int main(int argc, char** argv)
}
cout<<"Loading net information..."<<endl;
ModelCheckBaseMT* mcl;
- if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(Rnewnet,bound,nb_th);
+ if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(Rnewnet,nb_th);
else
- mcl=new ModelCheckerTh(Rnewnet,bound,nb_th);
+ mcl=new ModelCheckerTh(Rnewnet,nb_th);
mcl->loadNet();
double tps;
@@ -214,7 +213,7 @@ int main(int argc, char** argv)
{
cout<<"number of task = 1 \n " <<endl;
bool uselace=(!strcmp(argv[1],"lc")) || (!strcmp(argv[1],"l"));
- threadSOG DR(Rnewnet, bound,nb_th,uselace);
+ threadSOG DR(Rnewnet,nb_th,uselace);
LDDGraph g(&DR);
if (nb_th==1)
@@ -319,7 +318,7 @@ int main(int argc, char** argv)
if (task_id==0) cout<<"**************Hybrid version**************** \n" <<endl;
if (strcmp(argv[1],"otf"))
{
- HybridSOG DR(Rnewnet, bound);
+ HybridSOG DR(Rnewnet);
LDDGraph g(&DR);
if (task_id==0) cout<<"Building the Distributed SOG by "<<n_tasks<<" processes..."<<endl;
DR.computeDSOG(g);
@@ -339,7 +338,7 @@ int main(int argc, char** argv)
if (task_id!=n_tasks)
{
cout<<"N task :"<<n_tasks<<endl;
- MCHybridSOG DR(Rnewnet,gprocess, bound,false);
+ MCHybridSOG DR(Rnewnet,gprocess,false);
LDDGraph g(&DR);
DR.computeDSOG(g);
}
@@ -379,7 +378,7 @@ int main(int argc, char** argv)
{
cout<<"*************Distibuted version******************* \n" <<endl;
{
- DistributedSOG DR(Rnewnet, bound);
+ DistributedSOG DR(Rnewnet);
LDDGraph g(nullptr);
DR.computeDSOG(g);
}
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 231b1b0..b6cf5bc 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -26,7 +26,7 @@ void write_to_dot(const char *ch,MDD m)
/*************************************************/
-threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool init)
+threadSOG::threadSOG(const NewNet &R, int nbThread,bool uselace,bool init)
{
m_nb_thread=nbThread;
if (uselace) {
diff --git a/src/threadSOG.h b/src/threadSOG.h
index fcce6dc..0beeb10 100644
--- a/src/threadSOG.h
+++ b/src/threadSOG.h
@@ -12,7 +12,7 @@
#include <sys/types.h>
#include <unistd.h>
#include "LDDGraph.h"
-#include "TransSylvan.h"
+#include "TransSylvan.h"
#include "CommonSOG.h"
@@ -23,23 +23,23 @@ extern unsigned int nb_th;
class threadSOG : public CommonSOG{
public:
- threadSOG(const NewNet &, int BOUND = 32, int nbThread=2,bool uselace=false,bool init = false);
+ threadSOG(const NewNet &, int nbThread=2,bool uselace=false,bool init = false);
void buildFromNet(int index);
void computeDSOG(LDDGraph &g,bool canonised);
void computeSeqSOG(LDDGraph &g);
virtual ~threadSOG();
- static void *threadHandler(void *context);
+ static void *threadHandler(void *context);
static void *threadHandlerCanonized(void *context);
- void *doCompute();
- void *doComputeCanonized();
- void computeSOGLace(LDDGraph &g);
- void computeSOGLaceCanonized(LDDGraph &g);
-
-
+ void *doCompute();
+ void *doComputeCanonized();
+ void computeSOGLace(LDDGraph &g);
+ void computeSOGLaceCanonized(LDDGraph &g);
+
+
protected:
- private:
- ////////////////////////////////
+ private:
+ ////////////////////////////////
int minCharge();
--
GitLab