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

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9 
node Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action(a_1:real) 
10  
11 
returns (a:real); 
12  
13  
14 
var a_2:real; 
15  
16  
17 
let 
18  
19  
20  
21 
a_2 
22 
= a_1 +1.; 
23 

24  
25 
(a) 
26 
= (a_2); 
27 

28  
29 
tel 
30  
31  
32  
33  
34  
35  
36 
node Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action(a_1:real) 
37  
38 
returns (a:real); 
39  
40  
41 
var a_2:real; 
42  
43  
44 
let 
45  
46  
47  
48 
a_2 
49 
= a_1 +10.; 
50 

51  
52 
(a) 
53 
= (a_2); 
54 

55  
56 
tel 
57  
58  
59  
60  
61  
62  
63  
64 
node Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_1:real) 
65  
66 
returns (a:real); 
67  
68  
69 
var a_2:real; 
70  
71  
72 
let 
73  
74  
75  
76 
a_2 
77 
= a_1 +1000.; 
78 

79  
80 
(a) 
81 
= (a_2); 
82 

83  
84 
tel 
85  
86  
87  
88  
89  
90  
91 
node Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_1:real) 
92  
93 
returns (a:real); 
94  
95  
96 
var a_2:real; 
97  
98  
99 
let 
100  
101  
102  
103 
a_2 
104 
= a_1 +100.; 
105 

106  
107 
(a) 
108 
= (a_2); 
109 

110  
111 
tel 
112  
113  
114  
115  
116  
117  
118 
 Exit action for state :Junctions5_A 
119 
node Junctions5_A_ex(a_1:real; 
120 
idJunctions5_Junctions5_1:int; 
121 
isInner:bool) 
122  
123 
returns (a:real; 
124 
idJunctions5_Junctions5:int); 
125  
126  
127 
var a_2:real; 
128 
idJunctions5_Junctions5_2:int; 
129  
130  
131 
let 
132  
133  
134  
135 
a_2 
136 
= if (not isInner) then a_1 +10000. 
137 
else a_1; 
138 

139  
140 
 set state as inactive 
141 
idJunctions5_Junctions5_2 
142 
= if (not isInner) then 0 else idJunctions5_Junctions5_1; 
143  
144  
145 
(a, idJunctions5_Junctions5) 
146 
= (a_2, idJunctions5_Junctions5_1); 
147 

148  
149 
tel 
150  
151  
152  
153  
154  
155 
 Entry action for state :Junctions5_A 
156 
node Junctions5_A_en(idJunctions5_Junctions5_1:int; 
157 
isInner:bool) 
158  
159 
returns (idJunctions5_Junctions5:int); 
160  
161  
162 
var idJunctions5_Junctions5_2:int; 
163  
164  
165 
let 
166  
167  
168  
169 
 set state as active 
170 
idJunctions5_Junctions5_2 
171 
= 1282; 
172 

173  
174 
(idJunctions5_Junctions5) 
175 
= (idJunctions5_Junctions5_2); 
176 

177  
178 
tel 
179  
180  
181  
182  
183  
184  
185 
 Exit action for state :Junctions5_B 
186 
node Junctions5_B_ex(a_1:real; 
187 
idJunctions5_Junctions5_1:int; 
188 
isInner:bool) 
189  
190 
returns (a:real; 
191 
idJunctions5_Junctions5:int); 
192  
193  
194 
var a_2:real; 
195 
idJunctions5_Junctions5_2:int; 
196  
197  
198 
let 
199  
200  
201  
202 
a_2 
203 
= if (not isInner) then 0. 
204 
else a_1; 
205 

206  
207 
 set state as inactive 
208 
idJunctions5_Junctions5_2 
209 
= if (not isInner) then 0 else idJunctions5_Junctions5_1; 
210  
211  
212 
(a, idJunctions5_Junctions5) 
213 
= (a_2, idJunctions5_Junctions5_1); 
214 

215  
216 
tel 
217  
218  
219  
220  
221  
222 
 Entry action for state :Junctions5_B 
223 
node Junctions5_B_en(idJunctions5_Junctions5_1:int; 
224 
isInner:bool) 
225  
226 
returns (idJunctions5_Junctions5:int); 
227  
228  
229 
var idJunctions5_Junctions5_2:int; 
230  
231  
232 
let 
233  
234  
235  
236 
 set state as active 
