lustrectests / regression_tests / lustre_files / success / Stateflow / src_Temporal1 / Temporal1.lus @ eb639349
History  View  Annotate  Download (5.21 KB)
1 
 This file has been generated by cocoSim 

2  
3 
 External Stateflow functions 
4 
node after(n:int; E : bool; id:int ) returns ( Y : bool ); 
5 
var count:int; 
6 
let 
7 
count = 0 > if (pre id != id) then 
8 
if E then 1 else 0 
9 
else 
10 
if E then (pre count) + 1 else pre count; 
11 
Y = count >= n ; 
12 
tel 
13 
 System nodes 
14  
15  
16  
17  
18  
19  
20  
21 
 Entry action for state :Temporal1_B 
22 
node Temporal1_B_en(idTemporal1_Temporal1_1:int; 
23 
x_1:int; 
24 
isInner:bool) 
25  
26 
returns (idTemporal1_Temporal1:int; 
27 
x:int); 
28  
29  
30 
var idTemporal1_Temporal1_2:int; 
31 
x_2:int; 
32  
33  
34 
let 
35  
36  
37  
38 
 set state as active 
39 
idTemporal1_Temporal1_2 
40 
= 123; 
41 

42  
43 
x_2 
44 
= if (not isInner) then x_1 + 1 
45 
else x_1; 
46 

47  
48 
(idTemporal1_Temporal1, x) 
49 
= (idTemporal1_Temporal1_2, x_2); 
50 

51  
52 
tel 
53  
54  
55  
56  
57  
58 
 Exit action for state :Temporal1_B 
59 
node Temporal1_B_ex(idTemporal1_Temporal1_1:int; 
60 
isInner:bool) 
61  
62 
returns (idTemporal1_Temporal1:int); 
63  
64  
65 
var idTemporal1_Temporal1_2:int; 
66  
67  
68 
let 
69  
70  
71  
72 
 set state as inactive 
73 
idTemporal1_Temporal1_2 
74 
= if (not isInner) then 0 else idTemporal1_Temporal1_1; 
75  
76  
77 
(idTemporal1_Temporal1) 
78 
= (idTemporal1_Temporal1_1); 
79 

80  
81 
tel 
82  
83  
84  
85  
86  
87  
88 
 Entry action for state :Temporal1_A 
89 
node Temporal1_A_en(idTemporal1_Temporal1_1:int; 
90 
x_1:int; 
91 
isInner:bool) 
92  
93 
returns (idTemporal1_Temporal1:int; 
94 
x:int); 
95  
96  
97 
var idTemporal1_Temporal1_2:int; 
98 
x_2:int; 
99  
100  
101 
let 
102  
103  
104  
105 
 set state as active 
106 
idTemporal1_Temporal1_2 
107 
= 122; 
108 

109  
110 
x_2 
111 
= if (not isInner) then x_1 + 1 
112 
else x_1; 
113 

114  
115 
(idTemporal1_Temporal1, x) 
116 
= (idTemporal1_Temporal1_2, x_2); 
117 

118  
119 
tel 
120  
121  
122  
123  
124  
125 
 Exit action for state :Temporal1_A 
126 
node Temporal1_A_ex(idTemporal1_Temporal1_1:int; 
127 
isInner:bool) 
128  
129 
returns (idTemporal1_Temporal1:int); 
130  
131  
132 
var idTemporal1_Temporal1_2:int; 
133  
134  
135 
let 
136  
137  
138  
139 
 set state as inactive 
140 
idTemporal1_Temporal1_2 
141 
= if (not isInner) then 0 else idTemporal1_Temporal1_1; 
142  
143  
144 
(idTemporal1_Temporal1) 
145 
= (idTemporal1_Temporal1_1); 
146 

147  
148 
tel 
149  
150  
151 
***************************************************State :Temporal1_Temporal1 Automaton*************************************************** 
152  
153 
node Temporal1_Temporal1_node(idTemporal1_Temporal1_1:int; 
154 
x_1:int; 
155 
E:bool) 
156  
157 
returns (idTemporal1_Temporal1:int; 
158 
x:int); 
159 
var after_E_2_output: bool; 
160 
after_E_3_output: bool; 
161  
162  
163 
let 
164  
165 
after_E_2_output =after(2,E,idTemporal1_Temporal1_1); 
166 
after_E_3_output =after(3,E,idTemporal1_Temporal1_1); 
167 
automaton temporal1_temporal1 
168  
169 
state POINTTemporal1_Temporal1: 
170 
unless (idTemporal1_Temporal1_1=0) restart POINT__TO__TEMPORAL1_A_1 
171  
172  
173  
174 
unless (idTemporal1_Temporal1_1=122) and E and ( after_E_2_output ) restart TEMPORAL1_A__TO__TEMPORAL1_B_1 
175  
176  
177  
178 
unless (idTemporal1_Temporal1_1=123) and after_E_3_output restart TEMPORAL1_B__TO__TEMPORAL1_A_1 
179  
180  
181  
182 
unless (idTemporal1_Temporal1_1=122) restart TEMPORAL1_A_IDL 
183  
184 
unless (idTemporal1_Temporal1_1=123) restart TEMPORAL1_B_IDL 
185  
186 
let 
187  
188 
(idTemporal1_Temporal1, x) 
189 
= (idTemporal1_Temporal1_1, x_1); 
190 

