RdPBDD.h 2.73 KB
Newer Older
Jaime Arias's avatar
Jaime Arias committed
1
2
3
4
5
/* -*- C++ -*- */
#ifndef RdPBDD_H
#define RdPBDD_H
#include <math.h>
#include <stack>
Jaime Arias's avatar
Jaime Arias committed
6
7
#include <vector>
#include "MDGraph.h"
Jaime Arias's avatar
Jaime Arias committed
8
#include "Modular_Class_of_state.h"
Jaime Arias's avatar
Jaime Arias committed
9
10
11
12
#include "Modular_Obs_Graph.h"
#include "Net.hpp"
#include "bdd.h"
#include "bvec.h"
Jaime Arias's avatar
Jaime Arias committed
13
14
15
//#include"Modular_Obs_Graph.hpp"
/***********************************************/
class Trans {
Jaime Arias's avatar
Jaime Arias committed
16
17
18
19
20
 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;
Jaime Arias's avatar
Jaime Arias committed
21
22

  friend class RdPBDD;
Jaime Arias's avatar
Jaime Arias committed
23
24
25
26
27
28
29
30

 private:
  bdd var;
  bddPair* pair;
  bdd Precond;
  bdd Postcond;
  bdd rel;
  bdd prerel;
Jaime Arias's avatar
Jaime Arias committed
31
32
33
};

class RdPBDD {
Jaime Arias's avatar
Jaime Arias committed
34
 private:
Jaime Arias's avatar
Jaime Arias committed
35
36
37
  vector<class Transition> transitions;
  Set Observable;
  Set NonObservable;
Jaime Arias's avatar
Jaime Arias committed
38
  map<string, int> transitionName;
Jaime Arias's avatar
Jaime Arias committed
39
40
41
  Set InterfaceTrans;
  Set Formula_Trans;
  unsigned int Nb_places;
Jaime Arias's avatar
Jaime Arias committed
42
43

 public:
Jaime Arias's avatar
Jaime Arias committed
44
45
46
47
48
49
  bdd M0;
  bdd currentvar;
  vector<Trans> relation;
  bdd ReachableBDD1();
  bdd ReachableBDD2();
  bdd ReachableBDD3();
Jaime Arias's avatar
Jaime Arias committed
50
51
  /* G�n�ration de graphes d'observation */
  void compute_canonical_deterministic_graph_Opt(MDGraph& g);
Jaime Arias's avatar
Jaime Arias committed
52
53
54
55
56
57
58
59
  bdd Accessible_epsilon(bdd From);
  bdd Accessible_epsilon2(bdd From);
  bdd StepForward(bdd From);
  bdd StepForward2(bdd From);
  bdd StepBackward(bdd From);
  bdd StepBackward2(bdd From);
  bdd EmersonLey(bdd S, bool trace);
  Set firable_obs(bdd State);
Jaime Arias's avatar
Jaime Arias committed
60
61
62
63
64
65
66
67
  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);
Jaime Arias's avatar
Jaime Arias committed
68
69
  ~RdPBDD(){};
};
Jaime Arias's avatar
Jaime Arias committed
70
71
/*____________Structure utiles aux produit synchronis� g�n�ralis� de n graphes
 * d'observations ________*/
Jaime Arias's avatar
Jaime Arias committed
72

Jaime Arias's avatar
Jaime Arias committed
73
74
75
76
77
78
79
80
81
/*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
pair<CoupleNodes,CoupleSets> PairProduct; // Couple + ens des ens des
transitions franchissables non encore trait�es typedef pair<PairProduct,bool>
StackElt; typedef vector<StackElt> Stack;*/
typedef pair<Modular_Class_Of_State*, bdd*> Couple;
typedef pair<Couple, Set*> StackElt;
Jaime Arias's avatar
Jaime Arias committed
82
83
typedef stack<StackElt> Stack;
typedef vector<StackElt> PileInt;
Jaime Arias's avatar
Jaime Arias committed
84
85
typedef pair<StackElt, PileInt> CanonicRep;
// typedef stack<CanonicRep> STACK;
Jaime Arias's avatar
Jaime Arias committed
86
typedef stack<PileInt> STACK;
Jaime Arias's avatar
Jaime Arias committed
87
88
89
int InStack(PileInt, Modular_Class_Of_State*);
bool MemeVecteur(vector<bdd>, vector<bdd>);
bool Inferieur(vector<bdd>, vector<bdd>);
Jaime Arias's avatar
Jaime Arias committed
90
91

#endif