diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 3c5a77cd18cacaaafc41c5963fb336c2a22d4d2f..8284488f3c6fa6acae8a88dafcb14eac78982518 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 d608110c62b977eabb3e65b0572268e89cff5b48..16c4327ee9d1c9a42fe925bf25067c01bee39bd1 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 4da85135feb6a97fc2329a2de3481f2d5004a5a6..4d60c90e8a4097760e4f4592b85dc30556f5720f 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 f480981e0704aaae9f072d1c5f75b505c63b322b..dab4baa61bd1a1b573d26a5f233cb9e136a3e087 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 c0d31b827933bc243cb8b51b62685e4a1d8edd7a..e793f5d272af8205cb352736132099a4056410a5 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 ae70af3e2739e1c8cc3eab2162447802c1a0fb10..f41218b0938aa3366e9bdf46efb07998b6ff56bd 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 4e8df685fe1b365ccd5d90965a331e3c2964e8fa..c9e7a49097597a6b5133a92ae1feca603f95ec93 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 0215fc2fa62f72e0a40f867ba9fb1347f7f1acd4..d6dbd4cc30231fc7a25a5f9d7fac1cd90fe07c57 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 740269a8874e69f96aaf8ace39cb722bdbb18e81..01b157e0be74b2cd9503a18b8a3737e6c2307373 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 bd2e6f8c7ad2093d7ca9264373ec34aa02a871c2..1b540b48da9477cbf35446669b70968a762e36a9 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 9a4af0322b55ab5c52e230d402d9986918ad6d8d..ab91b126a58946c699a82ce407673e3e78f6f39d 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 f03025cbf4ea3467bd51b3f1bca45946a5dbc066..c274d1968ed9354223096432968443bbcfcb6e7a 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 eca281346f06e7a281f69f555b46f53ee8660f65..f9ba315052c66c34275c51316ded5929ee6477e9 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 231b1b0fe1aa987f94c168a1a1d97137d2a2ef8b..b6cf5bc8287217c8557d1a9427d21709f28e92a4 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 fcce6dcd29cabc0a48bcfb2991ceae19758740ae..0beeb1036150d318f1ac0249a5eb82bffb47f3a2 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();