191  
192 
tel 
193  
194  
195  
196 
state POINT__TO__TEMPORAL1_A_1: 
197  
198 
var idTemporal1_Temporal1_2:int; 
199 
x_2:int; 
200 
let 
201  
202 
 transition trace : 
203 
POINT__To__Temporal1_A_1 
204 
(idTemporal1_Temporal1_2, x_2) 
205 
= Temporal1_A_en(idTemporal1_Temporal1_1, x_1, false); 
206 

207  
208 
(idTemporal1_Temporal1, x) 
209 
= (idTemporal1_Temporal1_2, x_2); 
210  
211  
212 
tel 
213  
214 
until true restart POINTTemporal1_Temporal1 
215  
216  
217  
218 
state TEMPORAL1_A__TO__TEMPORAL1_B_1: 
219  
220 
var idTemporal1_Temporal1_2, idTemporal1_Temporal1_3:int; 
221 
x_2:int; 
222 
let 
223  
224 
 transition trace : 
225 
Temporal1_A__To__Temporal1_B_1 
226 
(idTemporal1_Temporal1_2) 
227 
= Temporal1_A_ex(idTemporal1_Temporal1_1, false); 
228 

229  
230 
(idTemporal1_Temporal1_3, x_2) 
231 
= Temporal1_B_en(idTemporal1_Temporal1_2, x_1, false); 
232 

233  
234 
(idTemporal1_Temporal1, x) 
235 
= (idTemporal1_Temporal1_3, x_2); 
236  
237  
238 
tel 
239  
240 
until true restart POINTTemporal1_Temporal1 
241  
242  
243  
244 
state TEMPORAL1_B__TO__TEMPORAL1_A_1: 
245  
246 
var idTemporal1_Temporal1_2, idTemporal1_Temporal1_3:int; 
247 
x_2:int; 
248 
let 
249  
250 
 transition trace : 
251 
Temporal1_B__To__Temporal1_A_1 
252 
(idTemporal1_Temporal1_2) 
253 
= Temporal1_B_ex(idTemporal1_Temporal1_1, false); 
254 

255  
256 
(idTemporal1_Temporal1_3, x_2) 
257 
= Temporal1_A_en(idTemporal1_Temporal1_2, x_1, false); 
258 

259  
260 
(idTemporal1_Temporal1, x) 
261 
= (idTemporal1_Temporal1_3, x_2); 
262  
263  
264 
tel 
265  
266 
until true restart POINTTemporal1_Temporal1 
267  
268  
269  
270 
state TEMPORAL1_A_IDL: 
271  
272 
let 
273  
274 

275  
276 
(idTemporal1_Temporal1, x) 
277 
= (idTemporal1_Temporal1_1, x_1); 
278 

279  
280 
tel 
281  
282 
until true restart POINTTemporal1_Temporal1 
283  
284  
285  
286 
state TEMPORAL1_B_IDL: 
287  
288 
let 
289  
290 

291  
292 
(idTemporal1_Temporal1, x) 
293 
= (idTemporal1_Temporal1_1, x_1); 
294 

295  
296 
tel 
297  
298 
until true restart POINTTemporal1_Temporal1 
299  
300  
301  
302 
tel 
303  
304  
305 
***************************************************State :Temporal1_Temporal1 Automaton*************************************************** 
306  
307 
node Temporal1_Temporal1(E:bool) 
308  
309 
returns (x:int); 
310  
311  
312 
var x_1: int; 
313  
314 
idTemporal1_Temporal1, idTemporal1_Temporal1_1: int; 
315  
316 
let 
317  
318 
x_1 = 0 > pre x; 
319  
320 
idTemporal1_Temporal1_1 = 0 > pre idTemporal1_Temporal1; 
321  
322 

323  
324  
325  
326 
(idTemporal1_Temporal1, x) 
327 
= 
328  
329 
if E then Temporal1_Temporal1_node(idTemporal1_Temporal1_1, x_1, E) 
330  
331 
else (idTemporal1_Temporal1_1, x_1); 
332  
333 

334  
335  
336 
unused outputs 
337 

338  
339 
tel 
340  
341  
342  
343 
node Temporal1 (E_1_1 : real) 
344 
returns (x_1_1 : int); 
345 
var 
346 
Temporal1_1_1 : int; 
347 
i_virtual_local : real; 
348 
Temporal1E_1_1_event: bool; 
349 
let 
350 
Temporal1E_1_1_event = false > (pre(E_1_1) <= 0.0 and E_1_1 > 0.0); 
351 
Temporal1_1_1 = Temporal1_Temporal1(Temporal1E_1_1_event); 
352 
x_1_1 = Temporal1_1_1; 
353 
i_virtual_local= 0.0 > 1.0; 
354 
tel 
355 