DistributedSOG.h 3.02 KB
Newer Older
Jaime Arias's avatar
Jaime Arias committed
1
2
3
4
5
6
#ifndef DISTRIBUTEDSOG_H
#define DISTRIBUTEDSOG_H
// #include "RdPBDD.h"
#include <stack>
#include <vector>
#include "Net.hpp"
Jaime Arias's avatar
Jaime Arias committed
7
// #include "MDD.h"
Jaime Arias's avatar
Jaime Arias committed
8
9
10
11
12
13
//#include "MDGraph.h"
//#include "bvec.h"
#include <pthread.h>
#include <stdio.h>
#include <sys/types.h>
#include <unistd.h>
Jaime Arias's avatar
Jaime Arias committed
14
#include "LDDGraph.h"
Jaime Arias's avatar
Jaime Arias committed
15
#include "TransSylvan.h"
Jaime Arias's avatar
Jaime Arias committed
16
17
18

#include <mpi.h>
#include <sha2.h>
Jaime Arias's avatar
Jaime Arias committed
19
20
21
22
23
24
#include <stdio.h>
#include <sys/ipc.h>
#include <sys/shm.h>
#include <sys/types.h>
#include <cstdlib>  //std::system
#include <sstream>
Jaime Arias's avatar
Jaime Arias committed
25
26
27
28
29
30
31
//#include <boost/mpi.hpp>
#include <iostream>
#include <string>
//#include <boost/serialization/string.hpp>
//#include <boost/mpi.hpp>
#include <iostream>
#include <queue>
Jaime Arias's avatar
Jaime Arias committed
32
#include <string>
Jaime Arias's avatar
Jaime Arias committed
33
34
35
//#include <boost/serialization/string.hpp>
#include <time.h>
#include <chrono>
Jaime Arias's avatar
Jaime Arias committed
36
// namespace mpi = boost::mpi;
Jaime Arias's avatar
Jaime Arias committed
37
38
39
40

#define MASTER 0
#define large 128

Jaime Arias's avatar
Jaime Arias committed
41
typedef pair<LDDState *, MDD> couple;
Jaime Arias's avatar
Jaime Arias committed
42
43
44
typedef pair<couple, Set> Pair;
typedef stack<Pair> pile;

Jaime Arias's avatar
Jaime Arias committed
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
// 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