Commit bb1fa072 authored by Jaime Arias's avatar Jaime Arias
Browse files

Add cmake files

parent 8b9701a7
# Created by https://www.gitignore.io/api/cmake
# Edit at https://www.gitignore.io/?templates=cmake
### CMake ###
CMakeLists.txt.user
CMakeCache.txt
CMakeFiles
CMakeScripts
Testing
Makefile
cmake_install.cmake
install_manifest.txt
compile_commands.json
CTestTestfile.cmake
build
.vscode
# End of https://www.gitignore.io/api/cmake
[submodule "third-party/buddy"]
path = third-party/buddy
url = https://github.com/jgcoded/BuDDy
[submodule "third-party/sylvan"]
path = third-party/sylvan
url = git@depot.lipn.univ-paris13.fr:PMC-SOG/sylvan.git
[submodule "libraries/parser"]
path = libraries/parser
url = git@depot.lipn.univ-paris13.fr:PMC-SOG/pn-parser.git
# set minimum cmake version
cmake_minimum_required(VERSION 3.5 FATAL_ERROR)
# project name and language
project(distributed-sog C CXX)
# add pn parser
set(PARSER_DIR "${CMAKE_SOURCE_DIR}/libraries/parser")
message(STATUS "Building Petri Net parser ...")
include_directories("${PARSER_DIR}/src")
add_subdirectory(${PARSER_DIR})
# add buddy
set(BUDDY_DIR "${CMAKE_SOURCE_DIR}/third-party/buddy")
message(STATUS "Building BuDDy library ...")
include_directories("${BUDDY_DIR}/src")
add_subdirectory(third-party/buddy)
# add sylvan
message(STATUS "Building Sylvan ...")
set(SYLVAN_DIR "${CMAKE_SOURCE_DIR}/third-party/sylvan")
include_directories(${SYLVAN_DIR})
add_subdirectory(${SYLVAN_DIR})
# add source folder
include_directories(src)
add_subdirectory(src)
# add tests
# enable_testing()
# add_subdirectory(tests)
Subproject commit 2952aa661fa7245f90f6e152c5bac76b0234e502
# set minimum cmake version
cmake_minimum_required(VERSION 3.5 FATAL_ERROR)
# include MPI
find_package(MPI REQUIRED)
include_directories(${MPI_INCLUDE_PATH})
# Thread SOG executable
add_executable(distributed-sog main.cpp
DistributedSOG.cpp
DistributedSOG.h
LDDGraph.cpp
LDDState.cpp
TransSylvan.cpp
)
target_link_libraries(distributed-sog
sylvan
bdd
RdP
${MPI_LIBRARIES}
)
#ifndef DISTRIBUTEDSOG_H
#define DISTRIBUTEDSOG_H
// #include "RdPBDD.h"
#include <vector>
#include <stack>
#include "Net.h"
#ifndef DISTRIBUTEDSOG_H
#define DISTRIBUTEDSOG_H
// #include "RdPBDD.h"
#include <stack>
#include <vector>
#include "Net.hpp"
// #include "MDD.h"
//#include "MDGraph.h"
//#include "bvec.h"
#include <pthread.h>
#include <unistd.h>
#include <sys/types.h>
#include <stdio.h>
#include "TransSylvan.h"
//#include "MDGraph.h"
//#include "bvec.h"
#include <pthread.h>
#include <stdio.h>
#include <sys/types.h>
#include <unistd.h>
#include "LDDGraph.h"
#include "TransSylvan.h"
#include <sys/types.h>
#include <sys/ipc.h>
#include <sys/shm.h>
#include <stdio.h>
#include <mpi.h>
#include <cstdlib> //std::system
#include <sstream>
#include <sha2.h>
#include <stdio.h>
#include <sys/ipc.h>
#include <sys/shm.h>
#include <sys/types.h>
#include <cstdlib> //std::system
#include <sstream>
//#include <boost/mpi.hpp>
#include <iostream>
#include <string>
//#include <boost/serialization/string.hpp>
//#include <boost/mpi.hpp>
#include <iostream>
#include <string>
#include <queue>
#include <string>
//#include <boost/serialization/string.hpp>
#include <time.h>
#include <chrono>
//namespace mpi = boost::mpi;
// namespace mpi = boost::mpi;
#define MASTER 0
#define large 128
typedef pair<LDDState*,MDD> couple;
typedef pair<LDDState *, MDD> couple;
typedef pair<couple, Set> Pair;
typedef stack<Pair> pile;
// typedef vector<Trans> vec_trans;
class DistributedSOG
{
public:
DistributedSOG(const net&,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();
void * MasterProcess();
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) ;
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;
MDD *m_TabMeta;
int m_nbmetastate;
double m_old_size;
int nb_failed;
int nb_success;
pile m_st;
void MarquageString(char *dest,const char *source);
int n_tasks, task_id;
int tag=0;
int m_charge;
MPI_Status m_status;
MPI_Request m_request;
net m_net;
int m_bound,m_init;
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,int level);
MDD ImageForward(MDD From);
// named_mutex m_initial_mtx{open_or_create, "initial"};
};
#endif // DISTRIBUTEDSOG_H
// typedef vector<Trans> vec_trans;
class DistributedSOG {
public:
DistributedSOG(const net &, 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();
void *MasterProcess();
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);
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;
MDD *m_TabMeta;
int m_nbmetastate;
double m_old_size;
int nb_failed;
int nb_success;
pile m_st;
void MarquageString(char *dest, const char *source);
int n_tasks, task_id;
int tag = 0;
int m_charge;
MPI_Status m_status;
MPI_Request m_request;
net m_net;
int m_bound, m_init;
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, int level);
MDD ImageForward(MDD From);
// named_mutex m_initial_mtx{open_or_create, "initial"};
};
#endif // DISTRIBUTEDSOG_H
#ifndef LDDGRAPH_H
#define LDDGRAPH_H
#include "LDDState.h"
//#include "LDDStateExtend.h"
using namespace std;
#include <iostream>
typedef set<int> Set;
typedef vector<LDDState*> MetaLDDNodes;
class LDDGraph
{
private:
MDD * m_tab;
void printGraph(LDDState *, size_t &);
MetaLDDNodes m_GONodes;
public:
void Reset();
LDDState *m_initialstate;
LDDState *m_currentstate;
double m_nbStates;
double m_nbMarking;
double m_nbArcs;
LDDState* find(LDDState*);
LDDState* findSHA(char*);
void insertSHA(LDDState *c);
LDDEdges& get_successor(LDDState*);
void printsuccessors(LDDState *);
int NbBddNode(LDDState*,size_t&);
void InitVisit(LDDState * S,size_t nb);
void printpredecessors(LDDState *);
void addArc(){m_nbArcs++;}
void insert(LDDState*);
LDDGraph() {m_nbStates=m_nbArcs=m_nbMarking=0;}
void setInitialState(LDDState*); //Define the initial state of this graph
void printCompleteInformation();
virtual ~LDDGraph();
};
#endif // LDDGRAPH_H
#ifndef LDDSTATE_H
#define LDDSTATE_H
#include <set>
#include <vector>
#include <sylvan.h>
using namespace std;
typedef set<int> Set;
class LDDState
{
public:
LDDState(){m_boucle=m_blocage=m_visited=false;m_virtual=false;}
virtual ~LDDState();
Set firable;
void * Class_Appartenance;
vector<pair<LDDState*,int> > Predecessors, Successors;
pair<LDDState*,int> LastEdge;
void setLDDValue(MDD m);
MDD getLDDValue();
MDD m_lddstate;
char m_SHA2[80];
char* getSHAValue();
bool m_boucle;
bool m_blocage;
bool m_visited;
bool isVirtual();
void setVirtual();
protected:
private:
bool m_virtual=false;
};
typedef pair<LDDState*, int> LDDEdge;
typedef vector<LDDEdge> LDDEdges;
#endif // LDDSTATE_H
......@@ -2,56 +2,56 @@
#define MODULAR_CLASS_OF_STATE
//#include"Modular_Edge.h"
//#include<hash_map.h>
#include"Net.h"
#include <set>
#include "Net.hpp"
//#include <vector>
#include"bdd.h"
//_____________________ Vecteur d'entier : reprsente les id des bdd relatifs un tat synchronis de n GO _________________________
//typedef vector<bdd> SynchronizedState;
//struct less_SynchronizedState
#include "bdd.h"
//_____________________ Vecteur d'entier : reprsente les id des bdd relatifs
//� un �tat synchronis� de n GO _________________________ typedef vector<bdd>
// SynchronizedState; struct less_SynchronizedState
//{
//bool operator()(const SynchronizedState,const SynchronizedState)const;
// bool operator()(const SynchronizedState,const SynchronizedState)const;
//};
//inline bool less_SynchronizedState::operator ()(const SynchronizedState p1,const SynchronizedState p2)const
// inline bool less_SynchronizedState::operator ()(const SynchronizedState
// p1,const SynchronizedState p2)const
//{
//for(int i=0;i<p1.size();i++)
// for(int i=0;i<p1.size();i++)
// if(p1[i].id()>p2[i].id())
// return false;
//return true;
// return true;
//}
//typedef set<SynchronizedState, less_SynchronizedState> Gen_Prod_Synch;
class Modular_Class_Of_State
{
//friend struct less_modular_class_of_state;
public:
Modular_Class_Of_State(){boucle=blocage=Visited=0;}
vector <bdd> State;
bool boucle;
bool blocage;
bool Visited;
set<pair<Modular_Class_Of_State*, string> > Predecessors;
set<pair<Modular_Class_Of_State*, string> > Successors;
friend ostream& operator<<(ostream &os,const Modular_Class_Of_State &c){
os<<"{";
for(unsigned int k=0;k<c.State.size();k++)
os<<c.State[k].id()<<", ";
os<<"}";
return(os);}
// typedef set<SynchronizedState, less_SynchronizedState> Gen_Prod_Synch;
class Modular_Class_Of_State {
// friend struct less_modular_class_of_state;
public:
Modular_Class_Of_State() { boucle = blocage = Visited = 0; }
vector<bdd> State;
bool boucle;
bool blocage;
bool Visited;
set<pair<Modular_Class_Of_State *, string> > Predecessors;
set<pair<Modular_Class_Of_State *, string> > Successors;
friend ostream &operator<<(ostream &os, const Modular_Class_Of_State &c) {
os << "{";
for (unsigned int k = 0; k < c.State.size(); k++)
os << c.State[k].id() << ", ";
os << "}";
return (os);
}
};
/*____________________ MODULAR EDGE________________*/
class Modular_Class_Of_State;
typedef pair<Modular_Class_Of_State*, string> Modular_Edge;
struct LessModularEdge
{
bool operator()(const Modular_Edge,const Modular_Edge)const;
typedef pair<Modular_Class_Of_State *, string> Modular_Edge;
struct LessModularEdge {
bool operator()(const Modular_Edge, const Modular_Edge) const;
};
inline bool LessModularEdge::operator ()(const Modular_Edge a1,const Modular_Edge a2)const
{
//cout<<"on compare les etiquettes des arcs : "<<a1.second<<" avec "<<a2.second<<endl;
return (a1.first<a2.first);
inline bool LessModularEdge::operator()(const Modular_Edge a1,
const Modular_Edge a2) const {
// cout<<"on compare les etiquettes des arcs : "<<a1.second<<" avec
// "<<a2.second<<endl;
return (a1.first < a2.first);
}
typedef set<Modular_Edge,LessModularEdge> Modular_Edges;
typedef set<Modular_Edge, LessModularEdge> Modular_Edges;
#endif
......@@ -2,50 +2,53 @@
#ifndef RdPBDD_H
#define RdPBDD_H
#include <math.h>
#include "bvec.h"
#include <vector>
#include <stack>
#include "Net.h"
#include "bdd.h"
#include"MDGraph.h"
#include"Modular_Obs_Graph.h"
#include <vector>
#include "MDGraph.h"
#include "Modular_Class_of_state.h"
#include "Modular_Obs_Graph.h"
#include "Net.hpp"
#include "bdd.h"
#include "bvec.h"
//#include"Modular_Obs_Graph.hpp"
/***********************************************/
class Trans {
public:
Trans(const bdd& var, bddPair* pair, const bdd& rel,const bdd& prerel,const bdd& Precond, const bdd& Postcond);
bdd operator()(const bdd& op) const;
bdd operator[](const bdd& op) const;
public:
Trans(const bdd& var, bddPair* pair, const bdd& rel, const bdd& prerel,
const bdd& Precond, const bdd& Postcond);
bdd operator()(const bdd& op) const;
bdd operator[](const bdd& op) const;
friend class RdPBDD;
private:
bdd var;
bddPair* pair;
bdd Precond;
bdd Postcond;
bdd rel;
bdd prerel;
private:
bdd var;
bddPair* pair;
bdd Precond;
bdd Postcond;
bdd rel;
bdd prerel;
};
class RdPBDD {
private :
private:
vector<class Transition> transitions;
Set Observable;
Set NonObservable;
map<string,int> transitionName;
map<string, int> transitionName;
Set InterfaceTrans;
Set Formula_Trans;
unsigned int Nb_places;
public:
public:
bdd M0;
bdd currentvar;
vector<Trans> relation;
bdd ReachableBDD1();
bdd ReachableBDD2();
bdd ReachableBDD3();
/* Gnration de graphes d'observation */
void compute_canonical_deterministic_graph_Opt(MDGraph& g) ;
/* G�n�ration de graphes d'observation */
void compute_canonical_deterministic_graph_Opt(MDGraph& g);
bdd Accessible_epsilon(bdd From);
bdd Accessible_epsilon2(bdd From);
bdd StepForward(bdd From);
......@@ -54,31 +57,35 @@ void compute_canonical_deterministic_graph_Opt(MDGraph& g) ;
bdd StepBackward2(bdd From);
bdd EmersonLey(bdd S, bool trace);
Set firable_obs(bdd State);
bdd get_successor(bdd From,int t);
void GeneralizedSynchProduct1(Modular_Obs_Graph& Gv, int NbSubnets,RdPBDD* Subnets[] ,int nbbddvar) ;
bool Set_Div(bdd &S) const;
bool Set_Bloc(bdd &S) const;
bdd FrontiereNodes(bdd From) const ;
bdd CanonizeR(bdd s, unsigned int i) ;
RdPBDD(const net&,int BOUND=32,bool init=false);
bdd get_successor(bdd From, int t);
void GeneralizedSynchProduct1(Modular_Obs_Graph& Gv, int NbSubnets,
RdPBDD* Subnets[], int nbbddvar);
bool Set_Div(bdd& S) const;
bool Set_Bloc(bdd& S) const;
bdd FrontiereNodes(bdd From) const;
bdd CanonizeR(bdd s, unsigned int i);
RdPBDD(const net&, int BOUND = 32, bool init = false);
~RdPBDD(){};
};
/*____________Structure utiles aux produit synchronis gnralis de n graphes d'observations ________*/
/*____________Structure utiles aux produit synchronis� g�n�ralis� de n graphes
* d'observations ________*/
/*typedef pair<Modular_Class_Of_State*,bdd*> CoupleNodes; // Mta-tat (canonis) + vecteur des bdds complets
typedef pair<Set*,Set*> CoupleSets;//ens d'ens des trans de la formule franchissables non encore traites + ens d'ens des trans de l'interface franchissables non encore traites
typedef pair<CoupleNodes,CoupleSets> PairProduct; // Couple + ens des ens des transitions franchissables non encore traites
typedef pair<PairProduct,bool> StackElt;
typedef vector<StackElt> Stack;*/
typedef pair<Modular_Class_Of_State*,bdd*> Couple;
typedef pair<Couple,Set*> StackElt;
/*typedef pair<Modular_Class_Of_State*,bdd*> CoupleNodes; // M�ta-�tat
(canonis�) + vecteur des bdds complets typedef pair<Set*,Set*> CoupleSets;//ens
d'ens des trans de la formule franchissables non encore trait�es + ens d'ens des
trans de l'interface franchissables non encore trait�es typedef