Line data Source code
1 : /*******************************************************************************
2 : * *
3 : * Cosmos:(C)oncept et (O)utils (S)tatistique pour les (Mo)deles *
4 : * (S)tochastiques *
5 : * *
6 : * Copyright (C) 2009-2012 LSV & LACL *
7 : * Authors: Paolo Ballarini & Hilal Djafri *
8 : * Website: http://www.lsv.ens-cachan.fr/Software/cosmos *
9 : * *
10 : * This program is free software; you can redistribute it and/or modify *
11 : * it under the terms of the GNU General Public License as published by *
12 : * the Free Software Foundation; either version 3 of the License, or *
13 : * (at your option) any later version. *
14 : * *
15 : * This program is distributed in the hope that it will be useful, *
16 : * but WITHOUT ANY WARRANTY; without even the implied warranty of *
17 : * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *
18 : * GNU General Public License for more details. *
19 : * *
20 : * You should have received a copy of the GNU General Public License along *
21 : * with this program; if not, write to the Free Software Foundation, Inc., *
22 : * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *
23 : *******************************************************************************
24 : */
25 :
26 : #include <iostream>
27 : #include <string>
28 : #include <sstream>
29 : #include <set>
30 : #include <vector>
31 : #include <map>
32 : #include <memory>
33 :
34 : #include "spn.hpp"
35 : #include "marking.hpp"
36 :
37 : #include <stdlib.h>
38 :
39 : #ifndef _LHA_HPP
40 : #define _LHA_HPP
41 :
42 :
43 : typedef std::pair <double, double> t_interval;
44 :
45 : using namespace std;
46 :
47 : //!< A simple type to know if an edge is synchronize with the SPN.
48 : enum EdgeType {
49 : Auto, Synch
50 : };
51 :
52 : /**
53 : * Type for edge of the LHA.
54 : */
55 : struct LhaEdge {
56 : unsigned int Index;
57 : unsigned int Source;
58 : unsigned int Target;
59 : EdgeType Type;
60 : LhaEdge():Index(0),Source(0),Target(0),Type(Auto){};
61 : LhaEdge(unsigned int i,unsigned int s,unsigned int t,const EdgeType &ty):Index(i),Source(s),Target(t),Type(ty){};
62 : };
63 :
64 :
65 : /**
66 : * Auto edge need a firing time
67 : */
68 : struct _AutEdge {
69 : int Index;
70 : double FiringTime;
71 : };
72 : typedef struct _AutEdge AutEdge;
73 :
74 : /**
75 : * Strucuture for the variable of the automaton.
76 : * Implementation is provide only at runtime.
77 : */
78 : struct Variables;
79 : /**
80 : Strict order on valuation set provide at runtime.
81 : */
82 : bool varOrder(const Variables &,const Variables &);
83 :
84 : extern bool IsLHADeterministic;
85 :
86 : /**
87 : * Class implementing the Linear Hybrid Automaton.
88 : * Part of the implementation is generated at runtime for efficiency.
89 : */
90 : template<class DEDState>
91 21 : class LHA {
92 : public:
93 : LHA();
94 :
95 : // number of locations
96 : const unsigned int NbLoc;
97 :
98 : /**
99 : * Current location of the LHA
100 : */
101 : int CurrentLocation;
102 :
103 : /**
104 : * Current time of the LHA
105 : */
106 : double CurrentTime;
107 :
108 : // Result of Computation
109 : vector<double> FormulaVal;
110 : vector<bool> FormulaValQual;
111 :
112 : // Pretty printing
113 : void printHeader(ostream &)const;
114 : virtual void printState(ostream &);
115 :
116 : // Topologie of automata
117 : const size_t NbTrans;
118 : const size_t NbVar;
119 :
120 : protected:
121 :
122 : vector <LhaEdge> Edge;
123 : vector <int> EdgeCounter;
124 : set <int> InitLoc; // initial locations
125 : vector<bool> FinalLoc; // final locations
126 : vector < set <int> > Out_A_Edges; // for a given location l returns the set of autonomous edges starting from l
127 : static const int ActionEdgesAr[];
128 :
129 : // Labels for pretty printing, empty when verbose < 4
130 : vector <string> VarLabel;
131 : string label;
132 : vector <string> LocLabel;
133 :
134 : // Runtime variables
135 : Variables *Vars; // Var[i] value of the variable indexed by i
136 : Variables *tempVars; //Temporary compy of vars
137 : vector<double> LinForm;
138 : vector<double> OldLinForm;
139 : vector<double> LhaFunc;
140 : vector<double> LhaFuncDefaults;
141 :
142 :
143 : void resetVariables();
144 : void DoElapsedTimeUpdate(double, const DEDState&);
145 : double GetFlow(int, const DEDState&)const;
146 : bool CheckLocation(int,const DEDState&)const;
147 : bool CheckEdgeContraints(int,size_t, const abstractBinding&, const DEDState&)const;
148 : t_interval GetEdgeEnablingTime(int,const DEDState&)const;
149 : void DoEdgeUpdates(int, const DEDState&, const abstractBinding&);
150 : void UpdateLinForm(const DEDState&);
151 : void UpdateLhaFunc( double&);
152 : void UpdateFormulaVal(const DEDState&);
153 :
154 : double Min(double, double, double);
155 : double Max(double, double, double);
156 : double Integral(double, double, double, double, double);
157 : double BoxedIntegral(double OldInt, double t, double Delta, double x, double y, double t1,double t2);
158 : };
159 :
160 : class fullState {
161 : public:
162 : int loc;
163 : Variables* var;
164 : inline bool operator< (const fullState& other)const {
165 : return this->loc < other.loc
166 : || (this->loc == other.loc && varOrder( *(this->var), *(other.var)));
167 : }
168 : fullState();
169 : fullState(int l,const Variables &v);
170 : fullState(const fullState&);
171 : ~fullState();
172 :
173 : };
174 : #endif /* _LHA_HPP */
175 :
|
