diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4a476dd2cd49c0eb5e8c05334843f7488fda8c6e..d4c956ecdb8c76a308491ad9b6ef439a33e98c89 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -58,6 +58,8 @@ add_executable(hybrid-sog main.cpp
SogKripkeIterator.h
SogKripke.cpp
SogKripke.h
+ ModelCheckBaseMT.cpp
+ ModelCheckBaseMT.h
ModelCheckLace.cpp
ModelCheckLace.h
SogKripkeStateOTF.cpp
diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..1b54f664724b7fbccd4705bda3bf4617054b4edb
--- /dev/null
+++ b/src/ModelCheckBaseMT.cpp
@@ -0,0 +1,27 @@
+#include "ModelCheckBaseMT.h"
+
+#include "sylvan.h"
+#include "sylvan_seq.h"
+#include <sylvan_sog.h>
+#include <sylvan_int.h>
+
+using namespace sylvan;
+ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R, int BOUND,int nbThread)
+{
+ m_nb_thread=nbThread;
+ m_net=R;
+ m_nbPlaces=m_net.places.size();
+}
+void ModelCheckBaseMT::loadNet()
+{
+ preConfigure();
+ m_graph=new LDDGraph(this);
+ m_graph->setTransition(m_transitionName);
+ m_graph->setPlace(m_placeName);
+}
+
+
+
+
+
+
diff --git a/src/ModelCheckBaseMT.h b/src/ModelCheckBaseMT.h
new file mode 100644
index 0000000000000000000000000000000000000000..00d313c616c24e80a58c51cd2e025d68c40aeac8
--- /dev/null
+++ b/src/ModelCheckBaseMT.h
@@ -0,0 +1,16 @@
+#ifndef MODELCHECKBASEMT_H
+#define MODELCHECKBASEMT_H
+#include "CommonSOG.h"
+class ModelCheckBaseMT : public CommonSOG {
+public:
+ ModelCheckBaseMT(const NewNet &R, int BOUND,int nbThread);
+ virtual LDDState * buildInitialMetaState()=0;
+ virtual void buildSucc(LDDState *agregate)=0;
+ void loadNet();
+protected:
+ int m_nb_thread;
+private:
+ virtual void preConfigure()=0;
+
+};
+#endif
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 47c9e0e74c9bdd8a5b963f06825ed48cf98be421..1b98ada04aab3b49c62c38a06e55af7e773735f4 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -6,18 +6,18 @@
#include <sylvan_int.h>
using namespace sylvan;
-ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
+ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread):ModelCheckBaseMT(R,BOUND,nbThread)
{
- m_nb_thread=nbThread;
+}
+void ModelCheckLace::preConfigure() {
+ cout<<__func__<<endl;
lace_init(m_nb_thread, 10000000);
lace_startup(0, NULL, NULL);
sylvan_set_limits(2LL<<30, 16, 3);
sylvan_init_package();
sylvan_init_ldd();
LACE_ME;
- m_net=R;
-
-
+
int i;
vector<Place>::const_iterator it_places;
@@ -26,13 +26,13 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
//_______________
- transitions=R.transitions;
- m_observable=R.Observable;
- m_place_proposition=R.m_formula_place;
- m_nonObservable=R.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=R.transitionName;
- m_placeName=R.m_placePosName;
+ m_transitionName=m_net.transitionName;
+ m_placeName=m_net.m_placePosName;
cout<<"Toutes les Transitions:"<<endl;
map<string,int>::iterator it2=m_transitionName.begin();
@@ -50,18 +50,18 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
cout<<*it<<" ";
}
cout<<endl;
- InterfaceTrans=R.InterfaceTrans;
- m_nbPlaces=R.places.size();
+ InterfaceTrans=m_net.InterfaceTrans;
+
cout<<"Nombre de places : "<<m_nbPlaces<<endl;
- cout<<"Derniere place : "<<R.places[m_nbPlaces-1].name<<endl;
+ cout<<"Derniere place : "<<m_net.places[m_nbPlaces-1].name<<endl;
- uint32_t * liste_marques=new uint32_t[R.places.size()];
- for(i=0,it_places=R.places.begin(); it_places!=R.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,R.places.size());
+ m_initialMarking=lddmc_cube(liste_marques,m_net.places.size());
@@ -70,8 +70,8 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc= new uint32_t [m_nbPlaces];
// Transition relation
- for(vector<Transition>::const_iterator t=R.transitions.begin();
- t!=R.transitions.end(); t++)
+ for(auto t=m_net.transitions.begin();
+ t!=m_net.transitions.end(); t++)
{
// Initialisation
for(i=0; i<m_nbPlaces; i++)
@@ -109,9 +109,6 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
}
delete [] prec;
delete [] postc;
- m_graph=new LDDGraph(this);
- m_graph->setTransition(m_transitionName);
- m_graph->setPlace(m_placeName);
}
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index 75c13d810fe15193efcdcd353f80930be02132d7..3893888eea6fc705fa2b8afe52404a8f7d3c6d87 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -1,13 +1,13 @@
#ifndef MODELCHECKLACE_H
-#define MODELCHECKLACE_H
-#include "CommonSOG.h"
-class ModelCheckLace : public CommonSOG {
-public:
- ModelCheckLace(const NewNet &R, int BOUND,int nbThread);
- LDDState * buildInitialMetaState();
- void buildSucc(LDDState *agregate);
-private:
- int m_nb_thread;
-
-};
-#endif
+#define MODELCHECKLACE_H
+#include "ModelCheckBaseMT.h"
+class ModelCheckLace : public ModelCheckBaseMT {
+public:
+ ModelCheckLace(const NewNet &R, int BOUND,int nbThread);
+ LDDState * buildInitialMetaState();
+ void buildSucc(LDDState *agregate);
+private:
+ void preConfigure();
+
+};
+#endif
diff --git a/src/main.cpp b/src/main.cpp
index 0e11bdfec30d92ab5f82ba0e95580258ed943e51..cc3535a9a9af76b9c0fcd94fd613108ef97ae06e 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -149,7 +149,7 @@ int main(int argc, char** argv)
}
// Initialize SOG builder
ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
- cout<<"Created"<<endl;
+ mcl->loadNet();
auto k =
std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
cout<<"Want to save the graph in a dot file ?";