diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index dcc56ac45c9c3e3b04ccff9b5d53e05fe0566395..f4953cc3b80278b1043e7a2978f3cf5f81382792 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -18,7 +18,11 @@ 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/"
+)
@@ -26,6 +30,10 @@ set_target_properties(spot PROPERTIES
# Hybrid SOG executable
add_executable(hybrid-sog main.cpp
+ NewNet.cpp
+ NewNet.h
+ CommonSOG.cpp
+ CommonSOG.h
DistributedSOG.cpp
DistributedSOG.h
HybridSOG.cpp
@@ -33,12 +41,22 @@ 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 38b11a187cfec559d285d766b8d9216f87ec4cad..5c45ea7e9e1cc6d689e69cbcd85a6cff4b301f52 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 "bddx.h"
+#include "bdd.h"
//#include <map.h>
#include<unordered_map>
#include <set>
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index ead7db62075752e4aacfbc244895e8c095f87bb7..410d9d5b38dbd51487b4a3bed73c50c98e09fc69 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -172,3 +172,44 @@ unsigned int CommonSOG::getPlacesCount() {
return m_nbPlaces;
}
+/**** Detect divergence in an agregate ****/
+bool CommonSOG::Set_Div(MDD &M) const
+{
+ if (m_nonObservable.empty())
+ return false;
+ Set::const_iterator i;
+ MDD Reached,From;
+ //cout<<"Ici detect divergence \n";
+ Reached=M;
+ do
+ {
+ From=Reached;
+ for(i=m_nonObservable.begin();!(i==m_nonObservable.end());i++)
+ {
+
+ MDD To= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
+ Reached=lddmc_union_mono(Reached,To);
+ //Reached=To;
+ }
+ if(Reached==From) return true;
+
+ }while(Reached!=lddmc_false && Reached != From);
+ // cout<<"PAS DE SEQUENCE DIVERGENTE \n";
+ return false;
+}
+
+/**** Detetc deadlocks ****/
+bool CommonSOG::Set_Bloc(MDD &M) const
+{
+
+ MDD cur=lddmc_true;
+ for(vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i!=m_tb_relation.end();i++)
+ {
+
+ cur=cur&(TransSylvan(*i).getMinus());
+
+ }
+return ((M&cur)!=lddmc_false);
+ //BLOCAGE
+}
+
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 2132dca6f5ac2cc8dbab0d379253cc4993623c3a..8ff04f23577a3cda6a6689f4da05130090b3a513 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -2,7 +2,7 @@
#define COMMONSOG_H
#include "LDDGraph.h"
#include "TransSylvan.h"
-#include "Net.hpp"
+#include "NewNet.h"
#include <stack>
typedef pair<LDDState *, MDD> couple;
@@ -19,7 +19,7 @@ class CommonSOG
Set * getNonObservable();
unsigned int getPlacesCount();
protected:
- net m_net;
+ NewNet m_net;
int m_nbPlaces = 0;
LDDGraph *m_graph;
vector<TransSylvan> m_tb_relation;
@@ -28,7 +28,8 @@ class CommonSOG
Set m_observable;
Set m_nonObservable;
Set InterfaceTrans;
- Set Formula_Trans;
+ Set m_place_proposition;
+
vector<class Transition> transitions;
MDD Accessible_epsilon(MDD From);
@@ -36,6 +37,8 @@ class CommonSOG
MDD get_successor(MDD From, int t);
MDD ImageForward(MDD From);
MDD Canonize(MDD s, unsigned int level);
+ bool Set_Div(MDD &M) const;
+ bool Set_Bloc(MDD &M) const;
private:
};
diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 73832c1ff022f188863bdbb5ec5df39c42417da1..3c5a77cd18cacaaafc41c5963fb336c2a22d4d2f 100644
--- a/src/DistributedSOG.cpp
+++ b/src/DistributedSOG.cpp
@@ -25,13 +25,7 @@ using namespace sylvan;
/**************************************************/
-
-
-
-const vector<class Place> *__vplaces = NULL;
-
-
-DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
+DistributedSOG::DistributedSOG(const NewNet &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;
- Formula_Trans=R.Formula_Trans;
- transitionName=R.transitionName;
+ m_observable=R.Observable;
+ m_nonObservable=R.NonObservable;
+ m_place_proposition=R.m_formula_place;
+ 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;
@@ -129,7 +123,7 @@ void *DistributedSOG::doCompute()
Pair S;
// pile m_st;
- unsigned char msg[LENGTH_ID];
+ char msg[LENGTH_ID];
int v_nbmetastate=0;
int term=0;
@@ -150,7 +144,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);
@@ -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,10 +199,10 @@ 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);
+ lddmc_getsha(lddmarq, msg);
int destination=(int)abs((msg[0])%n_tasks);
@@ -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)
{
@@ -639,7 +572,7 @@ char * DistributedSOG::concat_string(const char *s1,int longueur1,const char *s2
}
-void DistributedSOG::strcpySHA(unsigned char *dest,const unsigned char *source)
+void DistributedSOG::strcpySHA(char *dest,const char *source)
{
for (int i=0; i<LENGTH_ID; i++)
{
@@ -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 ed845624cee0b7499ac6d6bbec6637fa6d0d3df7..d608110c62b977eabb3e65b0572268e89cff5b48 100644
--- a/src/DistributedSOG.h
+++ b/src/DistributedSOG.h
@@ -3,7 +3,7 @@
// #include "RdPBDD.h"
#include <stack>
#include <vector>
-#include "Net.hpp"
+#include "NewNet.h"
// #include "MDD.h"
//#include "MDGraph.h"
//#include "bvec.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,20 +41,17 @@
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);
+ DistributedSOG(const NewNet &, int BOUND = 32, bool init = false);
void buildFromNet(int index);
void computeDSOG(LDDGraph &g);
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,34 +59,20 @@ 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();
- void strcpySHA(unsigned char *dest, const unsigned char *source);
+ void strcpySHA(char *dest, const 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;
@@ -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 02c7b65549189792d66ca85ce12906d03a3dcba5..8ca3114fbe84ef951d22f668db67ba40b54a6802 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;
@@ -50,7 +50,7 @@ const vector<class Place> *_vplaces = NULL;
} */
-HybridSOG::HybridSOG(const net &R, int BOUND,bool init)
+HybridSOG::HybridSOG(const NewNet &R, int BOUND,bool init)
{
@@ -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;
- Formula_Trans=R.Formula_Trans;
- transitionName=R.transitionName;
+ m_observable=R.Observable;
+ m_nonObservable=R.NonObservable;
+ m_place_proposition=R.m_formula_place;
+ 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 8011e98f1226c73c4c5392e6d9a889b5b44a0363..f480981e0704aaae9f072d1c5f75b505c63b322b 100644
--- a/src/HybridSOG.h
+++ b/src/HybridSOG.h
@@ -3,7 +3,7 @@
#include <stack>
#include <vector>
-#include "Net.hpp"
+#include "NewNet.h"
// #include "MDD.h"
//#include "MDGraph.h"
//#include "bvec.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 NewNet &, 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 8a7bc244ee542a6ff27aedd88c064bdebdfd1d44..13a89d31b4646fda81c3f422c23739b11eebd0ed 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,6 +14,10 @@ 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)
{
@@ -104,7 +108,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);
@@ -119,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;
@@ -172,33 +173,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 4399850d93fa6a27c57e1e763da4e3bae0cdddf6..3c1b356dae33d2e4891827dca50c3db89dec2d51 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -4,18 +4,21 @@
//#include "LDDStateExtend.h"
using namespace std;
#include <iostream>
-
+#include <map>
typedef set<int> Set;
typedef vector<LDDState*> MetaLDDNodes;
class LDDGraph
{
private:
- MDD * m_tab;
+ map<string,int>* m_transition;
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;
@@ -35,6 +38,7 @@ 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 616246c9f50feee32877293a08139d3907444bc6..a6f372b3af40b1a4f516c2de908a5cbc5aa4659e 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -24,3 +24,7 @@ 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 17b342002c7c96195fc97d3f8b871cf07c50a12e..4337d85aa02a692107d5cc4382a10c31d06156fd 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -16,6 +16,7 @@ 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);
@@ -28,7 +29,10 @@ class LDDState {
bool m_visited;
bool isVirtual();
void setVirtual();
-
+ void setDiv(bool di) {m_boucle=di;}
+ bool isDiv() {return m_boucle;}
+ void setDeadLock(bool de) {m_blocage=de;}
+ bool isDeadLock() {return m_blocage;}
protected:
private:
bool m_virtual = false;
diff --git a/src/NewNet.cpp b/src/NewNet.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..e9d7625eca23b737b040dae2caa1eb7845ebbd49
--- /dev/null
+++ b/src/NewNet.cpp
@@ -0,0 +1,551 @@
+#include "NewNet.h"
+#include <spot/misc/version.hh>
+#include <spot/twaalgos/dot.hh>
+#include <spot/tl/parse.hh>
+#include <spot/tl/print.hh>
+#include <spot/twaalgos/translate.hh>
+#include <spot/twaalgos/emptiness.hh>
+
+
+#include <algorithm>
+#include <ext/hash_map>
+#include <iomanip>
+#include <iostream>
+#include <fstream>
+#include <map>
+#include <string>
+#include <vector>
+
+
+#define TAILLEBUFF 500
+using namespace std;
+/***********************************************************/
+/* class Node */
+/***********************************************************/
+
+void Node::addPre(int node, int valuation) {
+ pair<int, int> x(node, valuation);
+ pre.push_back(x);
+}
+
+void Node::addPost(int node, int valuation) {
+ pair<int, int> x(node, valuation);
+ post.push_back(x);
+}
+
+void Node::addInhibitor(int node, int valuation) {
+ pair<int, int> x(node, valuation);
+ inhibitor.push_back(x);
+}
+
+void Node::addPreAuto(int node, int valuation) {
+ pair<int, int> x(node, valuation);
+ preAuto.push_back(x);
+}
+
+void Node::addPostAuto(int node, int valuation) {
+ pair<int, int> x(node, valuation);
+ postAuto.push_back(x);
+}
+
+void Node::addReset(int node) { reset.push_back(node); }
+
+/***********************************************************/
+/* class RdPE */
+/***********************************************************/
+NewNet::NewNet(const char *f, const char *Formula_trans, const char *Int_trans) {
+
+ cout << "CREATION D'UN NOUVEAU SOUS-RESEAU \n";
+ if (create(f)) {
+ for (vector<class Place>::iterator p = places.begin(); p != places.end();
+ p++) {
+ sort(p->pre.begin(), p->pre.end());
+ sort(p->post.begin(), p->post.end());
+ }
+ for (vector<class Transition>::iterator p = transitions.begin();
+ p != transitions.end(); p++) {
+ sort(p->pre.begin(), p->pre.end());
+ sort(p->post.begin(), p->post.end());
+ }
+ } else {
+ places.clear();
+ transitions.clear();
+ placeName.clear();
+ transitionName.clear();
+ }
+ if (strlen(Formula_trans) > 0) {
+ cout<<"transitions de la formule non vide \n";
+
+ Set_Formula_Trans(Formula_trans);
+ if (strlen(Int_trans) > 0) {
+ Set_Interface_Trans(Int_trans);
+ // cout<<"transitions de l'interface non vide \n";
+ }
+ cout << "______________66666666666666666666666______________________\n";
+ set_union(InterfaceTrans.begin(), InterfaceTrans.end(),
+ Formula_Trans.begin(), Formula_Trans.end(),
+ inserter(Observable, Observable.begin()));
+ Set_Non_Observables();
+ } else
+ for (unsigned int i = 0; i < transitions.size(); i++) Observable.insert(i);
+ cout << "FIN CREATION \n";
+}
+/***************************** Constructor for Model checker******************/
+NewNet::NewNet(const char *f, const set<string> & f_trans) {
+
+ cout << "CREATION D'UN NOUVEAU SOUS-RESEAU \n";
+ if (create(f)) {
+ for (vector<class Place>::iterator p = places.begin(); p != places.end();
+ p++) {
+ sort(p->pre.begin(), p->pre.end());
+ sort(p->post.begin(), p->post.end());
+ }
+ for (vector<class Transition>::iterator p = transitions.begin();
+ p != transitions.end(); p++) {
+ sort(p->pre.begin(), p->pre.end());
+ sort(p->post.begin(), p->post.end());
+ }
+ } else {
+ places.clear();
+ transitions.clear();
+ placeName.clear();
+ transitionName.clear();
+ }
+ if (f_trans.size() > 0) {
+ cout<<"Transition set of formula is not empty\n";
+ for (set<string>::iterator p=f_trans.begin();p!=f_trans.end();p++) {
+ cout<<"Transition observable :"<<*p<<endl;
+ }
+ setListObservable(f_trans);
+ //for(Set::iterator p=Formula_Trans.begin();p!=Formula_Trans
+
+ cout << "______________66666666666666666666666______________________\n";
+ cout<<"Formula trans size "<<Formula_Trans.size()<<endl;
+ cout<<"Interface trans size "<<InterfaceTrans.size()<<endl;
+ set_union(InterfaceTrans.begin(), InterfaceTrans.end(),
+ Formula_Trans.begin(), Formula_Trans.end(),
+ inserter(Observable, Observable.begin()));
+ Set_Non_Observables();
+ } else
+ for (unsigned int i = 0; i < transitions.size(); i++) Observable.insert(i);
+ cout << "FIN CREATION \n";
+}
+/*---------------------------------Init Set of transitions
+ * ------------------------------*/
+ void NewNet::setListObservable(const set<string> & list_t) {
+ int pos_trans(TRANSITIONS T, string trans);
+ for (set<string>::const_iterator i=list_t.begin();i!=list_t.end();i++) {
+ int pos = pos_trans(transitions, *i);
+ if (pos==-1) {
+ cout<<"Error: "<<*i<<" is not a transition!"<<endl;
+ // Check if the proposition corresponds to a place
+ map<string, int>::iterator pi = placeName.find(*i);
+ if (pi!=placeName.end()) cout<<"Place was found!"<<endl;
+ m_formula_place.insert(pi->second);
+
+ } else {
+ Formula_Trans.insert(pos);
+ cout<<"Transition found pos="<<pos<<endl;
+ map<string,int>::iterator ti=transitionName.find(*i);
+ cout<<"pos= "<<ti->second<<endl;
+ }
+ }
+ }
+
+/*---------------------------------Set_formula_trans()------------------*/
+bool NewNet::Set_Formula_Trans(const char *f) {
+ FILE *in;
+ int i, nb;
+
+ // cout<<"ici set formula transitions \n";
+ int pos_trans(TRANSITIONS, string);
+ char Buff[TAILLEBUFF], *z;
+
+
+ in = fopen(f, "r");
+ if (in == NULL) {
+ cout << "file " << f << " doesn't exist" << endl;
+ exit(1);
+ }
+ int nb_formula_trans;
+ fscanf(in, "%d\n", &nb_formula_trans);
+ nb = fread(Buff, 1, TAILLEBUFF - 1, in);
+ Buff[nb] = '\0';
+ z = strtok(Buff, " \t\n");
+ cout << "taille " << TAILLEBUFF << " buff " << Buff << " z: " << z << endl;
+ for (i = 0; i < nb_formula_trans; i++) {
+ cout << " z: " << z << endl;
+ if (z == NULL) {
+ cout << "error in formula trans format " << endl;
+ return false;
+ }
+ string tmp(z);
+ int pos = pos_trans(transitions, tmp);
+ if (pos == -1) {
+ cout << z << " Error??? : observale transition " << tmp
+ << " doesn't exist \n";
+ // return false;
+ } else
+ Formula_Trans.insert(pos);
+ /*cout<<"insertion de :"<<transitions[pos].name<<endl;*/
+ z = strtok(NULL, " \t\n");
+ if (z == NULL) {
+ nb = fread(Buff, 1, TAILLEBUFF - 1, in);
+ Buff[nb] = '\0';
+ z = strtok(Buff, " \t\n");
+ }
+ }
+ fclose(in);
+ return true;
+}
+/*---------------------------------Set_Interface_trans()------------------*/
+bool NewNet::Set_Interface_Trans(const char *f) {
+ FILE *in;
+ int i, nb;
+ int pos_trans(TRANSITIONS, string);
+ char Buff[TAILLEBUFF], *z;
+ in = fopen(f, "r");
+ if (in == NULL) {
+ cout << "file " << f << " doesn't exist" << endl;
+ exit(1);
+ }
+ int int_trans;
+ fscanf(in, "%d\n", &int_trans);
+ nb = fread(Buff, 1, TAILLEBUFF - 1, in);
+ Buff[nb] = '\0';
+ z = strtok(Buff, " \t\n");
+ cout << "taille " << TAILLEBUFF << " buff " << Buff << " z: " << z << endl;
+ for (i = 0; i < int_trans; i++) {
+ cout << " z: " << z << endl;
+ if (z == NULL) {
+ cout << "error in interface format " << endl;
+ return false;
+ }
+ string tmp(z);
+ int pos = pos_trans(transitions, tmp);
+ // if(Formula_Trans.find(pos)==Formula_Trans.end())
+ if (pos == -1) {
+ cout << z << " Error??? : interface transition doesn't exist \n";
+ // return false;
+ } else
+ InterfaceTrans.insert(pos);
+ z = strtok(NULL, " \t\n");
+ if (z == NULL) {
+ nb = fread(Buff, 1, TAILLEBUFF - 1, in);
+ Buff[nb] = '\0';
+ z = strtok(Buff, " \t\n");
+ }
+ }
+ fclose(in);
+ return true;
+}
+/*---------------------------------Set_Non_Observables()------------------*/
+void NewNet::Set_Non_Observables() {
+ NonObservable.clear();
+ for (unsigned int i = 0; i < transitions.size(); i++)
+ if (Observable.find(i) == Observable.end()) {
+ NonObservable.insert(i);
+ }
+}
+/*-----------------------pos_trans()--------------------*/
+int pos_trans(TRANSITIONS T, string trans) {
+ int pos = 0;
+ // cout<<"on cherche "<<trans<<" dans :\n";
+ for (TRANSITIONS::const_iterator i = T.begin(); !(i == T.end()); i++, pos++) {
+ // cout<<i->name<<" ";
+ if (i->name == trans) return pos;
+ }
+ // cout<<"Non trouve :\n";
+ return -1;
+}
+/* ------------------------------ operator<< -------------------------------- */
+ostream &operator<<(ostream &os, const Set &s) {
+ bool b = false;
+
+ if (s.size()) {
+ for (Set::const_iterator i = s.begin(); !(i == s.end()); i++) {
+ if (b)
+ os << ", ";
+ else
+ os << "{";
+ os << *i << " ";
+ b = true;
+ }
+ os << "}";
+ } else
+ os << "empty set";
+ return os;
+}
+/*----------------------------------------------------------------------*/
+bool NewNet::addPlace(const string &place, int marking, int capacity) {
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end()) {
+ placeName[place] = places.size();
+ Place p(place, marking, capacity);
+ places.push_back(p);
+ return true;
+ } else
+ return false;
+}
+
+bool NewNet::addQueue(const string &place, int capacity) {
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end()) {
+ placeName[place] = places.size();
+ Place p(place, -1, capacity);
+ places.push_back(p);
+ return true;
+ } else
+ return false;
+}
+
+bool NewNet::addLossQueue(const string &place, int capacity) {
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end()) {
+ placeName[place] = places.size();
+ Place p(place, -2, capacity);
+ places.push_back(p);
+ return true;
+ } else
+ return false;
+}
+
+bool NewNet::addTrans(const string &trans) {
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end()) {
+ transitionName[trans] = transitions.size();
+ Transition t(trans);
+ transitions.push_back(t);
+ return true;
+ } else
+ return false;
+}
+
+bool NewNet::addPre(const string &place, const string &trans, int valuation) {
+ int p, t;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end() || places[pi->second].isQueue())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ transitions[t].addPre(p, valuation);
+ places[p].addPost(t, valuation);
+ return true;
+}
+
+bool NewNet::addPost(const string &place, const string &trans, int valuation) {
+ int p, t;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end() || places[pi->second].isQueue())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ transitions[t].addPost(p, valuation);
+ places[p].addPre(t, valuation);
+ return true;
+}
+
+bool NewNet::addPreQueue(const string &place, const string &trans, int valuation) {
+ int p, t;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end() || !places[pi->second].isQueue())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ transitions[t].addPre(p, valuation);
+ places[p].addPost(t, valuation);
+ return true;
+}
+
+bool NewNet::addPostQueue(const string &place, const string &trans,
+ int valuation) {
+ int p, t;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end() || !places[pi->second].isQueue())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ transitions[t].addPost(p, valuation);
+ places[p].addPre(t, valuation);
+ return true;
+}
+
+bool NewNet::addInhibitor(const string &place, const string &trans,
+ int valuation) {
+ int p, t;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ transitions[t].addInhibitor(p, valuation);
+ places[p].addInhibitor(t, valuation);
+ return true;
+}
+
+bool NewNet::addPreAuto(const string &place, const string &trans,
+ const string &valuation) {
+ int p, t, v;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end() || places[pi->second].isQueue())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ map<string, int>::const_iterator pv = placeName.find(valuation);
+ if (pv == placeName.end() || places[pv->second].isQueue())
+ return false;
+ else
+ v = pv->second;
+ transitions[t].addPreAuto(p, v);
+ places[p].addPostAuto(t, v);
+ return true;
+}
+
+bool NewNet::addPostAuto(const string &place, const string &trans,
+ const string &valuation) {
+ int p, t, v;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end() || places[pi->second].isQueue())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ map<string, int>::const_iterator pv = placeName.find(valuation);
+ if (pv == placeName.end() || places[pi->second].isQueue())
+ return false;
+ else
+ v = pv->second;
+ transitions[t].addPostAuto(p, v);
+ places[p].addPreAuto(t, v);
+ return true;
+}
+
+bool NewNet::addReset(const string &place, const string &trans) {
+ int p, t;
+ map<string, int>::const_iterator pi = placeName.find(place);
+ if (pi == placeName.end())
+ return false;
+ else
+ p = pi->second;
+ map<string, int>::const_iterator ti = transitionName.find(trans);
+ if (ti == transitionName.end())
+ return false;
+ else
+ t = ti->second;
+ transitions[t].addReset(p);
+ places[p].addReset(t);
+ return true;
+}
+
+/* Visualisation */
+ostream &operator<<(ostream &os, const NewNet &R) {
+ /* affichage nombre de places et de transitions */
+ os << "***************************" << endl;
+ os << "Nombre de places :" << R.nbPlace() << endl;
+ os << "Nombre de transitions:" << R.nbTransition() << endl;
+
+ /* affichage de la liste des places */
+ os << "********** places **********" << endl;
+ int i = 0;
+ for (vector<class Place>::const_iterator p = R.places.begin();
+ p != R.places.end(); p++, i++) {
+ if (p->isQueue()) {
+ os << "queue " << setw(4) << i << ":" << p->name << ", cp(" << p->capacity
+ << ")";
+ if (p->isLossQueue()) cout << " loss";
+ cout << endl;
+ } else
+ os << "place " << setw(4) << i << ":" << p->name << ":" << p->marking
+ << " <..>, cp(" << p->capacity << ")" << endl;
+ }
+ os << "********** transitions de la formule **********" << endl;
+ for (Set::const_iterator h = R.Formula_Trans.begin();
+ !(h == R.Formula_Trans.end()); h++)
+ cout << R.transitions[*h].name << endl;
+ os << "********** transitions de l'interface **********" << endl;
+ for (Set::const_iterator h = R.InterfaceTrans.begin();
+ !(h == R.InterfaceTrans.end()); h++)
+ cout << R.transitions[*h].name << endl;
+ os << "Nombre de transitions observable:" << R.Observable.size() << endl;
+ os << "********** transitions observables **********" << endl;
+ for (Set::const_iterator h = R.Observable.begin(); !(h == R.Observable.end());
+ h++)
+ cout << R.transitions[*h].name << endl;
+ os << "Nombre de transitions non observees:" << R.NonObservable.size()
+ << endl;
+ os << "********** transitions non observees **********" << endl;
+ for (Set::const_iterator h = R.NonObservable.begin();
+ !(h == R.NonObservable.end()); h++)
+ cout << R.transitions[*h].name << endl;
+ i = 0;
+ os << "Nombre global de transitions :" << R.nbTransition() << endl;
+ os << "********** transitions **********" << endl;
+ for (TRANSITIONS::const_iterator t = R.transitions.begin();
+ t != R.transitions.end(); t++, i++) {
+ os << setw(4) << i << ":" << t->name << endl;
+
+ // os<<" IN { ";
+ // for (vector< pair<int,int> >::const_iterator
+ // a=p->pre.begin();a!=p->pre.end();a++)
+ // if (R.places[a->first].isQueue())
+ // os<<R.places[a->first].name<<":<"<<a->second<<">;";
+ // else
+ // os<<R.places[a->first].name<<":"<<a->second<<";";
+ // for (vector< pair<int,int> >::const_iterator
+ // a=p->inhibitor.begin();a!=p->inhibitor.end();a++)
+ // os<<R.places[a->first].name<<"<"<<a->second<<";";
+ // for (vector< pair<int,int> >::const_iterator
+ // a=p->preAuto.begin();a!=p->preAuto.end();a++)
+ // os<<R.places[a->first].name<<":"<<R.places[a->second].name<<";";
+ // for (vector<int>::const_iterator
+ // a=p->reset.begin();a!=p->reset.end();a++) os<<R.places[*a].name<<":
+ // reset;"; os<<" }"<<endl;
+
+ // os<<" OUT { ";
+ // for (vector< pair<int,int> >::const_iterator
+ // a=p->post.begin();a!=p->post.end();a++)
+ // if (R.places[a->first].isQueue())
+ // os<<R.places[a->first].name<<":<"<<a->second<<">;";
+ // else
+ // os<<R.places[a->first].name<<":"<<a->second<<";";
+ // for (vector< pair<int,int> >::const_iterator
+ // a=p->postAuto.begin();a!=p->postAuto.end();a++)
+ // os<<R.places[a->first].name<<":"<<R.places[a->second].name<<";";
+ // os<<" }"<<endl;
+ }
+ return (os);
+}
diff --git a/src/NewNet.h b/src/NewNet.h
new file mode 100644
index 0000000000000000000000000000000000000000..5a75757e0363086f24364a7197f230300f207fce
--- /dev/null
+++ b/src/NewNet.h
@@ -0,0 +1,114 @@
+#ifndef NEWNET_H_INCLUDED
+#define NEWNET_H_INCLUDED
+/* -*- C++ -*- */
+#ifndef NET_H
+#define NET_H
+#include <cstring>
+#include <ext/hash_map>
+#include <iostream>
+#include <map>
+#include <set>
+#include <string>
+#include <vector>
+#include "RdPMonteur.hpp"
+typedef set<int> Set;
+class Node {
+ public:
+ Node(){};
+ ~Node(){};
+ vector<pair<int, int> > pre, post, inhibitor, preAuto, postAuto;
+ vector<int> reset;
+ void addPre(int, int);
+ void addPost(int, int);
+ void addInhibitor(int, int);
+ void addPreAuto(int, int);
+ void addPostAuto(int, int);
+ void addReset(int);
+};
+
+class Place : public Node {
+ public:
+ string name;
+ int marking, capacity;
+ Place(const string &p, int m = 0, int c = 0)
+ : name(p), marking(m), capacity(c){};
+ ~Place(){};
+ bool isLossQueue() const { return marking == -2; }
+ bool isQueue() const { return marking <= -1; }
+ bool hasCapacity() const { return capacity != 0; }
+};
+
+class Transition : public Node {
+ public:
+ string name;
+ Transition(const string &t) : name(t){};
+ ~Transition(){};
+};
+/*-----------------------------------------------------------------*/
+struct ltstr {
+ bool operator()(const char *s1, const char *s2) const {
+ return std::strcmp(s1, s2) < 0;
+ }
+};
+typedef set<const char *, ltstr> Set_mot;
+typedef vector<Place> PLACES;
+typedef vector<Transition> TRANSITIONS;
+
+class NewNet : public RdPMonteur {
+ public:
+ void setListObservable(const set<string> & list_t);
+ private:
+ /*Initialisation des attributs*/
+ bool Set_Observables(const char *file);
+ bool Set_Interface_Trans(const char *file);
+ bool Set_Formula_Trans(const char *file);
+ bool Set_ObsNonObservables(Set_mot obs);
+ void Set_Non_Observables();
+
+ public:
+ /* Attributs */
+ vector<class Place> places;
+ vector<class Transition> transitions;
+ map<string, int> placeName;
+ map<string, int> transitionName;
+ Set Observable;
+ Set NonObservable;
+ Set InterfaceTrans;
+ Set Formula_Trans;
+ Set m_formula_place;
+
+ /* Constructors */
+ NewNet(){};
+ ~NewNet(){};
+ NewNet(const char *file, const char *Obs = "", const char *Int = "");
+ NewNet(const char *f, const set<string> & f_trans);
+ /* Monteur */
+ bool addPlace(const string &place, int marking = 0, int capacity = 0);
+ bool addQueue(const string &place, int capacity = 0);
+ bool addLossQueue(const string &place, int capacity = 0);
+ bool addTrans(const string &transition);
+ bool addPre(const string &place, const string &transition, int valuation = 1);
+ bool addPost(const string &place, const string &transition,
+ int valuation = 1);
+ bool addPreQueue(const string &place, const string &transition,
+ int valuation = 1);
+ bool addPostQueue(const string &place, const string &transition,
+ int valuation = 1);
+ bool addInhibitor(const string &place, const string &transition,
+ int valuation = 1);
+ bool addPreAuto(const string &place, const string &transition,
+ const string &valuation);
+ bool addPostAuto(const string &place, const string &transition,
+ const string &valuation);
+ bool addReset(const string &place, const string &transition);
+ /* Visualisation */
+ int nbPlace() const { return places.size(); };
+ int nbTransition() const { return transitions.size(); };
+};
+
+ostream &operator<<(ostream &, const NewNet &);
+#endif
+
+
+
+#endif // NEWNET_H_INCLUDED
diff --git a/src/SpotSogIterator.cpp b/src/SpotSogIterator.cpp
index 5e8c76ee01f47faceaeba7ff9a8a8ce2aa0ebc10..8d3ba3f18a99cbb23e9da527a92cb60893122882 100644
--- a/src/SpotSogIterator.cpp
+++ b/src/SpotSogIterator.cpp
@@ -6,35 +6,45 @@
SpotSogIterator::SpotSogIterator(const LDDState* lddstate):m_lddstate(lddstate)
{
-
+ //vector<pair<LDDState*, int>>
+ m_lddstate->setDiv(true);
+ for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
+ m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
+ }
+ /* if (lddstate->isDeadLock()) {
+ m_lsucc.push_back(pair(,-1));
+ }*/
+ if (lddstate->isDiv()) {
+ m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
+ }
}
bool SpotSogIterator::first() {
// m_sog->getLDDStateById(m_id)->Successors().
//return m_sog->get_successor()
m_current_edge=0;
- return m_lddstate->getSuccessors()->size()!=0;
+ return m_lsucc.size()!=0;
}
bool SpotSogIterator::next() {
m_current_edge++;
- return m_current_edge<m_lddstate->getSuccessors()->size();
+ return m_current_edge<m_lsucc.size();
}
bool SpotSogIterator::done() const {
- return m_current_edge==m_lddstate->getSuccessors()->size();
+ return m_current_edge==m_lsucc.size();
}
SpotSogState* SpotSogIterator::dst() const
{
- return new SpotSogState(m_lddstate->getSuccessors()->at(m_current_edge).first);
+ return new SpotSogState(m_lsucc.at(m_current_edge).first);
}
bdd SpotSogIterator::cond() const {
- bdd a=bddtrue;//1;
- string name=m_graph->getTransition(m_lddstate->getSuccessors()->at(m_current_edge).second);
+ if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+ string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
//cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
spot::bdd_dict *p=m_dict_ptr->get();
diff --git a/src/SpotSogIterator.h b/src/SpotSogIterator.h
index 7a25b996a07cb9663fef2b4dcf37f8a6cafc3062..152912047bde8c7599131daac5ce86cdee07b9b4 100644
--- a/src/SpotSogIterator.h
+++ b/src/SpotSogIterator.h
@@ -6,6 +6,7 @@
class SpotSogIterator : public spot::twa_succ_iterator
{
public:
+
static LDDGraph * m_graph;
static spot::bdd_dict_ptr* m_dict_ptr;
SpotSogIterator(const LDDState *lddstate);
@@ -24,6 +25,7 @@ class SpotSogIterator : public spot::twa_succ_iterator
// Associated SOG graph
LDDState * m_lddstate;
+ vector<pair<LDDState*, int>> m_lsucc;
unsigned int m_current_edge=0;
};
diff --git a/src/main.cpp b/src/main.cpp
index aa4cbab925519010dd78698db666e4e4de5dcaa3..4922e4ac340fb910e85055a20c3e665f7411310c 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -21,7 +21,8 @@
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/tl/apcollect.hh>
-#include "Net.hpp"
+#include "NewNet.h"
+#include "SogTwa.h"
@@ -31,39 +32,47 @@
using namespace std;
#define MASTER 0
-int Formula_transitions(const char * f, Set_mot& formula_trans, net Rv) ;
+int Formula_transitions(const char * f, Set_mot& formula_trans, NewNet Rv) ;
//int nb_th;
unsigned int nb_th;
int n_tasks, task_id;
-
-set<string> buildObsTransitions(const string &fileName) {
+spot::formula not_f;
+set<string> buildPropositions(const string &fileName)
+{
string input;
set<string> transitionSet;
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++)
+ {
transitionSet.insert((*i).ap_name());
}
print_spin_ltl(std::cout, fo)<<'\n';
+ cout<<"Building formula negation\n";
+ not_f = spot::formula::Not(pf.f);
return transitionSet;
}
@@ -76,11 +85,13 @@ int main(int argc, char** argv)
exit(0);*/
- if(argc<3) return 0;
- char Obs[100]="";
+ if(argc<3)
+ return 0;
+ char formula[100]="";
char Int[100]="";
- strcpy(Obs, argv[4]);
- if (argc > 6) strcpy(Int, argv[5]);
+ strcpy(formula, argv[4]);
+ if (argc > 6)
+ strcpy(Int, argv[5]);
int bound = atoi(argv[argc - 1])==0?32:atoi(argv[argc - 1]);
//if(argc>5)
@@ -88,7 +99,7 @@ int main(int argc, char** argv)
cout<<"Fichier net : "<<argv[3]<<endl;
- cout<<"Fichier formule : "<<Obs<<endl;
+ cout<<"Fichier formule : "<<formula<<endl;
cout<<"Fichier Interface : "<<Int<<endl;
cout<<"Bound : "<<argv[argc-1]<<endl;
cout<<"thread : "<<argv[2]<<endl;
@@ -103,9 +114,9 @@ int main(int argc, char** argv)
cout<<"______________________________________\n";
cout<<"Fetching formula..."<<endl;
- set<string> list_transitions=buildObsTransitions(Obs);
+ set<string> list_propositions=buildPropositions(formula);
- net R(argv[3],list_transitions);
+ NewNet R(argv[3],list_propositions);
MPI_Init (&argc, &argv );
MPI_Comm_size(MPI_COMM_WORLD,&n_tasks);
@@ -130,31 +141,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<<"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(formula);
+ 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 40da1bfa08d4963f34ce6ba30e3120665a2c5e1f..917a54ce5d2229728b79551c008eb11cc57ae5b4 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,26 +21,12 @@ 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);
- }
-} */
/*************************************************/
-threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool init)
+threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool init)
{
m_nb_thread=nbThread;
if (uselace) {
@@ -80,23 +58,27 @@ threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool ini
//_______________
transitions=R.transitions;
- Observable=R.Observable;
- NonObservable=R.NonObservable;
- Formula_Trans=R.Formula_Trans;
- 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
+ m_observable=R.Observable;
+ m_place_proposition=R.m_formula_place;
+ m_nonObservable=R.NonObservable;
+ m_transitionName=R.transitionName;
- // bvec
+ 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;}
- // Computing initial marking
+ cout<<"Transitions observables :"<<endl;
+ 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;
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++)
@@ -106,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];
@@ -198,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);
@@ -206,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++;
@@ -241,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);
@@ -255,11 +227,7 @@ 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;
@@ -336,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++;
@@ -506,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++;
@@ -527,8 +486,7 @@ void * threadSOG::doComputeCanonized()
LDDState* reached_class;
- // size_t max_meta_state_size;
- // int min_charge;
+
do
{
@@ -663,6 +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(m_transitionName);
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
@@ -711,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;
@@ -832,230 +687,17 @@ 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++)
- {
-
- cur=cur&(TransSylvan(*i).getMinus());
-
- }
-return ((M&cur)!=lddmc_false);
- //BLOCAGE
-}
-bool threadSOG::Set_Div2( const MDD &M) const
-{
- if (NonObservable.empty())
- return false;
- Set::const_iterator i;
- MDD Reached,From;
- //cout<<"Ici detect divergence \n";
- Reached=M;
- do
- {
- From=Reached;
- for(i=NonObservable.begin();!(i==NonObservable.end());i++)
- {
- // To=relation[*i](Reached);
- // Reached=Reached|To; //Reached=To ???
- MDD To= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- Reached=lddmc_union_mono(Reached,To);
- //Reached=To;
- }
- //From=Reached;
- }while(Reached!=lddmc_false && Reached != From);
- // cout<<"PAS DE SEQUENCE DIVERGENTE \n";
- return Reached != lddmc_false;
-}
-
//}
-bool threadSOG::Set_Div(MDD &M) const
-{
- if (NonObservable.empty())
- return false;
- Set::const_iterator i;
- MDD Reached,From;
- //cout<<"Ici detect divergence \n";
- Reached=M;
- do
- {
- From=Reached;
- for(i=NonObservable.begin();!(i==NonObservable.end());i++)
- {
- // To=relation[*i](Reached);
- // Reached=Reached|To; //Reached=To ???
- MDD To= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- Reached=lddmc_union_mono(Reached,To);
- //Reached=To;
- }
- 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;
-}
+
threadSOG::~threadSOG()
{
//dtor
}
-/*********Returns the count of places******************************************/
-unsigned int threadSOG::getPlacesCount() {
- return m_nbPlaces;
-}
@@ -1091,6 +733,7 @@ TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*
if(succ!=lddmc_false)
{
res.insert(*i);
+
}
}
@@ -1130,6 +773,7 @@ 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;
@@ -1138,10 +782,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;
@@ -1154,10 +798,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())
{
@@ -1170,15 +811,18 @@ 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),&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();
- e.second.erase(t);
+ Set::iterator it = e.second.end();
+ it--;
+ int t=*it;
+ e.second.erase(it);
MDD Complete_meta_state=SYNC(Accessible_epsilon_lace);
reached_class=new LDDState;
reached_class->m_lddstate=Complete_meta_state;
@@ -1192,7 +836,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
@@ -1211,12 +855,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 **********************************/
@@ -1322,6 +961,7 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
+ m_graph->setTransition(m_transitionName);
m_nbmetastate=0;
@@ -1332,12 +972,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));
@@ -1364,14 +1004,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();
- e.second.erase(t);
+ Set::iterator it = e.second.end();
+ it--;
+ int t=*it;
+ e.second.erase(it);
+
MDD Complete_meta_state=SYNC(Accessible_epsilon_lace);
lddmc_refs_push(Complete_meta_state);
@@ -1390,7 +1033,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
@@ -1410,4 +1053,3 @@ 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 977526a655bf712fb4e390afa1ff66943f90ab99..f0880740447ef681031bf03b9f575a79bd34e5c2 100644
--- a/src/threadSOG.h
+++ b/src/threadSOG.h
@@ -3,7 +3,7 @@
// #include "RdPBDD.h"
#include <stack>
#include <vector>
-#include "Net.hpp"
+#include "NewNet.h"
// #include "MDD.h"
//#include "MDGraph.h"
//#include "bvec.h"
@@ -12,70 +12,47 @@
#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);
+ threadSOG(const NewNet &, 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;
@@ -91,7 +68,7 @@ class threadSOG {
int m_min_charge;
- net m_net;
+
int m_bound, m_init;
int m_id_thread;
pthread_mutex_t m_mutex;