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

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9  
10  
11  
12  
13  
14  
15  
16 
 Entry action for state :Super2_B 
17 
node Super2_B_en(idSuper2_Super2_1:int; 
18 
s_1:real; 
19 
isInner:bool) 
20  
21 
returns (idSuper2_Super2:int; 
22 
s:real); 
23  
24  
25 
var idSuper2_Super2_2:int; 
26 
s_2:real; 
27  
28  
29 
let 
30  
31  
32  
33 
 set state as active 
34 
idSuper2_Super2_2 
35 
= 1951; 
36 

37  
38 
s_2 
39 
= if (not isInner) then 3. 
40 
else s_1; 
41 

42  
43 
(idSuper2_Super2, s) 
44 
= (idSuper2_Super2_2, s_2); 
45 

46  
47 
tel 
48  
49  
50  
51  
52  
53 
 Exit action for state :Super2_B 
54 
node Super2_B_ex(idSuper2_Super2_1:int; 
55 
isInner:bool) 
56  
57 
returns (idSuper2_Super2:int); 
58  
59  
60 
var idSuper2_Super2_2:int; 
61  
62  
63 
let 
64  
65  
66  
67 
 set state as inactive 
68 
idSuper2_Super2_2 
69 
= if (not isInner) then 0 else idSuper2_Super2_1; 
70  
71  
72 
(idSuper2_Super2) 
73 
= (idSuper2_Super2_1); 
74 

75  
76 
tel 
77  
78  
79  
80  
81  
82  
83 
 Entry action for state :C_C1 
84 
node C_C1_en(idSuper2_C_1:int; 
85 
s_1:real; 
86 
isInner:bool) 
87  
88 
returns (idSuper2_C:int; 
89 
s:real); 
90  
91  
92 
var idSuper2_C_2:int; 
93 
s_2:real; 
94  
95  
96 
let 
97  
98  
99  
100 
 set state as active 
101 
idSuper2_C_2 
102 
= 1952; 
103 

104  
105 
s_2 
106 
= if (not isInner) then 2. 
107 
else s_1; 
108 

109  
110 
(idSuper2_C, s) 
111 
= (idSuper2_C_2, s_2); 
112 

113  
114 
tel 
115  
116  
117  
118  
119  
120 
 Exit action for state :C_C1 
121 
node C_C1_ex(idSuper2_C_1:int; 
122 
isInner:bool) 
123  
124 
returns (idSuper2_C:int); 
125  
126  
127 
var idSuper2_C_2:int; 
128  
129  
130 
let 
131  
132  
133  
134 
 set state as inactive 
135 
idSuper2_C_2 
136 
= if (not isInner) then 0 else idSuper2_C_1; 
137  
138  
139 
(idSuper2_C) 
140 
= (idSuper2_C_1); 
141 

142  
143 
tel 
144  
145  
146  
147  
148  
149  
150 
 Entry action for state :Super2_C 
151 
node Super2_C_en(idSuper2_C_1:int; 
152 
idSuper2_Super2_1:int; 
153 
s_1:real; 
154 
isInner:bool) 
155  
156 
returns (idSuper2_C:int; 
157 
idSuper2_Super2:int; 
158 
s:real); 
159  
160  
161 
var idSuper2_C_2, idSuper2_C_3, idSuper2_C_4, idSuper2_C_5:int; 
162 
idSuper2_Super2_2, idSuper2_Super2_3, idSuper2_Super2_4:int; 
163 
s_2, s_3, s_4, s_5:real; 
164  
165  
166 
let 
167  
168  
169  
170 
 set state as active 
171 
idSuper2_Super2_2 
172 
= 1953; 
173 

174  
175 

176 
 transition trace : 
177 
POINT__To__C_C1_1 
178 
(idSuper2_C_2, s_2) 
179 
= C_C1_en(idSuper2_C_1, s_1, false); 
180 

181  
182 
(idSuper2_C_3, idSuper2_Super2_3, s_3) 
183 
= 
184  
185 
if ( idSuper2_C_1 = 0) then 
186  
187 
(idSuper2_C_2, idSuper2_Super2_2, s_2) 
188  
189 
else(idSuper2_C_1, idSuper2_Super2_2, s_1); 
190  
191 

192  
193 
(idSuper2_C_4, s_4) 
194 
= 
195 
if ( idSuper2_C_1 = 1952) then 
196 
C_C1_en(idSuper2_C_1, s_1, false) 
197 
else (idSuper2_C_1, s_1); 
198  
199 

