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 "LHA.hpp"
27 : #include "LHA_orig.hpp"
28 :
29 : #include <map>
30 : #include <float.h>
31 : #include <math.h>
32 :
33 :
34 : using namespace std;
35 :
36 : template<class DEDState>
37 0 : void LHA_orig<DEDState>::copyState(LHA_orig *A){
38 0 : this->Vars = A->Vars;
39 0 : this->LinForm.swap(A->LinForm);
40 0 : this->OldLinForm.swap(A->OldLinForm);
41 0 : this->LhaFunc.swap(A->LhaFunc);
42 0 : this->Likelihood = A->Likelihood;
43 0 : this->CurrentTime =A->CurrentTime;
44 0 : this->CurrentLocation=A->CurrentLocation;
45 0 : }
46 :
47 :
48 :
49 : /**
50 : * This function makes the automaton takes an autonomous edge.
51 : * @param EdgeIndex the number of the edge of the LHA
52 : * @param M is the marking of the SPN
53 : */
54 : template<class DEDState>
55 242875 : void LHA_orig<DEDState>::fireAutonomous(int EdgeIndex,const DEDState &M){
56 242875 : static const abstractBinding dummyBinding;
57 242875 : this->DoEdgeUpdates(EdgeIndex, M, dummyBinding);
58 242875 : this->CurrentLocation = this->Edge[EdgeIndex].Target;
59 242875 : }
60 :
61 :
62 : /**
63 : * Find a suitable syncronized transitions in the LHA
64 : * @param tr a SPN transiiton index
65 : * @param M is the marking of the SPN
66 : * @param b a binding of the colored variable of the SPN for the transition.
67 : */
68 : template<class DEDState>
69 52293716 : int LHA_orig<DEDState>::synchroniseWith(size_t tr, const DEDState& m,const abstractBinding& b){
70 : //Check if there exist a valid transition in the automata.
71 :
72 52293716 : int SE = GetEnabled_S_Edges(tr, m, b);
73 :
74 52293716 : if (SE >= 0) {
75 : //If synchronisation is possible fire it
76 52220610 : fireLHA(SE,m, b);
77 : }
78 52293716 : return SE;
79 : }
80 :
81 : /**
82 : * Return the next autonomous edge.
83 : * @param Marking is the current marking of the Petri net.
84 : * @return the most urgent autonomous edge
85 : */
86 : template<class DEDState>
87 52534062 : AutEdge LHA_orig<DEDState>::GetEnabled_A_Edges(const DEDState& Marking) {
88 : AutEdge Ed;
89 52534062 : Ed.Index = -1;
90 52534062 : Ed.FiringTime = DBL_MAX;
91 52534062 : static const abstractBinding dummyBinding;
92 102651091 : for (auto it : this->Out_A_Edges[this->CurrentLocation]) {
93 50117029 : if (this->CheckLocation(this->Edge[it].Target, Marking) && this->CheckEdgeContraints(it, 0, dummyBinding, Marking)) {
94 49999766 : t_interval I = this->GetEdgeEnablingTime(it, Marking);
95 49999766 : if (I.first <= I.second) {
96 49999766 : if (I.first < Ed.FiringTime) {
97 49999766 : Ed.Index = it;
98 49999766 : Ed.FiringTime = I.first;
99 : }
100 :
101 : }
102 : }
103 : }
104 :
105 52534062 : return Ed;
106 : }
107 :
108 : /**
109 : * This function makes time elapse in the automaton.
110 : * @param DeltaT the ammout of time the automaton should wait.
111 : * @param Marking is the Marking of the SPN.
112 : */
113 :
114 : template<class DEDState>
115 52533409 : void LHA_orig<DEDState>::updateLHA(double DeltaT, const DEDState &Marking){
116 52533409 : this->DoElapsedTimeUpdate(DeltaT, Marking);
117 52533409 : this->UpdateLinForm(Marking);
118 52533409 : this->UpdateLhaFunc(DeltaT);
119 52533409 : this->CurrentTime += DeltaT;
120 52533409 : }
121 :
122 :
123 : /**
124 : * Reset the whole automaton to its initial state for
125 : * the given Marking.
126 : */
127 : template<class DEDState>
128 222105 : void LHA_orig<DEDState>::reset(const DEDState& Marking) {
129 222105 : Likelihood = 1.0;
130 222105 : resetLinForms();
131 222105 : this->resetVariables();
132 222105 : setInitLocation(Marking);
133 222105 : this->CurrentTime = 0;
134 222105 : }
135 :
136 :
137 :
138 : /**
139 : * This function is called when the automaton reach a final state.
140 : * The result of path formula is stored in vector v
141 : */
142 : template<class DEDState>
143 148441 : void LHA_orig<DEDState>::getFinalValues(const DEDState& m,vector<double>& v,vector<bool>& v2){
144 148441 : this->UpdateLinForm(m);
145 148441 : this->UpdateFormulaVal(m);
146 148441 : v=this->FormulaVal;
147 148441 : v2=this->FormulaValQual;
148 148441 : }
149 :
150 : /**
151 : * This function makes the automaton takes an edge.
152 : * The edge can be either a autonomous or a synchronize on.
153 : * @param EdgeIndex the number of the edge of the LHA
154 : * @param M is the marking of the SPN
155 : * @param b a binding of the colored variable of the SPN for the transition.
156 : */
157 : template<class DEDState>
158 52220610 : void LHA_orig<DEDState>::fireLHA(int EdgeIndex,const DEDState &M, const abstractBinding &b){
159 52220610 : this->DoEdgeUpdates(EdgeIndex, M, b);
160 52220610 : this->CurrentLocation = this->Edge[EdgeIndex].Target;
161 52220610 : }
162 :
163 : /**
164 : * Set the automaton to its initial location.
165 : * If the automaton contain several initial state only one should satisfie
166 : * its invarient with the given Marking due to determinicity.
167 : * @param Marking, A marking of the Petri net in principle the initial marking.
168 : */
169 : template<class DEDState>
170 222105 : void LHA_orig<DEDState>::setInitLocation(const DEDState& Marking) {
171 222105 : for (const auto &l : this->InitLoc) {
172 222105 : if (this->CheckLocation(l, Marking)){
173 222105 : this->CurrentLocation = l;
174 444210 : return;
175 : }
176 : }
177 :
178 0 : cerr << "There is no initial location enabled with the initial marking" << endl;
179 0 : exit(EXIT_FAILURE);
180 : }
181 :
182 :
183 : /**
184 : * Return a sychronized edge index with a transition.
185 : * The edge is such that the location invariant will holds in the marking of the
186 : * Petri net after the transition.
187 : * @param PetriNetTransition, a Petri net transition index.
188 : * @param bindin, the color binding of the transition.
189 : * @param NextMarking, The marking in with the Petri net will be after the transition.
190 : * @return an index of synchronized edge or -1 if there is no suitable synchronized edge.
191 : */
192 : template<class DEDState>
193 52293716 : int LHA_orig<DEDState>::GetEnabled_S_Edges(size_t PetriNetTransition, const DEDState& NextMarking,const abstractBinding& binding) {
194 52293716 : const size_t mult = this->NbLoc * this->NbTrans;
195 54076220 : for (int i =1 ; i <= this->ActionEdgesAr[ this->NbTrans* this->CurrentLocation+ PetriNetTransition]; i++){
196 : //cerr << i << endl;
197 54003114 : const int it = this->ActionEdgesAr[this->NbTrans* this->CurrentLocation+ PetriNetTransition+i*mult];
198 : //cerr << it << endl;
199 54003114 : if ((this->CheckLocation(this->Edge[it].Target, NextMarking))) {
200 52259285 : if (this->CheckEdgeContraints(it,PetriNetTransition, binding, NextMarking)){
201 : //assert(it==oracle);
202 52220610 : return it;
203 : }
204 : }
205 : }
206 73106 : return (-1);
207 : }
208 :
209 :
210 : /**
211 : * Reset all linear form.
212 : */
213 : template<class DEDState>
214 222105 : void LHA_orig<DEDState>::resetLinForms() {
215 1311808 : for (size_t i = 0; i < this->LinForm.size(); i++) {
216 1089703 : this->LinForm[i] = 0;
217 1089703 : this->OldLinForm[i] = 0;
218 : }
219 1317808 : for (size_t i = 0; i < this->LhaFunc.size(); i++)
220 1095703 : this->LhaFunc[i] = this->LhaFuncDefaults[i];
221 222105 : }
222 :
223 :
224 :
225 : template<class DEDState>
226 0 : double LHA<DEDState>::Min(double a, double b, double c) {
227 0 : double x = min(b, c);
228 0 : return min(a, x);
229 : }
230 :
231 : template<class DEDState>
232 339187 : double LHA<DEDState>::Max(double a, double b, double c) {
233 339187 : double x = max(b, c);
234 339187 : return max(a, x);
235 : }
236 :
237 : template<class DEDState>
238 0 : double LHA<DEDState>::Integral(double OldInt, double, double Delta, double x, double y) {
239 0 : return (OldInt + Delta * (x + y) / 2);
240 : }
241 :
242 : template<class DEDState>
243 0 : double LHA<DEDState>::BoxedIntegral(double OldInt, double t, double Delta, double x, double y, double t1,double t2) {
244 0 : if(t>=t2 || t+Delta <= t1) return OldInt;
245 0 : double slope = (y-x)/Delta;
246 0 : if(t1>t){
247 0 : x += (t1-t)*slope;
248 0 : }else t1 = t;
249 0 : if(t2< t+Delta){
250 0 : y-= (t + Delta -t2)*slope;
251 0 : }else t2 = t+Delta;
252 0 : return (OldInt + (t2-t1) * (x + y) / 2);
253 : }
254 :
255 :
256 :
257 :
258 : //#include "MarkovChain.hpp"
259 : //template class LHA<State>;
260 : //template class LHA_orig<State>;
|
