From f0db5fbf877ac312fb51926fb83aab4321c8830a Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 6 Jun 2019 12:45:04 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/CommonSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/CommonSOG.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:?=
=?UTF-8?q?=20=20=20=20=20=20=20=20=20src/ModelCheckLace.h=20=09nouveau=20?=
=?UTF-8?q?fichier=C2=A0:=20src/ModelCheckerBase.cpp=20=09nouveau=20fichie?=
=?UTF-8?q?r=C2=A0:=20src/ModelCheckerBase.h=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/ModelCheckerTh.cpp=20=09modifi?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/ModelCheckerTh.h?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/CommonSOG.cpp | 10 ++
src/CommonSOG.h | 2 +
src/ModelCheckLace.cpp | 8 --
src/ModelCheckLace.h | 2 -
src/ModelCheckerBase.cpp | 248 +++++++++++++++++++++++++++++++++++++++
src/ModelCheckerBase.h | 24 ++++
src/ModelCheckerTh.cpp | 8 --
src/ModelCheckerTh.h | 2 -
8 files changed, 284 insertions(+), 20 deletions(-)
create mode 100644 src/ModelCheckerBase.cpp
create mode 100644 src/ModelCheckerBase.h
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 410d9d5..a373ab9 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -213,3 +213,13 @@ return ((M&cur)!=lddmc_false);
//BLOCAGE
}
+string CommonSOG::getTransition(int pos)
+{
+ return m_graph->getTransition(pos);
+}
+
+string CommonSOG::getPlace(int pos)
+{
+ return m_graph->getPlace(pos);
+}
+
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 94dedf5..01e4503 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -22,6 +22,8 @@ class CommonSOG
Set * getNonObservable();
unsigned int getPlacesCount();
Set & getPlaceProposition() {return m_place_proposition;}
+ string getTransition(int pos);
+ string getPlace(int pos);
protected:
NewNet m_net;
int m_nbPlaces = 0;
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index dd7e34c..d4a2b98 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -115,15 +115,7 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
}
-string ModelCheckLace::getTransition(int pos)
-{
- return m_graph->getTransition(pos);
-}
-string ModelCheckLace::getPlace(int pos)
-{
- return m_graph->getPlace(pos);
-}
TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation)
{
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index 1dfa14c..4499ba6 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -5,8 +5,6 @@ class ModelCheckLace : public CommonSOG {
public:
ModelCheckLace(const NewNet &R, int BOUND,int nbThread);
LDDState * buildInitialMetaState();
- string getTransition(int pos);
- string getPlace(int pos);
void buildSucc(LDDState *agregate);
private:
int m_nb_thread;
diff --git a/src/ModelCheckerBase.cpp b/src/ModelCheckerBase.cpp
new file mode 100644
index 0000000..2df38ca
--- /dev/null
+++ b/src/ModelCheckerBase.cpp
@@ -0,0 +1,248 @@
+#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
new file mode 100644
index 0000000..16cd29a
--- /dev/null
+++ b/src/ModelCheckerBase.h
@@ -0,0 +1,24 @@
+#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
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 159855c..42e106c 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -105,15 +105,7 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
}
-string ModelCheckerTh::getTransition(int pos)
-{
- return m_graph->getTransition(pos);
-}
-string ModelCheckerTh::getPlace(int pos)
-{
- return m_graph->getPlace(pos);
-}
LDDState * ModelCheckerTh::buildInitialMetaState()
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index b271d6c..d464de0 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -10,8 +10,6 @@ public:
ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
~ModelCheckerTh();
LDDState * buildInitialMetaState();
- string getTransition(int pos);
- string getPlace(int pos);
void buildSucc(LDDState *agregate);
static void *threadHandler(void *context);
void *Compute_successors();
--
GitLab