200  
201 
(idSuper2_C_5, idSuper2_Super2_4, s_5) 
202 
= 
203 
if ( idSuper2_C_1 = 0) then 
204 
(idSuper2_C_3, idSuper2_Super2_3, s_3) 
205 
else 
206 
if ( idSuper2_C_1 = 1952) then 
207 
(idSuper2_C_4, idSuper2_Super2_3, s_4) 
208 
else (idSuper2_C_1, idSuper2_Super2_2, s_1); 
209  
210  
211 
(idSuper2_C, idSuper2_Super2, s) 
212 
= (idSuper2_C_5, idSuper2_Super2_4, s_5); 
213 

214  
215 
tel 
216  
217  
218  
219  
220  
221 
 Exit action for state :Super2_C 
222 
node Super2_C_ex(idSuper2_C_1:int; 
223 
idSuper2_Super2_1:int; 
224 
isInner:bool) 
225  
226 
returns (idSuper2_C:int; 
227 
idSuper2_Super2:int); 
228  
229  
230 
var idSuper2_C_2, idSuper2_C_3, idSuper2_C_4:int; 
231 
idSuper2_Super2_2:int; 
232  
233  
234 
let 
235  
236  
237  
238 

239 
(idSuper2_C_2) 
240 
= 
241 
if ( idSuper2_C_1 = 1952) then 
242 
C_C1_ex(idSuper2_C_1, false) 
243 
else (idSuper2_C_1); 
244  
245 

246  
247 
(idSuper2_C_3) 
248 
= 
249 
if ( idSuper2_C_1 = 1952) then 
250 
(idSuper2_C_2) 
251 
else (idSuper2_C_1); 
252  
253  
254 
 set state as inactive 
255 
idSuper2_Super2_2 
256 
= if (not isInner) then 0 else idSuper2_Super2_1; 
257  
258 
idSuper2_C_4 
259 
= 0; 
260 

261  
262 
(idSuper2_C, idSuper2_Super2) 
263 
= (idSuper2_C_4, idSuper2_Super2_1); 
264 

265  
266 
tel 
267  
268  
269  
270  
271  
272  
273 
 Entry action for state :Super2_A 
274 
node Super2_A_en(idSuper2_Super2_1:int; 
275 
s_1:real; 
276 
isInner:bool) 
277  
278 
returns (idSuper2_Super2:int; 
279 
s:real); 
280  
281  
282 
var idSuper2_Super2_2:int; 
283 
s_2:real; 
284  
285  
286 
let 
287  
288  
289  
290 
 set state as active 
291 
idSuper2_Super2_2 
292 
= 1950; 
293 

294  
295 
s_2 
296 
= if (not isInner) then 1. 
297 
else s_1; 
298 

299  
300 
(idSuper2_Super2, s) 
301 
= (idSuper2_Super2_2, s_2); 
302 

303  
304 
tel 
305  
306  
307  
308  
309  
310 
 Exit action for state :Super2_A 
311 
node Super2_A_ex(idSuper2_Super2_1:int; 
312 
isInner:bool) 
313  
314 
returns (idSuper2_Super2:int); 
315  
316  
317 
var idSuper2_Super2_2:int; 
318  
319  
320 
let 
321  
322  
323  
324 
 set state as inactive 
325 
idSuper2_Super2_2 
326 
= if (not isInner) then 0 else idSuper2_Super2_1; 
327  
328  
329 
(idSuper2_Super2) 
330 
= (idSuper2_Super2_1); 
331 

332  
333 
tel 
334  
335  
336 
***************************************************State :Super2_C Automaton*************************************************** 
337  
338 
node Super2_C_node(idSuper2_C_1:int; 
339 
s_1:real; 
340 
E:bool; 
341 
idSuper2_Super2_1:int) 
342  
343 
returns (idSuper2_C:int; 
344 
s:real; 
345 
idSuper2_Super2:int); 
346  
347  
348 
let 
349  
350 
automaton super2_c 
351  
352 
state POINTSuper2_C: 
353 
unless (idSuper2_C_1=0) restart POINT__TO__C_C1_1 
354  
355  
356  
357 
unless (idSuper2_C_1=1952) and E restart C_C1__TO__SUPER2_B_1 
358  
359  
360  
361 
unless (idSuper2_C_1=1952) restart C_C1_IDL 
362  
363 
let 
364  
365 
(idSuper2_C, s, idSuper2_Super2) 
366 
= (idSuper2_C_1, s_1, idSuper2_Super2_1); 
367 