237 
idJunctions5_Junctions5_2 
238 
= 1283; 
239 

240  
241 
(idJunctions5_Junctions5) 
242 
= (idJunctions5_Junctions5_2); 
243 

244  
245 
tel 
246  
247  
248 
***************************************************State :Junctions5_Junctions5 Automaton*************************************************** 
249  
250 
node Junctions5_Junctions5_node(idJunctions5_Junctions5_1:int; 
251 
x:int; 
252 
a_1:real) 
253  
254 
returns (idJunctions5_Junctions5:int; 
255 
a:real); 
256  
257  
258 
let 
259  
260 
automaton junctions5_junctions5 
261  
262 
state POINTJunctions5_Junctions5: 
263 
unless (idJunctions5_Junctions5_1=0) restart POINT__TO__JUNCTIONS5_A_1 
264  
265  
266  
267 
unless (idJunctions5_Junctions5_1=1282) and ( x mod 3=1 ) restart JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1 
268  
269  
270  
271 
unless (idJunctions5_Junctions5_1=1282) and ( x mod 3=0 ) restart JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2 
272  
273  
274  
275 
unless (idJunctions5_Junctions5_1=1282) restart JUNCTIONS5_A_IDL 
276  
277 
unless (idJunctions5_Junctions5_1=1283) restart JUNCTIONS5_B_IDL 
278  
279 
let 
280  
281 
(idJunctions5_Junctions5, a) 
282 
= (idJunctions5_Junctions5_1, a_1); 
283 

284  
285 
tel 
286  
287  
288  
289 
state POINT__TO__JUNCTIONS5_A_1: 
290  
291 
var idJunctions5_Junctions5_2:int; 
292 
let 
293  
294 
 transition trace : 
295 
POINT__To__Junctions5_A_1 
296 
(idJunctions5_Junctions5_2) 
297 
= Junctions5_A_en(idJunctions5_Junctions5_1, false); 
298 

299  
300 
(idJunctions5_Junctions5) 
301 
= (idJunctions5_Junctions5_2); 
302  
303 
add unused variables 
304 
(a) 
305 
= (a_1); 
306 

307  
308 
tel 
309  
310 
until true restart POINTJunctions5_Junctions5 
311  
312  
313  
314 
state JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1: 
315  
316 
var idJunctions5_Junctions5_2, idJunctions5_Junctions5_3:int; 
317 
a_2, a_3, a_4, a_5:real; 
318 
let 
319  
320 

321  
322  
323  
324 
 transition trace : 
325 
Junctions5_A__To__Junction1286_1, Junction1286__To__Junction1287_1, Junction1287__To__Junctions5_B_1 
326 
 condition Action : a+=10 
327 

328 
(a_2) 
329 
= Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action(a_1); 
330 

331  
332 
 condition Action : a+=100 
333 

334 
(a_3) 
335 
= 
336 
if (( x>=2 )) then 
337 
Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_2) 
338 
else (a_2); 
339 

340  
341 
 condition Action : a+=1000 
342 

343 
(a_4) 
344 
= 
345 
if (( x>=2 ) and ( x>=4 )) then 
346 
Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_3) 
347 
else (a_3); 
348 

349  
350 
(a_5, idJunctions5_Junctions5_2) 
351 
= 
352 
if (( x>=2 ) and ( x>=4 )) then 
353 
Junctions5_A_ex(a_4, idJunctions5_Junctions5_1, false) 
354 
else (a_4, idJunctions5_Junctions5_1); 
355 

356  
357 
(idJunctions5_Junctions5_3) 
358 
= 
359 
if (( x>=2 ) and ( x>=4 )) then 
360 
Junctions5_B_en(idJunctions5_Junctions5_2, false) 
361 
else (idJunctions5_Junctions5_2); 
362 

