Commit 8b9701a7 authored by Jaime Arias's avatar Jaime Arias
Browse files

First commit

parent 77e59a97
#ifndef CLASS_OF_STATE
#define CLASS_OF_STATE
using namespace std;
#include "bdd.h"
//#include <map.h>
#include<unordered_map>
#include <set>
#include <vector>
//#include <pair>
//#include <ext/hash_map>
typedef set<int> Set;
class Class_Of_State
{
public:
Class_Of_State(){boucle=blocage=Visited=0;}
Set firable;
bdd class_state;
bool boucle;
bool blocage;
bool Visited;
void * Class_Appartenance;
vector<pair<Class_Of_State*,int> > Predecessors, Successors;
pair<Class_Of_State*,int> LastEdge;
};
typedef pair<Class_Of_State*, int> Edge;
typedef vector<Edge> Edges;
#endif
This diff is collapsed.
#ifndef DISTRIBUTEDSOG_H
#define DISTRIBUTEDSOG_H
// #include "RdPBDD.h"
#include <vector>
#include <stack>
#include "Net.h"
// #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 "LDDGraph.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 <boost/mpi.hpp>
#include <iostream>
#include <string>
//#include <boost/serialization/string.hpp>
//#include <boost/mpi.hpp>
#include <iostream>
#include <string>
#include <queue>
//#include <boost/serialization/string.hpp>
#include <time.h>
#include <chrono>
//namespace mpi = boost::mpi;
#define MASTER 0
#define large 128
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
#include "LDDGraph.h"
#include <sylvan.h>
#include <stdio.h>
#include <string.h>
LDDGraph::~LDDGraph()
{
//dtor
}
void LDDGraph::setInitialState(LDDState *c)
{
m_currentstate=m_initialstate=c;
}
/*----------------------find()----------------*/
LDDState * LDDGraph::find(LDDState* c)
{
for(MetaLDDNodes::const_iterator i=m_GONodes.begin();!(i==m_GONodes.end());i++)
//if((c->class_state.id()==(*i)->class_state.id())&&(c->blocage==(*i)->blocage)&&(c->boucle==(*i)->boucle))
if(c->m_lddstate==(*i)->m_lddstate)
return *i;
return NULL;
}
/*----------------------find()----------------*/
LDDState * LDDGraph::findSHA(char* c)
{
for(MetaLDDNodes::const_iterator i=m_GONodes.begin();!(i==m_GONodes.end());i++)
if ((*i)->isVirtual()==true)
if((strcmp(c,(char*)(*i)->m_SHA2)==0))
return *i;
return NULL;
}
/*----------------------insert() ------------*/
void LDDGraph::insert(LDDState *c)
{
c->m_visited=false;
this->m_GONodes.push_back(c);
m_nbStates++;
}
/*----------------------insert() ------------*/
void LDDGraph::insertSHA(LDDState *c)
{
c->m_visited=false;
//c->setLDDValue(lddmc_false);
c->setVirtual();
this->m_GONodes.push_back(c);
}
/*----------------------NbBddNod()------------------------*/
int LDDGraph::NbBddNode(LDDState * S, size_t& nb)
{
/*if(S->m_visited==false)
{
//cout<<"insertion du meta etat numero :"<<nb<<"son id est :"<<S->class_state.id()<<endl;
//cout<<"sa taille est :"<<bdd_nodecount(S->class_state)<<" noeuds \n";
Tab[nb-1]=S->class_state;
S->Visited=true;
int bddnode=bdd_nodecount(S->class_state);
int size_succ=0;
for(Edges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++)
{
if((*i).first->Visited==false)
{
nb++;
size_succ+=NbBddNode((*i).first,nb);
}
}
return size_succ+bddnode;
}
else*/
cout<<"Not implemented yet...."<<endl;
return 0;
}
/*----------------------Visualisation du graphe------------------------*/
void LDDGraph::printCompleteInformation()
{
cout << "\n\nGRAPH SIZE : \n";
cout<< "\n\tNB MARKING : "<< m_nbMarking;
cout<< "\n\tNB NODES : "<< m_nbStates;
cout<<"\n\tNB ARCS : " <<m_nbArcs<<endl;
cout<<" \n\nCOMPLETE INFORMATION ?(y/n)\n";
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);
// cout<<"NB BDD NODE : "<<bdd_anodecount(m_Tab,(int)m_nbStates)<<endl;
//cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
InitVisit(m_initialstate,1);
//int toto;cin>>toto;
//bdd Union=UnionMetaState(initialstate,1);
//cout<<"a titre indicatif taille de l'union : "<<bdd_nodecount(Union)<<endl;
if(c=='y'||c=='Y')
{
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;
for(LDDEdges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++)
{
if((*i).first->m_visited==true)
{
nb++;
InitVisit((*i).first,nb);
}
}
}
}
/********* printGraph *****/
void LDDGraph::printGraph(LDDState *s,size_t &nb)
{
if(nb<=m_nbStates)
{
cout<<"\nSTATE NUMBER "<<nb<<" : \n";
s->m_visited=true;
printsuccessors(s);
getchar();
printpredecessors(s);
getchar();
LDDEdges::const_iterator i;
for(i=s->Successors.begin();!(i==s->Successors.end());i++)
{
if((*i).first->m_visited==false)
{
nb++;
printGraph((*i).first, 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;
}
#include "LDDState.h"
LDDState::~LDDState()
{
//dtor
}
void LDDState::setLDDValue(MDD m) {
m_lddstate=m;
}
MDD LDDState::getLDDValue() {
return m_lddstate;
}
char* LDDState::getSHAValue() {
return m_SHA2;
}
bool LDDState::isVirtual() {
return m_virtual;
}
void LDDState::setVirtual() {
m_virtual=true;
}
#include "LDDStateExtend.h"
LDDStateExtend::~LDDStateExtend()
{
//dtor
}
void LDDStateExtend::setLDDExValue(MDD m) {
m_lddstate=m;
}
MDD LDDStateExtend::getLDDExValue() {
return m_lddstate;
}
#ifndef LDDSTATEEXTEND_H_INCLUDED
#define LDDSTATEEXTEND_H_INCLUDED
#include <set>
#include <vector>
#include <sylvan.h>
#include "LDDState.h"
using namespace std;
typedef set<int> Set;
class LDDStateExtend: public LDDState
{
public:
LDDStateExtend(){m_boucle=m_blocage=m_visited=false;}
virtual ~LDDStateExtend();
bool m_exist;
void setLDDExValue(MDD m);
MDD getLDDExValue();
protected:
private:
};
typedef pair<LDDStateExtend*, int> LDDExEdge;
typedef vector<LDDEdge> LDDExEdgedges;
#endif // LDDSTATEEXTEND_H_INCLUDED
/******** Graph.cpp *******/
#include "MDGraph.h"
/*#include <conio>*/
bdd * Tab;
/********* setInitialState *****/
void MDGraph::setInitialState(Class_Of_State *c)
{
currentstate=initialstate=c;
}
/*----------------------find()----------------*/
Class_Of_State * MDGraph::find(Class_Of_State* c)
{
for(MetaGrapheNodes::const_iterator i=GONodes.begin();!(i==GONodes.end());i++)
//if((c->class_state.id()==(*i)->class_state.id())&&(c->blocage==(*i)->blocage)&&(c->boucle==(*i)->boucle))
if(c->class_state.id()==(*i)->class_state.id())
return *i;
return NULL;
}
/*----------------------insert() ------------*/
void MDGraph::insert(Class_Of_State *c)
{
c->Visited=false;
this->GONodes.push_back(c);
nbStates++;
}
/*----------------------NbBddNod()------------------------*/
int MDGraph::NbBddNode(Class_Of_State * S, size_t& nb)
{
if(S->Visited==false)
{
//cout<<"insertion du meta etat numero :"<<nb<<"son id est :"<<S->class_state.id()<<endl;
//cout<<"sa taille est :"<<bdd_nodecount(S->class_state)<<" noeuds \n";
Tab[nb-1]=S->class_state;
S->Visited=true;
int bddnode=bdd_nodecount(S->class_state);
int size_succ=0;
for(Edges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++)
{
if((*i).first->Visited==false)
{
nb++;
size_succ+=NbBddNode((*i).first,nb);
}
}
return size_succ+bddnode;
}
else
return 0;
}
/*----------------------Visualisation du graphe------------------------*/
void MDGraph::printCompleteInformation()
{
cout << "\n\nGRAPH SIZE : \n";
cout<< "\n\tNB MARKING : "<< nbMarking;
cout<< "\n\tNB NODES : "<< nbStates;
cout<<"\n\tNB ARCS : " <<nbArcs<<endl;
cout<<" \n\nCOMPLETE INFORMATION ?(y/n)\n";
char c;
cin>>c;
//InitVisit(initialstate,n);
Tab=new bdd[(int)nbStates];
size_t n=1;
//cout<<"NB BDD NODE : "<<NbBddNode(initialstate,n)<<endl;
NbBddNode(initialstate,n);
cout<<"NB BDD NODE : "<<bdd_anodecount(Tab,(int)nbStates)<<endl;
//cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
InitVisit(initialstate,1);
//int toto;cin>>toto;
//bdd Union=UnionMetaState(initialstate,1);
//cout<<"a titre indicatif taille de l'union : "<<bdd_nodecount(Union)<<endl;
if(c=='y'||c=='Y')
{
size_t n=1;
printGraph(initialstate,n);
}
}
/*----------------------InitVisit()------------------------*/
void MDGraph::InitVisit(Class_Of_State * S,size_t nb)
{
if(nb<=nbStates)
{
S->Visited=false;
for(Edges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++)
{
if((*i).first->Visited==true)
{
nb++;
InitVisit((*i).first,nb);
}
}
}
}
/********* printGraph *****/
void MDGraph::printGraph(Class_Of_State *s,size_t &nb)
{
if(nb<=nbStates)
{
cout<<"\nSTATE NUMBER "<<nb<<" : \n";
s->Visited=true;
printsuccessors(s);
getchar();
printpredecessors(s);
getchar();
Edges::const_iterator i;
for(i=s->Successors.begin();!(i==s->Successors.end());i++)
{
if((*i).first->Visited==false)
{
nb++;
printGraph((*i).first, nb);
}
}
}
}
/*---------void print_successors_class(Class_Of_State *)------------*/
void MDGraph::printsuccessors(Class_Of_State *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();
}
}
/*---------void printpredescessors(Class_Of_State *)------------*/
void MDGraph::printpredecessors(Class_Of_State *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();
}
}
/****************** Graph.hpp **************************/
#ifndef _MDGRAPH_
#define _MDGRAPH_
using namespace std;
#include <iostream>
/*#include <time>*/
#include <vector>
#include "Class_of_state.h"
#include <list>
typedef set<int> Set;
typedef vector<Class_Of_State*> MetaGrapheNodes;
class MDGraph
{
private:
void printGraph(Class_Of_State *, size_t &);
MetaGrapheNodes GONodes;
public:
void Reset();
Class_Of_State *initialstate;
Class_Of_State *currentstate;
double nbStates;
double nbMarking;
double nbArcs;
Class_Of_State* find(Class_Of_State*);
Edges& get_successor(Class_Of_State*);