368  
369 
tel 
370  
371  
372  
373 
state POINT__TO__C_C1_1: 
374  
375 
var idSuper2_C_2:int; 
376 
s_2:real; 
377 
let 
378  
379 
 transition trace : 
380 
POINT__To__C_C1_1 
381 
(idSuper2_C_2, s_2) 
382 
= C_C1_en(idSuper2_C_1, s_1, false); 
383 

384  
385 
(idSuper2_C, s) 
386 
= (idSuper2_C_2, s_2); 
387  
388 
add unused variables 
389 
(idSuper2_Super2) 
390 
= (idSuper2_Super2_1); 
391 

392  
393 
tel 
394  
395 
until true restart POINTSuper2_C 
396  
397  
398  
399 
state C_C1__TO__SUPER2_B_1: 
400  
401 
var idSuper2_C_2:int; 
402 
s_2:real; 
403 
idSuper2_Super2_2, idSuper2_Super2_3:int; 
404 
let 
405  
406 
 transition trace : 
407 
C_C1__To__Super2_B_1 
408 
(idSuper2_C_2, idSuper2_Super2_2) 
409 
= Super2_C_ex(idSuper2_C_1, idSuper2_Super2_1, false); 
410 

411  
412 
(idSuper2_Super2_3, s_2) 
413 
= Super2_B_en(idSuper2_Super2_2, s_1, false); 
414 

415  
416 
(idSuper2_C, s, idSuper2_Super2) 
417 
= (idSuper2_C_2, s_2, idSuper2_Super2_3); 
418  
419  
420 
tel 
421  
422 
until true restart POINTSuper2_C 
423  
424  
425  
426 
state C_C1_IDL: 
427  
428 
let 
429  
430 

431  
432 
(idSuper2_C, s, idSuper2_Super2) 
433 
= (idSuper2_C_1, s_1, idSuper2_Super2_1); 
434 

435  
436 
tel 
437  
438 
until true restart POINTSuper2_C 
439  
440  
441  
442 
tel 
443  
444  
445 
***************************************************State :Super2_Super2 Automaton*************************************************** 
446  
447 
node Super2_Super2_node(idSuper2_Super2_1:int; 
448 
s_1:real; 
449 
F:bool; 
450 
idSuper2_C_1:int; 
451 
E:bool; 
452 
G:bool) 
453  
454 
returns (idSuper2_Super2:int; 
455 
s:real; 
456 
idSuper2_C:int); 
457  
458  
459 
let 
460  
461 
automaton super2_super2 
462  
463 
state POINTSuper2_Super2: 
464 
unless (idSuper2_Super2_1=0) restart POINT__TO__SUPER2_A_1 
465  
466  
467  
468 
unless (idSuper2_Super2_1=1950) and F restart SUPER2_A__TO__SUPER2_C_1 
469  
470  
471  
472 
unless (idSuper2_Super2_1=1950) and E restart SUPER2_A__TO__C_C1_2 
473  
474  
475  
476 
unless (idSuper2_Super2_1=1951) and G restart SUPER2_B__TO__SUPER2_A_1 
477  
478  
479  
480 
unless (idSuper2_Super2_1=1953) and F restart SUPER2_C__TO__SUPER2_B_1 
481  
482  
483  
484 
unless (idSuper2_Super2_1=1950) restart SUPER2_A_IDL 
485  
486 
unless (idSuper2_Super2_1=1951) restart SUPER2_B_IDL 
487  
488 
unless (idSuper2_Super2_1=1953) restart SUPER2_C_IDL 
489  
490 
let 
491  
492 
(idSuper2_Super2, s, idSuper2_C) 
493 
= (idSuper2_Super2_1, s_1, idSuper2_C_1); 
494 

495  
496 
tel 
497  
498  
499  
500 
state POINT__TO__SUPER2_A_1: 
501  
502 
var idSuper2_Super2_2:int; 
503 
s_2:real; 
504 
let 
505  
506 
 transition trace : 
507 
POINT__To__Super2_A_1 
508 
(idSuper2_Super2_2, s_2) 
509 
= Super2_A_en(idSuper2_Super2_1, s_1, false); 
510 

511  
512 
(idSuper2_Super2, s) 
513 
= (idSuper2_Super2_2, s_2); 
514  
515 
add unused variables 
516 
(idSuper2_C) 
517 
= (idSuper2_C_1); 
518 