363  
364 
(idJunctions5_Junctions5, a) 
365 
= 
366 
if (( x>=2 ) and ( x>=4 )) then 
367 
(idJunctions5_Junctions5_3, a_5) 
368 
else 
369 
if (( x>=2 )) then 
370 
(idJunctions5_Junctions5_1, a_3) 
371 
else (idJunctions5_Junctions5_1, a_2); 
372  
373  
374 
tel 
375  
376 
until true restart POINTJunctions5_Junctions5 
377  
378  
379  
380 
state JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2: 
381  
382 
var idJunctions5_Junctions5_2, idJunctions5_Junctions5_3:int; 
383 
a_2, a_3, a_4, a_5:real; 
384 
let 
385  
386 

387  
388  
389  
390 
 transition trace : 
391 
Junctions5_A__To__Junction1286_2, Junction1286__To__Junction1287_1, Junction1287__To__Junctions5_B_1 
392 
 condition Action : a+=1 
393 

394 
(a_2) 
395 
= Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action(a_1); 
396 

397  
398 
 condition Action : a+=100 
399 

400 
(a_3) 
401 
= 
402 
if (( x>=2 )) then 
403 
Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_2) 
404 
else (a_2); 
405 

406  
407 
 condition Action : a+=1000 
408 

409 
(a_4) 
410 
= 
411 
if (( x>=2 ) and ( x>=4 )) then 
412 
Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_3) 
413 
else (a_3); 
414 

415  
416 
(a_5, idJunctions5_Junctions5_2) 
417 
= 
418 
if (( x>=2 ) and ( x>=4 )) then 
419 
Junctions5_A_ex(a_4, idJunctions5_Junctions5_1, false) 
420 
else (a_4, idJunctions5_Junctions5_1); 
421 

422  
423 
(idJunctions5_Junctions5_3) 
424 
= 
425 
if (( x>=2 ) and ( x>=4 )) then 
426 
Junctions5_B_en(idJunctions5_Junctions5_2, false) 
427 
else (idJunctions5_Junctions5_2); 
428 

429  
430 
(idJunctions5_Junctions5, a) 
431 
= 
432 
if (( x>=2 ) and ( x>=4 )) then 
433 
(idJunctions5_Junctions5_3, a_5) 
434 
else 
435 
if (( x>=2 )) then 
436 
(idJunctions5_Junctions5_1, a_3) 
437 
else (idJunctions5_Junctions5_1, a_2); 
438  
439  
440 
tel 
441  
442 
until true restart POINTJunctions5_Junctions5 
443  
444  
445  
446 
state JUNCTIONS5_A_IDL: 
447  
448 
let 
449  
450 

451  
452 
(idJunctions5_Junctions5, a) 
453 
= (idJunctions5_Junctions5_1, a_1); 
454 

455  
456 
tel 
457  
458 
until true restart POINTJunctions5_Junctions5 
459  
460  
461  
462 
state JUNCTIONS5_B_IDL: 
463  
464 
let 
465  
466 

467  
468 
(idJunctions5_Junctions5, a) 
469 
= (idJunctions5_Junctions5_1, a_1); 
470 

471  
472 
tel 
473  
474 
until true restart POINTJunctions5_Junctions5 
475  
476  
477  
478 
tel 
479  
480  
481 
***************************************************State :Junctions5_Junctions5 Automaton*************************************************** 
482  
483 
node Junctions5_Junctions5(x:int) 
484  
485 
returns (a:real); 
486  
487  
488 
var a_1: real; 
489  
490 
idJunctions5_Junctions5, idJunctions5_Junctions5_1: int; 
491  
492 
let 
493  
494 
a_1 = 0.0 > pre a; 
495  
496 
idJunctions5_Junctions5_1 = 0 > pre idJunctions5_Junctions5; 
497  
498 

499  
500  
501  
502 
(idJunctions5_Junctions5, a) 
503 
= Junctions5_Junctions5_node(idJunctions5_Junctions5_1, x, a_1); 
504  
505  
506 
unused outputs 
507 

508  
509 
tel 
510  
511  
512  
513 
node Junctions5 (x_1_1 : int) 
514 
returns (a_1_1 : real); 
515 
var 
516 
Junctions5_1_1 : real; 
517 
i_virtual_local : real; 
518 
let 
519 
Junctions5_1_1 = Junctions5_Junctions5(x_1_1); 
520 
a_1_1 = Junctions5_1_1; 
521 
i_virtual_local= 0.0 > 1.0; 
522 
tel 
523 