diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index 3893888eea6fc705fa2b8afe52404a8f7d3c6d87..e85c30a6b4374bd6896ce94c3b82544c4c8308ac 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -7,7 +7,7 @@ public:
LDDState * buildInitialMetaState();
void buildSucc(LDDState *agregate);
private:
- void preConfigure();
+ void preConfigure();
};
#endif
diff --git a/src/ModelChecker.cpp b/src/ModelChecker.cpp
deleted file mode 100644
index 9fca2b52dedbd4beb4d9273a8d639046176f8cde..0000000000000000000000000000000000000000
--- a/src/ModelChecker.cpp
+++ /dev/null
@@ -1,11 +0,0 @@
-#include "ModelChecker.h"
-
-ModelChecker::ModelChecker()
-{
- //ctor
-}
-
-ModelChecker::~ModelChecker()
-{
- //dtor
-}
diff --git a/src/ModelChecker.h b/src/ModelChecker.h
deleted file mode 100644
index 93a6aa4d789e82f670b0e8e4b842d636a9fd5180..0000000000000000000000000000000000000000
--- a/src/ModelChecker.h
+++ /dev/null
@@ -1,16 +0,0 @@
-#ifndef MODELCHECKER_H
-#define MODELCHECKER_H
-
-
-class ModelChecker
-{
- public:
- ModelChecker();
- virtual ~ModelChecker();
-
- protected:
-
- private:
-};
-
-#endif // MODELCHECKER_H
diff --git a/src/ModelCheckerBase.cpp b/src/ModelCheckerBase.cpp
deleted file mode 100644
index 2df38ca5f4a56dab6b4d4d0ccf3eebc5b48544a6..0000000000000000000000000000000000000000
--- a/src/ModelCheckerBase.cpp
+++ /dev/null
@@ -1,248 +0,0 @@
-#include "ModelCheckerBase.h"
-
-#include "sylvan.h"
-#include "sylvan_seq.h"
-#include <sylvan_sog.h>
-#include <sylvan_int.h>
-
-using namespace sylvan;
-
-ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
-{
- m_nb_thread=nbThread;
- lace_init(1, 0);
- 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;
-
-
- init_gc_seq();
-
-
- //_______________
- transitions=R.transitions;
- m_observable=R.Observable;
- m_place_proposition=R.m_formula_place;
- m_nonObservable=R.NonObservable;
-
- m_transitionName=R.transitionName;
- m_placeName=R.m_placePosName;
-
- /* cout<<"Toutes les Transitions:"<<endl;
- map<string,int>::iterator it2=m_transitionName.begin();
- for (; it2!=m_transitionName.end(); it2++)
- {
- cout<<(*it2).first<<" : "<<(*it2).second<<endl;
- }*/
-
-
- InterfaceTrans=R.InterfaceTrans;
- m_nbPlaces=R.places.size();
- cout<<"Nombre de places : "<<m_nbPlaces<<endl;
- cout<<"Derniere place : "<<R.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++)
- {
- liste_marques[i] =it_places->marking;
- }
-
- m_initalMarking=lddmc_cube(liste_marques,R.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=R.transitions.begin();
- t!=R.transitions.end(); t++)
- {
- // Initialisation
- for(i=0; i<m_nbPlaces; i++)
- {
- prec[i]=0;
- postc[i]=0;
- }
- // Calculer les places adjacentes a la transition t
- set<int> adjacentPlace;
- for(vector< pair<int,int> >::const_iterator it=t->pre.begin(); it!=t->pre.end(); it++)
- {
- adjacentPlace.insert(it->first);
- prec[it->first] = prec[it->first] + it->second;
- //printf("It first %d \n",it->first);
- //printf("In prec %d \n",prec[it->first]);
- }
- // arcs post
- for(vector< pair<int,int> >::const_iterator it=t->post.begin(); it!=t->post.end(); it++)
- {
- adjacentPlace.insert(it->first);
- postc[it->first] = postc[it->first] + it->second;
-
- }
- for(set<int>::const_iterator it=adjacentPlace.begin(); it!=adjacentPlace.end(); it++)
- {
- MDD Precond=lddmc_true;
- Precond = Precond & ((*it) >= prec[*it]);
- }
-
- MDD _minus=lddmc_cube(prec,m_nbPlaces);
- ldd_refs_push(_minus);
- MDD _plus=lddmc_cube(postc,m_nbPlaces);
- ldd_refs_push(_plus);
- m_tb_relation.push_back(TransSylvan(_minus,_plus));
- }
- delete [] prec;
- delete [] postc;
- m_graph=new LDDGraph(this);
- m_graph->setTransition(m_transitionName);
- m_graph->setPlace(m_placeName);
-}
-
-
-string ModelCheckerTh::getTransition(int pos)
-{
- return m_graph->getTransition(pos);
-}
-
-string ModelCheckerTh::getPlace(int pos)
-{
- return m_graph->getPlace(pos);
-}
-
-
-LDDState * ModelCheckerTh::buildInitialMetaState()
-{
- ComputeTh_Succ();
- LDDState *c=new LDDState;
- MDD initial_meta_state=Accessible_epsilon(m_initalMarking);
- ldd_refs_push(initial_meta_state);
- c->m_lddstate=initial_meta_state;
- m_graph->setInitialState(c);
- m_graph->insert(c);
- Set fire=firable_obs(initial_meta_state);
- int j=0;
- for(auto it=fire.begin(); it!=fire.end(); it++,j++)
- m_st[j%m_nb_thread].push(couple_th(c,*it));
- pthread_barrier_wait(&m_barrier_threads);
- pthread_barrier_wait(&m_barrier_builder);
- c->setVisited();
- return c;
-}
-
-void ModelCheckerTh::buildSucc(LDDState *agregate)
-{
- if (!agregate->isVisited())
- {
- agregate->setVisited();
- Set fire=firable_obs(agregate->getLDDValue());
- int j=0;
- for(auto it=fire.begin(); it!=fire.end(); it++,j++)
- m_st[j%m_nb_thread].push(couple_th(agregate,*it));
- pthread_barrier_wait(&m_barrier_threads);
- pthread_barrier_wait(&m_barrier_builder);
- //Wait for all threads to finish their work
-
- }
-}
-
-void * ModelCheckerTh::Compute_successors()
-{
- int id_thread;
- int nb_it=0,nb_failed=0,max_succ=0;
- pthread_mutex_lock(&m_mutex);
- id_thread=m_id_thread++;
- pthread_mutex_unlock(&m_mutex);
- LDDState* reached_class=nullptr;
-
- do
- {
- pthread_barrier_wait(&m_barrier_threads);
- while (!m_st[id_thread].empty())
- {
- couple_th elt=m_st[id_thread].top();
- m_st[id_thread].pop();
- LDDState *aggregate=elt.first;
- MDD meta_state=aggregate->getLDDValue();
- int transition=elt.second;
- MDD complete_state=Accessible_epsilon(get_successor(meta_state,transition));
- reached_class=new LDDState;
- reached_class->m_lddstate=complete_state;
- pthread_mutex_lock(&m_graph_mutex);
- LDDState* pos=m_graph->find(reached_class);
- if(!pos)
- {
- m_graph->addArc();
- m_graph->insert(reached_class);
- pthread_mutex_unlock(&m_graph_mutex);
- aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(reached_class,transition));
- reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(aggregate,transition));
- }
- else
- {
- m_graph->addArc();
- pthread_mutex_unlock(&m_graph_mutex);
- aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(pos,transition));
- pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(aggregate,transition));
- delete reached_class;
- }
-
- }
- pthread_barrier_wait(&m_barrier_builder);
- }
- while (!m_finish);
-}
-
-
-
-void * ModelCheckerTh::threadHandler(void *context)
-{
- return ((ModelCheckerTh*)context)->Compute_successors();
-}
-
-void ModelCheckerTh::ComputeTh_Succ()
-{
-
-
- int rc;
-// m_graph=&g;
-// m_graph->setTransition(m_transitionName);
-// m_graph->setPlace(m_placeName);
- m_id_thread=0;
-
- pthread_mutex_init(&m_mutex, NULL);
- //pthread_mutex_init(&m_gc_mutex,NULL);
- pthread_mutex_init(&m_graph_mutex,NULL);
- //pthread_mutex_init(&m_supervise_gc_mutex,NULL);
- pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);
- pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread+1);
-
- for (int i=0; i<m_nb_thread; i++)
- {
- if ((rc = pthread_create(&m_list_thread[i], NULL,threadHandler,this)))
- {
- cout<<"error: pthread_create, rc: "<<rc<<endl;
- }
- }
- /* Compute_successors();
- for (int i = 0; i < m_nb_thread-1; i++)
- {
- pthread_join(m_list_thread[i], NULL);
- }*/
-
-
-}
-ModelCheckerTh::~ModelCheckerTh() {
- m_finish=true;
- pthread_barrier_wait(&m_barrier_threads);
- pthread_barrier_wait(&m_barrier_builder);
- for (int i = 0; i < m_nb_thread-1; i++)
- {
- pthread_join(m_list_thread[i], NULL);
- }
-}
diff --git a/src/ModelCheckerBase.h b/src/ModelCheckerBase.h
deleted file mode 100644
index 16cd29acd59362bf519806dc08a171b474154229..0000000000000000000000000000000000000000
--- a/src/ModelCheckerBase.h
+++ /dev/null
@@ -1,24 +0,0 @@
-#ifndef MODELCHECKERBASE_H
-#define MODELCHECKERBASE_H
-#include "CommonSOG.h"
-typedef pair<LDDState *, int> couple_th;
-typedef stack<pair<LDDState *,int>> pile_t;
-
-class ModelCheckerBase : public CommonSOG
-{
-public:
- virtual ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
- virtual ~ModelCheckerTh();
- LDDState * buildInitialMetaState();
-
- void buildSucc(LDDState *agregate);
-
- void *Compute_successors();
- void ComputeTh_Succ();
-private:
-
- MDD m_initalMarking;
-
-
-};
-#endif