519  
520 
tel 
521  
522 
until true restart POINTSuper2_Super2 
523  
524  
525  
526 
state SUPER2_A__TO__SUPER2_C_1: 
527  
528 
var idSuper2_Super2_2, idSuper2_Super2_3:int; 
529 
s_2:real; 
530 
idSuper2_C_2:int; 
531 
let 
532  
533 
 transition trace : 
534 
Super2_A__To__Super2_C_1 
535 
(idSuper2_Super2_2) 
536 
= Super2_A_ex(idSuper2_Super2_1, false); 
537 

538  
539 
(idSuper2_C_2, idSuper2_Super2_3, s_2) 
540 
= Super2_C_en(idSuper2_C_1, idSuper2_Super2_2, s_1, false); 
541 

542  
543 
(idSuper2_Super2, s, idSuper2_C) 
544 
= (idSuper2_Super2_3, s_2, idSuper2_C_2); 
545  
546  
547 
tel 
548  
549 
until true restart POINTSuper2_Super2 
550  
551  
552  
553 
state SUPER2_A__TO__C_C1_2: 
554  
555 
var idSuper2_Super2_2, idSuper2_Super2_3:int; 
556 
s_2:real; 
557 
idSuper2_C_2, idSuper2_C_3:int; 
558 
let 
559  
560 
 transition trace : 
561 
Super2_A__To__C_C1_2 
562 
(idSuper2_Super2_2) 
563 
= Super2_A_ex(idSuper2_Super2_1, false); 
564 

565  
566 
idSuper2_C_2 
567 
= 1952; 
568 

569 
(idSuper2_C_3, idSuper2_Super2_3, s_2) 
570 
= Super2_C_en(idSuper2_C_2, idSuper2_Super2_2, s_1, false); 
571 

572  
573 
(idSuper2_Super2, s, idSuper2_C) 
574 
= (idSuper2_Super2_3, s_2, idSuper2_C_3); 
575  
576  
577 
tel 
578  
579 
until true restart POINTSuper2_Super2 
580  
581  
582  
583 
state SUPER2_B__TO__SUPER2_A_1: 
584  
585 
var idSuper2_Super2_2, idSuper2_Super2_3:int; 
586 
s_2:real; 
587 
let 
588  
589 
 transition trace : 
590 
Super2_B__To__Super2_A_1 
591 
(idSuper2_Super2_2) 
592 
= Super2_B_ex(idSuper2_Super2_1, false); 
593 

594  
595 
(idSuper2_Super2_3, s_2) 
596 
= Super2_A_en(idSuper2_Super2_2, s_1, false); 
597 

598  
599 
(idSuper2_Super2, s, idSuper2_C) 
600 
= (idSuper2_Super2_3, s_2, idSuper2_C_1); 
601  
602  
603 
tel 
604  
605 
until true restart POINTSuper2_Super2 
606  
607  
608  
609 
state SUPER2_C__TO__SUPER2_B_1: 
610  
611 
var idSuper2_Super2_2, idSuper2_Super2_3:int; 
612 
s_2:real; 
613 
idSuper2_C_2:int; 
614 
let 
615  
616 
 transition trace : 
617 
Super2_C__To__Super2_B_1 
618 
(idSuper2_C_2, idSuper2_Super2_2) 
619 
= Super2_C_ex(idSuper2_C_1, idSuper2_Super2_1, false); 
620 

621  
622 
(idSuper2_Super2_3, s_2) 
623 
= Super2_B_en(idSuper2_Super2_2, s_1, false); 
624 

625  
626 
(idSuper2_Super2, s, idSuper2_C) 
627 
= (idSuper2_Super2_3, s_2, idSuper2_C_2); 
628  
629  
630 
tel 
631  
632 
until true restart POINTSuper2_Super2 
633  
634  
635  
636 
state SUPER2_A_IDL: 
637  
638 
let 
639  
640 

641  
642 
(idSuper2_Super2, s, idSuper2_C) 
643 
= (idSuper2_Super2_1, s_1, idSuper2_C_1); 
644 

645  
646 
tel 
647  
648 
until true restart POINTSuper2_Super2 
649  
650  
651  
652 
state SUPER2_B_IDL: 
653  
654 
let 
655  
656 

657  
658 
(idSuper2_Super2, s, idSuper2_C) 
659 
= (idSuper2_Super2_1, s_1, idSuper2_C_1); 
660 

