diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..378eac25d311703f3f2cd456d8036da525cd0366
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+build
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 84f9f4eeb27f5cd5de480c6edd814841f3b5bbe3..dcc56ac45c9c3e3b04ccff9b5d53e05fe0566395 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -18,11 +18,7 @@ set_target_properties(spot PROPERTIES
INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
)
-add_library(bddx SHARED IMPORTED) # or STATIC instead of SHARED
-set_target_properties(bddx PROPERTIES
- IMPORTED_LOCATION "/usr/lib/x86_64-linux-gnu/libbddx.so"
- INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
-)
+
@@ -37,22 +33,12 @@ add_executable(hybrid-sog main.cpp
threadSOG.cpp
threadSOG.h
LDDGraph.cpp
- LDDGraph.h
LDDState.cpp
- LDDState.h
TransSylvan.cpp
sylvan_sog.c
- SpotSogState.cpp
- SpotSogState.h
- SpotSogIterator.cpp
- SpotSogIterator.h
- SogTwa.cpp
- SogTwa.h
-
)
target_link_libraries(hybrid-sog
- bddx
spot
sylvan
RdP
diff --git a/src/Class_of_state.h b/src/Class_of_state.h
index 5c45ea7e9e1cc6d689e69cbcd85a6cff4b301f52..38b11a187cfec559d285d766b8d9216f87ec4cad 100644
--- a/src/Class_of_state.h
+++ b/src/Class_of_state.h
@@ -1,7 +1,7 @@
#ifndef CLASS_OF_STATE
#define CLASS_OF_STATE
using namespace std;
-#include "bdd.h"
+#include "bddx.h"
//#include <map.h>
#include<unordered_map>
#include <set>
diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 627a4744de6e8fb30a06afd48151ca8de64fba1b..73832c1ff022f188863bdbb5ec5df39c42417da1 100644
--- a/src/DistributedSOG.cpp
+++ b/src/DistributedSOG.cpp
@@ -25,6 +25,12 @@ using namespace sylvan;
/**************************************************/
+
+
+
+const vector<class Place> *__vplaces = NULL;
+
+
DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
{
@@ -41,20 +47,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;
- m_observable=R.Observable;
- m_nonObservable=R.NonObservable;
+ Observable=R.Observable;
+ NonObservable=R.NonObservable;
Formula_Trans=R.Formula_Trans;
- m_transitionName=R.transitionName;
+ transitionName=R.transitionName;
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;
+ Nb_places=R.places.size();
+ cout<<"Nombre de places : "<<Nb_places<<endl;
+ cout<<"Derniere place : "<<R.places[Nb_places-1].name<<endl;
// place domain, place bvect, place initial marking and place name
@@ -66,17 +72,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[m_nbPlaces];
- uint32_t *postc= new uint32_t [m_nbPlaces];
+ uint32_t *prec = new uint32_t[nbPlaces];
+ uint32_t *postc= new uint32_t [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++)
+ for(i=0; i<nbPlaces; i++)
{
prec[i]=0;
postc[i]=0;
@@ -97,8 +103,8 @@ DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
postc[it->first] = postc[it->first] + it->second;
}
- MDD _minus=lddmc_cube(prec,m_nbPlaces);
- MDD _plus=lddmc_cube(postc,m_nbPlaces);
+ MDD _minus=lddmc_cube(prec,nbPlaces);
+ MDD _plus=lddmc_cube(postc,nbPlaces);
m_tb_relation.push_back(TransSylvan(_minus,_plus));
}
delete [] prec;
@@ -123,7 +129,7 @@ void *DistributedSOG::doCompute()
Pair S;
// pile m_st;
- char msg[LENGTH_ID];
+ unsigned char msg[LENGTH_ID];
int v_nbmetastate=0;
int term=0;
@@ -144,7 +150,7 @@ void *DistributedSOG::doCompute()
c->m_lddstate=Complete_meta_state;
- lddmc_getsha(Complete_meta_state, msg);
+ // lddmc_getsha(Complete_meta_state, msg);
cout <<"nb task "<<n_tasks<<endl;
int destination=(int)abs((msg[0])%n_tasks);
@@ -152,8 +158,7 @@ void *DistributedSOG::doCompute()
{
m_nbmetastate++;
//m_old_size=lddmc_nodecount(c->m_lddstate);
-
- Set fire=firable_obs(Complete_meta_state);
+ fire=firable_obs(Complete_meta_state);
m_st.push(Pair(couple(c,Complete_meta_state),fire));
m_graph->setInitialState(c);
m_graph->insert(c);
@@ -199,10 +204,10 @@ void *DistributedSOG::doCompute()
reached_class=new LDDState;
// lddmc_fprintdot(fp,Complete_meta_state);
- MDD marking=get_successor(e.first.second,t);
+ MDD marking=get_successorMDD(e.first.second,t);
MDD lddmarq=Accessible_epsilon(marking);
reached_class->m_lddstate=lddmarq;
- lddmc_getsha(lddmarq, msg);
+// lddmc_getsha(lddmarq, msg);
int destination=(int)abs((msg[0])%n_tasks);
@@ -224,7 +229,7 @@ void *DistributedSOG::doCompute()
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(e.first.first,t));
m_nbmetastate++;
- Set fire=firable_obs(lddmarq);
+ fire=firable_obs(lddmarq);
m_st.push(Pair(couple(reached_class,lddmarq),fire));
nb_success++;
@@ -453,7 +458,7 @@ void DistributedSOG::read_state_message()
if (!m_graph->find(Agregate))
{
m_graph->insert(Agregate);
- Set fire=firable_obs(MState);
+ fire=firable_obs(MState);
m_nbmetastate++;
m_old_size=lddmc_nodecount(Agregate->m_lddstate);
m_st.push(Pair(couple(Agregate,MState),fire));
@@ -546,8 +551,70 @@ 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)
{
@@ -572,7 +639,7 @@ char * DistributedSOG::concat_string(const char *s1,int longueur1,const char *s2
}
-void DistributedSOG::strcpySHA(char *dest,const char *source)
+void DistributedSOG::strcpySHA(unsigned char *dest,const unsigned char *source)
{
for (int i=0; i<LENGTH_ID; i++)
{
@@ -641,15 +708,15 @@ MDD DistributedSOG::decodage_message(char *chaine)
nb_marq=(nb_marq<<8) | (unsigned char)chaine[0];
unsigned int index=2;
- uint32_t list_marq[m_nbPlaces];
+ uint32_t list_marq[nbPlaces];
for (unsigned int i=0; i<nb_marq; i++)
{
- for (unsigned int j=0; j<m_nbPlaces; j++)
+ for (unsigned int j=0; j<nbPlaces; j++)
{
list_marq[j]=chaine[index];
index++;
}
- MDD N=lddmc_cube(list_marq,m_nbPlaces);
+ MDD N=lddmc_cube(list_marq,nbPlaces);
M=lddmc_union_mono(M,N);
}
return M;
@@ -663,7 +730,7 @@ void DistributedSOG::MarquageString(char *dest,const char *source)
int index=1;
for (int nb=0; nb<length; nb++)
{
- for (int i=0; i<m_nbPlaces; i++)
+ for (int i=0; i<nbPlaces; i++)
{
dest[index]=(unsigned char)source[index]+(unsigned char)'0';
printf("%d",source[index]);
@@ -675,6 +742,95 @@ 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 f10880f5f36e5d7dfb87a169226d3af33dfd5f0b..ed845624cee0b7499ac6d6bbec6637fa6d0d3df7 100644
--- a/src/DistributedSOG.h
+++ b/src/DistributedSOG.h
@@ -28,12 +28,11 @@
//#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
@@ -41,10 +40,12 @@
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 : public CommonSOG{
+class DistributedSOG {
public:
DistributedSOG(const net &, int BOUND = 32, bool init = false);
void buildFromNet(int index);
@@ -52,6 +53,7 @@ class DistributedSOG : public CommonSOG{
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();
@@ -59,20 +61,34 @@ class DistributedSOG : public CommonSOG{
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();
- void strcpySHA(char *dest, const char *source);
+ void strcpySHA(unsigned char *dest, const unsigned char *source);
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;
@@ -93,21 +109,27 @@ class DistributedSOG : public CommonSOG{
MPI_Request m_request;
-
- int m_init;
+ net m_net;
+ int m_bound, 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 31c6c0fbec56c7c232e7a931eec01e3d924d8f67..02c7b65549189792d66ca85ce12906d03a3dcba5 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;
- m_observable=R.Observable;
- m_nonObservable=R.NonObservable;
+ Observable=R.Observable;
+ NonObservable=R.NonObservable;
Formula_Trans=R.Formula_Trans;
- m_transitionName=R.transitionName;
+ 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,6 +829,15 @@ 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;
@@ -845,6 +854,65 @@ 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++)
@@ -911,14 +979,109 @@ 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 6511d11790f765010a9352a70bb5943db7bd32a2..8011e98f1226c73c4c5392e6d9a889b5b44a0363 100644
--- a/src/HybridSOG.h
+++ b/src/HybridSOG.h
@@ -29,7 +29,6 @@
//#include <boost/serialization/string.hpp>
#include <time.h>
#include <chrono>
-#include "CommonSOG.h"
// namespace mpi = boost::mpi;
//#define MASTER 0
@@ -37,103 +36,125 @@
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 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;
-
+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"};
};
#endif // HybridSOG_H
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index 13a89d31b4646fda81c3f422c23739b11eebd0ed..8a7bc244ee542a6ff27aedd88c064bdebdfd1d44 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -2,7 +2,7 @@
#include <sylvan.h>
#include <stdio.h>
#include <string.h>
-#include <map>
+
LDDGraph::~LDDGraph()
{
//dtor
@@ -14,10 +14,6 @@ void LDDGraph::setInitialState(LDDState *c)
m_currentstate=m_initialstate=c;
}
-
-LDDState* LDDGraph::getInitialState() const {
- return m_GONodes.at(0);
-}
/*----------------------find()----------------*/
LDDState * LDDGraph::find(LDDState* c)
{
@@ -108,7 +104,7 @@ void LDDGraph::printCompleteInformation()
char c;
cin>>c;
//InitVisit(initialstate,n);
-
+ m_tab=new MDD[(int)m_nbStates];
size_t n=1;
//cout<<"NB BDD NODE : "<<NbBddNode(initialstate,n)<<endl;
NbBddNode(m_initialstate,n);
@@ -123,10 +119,13 @@ 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;
@@ -173,33 +172,33 @@ 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 ****/
-LDDState *LDDGraph::getLDDStateById(unsigned int id) {
- return m_GONodes.at(id);
-}
-
-string LDDGraph::getTransition(int pos) {
- cout<<"********** Pos "<<pos<<endl;
- map<string,int>::iterator it=m_transition->begin();
- while(it != m_transition->end())
- {
- if(it->second == pos)
- return it->first;
- it++;
- }
- return it->first;
-}
-
-void LDDGraph::setTransition(map<string,int>& list_transitions) {
- m_transition=&list_transitions;
-}
-
-//void LDDGraph::setTransition(vector<string> list)
-
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index 3c1b356dae33d2e4891827dca50c3db89dec2d51..4399850d93fa6a27c57e1e763da4e3bae0cdddf6 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -4,21 +4,18 @@
//#include "LDDStateExtend.h"
using namespace std;
#include <iostream>
-#include <map>
+
typedef set<int> Set;
typedef vector<LDDState*> MetaLDDNodes;
class LDDGraph
{
private:
- map<string,int>* m_transition;
+ MDD * m_tab;
void printGraph(LDDState *, size_t &);
public:
- string getTransition(int pos);
- void setTransition(map<string,int>& list_transitions);
MetaLDDNodes m_GONodes;
- LDDState *getLDDStateById(unsigned int id);
void Reset();
LDDState *m_initialstate;
LDDState *m_currentstate;
@@ -38,7 +35,6 @@ class LDDGraph
void insert(LDDState*);
LDDGraph() {m_nbStates=m_nbArcs=m_nbMarking=0;}
void setInitialState(LDDState*); //Define the initial state of this graph
- LDDState* getInitialState() const;
void printCompleteInformation();
virtual ~LDDGraph();
};
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index a6f372b3af40b1a4f516c2de908a5cbc5aa4659e..616246c9f50feee32877293a08139d3907444bc6 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -24,7 +24,3 @@ bool LDDState::isVirtual() {
void LDDState::setVirtual() {
m_virtual=true;
}
-
-vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
- return &Successors;
-}
diff --git a/src/LDDState.h b/src/LDDState.h
index 582900826df1cd2ac21b73d6982224f1514e3955..17b342002c7c96195fc97d3f8b871cf07c50a12e 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -16,7 +16,6 @@ class LDDState {
virtual ~LDDState();
Set firable;
void* Class_Appartenance;
- vector<pair<LDDState*, int>>* getSuccessors();
vector<pair<LDDState*, int> > Predecessors, Successors;
pair<LDDState*, int> LastEdge;
void setLDDValue(MDD m);
diff --git a/src/main.cpp b/src/main.cpp
index 3e4564c774d8a277cae34912c7acdca2a80fba28..aa4cbab925519010dd78698db666e4e4de5dcaa3 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -22,7 +22,6 @@
#include <spot/twaalgos/emptiness.hh>
#include <spot/tl/apcollect.hh>
#include "Net.hpp"
-#include "SogTwa.h"
@@ -37,66 +36,34 @@ 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, const net &p) {
+
+set<string> buildObsTransitions(const string &fileName) {
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(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);
- }
+ for (spot::atomic_prop_set::const_iterator i=p_list->begin();i!=p_list->end();i++) {
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);
return transitionSet;
}
@@ -109,16 +76,11 @@ 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]);
- strcpy(pnet, argv[3]);
-
- if (argc > 6)
- strcpy(Int, argv[5]);
+ if (argc > 6) strcpy(Int, argv[5]);
int bound = atoi(argv[argc - 1])==0?32:atoi(argv[argc - 1]);
//if(argc>5)
@@ -141,8 +103,7 @@ int main(int argc, char** argv)
cout<<"______________________________________\n";
cout<<"Fetching formula..."<<endl;
- net p(pnet);
- set<string> list_transitions=buildObsTransitions(Obs,p);
+ set<string> list_transitions=buildObsTransitions(Obs);
net R(argv[3],list_transitions);
@@ -169,73 +130,31 @@ 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<<"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 d6a7ee380014c5c51ee013a97a9e98358e4eed0b..40da1bfa08d4963f34ce6ba30e3120665a2c5e1f 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -5,6 +5,12 @@
//#define DEBUG_GC
#include "threadSOG.h"
+
+// #include <vec.h>
+
+
+// #include "test_assert.h"
+
#include "sylvan.h"
#include "sylvan_seq.h"
#include <sylvan_sog.h>
@@ -12,6 +18,8 @@
using namespace sylvan;
+
+
void write_to_dot(const char *ch,MDD m)
{
FILE *fp=fopen(ch,"w");
@@ -21,6 +29,20 @@ 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);
+ }
+} */
@@ -58,27 +80,23 @@ threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool ini
//_______________
transitions=R.transitions;
- m_observable=R.Observable;
-
- m_nonObservable=R.NonObservable;
+ Observable=R.Observable;
+ NonObservable=R.NonObservable;
Formula_Trans=R.Formula_Trans;
- m_transitionName=R.transitionName;
-
- 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;}
-
-
-
- cout<<"Transitions observables :"<<endl;
- Set::iterator it=m_observable.begin();
- for (;it!=m_observable.end();it++) {cout<<*it<<" ";}
- cout<<endl;
+ transitionName=R.transitionName;
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++)
@@ -88,8 +106,10 @@ 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];
@@ -178,7 +198,7 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
// cout<<"Marquage initial :\n";
//cout<<bddtable<<M0<<endl;
- MDD Complete_meta_state=Accessible_epsilon(M0);
+ MDD Complete_meta_state=Accessible_epsilon2(M0);
// write_to_dot("detectDiv.dot",Complete_meta_state);
//cout<<" div "<<Set_Div(Complete_meta_state)<<endl;
//lddmc_fprintdot(fp,Complete_meta_state);
@@ -186,7 +206,15 @@ 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++;
@@ -213,7 +241,7 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
reached_class=new LDDState;
{
// cout<<"Avant Accessible epsilon \n";
- MDD Complete_meta_state=Accessible_epsilon(get_successor(e.first.second,t));
+ MDD Complete_meta_state=Accessible_epsilon2(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);
@@ -227,7 +255,11 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
{
// cout<<"not found"<<endl;
reached_class->m_boucle=Set_Div(Complete_meta_state);
+ // cout<<"Divergence "<<Set_Div(Complete_meta_state)<<endl;
+ // cout<<"blocage "<<Set_Bloc(Complete_meta_state)<<endl;
+ //reached_class->blocage=Set_Bloc(Complete_meta_state);
+ //reached_class->boucle=Set_Div(Complete_meta_state);
fire=firable_obs(Complete_meta_state);
st.push(Pair(couple(reached_class,Complete_meta_state),fire));
//TabMeta[nbmetastate]=reached_class->m_lddstate;
@@ -304,6 +336,11 @@ 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++;
@@ -469,7 +506,11 @@ 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++;
@@ -486,7 +527,8 @@ void * threadSOG::doComputeCanonized()
LDDState* reached_class;
-
+ // size_t max_meta_state_size;
+ // int min_charge;
do
{
@@ -621,7 +663,6 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised)
cout << "number of threads "<<m_nb_thread<<endl;
int rc;
m_graph=&g;
- m_graph->setTransition(m_transitionName);
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
@@ -670,6 +711,110 @@ 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;
@@ -687,10 +832,155 @@ int threadSOG::minCharge()
}
+/*--------------------------- Set_Bloc() -------*/
+/*bool DistributedSOG::Set_Bloc(MDD &S) const {
-bool threadSOG::Set_Bloc(MDD &M) 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++)
{
@@ -703,7 +993,7 @@ return ((M&cur)!=lddmc_false);
}
bool threadSOG::Set_Div2( const MDD &M) const
{
- if (m_nonObservable.empty())
+ if (NonObservable.empty())
return false;
Set::const_iterator i;
MDD Reached,From;
@@ -712,7 +1002,7 @@ bool threadSOG::Set_Div2( const MDD &M) const
do
{
From=Reached;
- for(i=m_nonObservable.begin();!(i==m_nonObservable.end());i++)
+ for(i=NonObservable.begin();!(i==NonObservable.end());i++)
{
// To=relation[*i](Reached);
// Reached=Reached|To; //Reached=To ???
@@ -729,7 +1019,7 @@ bool threadSOG::Set_Div2( const MDD &M) const
//}
bool threadSOG::Set_Div(MDD &M) const
{
- if (m_nonObservable.empty())
+ if (NonObservable.empty())
return false;
Set::const_iterator i;
MDD Reached,From;
@@ -738,7 +1028,7 @@ bool threadSOG::Set_Div(MDD &M) const
do
{
From=Reached;
- for(i=m_nonObservable.begin();!(i==m_nonObservable.end());i++)
+ for(i=NonObservable.begin();!(i==NonObservable.end());i++)
{
// To=relation[*i](Reached);
// Reached=Reached|To; //Reached=To ???
@@ -746,8 +1036,12 @@ bool threadSOG::Set_Div(MDD &M) const
Reached=lddmc_union_mono(Reached,To);
//Reached=To;
}
- if(Reached==From) return true;
-
+ if(Reached==From)
+ //{
+ //cout << " sequence divergente "<<endl;
+ return true;
+ //}
+ //From=Reached;
}while(Reached!=lddmc_false && Reached != From);
// cout<<"PAS DE SEQUENCE DIVERGENTE \n";
return false;
@@ -758,6 +1052,10 @@ threadSOG::~threadSOG()
//dtor
}
+/*********Returns the count of places******************************************/
+unsigned int threadSOG::getPlacesCount() {
+ return m_nbPlaces;
+}
@@ -793,7 +1091,6 @@ TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*
if(succ!=lddmc_false)
{
res.insert(*i);
-
}
}
@@ -833,7 +1130,6 @@ void threadSOG::computeSOGLace(LDDGraph &g)
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
- m_graph->setTransition(m_transitionName);
m_nbmetastate=0;
m_MaxIntBdd=0;
@@ -842,10 +1138,10 @@ void threadSOG::computeSOGLace(LDDGraph &g)
//cout<<"Marquage initial is being built..."<<endl;
LACE_ME;
- MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&m_nonObservable,&m_tb_relation));
+ MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&NonObservable,&m_tb_relation));
- fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
+ fire=firable_obs_lace(initial_meta_state,&Observable,&m_tb_relation);
c->m_lddstate=initial_meta_state;
@@ -858,7 +1154,10 @@ 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())
{
@@ -871,18 +1170,15 @@ void threadSOG::computeSOGLace(LDDGraph &g)
while(iter!=e.second.end())
{
int t = *iter;
- cout<<"Transition order1: "<<*iter<<endl;
//e.second.erase(t);
- SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&m_nonObservable,&m_tb_relation);
+ SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&NonObservable,&m_tb_relation);
onb_it++;iter++;
}
for (unsigned int i=0; i<onb_it; i++)
{
- Set::iterator it = e.second.end();
- it--;
- int t=*it;
- e.second.erase(it);
+ int t = *e.second.end();
+ e.second.erase(t);
MDD Complete_meta_state=SYNC(Accessible_epsilon_lace);
reached_class=new LDDState;
reached_class->m_lddstate=Complete_meta_state;
@@ -896,7 +1192,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,&m_observable,&m_tb_relation);
+ fire=firable_obs_lace(Complete_meta_state,&Observable,&m_tb_relation);
m_st[0].push(Pair(couple(reached_class,Complete_meta_state),fire));
}
else
@@ -915,7 +1211,12 @@ 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 **********************************/
@@ -1021,7 +1322,6 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
- m_graph->setTransition(m_transitionName);
m_nbmetastate=0;
@@ -1032,12 +1332,12 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
//cout<<"Marquage initial is being built..."<<endl;
LACE_ME;
- MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&m_nonObservable,&m_tb_relation));
+ MDD initial_meta_state(CALL(Accessible_epsilon_lace,M0,&NonObservable,&m_tb_relation));
//lddmc_refs_spawn(SPAWN(lddmc_canonize,initial_meta_state,0,*this));
- fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
+ fire=firable_obs_lace(initial_meta_state,&Observable,&m_tb_relation);
m_nbmetastate++;
//m_old_size=lddmc_nodecount(c->m_lddstate);
//reduced_initial=lddmc_refs_sync(SYNC(lddmc_canonize));
@@ -1064,17 +1364,14 @@ cout<<"\n=========================================\n";
{
int t = *iter;
//e.second.erase(t);
- SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&m_nonObservable,&m_tb_relation);
+ SPAWN(Accessible_epsilon_lace,get_successor(e.first.second,t),&NonObservable,&m_tb_relation);
onb_it++;iter++;
}
for (unsigned int i=0; i<onb_it; i++)
{
- Set::iterator it = e.second.end();
- it--;
- int t=*it;
- e.second.erase(it);
-
+ int t = *e.second.end();
+ e.second.erase(t);
MDD Complete_meta_state=SYNC(Accessible_epsilon_lace);
lddmc_refs_push(Complete_meta_state);
@@ -1093,7 +1390,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,&m_observable,&m_tb_relation);
+ fire=firable_obs_lace(Complete_meta_state,&Observable,&m_tb_relation);
m_st[0].push(Pair(couple(reached_class,Complete_meta_state),fire));
}
else
@@ -1113,3 +1410,4 @@ cout<<"\n=========================================\n";
std::cout << "TIME OF CONSTRUCTION OF THE SOG " << tps << " seconds\n";
}
+
diff --git a/src/threadSOG.h b/src/threadSOG.h
index d6dc0a14b1f27f6ca7765f0c36699e1e740795a9..977526a655bf712fb4e390afa1ff66943f90ab99 100644
--- a/src/threadSOG.h
+++ b/src/threadSOG.h
@@ -12,53 +12,70 @@
#include <sys/types.h>
#include <unistd.h>
#include "LDDGraph.h"
-#include "TransSylvan.h"
-#include "CommonSOG.h"
-
-
-
+#include "TransSylvan.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 : public CommonSOG{
+class threadSOG {
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();
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;
@@ -74,7 +91,7 @@ class threadSOG : public CommonSOG{
int m_min_charge;
-
+ net m_net;
int m_bound, m_init;
int m_id_thread;
pthread_mutex_t m_mutex;