From d462294be83a9ab781013e970a7ff77f83ac61c5 Mon Sep 17 00:00:00 2001
From: ouni <ouni@lipn.univ-paris13.fr>
Date: Thu, 25 Apr 2019 14:57:21 +0200
Subject: [PATCH] src
---
.gitmodules.save | 4 +
src/CommonSOG.cpp | 174 ++++++++++++++++++
src/CommonSOG.h | 42 +++++
src/DistributedSOG.cpp | 200 +++------------------
src/DistributedSOG.h | 42 ++---
src/HybridSOG.cpp | 173 +-----------------
src/HybridSOG.h | 205 ++++++++++-----------
src/LDDGraph.cpp | 31 ----
src/SpotSogIterator.cpp | 4 +-
src/SpotSogIterator.h | 4 +-
src/main.cpp | 121 ++++++++++---
src/threadSOG.cpp | 390 ++++------------------------------------
src/threadSOG.h | 52 ++----
13 files changed, 497 insertions(+), 945 deletions(-)
create mode 100644 .gitmodules.save
create mode 100644 src/CommonSOG.cpp
create mode 100644 src/CommonSOG.h
diff --git a/.gitmodules.save b/.gitmodules.save
new file mode 100644
index 0000000..10d37a8
--- /dev/null
+++ b/.gitmodules.save
@@ -0,0 +1,4 @@
+[submodule "libraries/parser"]
+ path = libraries/parser
+ url = https://depot.lipn.univ-paris13.fr/PMC-SOG/pn-parser/tree/mc-sog-parser
+URL non trouvée pour le chemin de sous-mod
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
new file mode 100644
index 0000000..ead7db6
--- /dev/null
+++ b/src/CommonSOG.cpp
@@ -0,0 +1,174 @@
+#include "CommonSOG.h"
+#include "sylvan_seq.h"
+
+const vector<class Place> *_places = NULL;
+CommonSOG::CommonSOG()
+{
+ //ctor
+}
+
+CommonSOG::~CommonSOG()
+{
+ //dtor
+}
+
+LDDGraph *CommonSOG::getGraph() const {
+ return m_graph;
+}
+
+MDD CommonSOG::Accessible_epsilon(MDD From)
+{
+ MDD M1;
+ MDD M2=From;
+
+ do
+ {
+ M1=M2;
+ for(Set::const_iterator i=m_nonObservable.begin(); !(i==m_nonObservable.end()); i++)
+ {
+
+ MDD succ= lddmc_firing_mono(M2,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
+ M2=lddmc_union_mono(M2,succ);
+ //M2=succ|M2;
+ }
+
+ }
+ while(M1!=M2);
+ return M2;
+}
+// Return the set of firable observable transitions from an agregate
+Set CommonSOG::firable_obs(MDD State)
+{
+ Set res;
+ for(Set::const_iterator i=m_observable.begin(); !(i==m_observable.end()); i++)
+ {
+ //cout<<"firable..."<<endl;
+ MDD succ = lddmc_firing_mono(State,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
+ if(succ!=lddmc_false)
+ {
+ res.insert(*i);
+ }
+
+ }
+ return res;
+}
+
+MDD CommonSOG::get_successor(MDD From,int t)
+{
+ return lddmc_firing_mono(From,m_tb_relation[(t)].getMinus(),m_tb_relation[(t)].getPlus());
+}
+
+
+MDD CommonSOG::ImageForward(MDD From)
+{
+ MDD Res=lddmc_false;
+ for(Set::const_iterator i=m_nonObservable.begin(); !(i==m_nonObservable.end()); i++)
+ {
+ MDD succ= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
+ Res=lddmc_union_mono(Res,succ);
+ }
+ return Res;
+}
+
+
+/*----------------------------------------------CanonizeR()------------------------------------*/
+MDD CommonSOG::Canonize(MDD s,unsigned int level)
+{
+ if (level>m_nbPlaces || s==lddmc_false) return lddmc_false;
+ if(isSingleMDD(s)) return s;
+ MDD s0=lddmc_false,s1=lddmc_false;
+
+ bool res=false;
+ do
+ {
+ if (get_mddnbr(s,level)>1)
+ {
+ s0=ldd_divide_rec(s,level);
+ s1=ldd_minus(s,s0);
+ res=true;
+ }
+ else
+ level++;
+ }
+ while(level<m_nbPlaces && !res);
+
+
+ if (s0==lddmc_false && s1==lddmc_false)
+ return lddmc_false;
+ // if (level==nbPlaces) return lddmc_false;
+ MDD Front,Reach;
+ if (s0!=lddmc_false && s1!=lddmc_false)
+ {
+ Front=s1;
+ Reach=s1;
+ do
+ {
+ // cout<<"premiere boucle interne \n";
+ Front=ldd_minus(ImageForward(Front),Reach);
+ Reach = lddmc_union_mono(Reach,Front);
+ s0 = ldd_minus(s0,Front);
+ }
+ while((Front!=lddmc_false)&&(s0!=lddmc_false));
+ }
+ if((s0!=lddmc_false)&&(s1!=lddmc_false))
+ {
+ Front=s0;
+ Reach = s0;
+ do
+ {
+ // cout<<"deuxieme boucle interne \n";
+ Front=ldd_minus(ImageForward(Front),Reach);
+ Reach = lddmc_union_mono(Reach,Front);
+ s1 = ldd_minus(s1,Front);
+ }
+ while( Front!=lddmc_false && s1!=lddmc_false );
+ }
+
+
+
+ MDD Repr=lddmc_false;
+
+ if (isSingleMDD(s0))
+ {
+ Repr=s0;
+ }
+ else
+ {
+
+ Repr=Canonize(s0,level);
+
+ }
+
+ if (isSingleMDD(s1))
+ Repr=lddmc_union_mono(Repr,s1);
+ else
+ Repr=lddmc_union_mono(Repr,Canonize(s1,level));
+
+
+ return Repr;
+
+
+}
+
+void CommonSOG::printhandler(ostream &o, int var)
+{
+ o << (*_places)[var/2].name;
+ if (var%2)
+ o << "_p";
+}
+
+
+vector<TransSylvan>* CommonSOG::getTBRelation() {
+ return &m_tb_relation;
+}
+
+Set * CommonSOG::getNonObservable() {
+ return &m_nonObservable;
+}
+
+
+/*********Returns the count of places******************************************/
+unsigned int CommonSOG::getPlacesCount() {
+ return m_nbPlaces;
+}
+
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
new file mode 100644
index 0000000..2132dca
--- /dev/null
+++ b/src/CommonSOG.h
@@ -0,0 +1,42 @@
+#ifndef COMMONSOG_H
+#define COMMONSOG_H
+#include "LDDGraph.h"
+#include "TransSylvan.h"
+#include "Net.hpp"
+#include <stack>
+
+typedef pair<LDDState *, MDD> couple;
+typedef pair<couple, Set> Pair;
+typedef stack<Pair> pile;
+class CommonSOG
+{
+ public:
+ CommonSOG();
+ virtual ~CommonSOG();
+ LDDGraph *getGraph() const;
+ static void printhandler(ostream &o, int var);
+ vector<TransSylvan>* getTBRelation();
+ Set * getNonObservable();
+ unsigned int getPlacesCount();
+ protected:
+ net m_net;
+ int m_nbPlaces = 0;
+ LDDGraph *m_graph;
+ vector<TransSylvan> m_tb_relation;
+ LDDState m_M0;
+ map<string, int> m_transitionName;
+ Set m_observable;
+ Set m_nonObservable;
+ Set InterfaceTrans;
+ Set Formula_Trans;
+ vector<class Transition> transitions;
+
+ MDD Accessible_epsilon(MDD From);
+ Set firable_obs(MDD State);
+ MDD get_successor(MDD From, int t);
+ MDD ImageForward(MDD From);
+ MDD Canonize(MDD s, unsigned int level);
+ private:
+};
+
+#endif // COMMONSOG_H
diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 8c8ba94..627a474 100644
--- a/src/DistributedSOG.cpp
+++ b/src/DistributedSOG.cpp
@@ -25,12 +25,6 @@ using namespace sylvan;
/**************************************************/
-
-
-
-const vector<class Place> *__vplaces = NULL;
-
-
DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
{
@@ -47,20 +41,20 @@ DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
m_net=R;
m_init=init;
- nbPlaces=R.places.size();
+
int i, domain;
vector<Place>::const_iterator it_places;
//_______________
transitions=R.transitions;
- Observable=R.Observable;
- NonObservable=R.NonObservable;
+ m_observable=R.Observable;
+ m_nonObservable=R.NonObservable;
Formula_Trans=R.Formula_Trans;
- transitionName=R.transitionName;
+ m_transitionName=R.transitionName;
InterfaceTrans=R.InterfaceTrans;
- Nb_places=R.places.size();
- cout<<"Nombre de places : "<<Nb_places<<endl;
- cout<<"Derniere place : "<<R.places[Nb_places-1].name<<endl;
+ m_nbPlaces=R.places.size();
+ cout<<"Nombre de places : "<<m_nbPlaces<<endl;
+ cout<<"Derniere place : "<<R.places[m_nbPlaces-1].name<<endl;
// place domain, place bvect, place initial marking and place name
@@ -72,17 +66,17 @@ DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
M0=lddmc_cube(liste_marques,R.places.size());
delete []liste_marques;
// place names
- __vplaces = &R.places;
+// __vplaces = &R.places;
- uint32_t *prec = new uint32_t[nbPlaces];
- uint32_t *postc= new uint32_t [nbPlaces];
+ 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<nbPlaces; i++)
+ for(i=0; i<m_nbPlaces; i++)
{
prec[i]=0;
postc[i]=0;
@@ -103,8 +97,8 @@ DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
postc[it->first] = postc[it->first] + it->second;
}
- MDD _minus=lddmc_cube(prec,nbPlaces);
- MDD _plus=lddmc_cube(postc,nbPlaces);
+ MDD _minus=lddmc_cube(prec,m_nbPlaces);
+ MDD _plus=lddmc_cube(postc,m_nbPlaces);
m_tb_relation.push_back(TransSylvan(_minus,_plus));
}
delete [] prec;
@@ -158,7 +152,8 @@ void *DistributedSOG::doCompute()
{
m_nbmetastate++;
//m_old_size=lddmc_nodecount(c->m_lddstate);
- fire=firable_obs(Complete_meta_state);
+
+ Set fire=firable_obs(Complete_meta_state);
m_st.push(Pair(couple(c,Complete_meta_state),fire));
m_graph->setInitialState(c);
m_graph->insert(c);
@@ -204,7 +199,7 @@ void *DistributedSOG::doCompute()
reached_class=new LDDState;
// lddmc_fprintdot(fp,Complete_meta_state);
- MDD marking=get_successorMDD(e.first.second,t);
+ MDD marking=get_successor(e.first.second,t);
MDD lddmarq=Accessible_epsilon(marking);
reached_class->m_lddstate=lddmarq;
lddmc_getsha(lddmarq, msg);
@@ -229,7 +224,7 @@ void *DistributedSOG::doCompute()
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(e.first.first,t));
m_nbmetastate++;
- fire=firable_obs(lddmarq);
+ Set fire=firable_obs(lddmarq);
m_st.push(Pair(couple(reached_class,lddmarq),fire));
nb_success++;
@@ -458,7 +453,7 @@ void DistributedSOG::read_state_message()
if (!m_graph->find(Agregate))
{
m_graph->insert(Agregate);
- fire=firable_obs(MState);
+ Set fire=firable_obs(MState);
m_nbmetastate++;
m_old_size=lddmc_nodecount(Agregate->m_lddstate);
m_st.push(Pair(couple(Agregate,MState),fire));
@@ -551,70 +546,8 @@ void DistributedSOG::computeDSOG(LDDGraph &g)
-void DistributedSOG::printhandler(ostream &o, int var)
-{
- o << (*__vplaces)[var/2].name;
- if (var%2)
- o << "_p";
-}
-
-
-//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////////////////////////////// /////////////////////////////////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-Set DistributedSOG::firable_obs(MDD State)
-{
- Set res;
- for(Set::const_iterator i=Observable.begin(); !(i==Observable.end()); i++)
- {
-
- //cout<<"firable..."<<endl;
- MDD succ = lddmc_firing_mono(State,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- if(succ!=lddmc_false)
- {
- //cout<<"firable..."<<endl;
- res.insert(*i);
- }
-
- }
- return res;
-}
-
-MDD DistributedSOG::get_successorMDD(MDD From,int t)
-{
-
- MDD res=lddmc_firing_mono(From,m_tb_relation[(t)].getMinus(),m_tb_relation[(t)].getPlus());
- return res;
-}
-
-
-MDD DistributedSOG::Accessible_epsilon(MDD From)
-{
- MDD M1;
- MDD M2=From;
- int it=0;
- do
- {
- M1=M2;
- for(Set::const_iterator i=NonObservable.begin(); !(i==NonObservable.end()); i++)
- {
-
- MDD succ= lddmc_firing_mono(M2,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- M2=lddmc_union_mono(M2,succ);
- //M2=succ|M2;
- }
- //TabMeta[nbmetastate]=M2;
- //int intsize=sylvan_anodecount(TabMeta,nbmetastate+1);
- //if(m_MaxIntBdd<intsize)
- // m_MaxIntBdd=intsize;
- it++;
- // cout << bdd_nodecount(M2) << endl;
- }
- while(M1!=M2);
- return M2;
-}
-
string to_hex(unsigned char s)
{
@@ -708,15 +641,15 @@ MDD DistributedSOG::decodage_message(char *chaine)
nb_marq=(nb_marq<<8) | (unsigned char)chaine[0];
unsigned int index=2;
- uint32_t list_marq[nbPlaces];
+ uint32_t list_marq[m_nbPlaces];
for (unsigned int i=0; i<nb_marq; i++)
{
- for (unsigned int j=0; j<nbPlaces; j++)
+ for (unsigned int j=0; j<m_nbPlaces; j++)
{
list_marq[j]=chaine[index];
index++;
}
- MDD N=lddmc_cube(list_marq,nbPlaces);
+ MDD N=lddmc_cube(list_marq,m_nbPlaces);
M=lddmc_union_mono(M,N);
}
return M;
@@ -730,7 +663,7 @@ void DistributedSOG::MarquageString(char *dest,const char *source)
int index=1;
for (int nb=0; nb<length; nb++)
{
- for (int i=0; i<nbPlaces; i++)
+ for (int i=0; i<m_nbPlaces; i++)
{
dest[index]=(unsigned char)source[index]+(unsigned char)'0';
printf("%d",source[index]);
@@ -742,95 +675,6 @@ void DistributedSOG::MarquageString(char *dest,const char *source)
}
/******************************************************************************/
-MDD DistributedSOG::ImageForward(MDD From)
-{
- MDD Res=lddmc_false;
- for(Set::const_iterator i=NonObservable.begin(); !(i==NonObservable.end()); i++)
- {
- MDD succ= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- Res=lddmc_union_mono(Res,succ);
- }
- return Res;
-}
-
-
-/*----------------------------------------------CanonizeR()------------------------------------*/
-MDD DistributedSOG::Canonize(MDD s,unsigned int level)
-{
- if (level>nbPlaces || s==lddmc_false) return lddmc_false;
- if(isSingleMDD(s)) return s;
- MDD s0=lddmc_false,s1=lddmc_false;
- bool res=false;
- do
- {
- if (get_mddnbr(s,level)>1)
- {
- s0=ldd_divide_rec(s,level);
- s1=ldd_minus(s,s0);
- res=true;
- }
- else
- level++;
- }
- while(level<nbPlaces && !res);
-
-
- if (s0==lddmc_false && s1==lddmc_false)
- return lddmc_false;
- // if (level==nbPlaces) return lddmc_false;
- MDD Front,Reach;
- if (s0!=lddmc_false && s1!=lddmc_false)
- {
- Front=s1;
- Reach=s1;
- do
- {
- // cout<<"premiere boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s0 = ldd_minus(s0,Front);
- }
- while((Front!=lddmc_false)&&(s0!=lddmc_false));
- }
- if((s0!=lddmc_false)&&(s1!=lddmc_false))
- {
- Front=s0;
- Reach = s0;
- do
- {
- // cout<<"deuxieme boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s1 = ldd_minus(s1,Front);
- }
- while( Front!=lddmc_false && s1!=lddmc_false );
- }
-
-
-
- MDD Repr=lddmc_false;
-
- if (isSingleMDD(s0))
- {
- Repr=s0;
- }
- else
- {
-
- Repr=Canonize(s0,level);
-
- }
-
- if (isSingleMDD(s1))
- Repr=lddmc_union_mono(Repr,s1);
- else
- Repr=lddmc_union_mono(Repr,Canonize(s1,level));
-
-
- return Repr;
-
-
-}
diff --git a/src/DistributedSOG.h b/src/DistributedSOG.h
index 41cd1c6..f10880f 100644
--- a/src/DistributedSOG.h
+++ b/src/DistributedSOG.h
@@ -28,11 +28,12 @@
//#include <boost/serialization/string.hpp>
//#include <boost/mpi.hpp>
#include <iostream>
-#include <queue>
+
#include <string>
//#include <boost/serialization/string.hpp>
#include <time.h>
#include <chrono>
+#include "CommonSOG.h"
// namespace mpi = boost::mpi;
#define MASTER 0
@@ -40,12 +41,10 @@
extern int n_tasks, task_id;
-typedef pair<LDDState *, MDD> couple;
-typedef pair<couple, Set> Pair;
-typedef stack<Pair> pile;
+
// typedef vector<Trans> vec_trans;
-class DistributedSOG {
+class DistributedSOG : public CommonSOG{
public:
DistributedSOG(const net &, int BOUND = 32, bool init = false);
void buildFromNet(int index);
@@ -53,7 +52,6 @@ class DistributedSOG {
void BuildInitialState(LDDState *m_state, MDD mdd);
void computeSeqSOG(LDDGraph &g);
virtual ~DistributedSOG();
- static void printhandler(ostream &o, int var);
static void *threadHandler(void *context);
void *doCompute();
void NonEmpty();
@@ -61,11 +59,8 @@ class DistributedSOG {
protected:
private:
- LDDGraph *m_graph;
- MDD LDDAccessible_epsilon(MDD *m);
- MDD Accessible_epsilon(MDD From);
- Set firable_obs(MDD State);
- MDD get_successorMDD(MDD From, int t);
+
+
int minCharge();
bool isNotTerminated();
int Terminate();
@@ -73,22 +68,11 @@ class DistributedSOG {
char *concat_string(const char *s1, int longueur1, const char *s2,
int longueur2, char *dest);
void sha256(LDDState *state, char output[65]);
- //-----Original defined as members
- vector<class Transition> transitions;
- Set Observable;
- Set NonObservable;
- map<string, int> transitionName;
- Set InterfaceTrans;
- Set Formula_Trans;
- unsigned int Nb_places;
+
MDD M0;
- LDDState m_M0;
+
MDD currentvar;
- // vector<TransSylvan> m_relation;
- // vec_trans m_tb_relation[16];
- //-----------------
- vector<TransSylvan> m_tb_relation;
int m_NbIt;
int m_itext, m_itint;
int m_MaxIntBdd;
@@ -109,27 +93,21 @@ class DistributedSOG {
MPI_Request m_request;
- net m_net;
- int m_bound, m_init;
+
+ int m_init;
int tempCanoniz = 0;
int tempS = 0;
int tempR = 0;
long m_sizeMsg = 0;
long m_sizeMsgCanoniz = 0;
- std::queue<char *> m_queue; // empty queue
- int nbPlaces;
void convert_wholemdd_string(MDD cmark, char **result, unsigned int &length);
MDD decodage_message(char *chaine);
void read_state_message();
int nbsend = 0, nbrecv = 0;
int total_nb_send = 0, total_nb_recv = 0;
- Set fire;
- MDD Canonize(MDD s, unsigned int level);
- MDD ImageForward(MDD From);
- // named_mutex m_initial_mtx{open_or_create, "initial"};
};
#endif // DISTRIBUTEDSOG_H
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index 02c7b65..31c6c0f 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -35,7 +35,7 @@ using namespace sylvan;
-const vector<class Place> *_vplaces = NULL;
+
/*void my_error_handler_dist(int errcode) {
cout<<"errcode = "<<errcode<<endl;
@@ -74,10 +74,10 @@ HybridSOG::HybridSOG(const net &R, int BOUND,bool init)
init_gc_seq();
//_______________
transitions=R.transitions;
- Observable=R.Observable;
- NonObservable=R.NonObservable;
+ m_observable=R.Observable;
+ m_nonObservable=R.NonObservable;
Formula_Trans=R.Formula_Trans;
- transitionName=R.transitionName;
+ m_transitionName=R.transitionName;
InterfaceTrans=R.InterfaceTrans;
m_nbPlaces=R.places.size();
@@ -95,7 +95,7 @@ HybridSOG::HybridSOG(const net &R, int BOUND,bool init)
delete []liste_marques;
// place names
- _vplaces = &R.places;
+
uint32_t *prec = new uint32_t[m_nbPlaces];
@@ -829,15 +829,6 @@ void HybridSOG::computeDSOG(LDDGraph &g)
}
-
-void HybridSOG::printhandler(ostream &o, int var)
-{
- o << (*_vplaces)[var/2].name;
- if (var%2)
- o << "_p";
-}
-
-
int HybridSOG::minCharge()
{
int pos=1;
@@ -854,65 +845,6 @@ int HybridSOG::minCharge()
}
-
-//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////////////////////////////// /////////////////////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-
-Set HybridSOG::firable_obs(MDD State)
-{
- Set res;
- for(Set::const_iterator i=Observable.begin(); !(i==Observable.end()); i++)
- {
-
- //cout<<"firable..."<<endl;
- MDD succ = lddmc_firing_mono(State,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- if(succ!=lddmc_false)
- {
- res.insert(*i);
- }
- }
- return res;
-}
-
-
-
-
-MDD HybridSOG::get_successor(MDD From,int t)
-{
- return lddmc_firing_mono(From,m_tb_relation[t].getMinus(),m_tb_relation[t].getPlus());
-}
-
-
-MDD HybridSOG::Accessible_epsilon(MDD From)
-{
- MDD M1;
- MDD M2=From;
- do
- {
- M1=M2;
- for(Set::const_iterator i=NonObservable.begin(); !(i==NonObservable.end()); i++)
- {
-
- MDD succ= lddmc_firing_mono(M2,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- M2=lddmc_union_mono(succ,M2);
- //M2=succ|M2;
- }
- // cout << bdd_nodecount(M2) << endl;
- }
- while(M1!=M2);
- return M2;
-}
-
-
-/*string to_hex(unsigned char s)
-{
- stringstream ss;
- ss << hex << (int) s;
- return ss.str();
-} */
-
-
void HybridSOG::strcpySHA(unsigned char *dest,const unsigned char *source)
{
for (int i=0; i<LENGTH_ID; i++)
@@ -979,109 +911,14 @@ MDD HybridSOG::decodage_message(const char *chaine)
-/******************************************************************************/
-MDD HybridSOG::ImageForward(MDD From)
-{
- MDD Res=lddmc_false;
- for(Set::const_iterator i=NonObservable.begin(); !(i==NonObservable.end()); i++)
- {
- MDD succ= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- Res=lddmc_union_mono(Res,succ);
- }
- return Res;
-}
-
-/*----------------------------------------------CanonizeR()------------------------------------*/
-MDD HybridSOG::Canonize(MDD s,unsigned int level)
-{
- if (level>m_nbPlaces || s==lddmc_false) return lddmc_false;
- if(isSingleMDD(s)) return s;
- MDD s0=lddmc_false,s1=lddmc_false;
-
- bool res=false;
- do
- {
- if (get_mddnbr(s,level)>1)
- {
- s0=ldd_divide_rec(s,level);
- s1=ldd_minus(s,s0);
- res=true;
- }
- else
- level++;
- }
- while(level<m_nbPlaces && !res);
-
-
- if (s0==lddmc_false && s1==lddmc_false)
- return lddmc_false;
- // if (level==nbPlaces) return lddmc_false;
- MDD Front,Reach;
- if (s0!=lddmc_false && s1!=lddmc_false)
- {
- Front=s1;
- Reach=s1;
- do
- {
- // cout<<"premiere boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s0 = ldd_minus(s0,Front);
- }
- while((Front!=lddmc_false)&&(s0!=lddmc_false));
- }
- if((s0!=lddmc_false)&&(s1!=lddmc_false))
- {
- Front=s0;
- Reach = s0;
- do
- {
- // cout<<"deuxieme boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s1 = ldd_minus(s1,Front);
- }
- while( Front!=lddmc_false && s1!=lddmc_false );
- }
-
-
- MDD Repr=lddmc_false;
-
- if (isSingleMDD(s0))
- {
- Repr=s0;
- }
- else
- {
-
- Repr=Canonize(s0,level);
-
- }
-
- if (isSingleMDD(s1))
- Repr=lddmc_union_mono(Repr,s1);
- else
- Repr=lddmc_union_mono(Repr,Canonize(s1,level));
-
-
- return Repr;
-
-
-}
void * HybridSOG::threadHandler(void *context)
{
return ((HybridSOG*)context)->doCompute();
}
-
-void printchaine(string *s) {
- for (int i=0;i<s->size();i++)
- printf("%d",(s->at(i)-1));
-}
-
void HybridSOG::convert_wholemdd_stringcpp(MDD cmark,string &res)
{
typedef pair<string,MDD> Pair_stack;
diff --git a/src/HybridSOG.h b/src/HybridSOG.h
index 8011e98..6511d11 100644
--- a/src/HybridSOG.h
+++ b/src/HybridSOG.h
@@ -29,6 +29,7 @@
//#include <boost/serialization/string.hpp>
#include <time.h>
#include <chrono>
+#include "CommonSOG.h"
// namespace mpi = boost::mpi;
//#define MASTER 0
@@ -36,125 +37,103 @@
extern unsigned int nb_th;
extern int n_tasks, task_id;
-typedef pair<LDDState *, MDD> couple;
-typedef pair<couple, Set> Pair;
-typedef stack<Pair> pile;
+
typedef pair<string *, unsigned int> MSG;
typedef stack<MSG> pile_msg;
// typedef vector<Trans> vec_trans;
-class HybridSOG {
- public:
- HybridSOG(const net &, int BOUND = 32, bool init = false);
- void buildFromNet(int index);
- /// principal functions to construct the SOG
- void computeDSOG(LDDGraph &g);
- virtual ~HybridSOG();
- static void printhandler(ostream &o, int var);
- static void *threadHandler(void *context);
- void *doCompute();
-
- protected:
- private:
- /// \ hash function
- void get_md5(const string &chaine, unsigned char *md_chaine);
- /// Termination Detection functions
- inline void ReceiveTermSignal();
- inline void TermSendMsg();
- inline void startTermDetectionByMaster();
- inline void TermReceivedMsg();
- LDDGraph *m_graph;
- /// saturation
- inline MDD Accessible_epsilon(MDD From);
- inline MDD ImageForward(MDD From);
- /// Observable Transition
- Set firable_obs(MDD State);
- ///
- MDD get_successor(MDD From, int t);
-
- /// minimum charge function for the load balancing between thread
- inline int minCharge();
- inline bool isNotTerminated();
- /// Copie string of caracter
- void strcpySHA(unsigned char *dest, const unsigned char *source);
-
- vector<class Transition> transitions;
- Set Observable;
- Set NonObservable;
- map<string, int> transitionName;
- Set InterfaceTrans;
- Set Formula_Trans;
- unsigned int m_nbPlaces;
- MDD M0;
- LDDState m_M0;
-
- //-----------------
- vector<TransSylvan> m_tb_relation;
- int m_NbIt;
- int m_itext, m_itint;
- int m_MaxIntBdd;
-
- int m_nbmetastate;
-
- pile m_st[128];
- pile_msg m_msg[128];
-
- // void DisplayMessage(const char *chaine);
-
- // int n_tasks, task_id;
-
- int m_charge[128];
-
- net m_net;
- int m_bound, m_init;
-
- /// Convert an MDD to a string caracter (for the send)
- void convert_wholemdd_stringcpp(MDD cmark, string &chaine);
- /// Convert a string caracter to an MDD
- MDD decodage_message(const char *chaine);
- /// there is a message to receive?
- void read_message();
- /// receive termination message
- void read_termination();
- void AbortTerm();
- /// receive state message
- void read_state_message();
- /// send state message
- void send_state_message();
- /// canonicalization of an aggregate represented by an MDD
- MDD Canonize(MDD s, unsigned int level);
-
- int m_nb_thread;
- pthread_t m_list_thread[128];
-
- int m_id_thread;
- /// Mutex declaration
- pthread_mutex_t m_mutex;
- pthread_mutex_t m_graph_mutex;
- pthread_mutex_t m_gc_mutex;
- pthread_mutex_t m_supervise_gc_mutex;
- unsigned int m_gc;
-
- pthread_mutex_t m_mutex_stack[128];
- pthread_mutex_t m_spin_stack[128];
- pthread_mutex_t m_spin_msg[128];
- // pthread_mutex_t m_spin_charge;
- pthread_spinlock_t m_spin_md5;
- pthread_mutex_t m_spin_working;
- unsigned int m_working = 0;
-
- // unsigned int m_count_thread_working;
- bool m_Terminated = false;
- unsigned long m_size_mess = 0;
- int m_nbsend = 0, m_nbrecv = 0;
- int m_total_nb_send = 0, m_total_nb_recv = 0;
-
- MPI_Status m_status;
- bool m_Terminating = false;
-
- // named_mutex m_initial_mtx{open_or_create, "initial"};
+class HybridSOG : public CommonSOG
+{
+public:
+ HybridSOG(const net &, int BOUND = 32, bool init = false);
+ void buildFromNet(int index);
+ /// principal functions to construct the SOG
+ void computeDSOG(LDDGraph &g);
+ virtual ~HybridSOG();
+ static void *threadHandler(void *context);
+ void *doCompute();
+
+protected:
+private:
+ /// \ hash function
+ void get_md5(const string &chaine, unsigned char *md_chaine);
+ /// Termination Detection functions
+ inline void ReceiveTermSignal();
+ inline void TermSendMsg();
+ inline void startTermDetectionByMaster();
+ inline void TermReceivedMsg();
+
+
+
+ /// minimum charge function for the load balancing between thread
+ inline int minCharge();
+ inline bool isNotTerminated();
+ /// Copie string of caracter
+ void strcpySHA(unsigned char *dest, const unsigned char *source);
+
+ MDD M0;
+
+ int m_NbIt;
+ int m_itext, m_itint;
+ int m_MaxIntBdd;
+
+ int m_nbmetastate;
+
+ pile m_st[128];
+ pile_msg m_msg[128];
+
+ // void DisplayMessage(const char *chaine);
+
+ // int n_tasks, task_id;
+
+ int m_charge[128];
+ int m_init;
+
+ /// Convert an MDD to a string caracter (for the send)
+ void convert_wholemdd_stringcpp(MDD cmark, string &chaine);
+ /// Convert a string caracter to an MDD
+ MDD decodage_message(const char *chaine);
+ /// there is a message to receive?
+ void read_message();
+ /// receive termination message
+ void read_termination();
+ void AbortTerm();
+ /// receive state message
+ void read_state_message();
+ /// send state message
+ void send_state_message();
+
+
+ int m_nb_thread;
+ pthread_t m_list_thread[128];
+
+ int m_id_thread;
+ /// Mutex declaration
+ pthread_mutex_t m_mutex;
+ pthread_mutex_t m_graph_mutex;
+ pthread_mutex_t m_gc_mutex;
+ pthread_mutex_t m_supervise_gc_mutex;
+ unsigned int m_gc;
+
+ pthread_mutex_t m_mutex_stack[128];
+ pthread_mutex_t m_spin_stack[128];
+ pthread_mutex_t m_spin_msg[128];
+ // pthread_mutex_t m_spin_charge;
+ pthread_spinlock_t m_spin_md5;
+ pthread_mutex_t m_spin_working;
+ unsigned int m_working = 0;
+
+ // unsigned int m_count_thread_working;
+ bool m_Terminated = false;
+ unsigned long m_size_mess = 0;
+ int m_nbsend = 0, m_nbrecv = 0;
+ int m_total_nb_send = 0, m_total_nb_recv = 0;
+
+ MPI_Status m_status;
+ bool m_Terminating = false;
+
};
#endif // HybridSOG_H
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index c5e2ba0..13a89d3 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -123,13 +123,10 @@ void LDDGraph::printCompleteInformation()
size_t n=1;
printGraph(m_initialstate,n);
}
-
-
}
/*----------------------InitVisit()------------------------*/
void LDDGraph::InitVisit(LDDState * S,size_t nb)
{
-
if(nb<=m_nbStates)
{
S->m_visited=false;
@@ -176,34 +173,11 @@ void LDDGraph::printGraph(LDDState *s,size_t &nb)
/*---------void print_successors_class(Class_Of_State *)------------*/
void LDDGraph::printsuccessors(LDDState *s)
{
- /*Edges::const_iterator i;
- cout<<bddtable<<s->class_state<<endl;
- if(s->boucle)
- cout<<"\n\tON BOUCLE DESSUS AVEC EPSILON\n";
- if(s->blocage)
- cout<<"\n\tEXISTENCE D'UN ETAT BLOCANT\n";
- cout<<"\n\tSES SUCCESSEURS SONT ( "<<s->Successors.size()<<" ) :\n\n";
- getchar();
- for(i =s->Successors.begin();!(i==s->Successors.end());i++)
- {
- cout<<" \t- t"<<(*i).second<<" ->";
- cout<<bddtable<<(*i).first->class_state<<endl;
- getchar();
- }*/
cout<<"Not implemented yet!"<<endl;
}
/*---------void printpredescessors(Class_Of_State *)------------*/
void LDDGraph::printpredecessors(LDDState *s)
{
- /*Edges::const_iterator i;
- cout<<"\n\tSES PREDESCESSEURS SONT ( "<<s->Predecessors.size()<<" ) :\n\n";
- getchar();
- for(i =s->Predecessors.begin();!(i==s->Predecessors.end());i++)
- {
- cout<<" \t- t"<<(*i).second<<" ->";
- cout<<bddtable<<(*i).first->class_state<<endl;
- getchar();
- }*/
cout<<"Not implemented yet!"<<endl;
}
/*** Giving a position in m_GONodes Returns an LDDState ****/
@@ -212,11 +186,6 @@ LDDState *LDDGraph::getLDDStateById(unsigned int id) {
}
string LDDGraph::getTransition(int pos) {
- //return m_transition->at(pos);
- /* map<string,int>::iterator it=m_transition->begin();
- int i=0;
- while (i<pos) {it++;i++;}
- return it->first;*/
cout<<"********** Pos "<<pos<<endl;
map<string,int>::iterator it=m_transition->begin();
while(it != m_transition->end())
diff --git a/src/SpotSogIterator.cpp b/src/SpotSogIterator.cpp
index fc0a42e..5e8c76e 100644
--- a/src/SpotSogIterator.cpp
+++ b/src/SpotSogIterator.cpp
@@ -35,13 +35,13 @@ SpotSogState* SpotSogIterator::dst() const
bdd SpotSogIterator::cond() const {
bdd a=bddtrue;//1;
string name=m_graph->getTransition(m_lddstate->getSuccessors()->at(m_current_edge).second);
- cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
+ //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
spot::bdd_dict *p=m_dict_ptr->get();
spot::formula f=spot::formula::ap(name);
bdd result=bdd_ithvar((p->var_map.find(f))->second);
- //cout<<"Iterator cond()"<<m_current_edge<<"\n";
+ //cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n";
return result;
}
diff --git a/src/SpotSogIterator.h b/src/SpotSogIterator.h
index 6580ea2..7a25b99 100644
--- a/src/SpotSogIterator.h
+++ b/src/SpotSogIterator.h
@@ -14,9 +14,7 @@ class SpotSogIterator : public spot::twa_succ_iterator
bool next() override;
bool done() const override;
SpotSogState* dst() const override;
-// const state * dst () const override;//
- // a non derived function
- // std::string format_transition() const;
+
bdd cond() const override final;
spot::acc_cond::mark_t acc() const override final;
diff --git a/src/main.cpp b/src/main.cpp
index eef6a27..3e4564c 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -38,32 +38,62 @@ int Formula_transitions(const char * f, Set_mot& formula_trans, net Rv) ;
unsigned int nb_th;
int n_tasks, task_id;
spot::formula not_f;
-set<string> buildObsTransitions(const string &fileName) {
+set<string> buildObsTransitions(const string &fileName, const net &p) {
string input;
set<string> transitionSet;
+ vector<Place>::const_iterator it_Places;
ifstream file(fileName);
- if (file.is_open()) {
+ if (file.is_open())
+ {
getline (file,input);
cout<<"Loaded formula : "<<input<<endl;
file.close();
}
- else {
+ else
+ {
cout<<"Can not open formula file"<<endl;
exit(0);
}
spot::parsed_formula pf = spot::parse_infix_psl(input);
- if (pf.format_errors(std::cerr)) return transitionSet;
+ if (pf.format_errors(std::cerr))
+ return transitionSet;
spot::formula fo = pf.f;
- if (!fo.is_ltl_formula()) {
- std::cerr << "Only LTL formulas are supported.\n";
- return transitionSet;
+ if (!fo.is_ltl_formula())
+ {
+ std::cerr << "Only LTL formulas are supported.\n";
+ return transitionSet;
}
spot::atomic_prop_set *p_list=spot::atomic_prop_collect(fo,0);
- for (spot::atomic_prop_set::const_iterator i=p_list->begin();i!=p_list->end();i++) {
+ for (spot::atomic_prop_set::const_iterator i=p_list->begin(); i!=p_list->end(); i++)
+ {
+
+ for(it_Places=p.places.begin(); it_Places!=p.places.end();it_Places++)
+ {
+ //int pl = p.get_place_num((*it_Places)->name());
+
+ if (strcmp((*i).ap_name(),it_Places->name()))
+ if (p->get_incidence()[t].get(p) != 0)
+ transitionSet.insert(t);
+ }
transitionSet.insert((*i).ap_name());
+
+ //
}
+ /*places
+ for(it = sap->begin(); it != sap->end(); ++it) {
+ if(!p->place_exists( (*it)->name() )) {
+ std::string* s = new std::string((*it)->name());
+ delete sap;
+ sap = 0;
+ return s;
+ }
+ int pl = p->get_place_num((*it)->name());
+ for (int t = 0; t < p->t_size(); ++t)
+ if (p->get_incidence()[t].get(pl) != 0)
+ ob_tr.insert(t);
+ */
print_spin_ltl(std::cout, fo)<<'\n';
cout<<"Building formula negation\n";
not_f = spot::formula::Not(pf.f);
@@ -79,11 +109,16 @@ int main(int argc, char** argv)
exit(0);*/
- if(argc<3) return 0;
+ if(argc<3)
+ return 0;
char Obs[100]="";
char Int[100]="";
+ char pnet[100]="";
strcpy(Obs, argv[4]);
- if (argc > 6) strcpy(Int, argv[5]);
+ strcpy(pnet, argv[3]);
+
+ if (argc > 6)
+ strcpy(Int, argv[5]);
int bound = atoi(argv[argc - 1])==0?32:atoi(argv[argc - 1]);
//if(argc>5)
@@ -106,7 +141,8 @@ int main(int argc, char** argv)
cout<<"______________________________________\n";
cout<<"Fetching formula..."<<endl;
- set<string> list_transitions=buildObsTransitions(Obs);
+ net p(pnet);
+ set<string> list_transitions=buildObsTransitions(Obs,p);
net R(argv[3],list_transitions);
@@ -133,44 +169,73 @@ int main(int argc, char** argv)
else
{
cout<<"*******************Multithread version****************** \n" <<endl;
- if (!strcmp(argv[1],"p")) {
+ if (!strcmp(argv[1],"p"))
+ {
cout<<"Construction with pthread library."<<endl;
cout<<"Count of threads to be created: "<<nb_th<<endl;
DR.computeDSOG(g,false);
g.printCompleteInformation();
}
- else if (!strcmp(argv[1],"pc")) {
+ else if (!strcmp(argv[1],"pc"))
+ {
cout<<"Canonized construction with pthread library."<<endl;
cout<<"Count of threads to be created: "<<nb_th<<endl;
DR.computeDSOG(g,true);
g.printCompleteInformation();
}
- else if (!strcmp(argv[1],"l")) {
+ else if (!strcmp(argv[1],"l"))
+ {
cout<<"Construction with lace framework."<<endl;
cout<<"Count of workers to be created: "<<nb_th<<endl;
DR.computeSOGLace(g);
g.printCompleteInformation();
}
- else if (!strcmp(argv[1],"lc")) {
+ else if (!strcmp(argv[1],"lc"))
+ {
cout<<"Canonised construction with lace framework."<<endl;
cout<<"Count of workers to be created: "<<nb_th<<endl;
DR.computeSOGLaceCanonized(g);
g.printCompleteInformation();
}
- cout<<"Building automata for not(formula)\n";
- auto d = spot::make_bdd_dict();
- spot::twa_graph_ptr af = spot::translator(d).run(not_f);
- cout<<"Formula automata built.\n";
- auto k = std::make_shared<SogTwa>(d,DR.getGraph());
- spot::print_dot(std::cout, k);
-
- /*
- if (auto run = k->intersecting_run(af))
- std::cout << "formula is violated by the following run:\n" << *run;
- else
- std::cout << "formula is verified\n";*/
- }
+ cout<<"Perform Model checking ?";
+ char c;
+ cin>>c;
+ if (c='y')
+ {
+ cout<<"Building automata for not(formula)\n";
+ auto d = spot::make_bdd_dict();
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ cout<<"Formula automata built.\n";
+ cout<<"Want to save the graph in a dot file ?";
+ cin>>c;
+ if (c=='y') {
+ fstream file;
+ string st(Obs);
+ st+=".dot";
+ file.open(st.c_str(),fstream::out);
+ spot::print_dot(file, af);
+ file.close();
+ }
+ auto k = std::make_shared<SogTwa>(d,DR.getGraph());
+ cout<<"SOG translated to SPOT succeeded.."<<endl;
+ cout<<"Want to save the graph in a dot file ?";
+ cin>>c;
+ if (c=='y') {
+ fstream file;
+ string st(argv[3]);
+ st+=".dot";
+ file.open(st.c_str(),fstream::out);
+ spot::print_dot(file, k);
+ file.close();
+ }
+ if (auto run = k->intersecting_run(af))
+ std::cout << "formula is violated by the following run:\n" << *run;
+ else
+ std::cout << "formula is verified\n";
+ }
+
+ }
}
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 17f8baf..d6a7ee3 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -5,12 +5,6 @@
//#define DEBUG_GC
#include "threadSOG.h"
-
-// #include <vec.h>
-
-
-// #include "test_assert.h"
-
#include "sylvan.h"
#include "sylvan_seq.h"
#include <sylvan_sog.h>
@@ -18,8 +12,6 @@
using namespace sylvan;
-
-
void write_to_dot(const char *ch,MDD m)
{
FILE *fp=fopen(ch,"w");
@@ -29,20 +21,6 @@ void write_to_dot(const char *ch,MDD m)
/*************************************************/
-//#include <boost/thread.hpp>
-const vector<class Place> *_places = NULL;
-
-/*void my_error_handler_dist(int errcode) {
- cout<<"errcode = "<<errcode<<endl;
- if (errcode == BDD_RANGE) {
- // Value out of range : increase the size of the variables...
- // but which one???
- bdd_default_errhandler(errcode);
- }
- else {
- bdd_default_errhandler(errcode);
- }
-} */
@@ -80,36 +58,27 @@ threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool ini
//_______________
transitions=R.transitions;
- Observable=R.Observable;
+ m_observable=R.Observable;
- NonObservable=R.NonObservable;
+ m_nonObservable=R.NonObservable;
Formula_Trans=R.Formula_Trans;
- transitionName=R.transitionName;
+ m_transitionName=R.transitionName;
cout<<"Toutes les Transitions:"<<endl;
- map<string,int>::iterator it2=transitionName.begin();
- for (;it2!=transitionName.end();it2++) {
+ map<string,int>::iterator it2=m_transitionName.begin();
+ for (;it2!=m_transitionName.end();it2++) {
cout<<(*it2).first<<" : "<<(*it2).second<<endl;}
cout<<"Transitions observables :"<<endl;
- Set::iterator it=Observable.begin();
- for (;it!=Observable.end();it++) {cout<<*it<<" ";}
+ Set::iterator it=m_observable.begin();
+ for (;it!=m_observable.end();it++) {cout<<*it<<" ";}
cout<<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;
- // place domain, place bvect, place initial marking and place name
- // domains
-
-
- // bvec
-
-
- // Computing initial marking
-
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++)
@@ -119,10 +88,8 @@ threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool ini
M0=lddmc_cube(liste_marques,R.places.size());
- // ldd_refs_push(M0);
- // place names
- _places = &R.places;
+
uint32_t *prec = new uint32_t[m_nbPlaces];
@@ -211,7 +178,7 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
// cout<<"Marquage initial :\n";
//cout<<bddtable<<M0<<endl;
- MDD Complete_meta_state=Accessible_epsilon2(M0);
+ MDD Complete_meta_state=Accessible_epsilon(M0);
// write_to_dot("detectDiv.dot",Complete_meta_state);
//cout<<" div "<<Set_Div(Complete_meta_state)<<endl;
//lddmc_fprintdot(fp,Complete_meta_state);
@@ -219,15 +186,7 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
//cout<<"Apres accessible epsilon \n";
fire=firable_obs(Complete_meta_state);
- // MDD canonised_initial=Canonize(Complete_meta_state,0);
- //ldd_refs_push(canonised_initial);
-
- //c->blocage=Set_Bloc(Complete_meta_state);
- //c->boucle=Set_Div(Complete_meta_state);
- //c->m_lddstate=CanonizeR(Complete_meta_state,0);
- //cout<<"Apres CanonizeR nb representant : "<<bdd_pathcount(c->m_lddstate)<<endl;
- //c->m_lddstate=canonised_initial;
c->m_lddstate=Complete_meta_state;
//TabMeta[m_nbmetastate]=c->m_lddstate;
m_nbmetastate++;
@@ -254,7 +213,7 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
reached_class=new LDDState;
{
// cout<<"Avant Accessible epsilon \n";
- MDD Complete_meta_state=Accessible_epsilon2(get_successor(e.first.second,t));
+ MDD Complete_meta_state=Accessible_epsilon(get_successor(e.first.second,t));
//MDD reduced_meta=Canonize(Complete_meta_state,0);
ldd_refs_push(Complete_meta_state);
//ldd_refs_push(reduced_meta);
@@ -345,11 +304,6 @@ void * threadSOG::doCompute()
//ldd_refs_push(canonised_initial);
fire=firable_obs(Complete_meta_state);
- //c->blocage=Set_Bloc(Complete_meta_state);
- //c->boucle=Set_Div(Complete_meta_state);
- //c->m_lddstate=CanonizeR(Complete_meta_state,0);
- //cout<<"Apres CanonizeR nb representant : "<<bdd_pathcount(c->m_lddstate)<<endl;
- //c->m_lddstate=canonised_initial;
c->m_lddstate=Complete_meta_state;
//m_TabMeta[m_nbmetastate]=c->m_lddstate;
m_nbmetastate++;
@@ -515,11 +469,7 @@ void * threadSOG::doComputeCanonized()
ldd_refs_push(canonised_initial);
fire=firable_obs(Complete_meta_state);
- //c->blocage=Set_Bloc(Complete_meta_state);
- //c->boucle=Set_Div(Complete_meta_state);
- //c->m_lddstate=CanonizeR(Complete_meta_state,0);
- //cout<<"Apres CanonizeR nb representant : "<<bdd_pathcount(c->m_lddstate)<<endl;
- //c->m_lddstate=canonised_initial;
+
c->m_lddstate=canonised_initial;
//m_TabMeta[m_nbmetastate]=c->m_lddstate;
m_nbmetastate++;
@@ -536,8 +486,7 @@ void * threadSOG::doComputeCanonized()
LDDState* reached_class;
- // size_t max_meta_state_size;
- // int min_charge;
+
do
{
@@ -672,7 +621,7 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised)
cout << "number of threads "<<m_nb_thread<<endl;
int rc;
m_graph=&g;
- m_graph->setTransition(transitionName);
+ m_graph->setTransition(m_transitionName);
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
@@ -721,110 +670,6 @@ void * threadSOG::threadHandlerCanonized(void *context)
return ((threadSOG*)context)->doComputeCanonized();
}
-
-void threadSOG::printhandler(ostream &o, int var)
-{
- o << (*_places)[var/2].name;
- if (var%2)
- o << "_p";
-}
-
-
-
-
-
-
-
-
-
-
-Set threadSOG::firable_obs(MDD State)
-{
- Set res;
- for(Set::const_iterator i=Observable.begin(); !(i==Observable.end()); i++)
- {
- //cout<<"firable..."<<endl;
- MDD succ = lddmc_firing_mono(State,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- if(succ!=lddmc_false)
- {
- res.insert(*i);
- }
-
- }
- return res;
-}
-
-
-MDD threadSOG::get_successor(MDD From,int t)
-{
- return lddmc_firing_mono(From,m_tb_relation[(t)].getMinus(),m_tb_relation[(t)].getPlus());
-}
-
-MDD threadSOG::get_successor2(MDD From,int t)
-{
- // LACE_ME;
- return lddmc_firing_mono(From,m_tb_relation[(t)].getMinus(),m_tb_relation[(t)].getPlus());
-}
-
-MDD threadSOG::Accessible_epsilon2(MDD From)
-{
- MDD M1;
- MDD M2=From;
- int it=0;
-
-
- do
- {
-
- M1=M2;
- for(Set::const_iterator i=NonObservable.begin(); !(i==NonObservable.end()); i++)
- { LACE_ME;
-
- MDD succ= lddmc_firing_mono(M2,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- M2=lddmc_union(succ,M2);
-
- }
-
- it++;
-
- // cout << bdd_nodecount(M2) << endl;
- }
- while(M1!=M2);
-
- return M2;
-}
-
-MDD threadSOG::Accessible_epsilon(MDD From)
-{
- MDD M1;
- MDD M2=From;
- int it=0;
-
-
- do
- {
-
- M1=M2;
- for(Set::const_iterator i=NonObservable.begin(); !(i==NonObservable.end()); i++)
- {
-
- MDD succ= lddmc_firing_mono(M2,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- M2=lddmc_union_mono(succ,M2);
-
- }
-
- it++;
-
- // cout << bdd_nodecount(M2) << endl;
- }
- while(M1!=M2);
-
- return M2;
-}
-
-
-
-
int threadSOG::minCharge()
{
int pos=0;
@@ -842,155 +687,10 @@ int threadSOG::minCharge()
}
-/*--------------------------- Set_Bloc() -------*/
-/*bool DistributedSOG::Set_Bloc(MDD &S) const {
-
- cout<<"Ici detect blocage \n";
-int check_deadlocks = 0
-MDD cur;
- for(vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i!=m_tb_relation.end();i++)
- {
-
- cur=TransSylvan(*i).getMinus();
-
- }
-return ((S&cur)!=lddmc_false);
- //BLOCAGE
-}
-
-
-/*-------------------------Set_Div() à revoir -----------------------------*/
-/*bool threadSOG::Set_Div(MDD &S) const
-{
- Set::const_iterator i;
- MDD To,Reached;
- //cout<<"Ici detect divergence \n";
- Reached=S;
- do
- {
- MDD From=Reached;
- for(i=NonObservable.begin();!(i==NonObservable.end());i++)
- {
-
- To=lddmc_firing_mono(Reached,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- Reached=lddmc_union_mono(Reached,To);
- //To=m_tb_relation[*i](Reached);
- //Reached=Reached|To; //Reached=To ???
- //Reached=To;
- }
- if(Reached==From)
- //cout<<"SEQUENCE DIVERGENTE \n";
- return true;
- //From=Reached;
- }while(Reached!=bddfalse);
- return false;
- //cout<<"PAS DE SEQUENCE DIVERGENTE \n";
-}
-*/
-
-MDD threadSOG::Canonize(MDD s,unsigned int level)
-{
- if (level>m_nbPlaces || s==lddmc_false)
- return lddmc_false;
- if(isSingleMDD(s))
- return s;
- MDD s0=lddmc_false,s1=lddmc_false;
-
- bool res=false;
- do
- {
- if (get_mddnbr(s,level)>1)
- {
- s0=ldd_divide_rec(s,level);
- s1=ldd_minus(s,s0);
- res=true;
- }
- else
- level++;
- }
- while(level<m_nbPlaces && !res);
-
-
- if (s0==lddmc_false && s1==lddmc_false)
- return lddmc_false;
- // if (level==nbPlaces) return lddmc_false;
- MDD Front,Reach;
- if (s0!=lddmc_false && s1!=lddmc_false)
- {
- Front=s1;
- Reach=s1;
- do
- {
- // cout<<"premiere boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s0 = ldd_minus(s0,Front);
- }
- while((Front!=lddmc_false)&&(s0!=lddmc_false));
- }
- if((s0!=lddmc_false)&&(s1!=lddmc_false))
- {
- Front=s0;
- Reach = s0;
- do
- {
- // cout<<"deuxieme boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s1 = ldd_minus(s1,Front);
- }
- while( Front!=lddmc_false && s1!=lddmc_false );
- }
-
-
-
- MDD Repr=lddmc_false;
-
- if (isSingleMDD(s0))
- {
- Repr=s0;
- }
- else
- {
-
- Repr=Canonize(s0,level);
-
- }
-
- if (isSingleMDD(s1))
- Repr=lddmc_union_mono(Repr,s1);
- else
- Repr=lddmc_union_mono(Repr,Canonize(s1,level));
-
-
- return Repr;
-
-
-}
-MDD threadSOG::ImageForward(MDD From)
-{
- MDD Res=lddmc_false;
- for(Set::const_iterator i=NonObservable.begin(); !(i==NonObservable.end()); i++)
- {
- MDD succ= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- // bdd succ = relation[(*i)](From);
- Res=lddmc_union_mono(Res,succ);
- // Res=Res|succ;
-
- }
- return Res;
-}
-
bool threadSOG::Set_Bloc(MDD &M) const
{
- //bdd Mt = lddmc_true;
- //for(vector<Trans>::const_iterator i = relation.begin(); i != relation.end(); ++i) {
- // Mt = Mt & !(i->Precond);
- //}
- //return ((S & Mt) != bddfalse);
- cout<<"Ici detect blocage \n";
-//int check_deadlocks = 0
+
MDD cur=lddmc_true;
for(vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i!=m_tb_relation.end();i++)
{
@@ -1003,7 +703,7 @@ return ((M&cur)!=lddmc_false);
}
bool threadSOG::Set_Div2( const MDD &M) const
{
- if (NonObservable.empty())
+ if (m_nonObservable.empty())
return false;
Set::const_iterator i;
MDD Reached,From;
@@ -1012,7 +712,7 @@ bool threadSOG::Set_Div2( const MDD &M) const
do
{
From=Reached;
- for(i=NonObservable.begin();!(i==NonObservable.end());i++)
+ for(i=m_nonObservable.begin();!(i==m_nonObservable.end());i++)
{
// To=relation[*i](Reached);
// Reached=Reached|To; //Reached=To ???
@@ -1029,7 +729,7 @@ bool threadSOG::Set_Div2( const MDD &M) const
//}
bool threadSOG::Set_Div(MDD &M) const
{
- if (NonObservable.empty())
+ if (m_nonObservable.empty())
return false;
Set::const_iterator i;
MDD Reached,From;
@@ -1038,7 +738,7 @@ bool threadSOG::Set_Div(MDD &M) const
do
{
From=Reached;
- for(i=NonObservable.begin();!(i==NonObservable.end());i++)
+ for(i=m_nonObservable.begin();!(i==m_nonObservable.end());i++)
{
// To=relation[*i](Reached);
// Reached=Reached|To; //Reached=To ???
@@ -1046,12 +746,8 @@ bool threadSOG::Set_Div(MDD &M) const
Reached=lddmc_union_mono(Reached,To);
//Reached=To;
}
- if(Reached==From)
- //{
- //cout << " sequence divergente "<<endl;
- return true;
- //}
- //From=Reached;
+ if(Reached==From) return true;
+
}while(Reached!=lddmc_false && Reached != From);
// cout<<"PAS DE SEQUENCE DIVERGENTE \n";
return false;
@@ -1062,10 +758,6 @@ threadSOG::~threadSOG()
//dtor
}
-/*********Returns the count of places******************************************/
-unsigned int threadSOG::getPlacesCount() {
- return m_nbPlaces;
-}
@@ -1141,7 +833,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
- m_graph->setTransition(transitionName);
+ m_graph->setTransition(m_transitionName);
m_nbmetastate=0;
m_MaxIntBdd=0;
@@ -1150,10 +842,10 @@ void threadSOG::computeSOGLace(LDDGraph &g)
//cout<<"Marquage initial is being built..."<<endl;
LACE_ME;
- MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&NonObservable,&m_tb_relation));
+ MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&m_nonObservable,&m_tb_relation));
- fire=firable_obs_lace(initial_meta_state,&Observable,&m_tb_relation);
+ fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
c->m_lddstate=initial_meta_state;
@@ -1166,10 +858,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
m_graph->insert(c);
//m_graph->nbMarking+=bdd_pathcount(c->m_lddstate);
LDDState* reached_class;
- // MDD Complete_meta_state;*/
- // size_t max_meta_state_size;
- // int min_charge;
while (!m_st[0].empty())
{
@@ -1184,7 +873,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
int t = *iter;
cout<<"Transition order1: "<<*iter<<endl;
//e.second.erase(t);
- SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&NonObservable,&m_tb_relation);
+ SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&m_nonObservable,&m_tb_relation);
onb_it++;iter++;
}
@@ -1193,7 +882,6 @@ void threadSOG::computeSOGLace(LDDGraph &g)
Set::iterator it = e.second.end();
it--;
int t=*it;
- cout<<"Transition order2: "<<t<<endl;
e.second.erase(it);
MDD Complete_meta_state=SYNC(Accessible_epsilon_lace);
reached_class=new LDDState;
@@ -1208,7 +896,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
e.first.first->Successors.insert(e.first.first->Successors.begin(),LDDEdge(reached_class,t));
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(e.first.first,t));
m_nbmetastate++;
- fire=firable_obs_lace(Complete_meta_state,&Observable,&m_tb_relation);
+ fire=firable_obs_lace(Complete_meta_state,&m_observable,&m_tb_relation);
m_st[0].push(Pair(couple(reached_class,Complete_meta_state),fire));
}
else
@@ -1227,12 +915,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
std::cout << "TIME OF CONSTRUCTION OF THE SOG " << tps << " seconds\n";
}
-Set * threadSOG::getNonObservable() {
- return &NonObservable;
-}
-vector<TransSylvan>* threadSOG::getTBRelation() {
- return &m_tb_relation;
-}
+
/********************* Compute canonized SOG with lace *********************************************/
/******************************Canonizer with lace framework **********************************/
@@ -1338,7 +1021,7 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
- m_graph->setTransition(transitionName);
+ m_graph->setTransition(m_transitionName);
m_nbmetastate=0;
@@ -1349,12 +1032,12 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
//cout<<"Marquage initial is being built..."<<endl;
LACE_ME;
- MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&NonObservable,&m_tb_relation));
+ MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&m_nonObservable,&m_tb_relation));
//lddmc_refs_spawn(SPAWN(lddmc_canonize,initial_meta_state,0,*this));
- fire=firable_obs_lace(initial_meta_state,&Observable,&m_tb_relation);
+ fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
m_nbmetastate++;
//m_old_size=lddmc_nodecount(c->m_lddstate);
//reduced_initial=lddmc_refs_sync(SYNC(lddmc_canonize));
@@ -1381,15 +1064,17 @@ cout<<"\n=========================================\n";
{
int t = *iter;
//e.second.erase(t);
- SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&NonObservable,&m_tb_relation);
+ SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&m_nonObservable,&m_tb_relation);
onb_it++;iter++;
}
for (unsigned int i=0; i<onb_it; i++)
{
- int t = *e.second.end();
+ Set::iterator it = e.second.end();
+ it--;
+ int t=*it;
+ e.second.erase(it);
- e.second.erase(t);
MDD Complete_meta_state=SYNC(Accessible_epsilon_lace);
lddmc_refs_push(Complete_meta_state);
@@ -1408,7 +1093,7 @@ cout<<"\n=========================================\n";
e.first.first->Successors.insert(e.first.first->Successors.begin(),LDDEdge(reached_class,t));
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(e.first.first,t));
m_nbmetastate++;
- fire=firable_obs_lace(Complete_meta_state,&Observable,&m_tb_relation);
+ fire=firable_obs_lace(Complete_meta_state,&m_observable,&m_tb_relation);
m_st[0].push(Pair(couple(reached_class,Complete_meta_state),fire));
}
else
@@ -1428,8 +1113,3 @@ cout<<"\n=========================================\n";
std::cout << "TIME OF CONSTRUCTION OF THE SOG " << tps << " seconds\n";
}
-
-LDDGraph *threadSOG::getGraph() const {
- return m_graph;
-}
-
diff --git a/src/threadSOG.h b/src/threadSOG.h
index 26008f2..d6dc0a1 100644
--- a/src/threadSOG.h
+++ b/src/threadSOG.h
@@ -12,71 +12,53 @@
#include <sys/types.h>
#include <unistd.h>
#include "LDDGraph.h"
-#include "TransSylvan.h"
+#include "TransSylvan.h"
+#include "CommonSOG.h"
+
+
+
-typedef pair<LDDState *, MDD> couple;
-typedef pair<couple, Set> Pair;
-typedef stack<Pair> pile;
// typedef vector<Trans> vec_trans;
extern unsigned int nb_th;
-class threadSOG {
+class threadSOG : public CommonSOG{
public:
threadSOG(const net &, int BOUND = 32, 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 printhandler(ostream &o, int var);
static void *threadHandler(void *context);
static void *threadHandlerCanonized(void *context);
void *doCompute();
void *doComputeCanonized();
- unsigned int getPlacesCount();
- MDD ImageForward(MDD From);
+
+
void computeSOGLace(LDDGraph &g);
void computeSOGLaceCanonized(LDDGraph &g);
- Set * getNonObservable();
- vector<TransSylvan>* getTBRelation();
- LDDGraph *getGraph() const;
+
+
+
protected:
private:
////////////////////////////////
- //////////////////////////////
-
- int m_nbPlaces = 0;
- MDD Canonize(MDD s, unsigned int level);
- LDDGraph *m_graph;
- MDD LDDAccessible_epsilon(MDD *m);
- MDD LDDAccessible_epsilon2(MDD *m);
- MDD Accessible_epsilon(MDD From);
- MDD Accessible_epsilon2(MDD From);
- Set firable_obs(MDD State);
- MDD get_successor(MDD From, int t);
- MDD get_successor2(MDD From, int t);
+
+
+
int minCharge();
bool Set_Bloc(MDD &M) const;
bool Set_Bloc2(const MDD &M) const;
bool Set_Div(MDD &M) const;
bool Set_Div2(const MDD &M) const;
bool isNotTerminated();
- //-----Original defined as members
- vector<class Transition> transitions;
- Set Observable;
- Set NonObservable;
- map<string, int> transitionName;
- Set InterfaceTrans;
- Set Formula_Trans;
timespec start, finish;
MDD M0;
- LDDState m_M0;
- MDD currentvar;
- //-----------------
- vector<TransSylvan> m_tb_relation;
+ //-----------------
+
int m_NbIt;
int m_itext, m_itint;
int m_MaxIntBdd;
@@ -92,7 +74,7 @@ class threadSOG {
int m_min_charge;
- net m_net;
+
int m_bound, m_init;
int m_id_thread;
pthread_mutex_t m_mutex;
--
GitLab