661  
662 
tel 
663  
664 
until true restart POINTSuper2_Super2 
665  
666  
667  
668 
state SUPER2_C_IDL: 
669  
670 
var idSuper2_Super2_2:int; 
671 
s_2:real; 
672 
idSuper2_C_2:int; 
673 
let 
674  
675 

676 
(idSuper2_C_2, s_2, idSuper2_Super2_2) 
677 
= Super2_C_node(idSuper2_C_1, s_1, E, idSuper2_Super2_1); 
678  
679 

680  
681  
682 
(idSuper2_Super2, s, idSuper2_C) 
683 
= (idSuper2_Super2_2, s_2, idSuper2_C_2); 
684 

685  
686 
tel 
687  
688 
until true restart POINTSuper2_Super2 
689  
690  
691  
692 
tel 
693  
694  
695 
***************************************************State :Super2_Super2 Automaton*************************************************** 
696  
697 
node Super2_Super2(x:int; 
698 
E:bool; 
699 
F:bool; 
700 
G:bool) 
701  
702 
returns (s:real); 
703  
704  
705 
var s_1: real; 
706  
707 
idSuper2_Super2, idSuper2_Super2_1: int; 
708  
709 
idSuper2_C, idSuper2_C_1: int; 
710  
711 
idSuper2_Super2_2, idSuper2_Super2_3:int; 
712 
s_2, s_3:real; 
713 
idSuper2_C_2, idSuper2_C_3:int; 
714 
let 
715  
716 
s_1 = 0.0 > pre s; 
717  
718 
idSuper2_Super2_1 = 0 > pre idSuper2_Super2; 
719  
720 
idSuper2_C_1 = 0 > pre idSuper2_C; 
721  
722 

723  
724  
725  
726 
(idSuper2_Super2_2, s_2, idSuper2_C_2) 
727 
= 
728  
729 
if E then Super2_Super2_node(idSuper2_Super2_1, s_1, false, idSuper2_C_1, E, false) 
730  
731 
else (idSuper2_Super2_1, s_1, idSuper2_C_1); 
732  
733 

734  
735  
736  
737 
(idSuper2_Super2_3, s_3, idSuper2_C_3) 
738 
= 
739  
740 
if F then Super2_Super2_node(idSuper2_Super2_2, s_2, F, idSuper2_C_2, false, false) 
741  
742 
else (idSuper2_Super2_2, s_2, idSuper2_C_2); 
743  
744 

745  
746  
747  
748 
(idSuper2_Super2, s, idSuper2_C) 
749 
= 
750  
751 
if G then Super2_Super2_node(idSuper2_Super2_3, s_3, false, idSuper2_C_3, false, G) 
752  
753 
else (idSuper2_Super2_3, s_3, idSuper2_C_3); 
754  
755 

756  
757  
758 
unused outputs 
759 

760  
761 
tel 
762  
763  
764  
765 
node Super2 (x_1_1 : int; E_1_1 : real; F_1_1 : real; G_1_1 : real) 
766 
returns (state_1_1 : real); 
767 
var 
768 
Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real; 
769 
Super2_1_1 : real; 
770 
i_virtual_local : real; 
771 
Super2Mux_1_1_event: bool; 
772 
Super2Mux_1_2_event: bool; 
773 
Super2Mux_1_3_event: bool; 
774 
let 
775 
Mux_1_1 = E_1_1 ; 
776 
Mux_1_2 = F_1_1 ; 
777 
Mux_1_3 = G_1_1 ; 
778 
Super2Mux_1_1_event = false > ((pre(Mux_1_1) > 0.0 and Mux_1_1 <= 0.0) or (pre(Mux_1_1) <= 0.0 and Mux_1_1 > 0.0)); 
779 
Super2Mux_1_2_event = false > ((pre(Mux_1_2) > 0.0 and Mux_1_2 <= 0.0) or (pre(Mux_1_2) <= 0.0 and Mux_1_2 > 0.0)); 
780 
Super2Mux_1_3_event = false > ((pre(Mux_1_3) > 0.0 and Mux_1_3 <= 0.0) or (pre(Mux_1_3) <= 0.0 and Mux_1_3 > 0.0)); 
781 
Super2_1_1 = Super2_Super2(x_1_1, Super2Mux_1_1_event, Super2Mux_1_2_event, Super2Mux_1_3_event); 
782 
state_1_1 = Super2_1_1; 
783 
i_virtual_local= 0.0 > 1.0; 
784 
tel 
785 