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

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9  
10  
11  
12  
13 
 Entry action for state :Top2_C 
14 
node Top2_C_en(idEvents5_Top2_1:int; 
15 
x_1:real; 
16 
isInner:bool) 
17  
18 
returns (idEvents5_Top2:int; 
19 
x:real); 
20  
21  
22 
var idEvents5_Top2_2:int; 
23 
x_2:real; 
24  
25  
26 
let 
27  
28  
29  
30 
 set state as active 
31 
idEvents5_Top2_2 
32 
= 654; 
33 

34  
35 
x_2 
36 
= if (not isInner) then x_1 + 1. 
37 
else x_1; 
38 

39  
40 
(idEvents5_Top2, x) 
41 
= (idEvents5_Top2_2, x_2); 
42 

43  
44 
tel 
45  
46  
47  
48  
49  
50 
 Exit action for state :Top2_C 
51 
node Top2_C_ex(idEvents5_Top2_1:int; 
52 
isInner:bool) 
53  
54 
returns (idEvents5_Top2:int); 
55  
56  
57 
var idEvents5_Top2_2:int; 
58  
59  
60 
let 
61  
62  
63  
64 
 set state as inactive 
65 
idEvents5_Top2_2 
66 
= if (not isInner) then 0 else idEvents5_Top2_1; 
67  
68  
69 
(idEvents5_Top2) 
70 
= (idEvents5_Top2_1); 
71 

72  
73 
tel 
74  
75  
76  
77  
78  
79  
80 
 Entry action for state :Top2_B 
81 
node Top2_B_en(idEvents5_Top2_1:int; 
82 
x_1:real; 
83 
isInner:bool) 
84  
85 
returns (idEvents5_Top2:int; 
86 
x:real); 
87  
88  
89 
var idEvents5_Top2_2:int; 
90 
x_2:real; 
91  
92  
93 
let 
94  
95  
96  
97 
 set state as active 
98 
idEvents5_Top2_2 
99 
= 653; 
100 

101  
102 
x_2 
103 
= if (not isInner) then x_1 + 1. 
104 
else x_1; 
105 

106  
107 
(idEvents5_Top2, x) 
108 
= (idEvents5_Top2_2, x_2); 
109 

110  
111 
tel 
112  
113  
114  
115  
116  
117 
 Exit action for state :Top2_B 
118 
node Top2_B_ex(idEvents5_Top2_1:int; 
119 
isInner:bool) 
120  
121 
returns (idEvents5_Top2:int); 
122  
123  
124 
var idEvents5_Top2_2:int; 
125  
126  
127 
let 
128  
129  
130  
131 
 set state as inactive 
132 
idEvents5_Top2_2 
133 
= if (not isInner) then 0 else idEvents5_Top2_1; 
134  
135  
136 
(idEvents5_Top2) 
137 
= (idEvents5_Top2_1); 
138 

139  
140 
tel 
141  
142  
143  
144  
145  
146  
147 
 Entry action for state :Events5_Top2 
148 
node Events5_Top2_en(idEvents5_Top2_1:int; 
149 
idEvents5_Events5_1:int; 
150 
x_1:real; 
151 
isInner:bool) 
152  
153 
returns (idEvents5_Top2:int; 
154 
idEvents5_Events5:int; 
155 
x:real); 
156  
157  
158 
var idEvents5_Top2_2, idEvents5_Top2_3, idEvents5_Top2_4, idEvents5_Top2_5, idEvents5_Top2_6:int; 
159 
idEvents5_Events5_2, idEvents5_Events5_3, idEvents5_Events5_4:int; 
160 
x_2, x_3, x_4, x_5, x_6:real; 
161  
162  
163 
let 
164  
165  
166  
167 
 set state as active 
168 
idEvents5_Events5_2 
169 
= 656; 
170 

171  
172 

173 
 transition trace : 
174 
POINT__To__Top2_B_1 
175 
(idEvents5_Top2_2, x_2) 
176 
= Top2_B_en(idEvents5_Top2_1, x_1, false); 
177 

178  
179 
(idEvents5_Top2_3, idEvents5_Events5_3, x_3) 
180 
= 
181  
182 
if ( idEvents5_Top2_1 = 0) then 
183  
184 
(idEvents5_Top2_2, idEvents5_Events5_2, x_2) 
185  
186 
else(idEvents5_Top2_1, idEvents5_Events5_2, x_1); 
187  
188 

189  
190 
(idEvents5_Top2_4, x_4) 
191 
= 
192 
if ( idEvents5_Top2_1 = 653) then 
193 
Top2_B_en(idEvents5_Top2_1, x_1, false) 
194 
else (idEvents5_Top2_1, x_1); 
195  
196 

197  
198 
(idEvents5_Top2_5, x_5) 
199 
= 
200 
if ( idEvents5_Top2_1 = 654) then 
201 
Top2_C_en(idEvents5_Top2_1, x_1, false) 
202 
else (idEvents5_Top2_1, x_1); 
203  
204 

205  
206 
(idEvents5_Top2_6, idEvents5_Events5_4, x_6) 
207 
= 
208 
if ( idEvents5_Top2_1 = 0) then 
209 
(idEvents5_Top2_3, idEvents5_Events5_3, x_3) 
210 
else 
211 
if ( idEvents5_Top2_1 = 653) then 
212 
(idEvents5_Top2_4, idEvents5_Events5_3, x_4) 
213 
else 
214 
if ( idEvents5_Top2_1 = 654) then 
215 
(idEvents5_Top2_5, idEvents5_Events5_3, x_5) 
216 
else (idEvents5_Top2_1, idEvents5_Events5_2, x_1); 
217  
218  
219 
(idEvents5_Top2, idEvents5_Events5, x) 
220 
= (idEvents5_Top2_6, idEvents5_Events5_4, x_6); 
221 

222  
223 
tel 
224  
225  
226  
227  
228  
229 
 Exit action for state :Events5_Top2 
230 
node Events5_Top2_ex(idEvents5_Top2_1:int; 
231 
idEvents5_Events5_1:int; 
232 
isInner:bool) 
233  
234 
returns (idEvents5_Top2:int; 
235 
idEvents5_Events5:int); 
236  
237  
238 
var idEvents5_Top2_2, idEvents5_Top2_3, idEvents5_Top2_4, idEvents5_Top2_5:int; 
239 
idEvents5_Events5_2:int; 
240  
241  
242 
let 
243  
244  
245  
246 

247 
(idEvents5_Top2_2) 
248 
= 
249 
if ( idEvents5_Top2_1 = 653) then 
250 
Top2_B_ex(idEvents5_Top2_1, false) 
251 
else (idEvents5_Top2_1); 
252  
253 

254  
255 
(idEvents5_Top2_3) 
256 
= 
257 
if ( idEvents5_Top2_1 = 654) then 
258 
Top2_C_ex(idEvents5_Top2_1, false) 
259 
else (idEvents5_Top2_1); 
260  
261 

262  
263 
(idEvents5_Top2_4) 
264 
= 
265 
if ( idEvents5_Top2_1 = 653) then 
266 
(idEvents5_Top2_2) 
267 
else 
268 
if ( idEvents5_Top2_1 = 654) then 
269 
(idEvents5_Top2_3) 
270 
else (idEvents5_Top2_1); 
271  
272  
273 
 set state as inactive 
274 
idEvents5_Events5_2 
275 
= if (not isInner) then 0 else idEvents5_Events5_1; 
276  
277 
idEvents5_Top2_5 
278 
= 0; 
279 

280  
281 
(idEvents5_Top2, idEvents5_Events5) 
282 
= (idEvents5_Top2_5, idEvents5_Events5_1); 
283 

284  
285 
tel 
286  
287  
288  
289  
290  
291  
292 
 Entry action for state :Top1_E 
293 
node Top1_E_en(idEvents5_Top1_1:int; 
294 
y_1:real; 
295 
isInner:bool) 
296  
297 
returns (idEvents5_Top1:int; 
298 
y:real); 
299  
300  
301 
var idEvents5_Top1_2:int; 
302 
y_2:real; 
303  
304  
305 
let 
306  
307  
308  
309 
 set state as active 
310 
idEvents5_Top1_2 
311 
= 658; 
312 

313  
314 
y_2 
315 
= if (not isInner) then y_1 + 1. 
316 
else y_1; 
317 

318  
319 
(idEvents5_Top1, y) 
320 
= (idEvents5_Top1_2, y_2); 
321 

322  
323 
tel 
324  
325  
326  
327  
328  
329 
 Exit action for state :Top1_E 
330 
node Top1_E_ex(idEvents5_Top1_1:int; 
331 
isInner:bool) 
332  
333 
returns (idEvents5_Top1:int); 
334  
335  
336 
var idEvents5_Top1_2:int; 
337  
338  
339 
let 
340  
341  
342  
343 
 set state as inactive 
344 
idEvents5_Top1_2 
345 
= if (not isInner) then 0 else idEvents5_Top1_1; 
346  
347  
348 
(idEvents5_Top1) 
349 
= (idEvents5_Top1_1); 
350 

351  
352 
tel 
353  
354  
355  
356  
357  
358  
359 
 Entry action for state :Top1_D 
360 
node Top1_D_en(idEvents5_Top1_1:int; 
361 
y_1:real; 
362 
isInner:bool) 
363  
364 
returns (idEvents5_Top1:int; 
365 
y:real); 
366  
367  
368 
var idEvents5_Top1_2:int; 
369 
y_2:real; 
370  
371  
372 
let 
373  
374  
375  
376 
 set state as active 
377 
idEvents5_Top1_2 
378 
= 657; 
379 

380  
381 
y_2 
382 
= if (not isInner) then y_1 + 1. 
383 
else y_1; 
384 

385  
386 
(idEvents5_Top1, y) 
387 
= (idEvents5_Top1_2, y_2); 
388 

389  
390 
tel 
391  
392  
393  
394  
395  
396 
 Exit action for state :Top1_D 
397 
node Top1_D_ex(idEvents5_Top1_1:int; 
398 
isInner:bool) 
399  
400 
returns (idEvents5_Top1:int); 
401  
402  
403 
var idEvents5_Top1_2:int; 
404  
405  
406 
let 
407  
408  
409  
410 
 set state as inactive 
411 
idEvents5_Top1_2 
412 
= if (not isInner) then 0 else idEvents5_Top1_1; 
413  
414  
415 
(idEvents5_Top1) 
416 
= (idEvents5_Top1_1); 
417 

418  
419 
tel 
420  
421  
422  
423  
424  
425  
426 
 Entry action for state :Top1_A 
427 
node Top1_A_en(idEvents5_Top1_1:int; 
428 
y_1:real; 
429 
isInner:bool) 
430  
431 
returns (idEvents5_Top1:int; 
432 
y:real); 
433  
434  
435 
var idEvents5_Top1_2:int; 
436 
y_2:real; 
437  
438  
439 
let 
440  
441  
442  
443 
 set state as active 
444 
idEvents5_Top1_2 
445 
= 652; 
446 

447  
448 
y_2 
449 
= if (not isInner) then y_1 + 1. 
450 
else y_1; 
451 

452  
453 
(idEvents5_Top1, y) 
454 
= (idEvents5_Top1_2, y_2); 
455 

456  
457 
tel 
458  
459  
460  
461  
462  
463 
 Exit action for state :Top1_A 
464 
node Top1_A_ex(idEvents5_Top1_1:int; 
465 
isInner:bool) 
466  
467 
returns (idEvents5_Top1:int); 
468  
469  
470 
var idEvents5_Top1_2:int; 
471  
472  
473 
let 
474  
475  
476  
477 
 set state as inactive 
478 
idEvents5_Top1_2 
479 
= if (not isInner) then 0 else idEvents5_Top1_1; 
480  
481  
482 
(idEvents5_Top1) 
483 
= (idEvents5_Top1_1); 
484 

485  
486 
tel 
487  
488  
489  
490  
491  
492  
493 
 Entry action for state :Events5_Top1 
494 
node Events5_Top1_en(idEvents5_Top1_1:int; 
495 
idEvents5_Events5_1:int; 
496 
y_1:real; 
497 
isInner:bool) 
498  
499 
returns (idEvents5_Top1:int; 
500 
idEvents5_Events5:int; 
501 
y:real); 
502  
503  
504 
var idEvents5_Top1_2, idEvents5_Top1_3, idEvents5_Top1_4, idEvents5_Top1_5, idEvents5_Top1_6, idEvents5_Top1_7:int; 
505 
idEvents5_Events5_2, idEvents5_Events5_3, idEvents5_Events5_4:int; 
506 
y_2, y_3, y_4, y_5, y_6, y_7:real; 
507  
508  
509 
let 
510  
511  
512  
513 
 set state as active 
514 
idEvents5_Events5_2 
515 
= 655; 
516 

517  
518 

519 
 transition trace : 
520 
POINT__To__Top1_A_1 
521 
(idEvents5_Top1_2, y_2) 
522 
= Top1_A_en(idEvents5_Top1_1, y_1, false); 
523 

524  
525 
(idEvents5_Top1_3, idEvents5_Events5_3, y_3) 
526 
= 
527  
528 
if ( idEvents5_Top1_1 = 0) then 
529  
530 
(idEvents5_Top1_2, idEvents5_Events5_2, y_2) 
531  
532 
else(idEvents5_Top1_1, idEvents5_Events5_2, y_1); 
533  
534 

535  
536 
(idEvents5_Top1_4, y_4) 
537 
= 
538 
if ( idEvents5_Top1_1 = 652) then 
539 
Top1_A_en(idEvents5_Top1_1, y_1, false) 
540 
else (idEvents5_Top1_1, y_1); 
541  
542 

543  
544 
(idEvents5_Top1_5, y_5) 
545 
= 
546 
if ( idEvents5_Top1_1 = 658) then 
547 
Top1_E_en(idEvents5_Top1_1, y_1, false) 
548 
else (idEvents5_Top1_1, y_1); 
549  
550 

551  
552 
(idEvents5_Top1_6, y_6) 
553 
= 
554 
if ( idEvents5_Top1_1 = 657) then 
555 
Top1_D_en(idEvents5_Top1_1, y_1, false) 
556 
else (idEvents5_Top1_1, y_1); 
557  
558 

559  
560 
(idEvents5_Top1_7, idEvents5_Events5_4, y_7) 
561 
= 
562 
if ( idEvents5_Top1_1 = 0) then 
563 
(idEvents5_Top1_3, idEvents5_Events5_3, y_3) 
564 
else 
565 
if ( idEvents5_Top1_1 = 652) then 
566 
(idEvents5_Top1_4, idEvents5_Events5_3, y_4) 
567 
else 
568 
if ( idEvents5_Top1_1 = 658) then 
569 
(idEvents5_Top1_5, idEvents5_Events5_3, y_5) 
570 
else 
571 
if ( idEvents5_Top1_1 = 657) then 
572 
(idEvents5_Top1_6, idEvents5_Events5_3, y_6) 
573 
else (idEvents5_Top1_1, idEvents5_Events5_2, y_1); 
574  
575  
576 
(idEvents5_Top1, idEvents5_Events5, y) 
577 
= (idEvents5_Top1_7, idEvents5_Events5_4, y_7); 
578 

579  
580 
tel 
581  
582  
583  
584  
585  
586 
 Exit action for state :Events5_Top1 
587 
node Events5_Top1_ex(idEvents5_Top1_1:int; 
588 
idEvents5_Events5_1:int; 
589 
isInner:bool) 
590  
591 
returns (idEvents5_Top1:int; 
592 
idEvents5_Events5:int); 
593  
594  
595 
var idEvents5_Top1_2, idEvents5_Top1_3, idEvents5_Top1_4, idEvents5_Top1_5, idEvents5_Top1_6:int; 
596 
idEvents5_Events5_2:int; 
597  
598  
599 
let 
600  
601  
602  
603 

604 
(idEvents5_Top1_2) 
605 
= 
606 
if ( idEvents5_Top1_1 = 652) then 
607 
Top1_A_ex(idEvents5_Top1_1, false) 
608 
else (idEvents5_Top1_1); 
609  
610 

611  
612 
(idEvents5_Top1_3) 
613 
= 
614 
if ( idEvents5_Top1_1 = 658) then 
615 
Top1_E_ex(idEvents5_Top1_1, false) 
616 
else (idEvents5_Top1_1); 
617  
618 

619  
620 
(idEvents5_Top1_4) 
621 
= 
622 
if ( idEvents5_Top1_1 = 657) then 
623 
Top1_D_ex(idEvents5_Top1_1, false) 
624 
else (idEvents5_Top1_1); 
625  
626 

627  
628 
(idEvents5_Top1_5) 
629 
= 
630 
if ( idEvents5_Top1_1 = 652) then 
631 
(idEvents5_Top1_2) 
632 
else 
633 
if ( idEvents5_Top1_1 = 658) then 
634 
(idEvents5_Top1_3) 
635 
else 
636 
if ( idEvents5_Top1_1 = 657) then 
637 
(idEvents5_Top1_4) 
638 
else (idEvents5_Top1_1); 
639  
640  
641 
 set state as inactive 
642 
idEvents5_Events5_2 
643 
= if (not isInner) then 0 else idEvents5_Events5_1; 
644  
645 
idEvents5_Top1_6 
646 
= 0; 
647 

648  
649 
(idEvents5_Top1, idEvents5_Events5) 
650 
= (idEvents5_Top1_6, idEvents5_Events5_1); 
651 

652  
653 
tel 
654  
655  
656 
***************************************************State :Events5_Top2 Automaton*************************************************** 
657  
658 
node Events5_Top2_node(idEvents5_Top2_1:int; 
659 
x_1:real; 
660 
F:bool) 
661  
662 
returns (idEvents5_Top2:int; 
663 
x:real); 
664  
665  
666 
let 
667  
668 
automaton events5_top2 
669  
670 
state POINTEvents5_Top2: 
671 
unless (idEvents5_Top2_1=0) restart POINT__TO__TOP2_B_1 
672  
673  
674  
675 
unless (idEvents5_Top2_1=653) and F restart TOP2_B__TO__TOP2_C_1 
676  
677  
678  
679 
unless (idEvents5_Top2_1=654) and F restart TOP2_C__TO__TOP2_B_1 
680  
681  
682  
683 
unless (idEvents5_Top2_1=653) restart TOP2_B_IDL 
684  
685 
unless (idEvents5_Top2_1=654) restart TOP2_C_IDL 
686  
687 
let 
688  
689 
(idEvents5_Top2, x) 
690 
= (idEvents5_Top2_1, x_1); 
691 

692  
693 
tel 
694  
695  
696  
697 
state POINT__TO__TOP2_B_1: 
698  
699 
var idEvents5_Top2_2:int; 
700 
x_2:real; 
701 
let 
702  
703 
 transition trace : 
704 
POINT__To__Top2_B_1 
705 
(idEvents5_Top2_2, x_2) 
706 
= Top2_B_en(idEvents5_Top2_1, x_1, false); 
707 

708  
709 
(idEvents5_Top2, x) 
710 
= (idEvents5_Top2_2, x_2); 
711  
712  
713 
tel 
714  
715 
until true restart POINTEvents5_Top2 
716  
717  
718  
719 
state TOP2_B__TO__TOP2_C_1: 
720  
721 
var idEvents5_Top2_2, idEvents5_Top2_3:int; 
722 
x_2:real; 
723 
let 
724  
725 
 transition trace : 
726 
Top2_B__To__Top2_C_1 
727 
(idEvents5_Top2_2) 
728 
= Top2_B_ex(idEvents5_Top2_1, false); 
729 

730  
731 
(idEvents5_Top2_3, x_2) 
732 
= Top2_C_en(idEvents5_Top2_2, x_1, false); 
733 

734  
735 
(idEvents5_Top2, x) 
736 
= (idEvents5_Top2_3, x_2); 
737  
738  
739 
tel 
740  
741 
until true restart POINTEvents5_Top2 
742  
743  
744  
745 
state TOP2_C__TO__TOP2_B_1: 
746  
747 
var idEvents5_Top2_2, idEvents5_Top2_3:int; 
748 
x_2:real; 
749 
let 
750  
751 
 transition trace : 
752 
Top2_C__To__Top2_B_1 
753 
(idEvents5_Top2_2) 
754 
= Top2_C_ex(idEvents5_Top2_1, false); 
755 

756  
757 
(idEvents5_Top2_3, x_2) 
758 
= Top2_B_en(idEvents5_Top2_2, x_1, false); 
759 

760  
761 
(idEvents5_Top2, x) 
762 
= (idEvents5_Top2_3, x_2); 
763  
764  
765 
tel 
766  
767 
until true restart POINTEvents5_Top2 
768  
769  
770  
771 
state TOP2_B_IDL: 
772  
773 
let 
774  
775 

776  
777 
(idEvents5_Top2, x) 
778 
= (idEvents5_Top2_1, x_1); 
779 

780  
781 
tel 
782  
783 
until true restart POINTEvents5_Top2 
784  
785  
786  
787 
state TOP2_C_IDL: 
788  
789 
let 
790  
791 

792  
793 
(idEvents5_Top2, x) 
794 
= (idEvents5_Top2_1, x_1); 
795 

796  
797 
tel 
798  
799 
until true restart POINTEvents5_Top2 
800  
801  
802  
803 
tel 
804  
805  
806  
807  
808  
809  
810 
node Top1_E__To__Top1_A_1_Transition_Action(idEvents5_Top2_1:int; 
811 
x_1:real; 
812 
F:bool; 
813 
z_1:real) 
814  
815 
returns (idEvents5_Top2:int; 
816 
x:real; 
817 
z:real); 
818  
819  
820 
var idEvents5_Top2_2:int; 
821 
x_2:real; 
822 
z_2:real; 
823  
824  
825 
let 
826  
827  
828  
829 
(idEvents5_Top2_2, x_2) 
830 
= Events5_Top2_node(idEvents5_Top2_1, x_1, true); 
831 

832  
833 
z_2 
834 
= z_1 + 1.; 
835 

836  
837 
(idEvents5_Top2, x, z) 
838 
= (idEvents5_Top2_2, x_2, z_2); 
839 

840  
841 
tel 
842  
843  
844  
845  
846  
847  
848 
node Top1_A__To__Top1_D_1_Transition_Action(idEvents5_Top2_1:int; 
849 
x_1:real; 
850 
F:bool; 
851 
z_1:real) 
852  
853 
returns (idEvents5_Top2:int; 
854 
x:real; 
855 
z:real); 
856  
857  
858 
var idEvents5_Top2_2:int; 
859 
x_2:real; 
860 
z_2:real; 
861  
862  
863 
let 
864  
865  
866  
867 
(idEvents5_Top2_2, x_2) 
868 
= Events5_Top2_node(idEvents5_Top2_1, x_1, true); 
869 

870  
871 
z_2 
872 
= z_1 + 1.; 
873 

874  
875 
(idEvents5_Top2, x, z) 
876 
= (idEvents5_Top2_2, x_2, z_2); 
877 

878  
879 
tel 
880  
881  
882  
883  
884  
885  
886 
node Top1_D__To__Top1_E_1_Transition_Action(idEvents5_Top2_1:int; 
887 
x_1:real; 
888 
F:bool; 
889 
z_1:real) 
890  
891 
returns (idEvents5_Top2:int; 
892 
x:real; 
893 
z:real); 
894  
895  
896 
var idEvents5_Top2_2:int; 
897 
x_2:real; 
898 
z_2:real; 
899  
900  
901 
let 
902  
903  
904  
905 
(idEvents5_Top2_2, x_2) 
906 
= Events5_Top2_node(idEvents5_Top2_1, x_1, true); 
907 

908  
909 
z_2 
910 
= z_1 + 1.; 
911 

912  
913 
(idEvents5_Top2, x, z) 
914 
= (idEvents5_Top2_2, x_2, z_2); 
915 

916  
917 
tel 
918  
919  
920 
***************************************************State :Events5_Top1 Automaton*************************************************** 
921  
922 
node Events5_Top1_node(idEvents5_Top1_1:int; 
923 
y_1:real; 
924 
E:bool; 
925 
F:bool; 
926 
idEvents5_Top2_1:int; 
927 
x_1:real; 
928 
z_1:real) 
929  
930 
returns (idEvents5_Top1:int; 
931 
y:real; 
932 
idEvents5_Top2:int; 
933 
x:real; 
934 
z:real); 
935  
936  
937 
let 
938  
939 
automaton events5_top1 
940  
941 
state POINTEvents5_Top1: 
942 
unless (idEvents5_Top1_1=0) restart POINT__TO__TOP1_A_1 
943  
944  
945  
946 
unless (idEvents5_Top1_1=652) and E restart TOP1_A__TO__TOP1_D_1 
947  
948  
949  
950 
unless (idEvents5_Top1_1=658) and E restart TOP1_E__TO__TOP1_A_1 
951  
952  
953  
954 
unless (idEvents5_Top1_1=657) and E restart TOP1_D__TO__TOP1_E_1 
955  
956  
957  
958 
unless (idEvents5_Top1_1=652) restart TOP1_A_IDL 
959  
960 
unless (idEvents5_Top1_1=658) restart TOP1_E_IDL 
961  
962 
unless (idEvents5_Top1_1=657) restart TOP1_D_IDL 
963  
964 
let 
965  
966 
(idEvents5_Top1, y, idEvents5_Top2, x, z) 
967 
= (idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, z_1); 
968 

969  
970 
tel 
971  
972  
973  
974 
state POINT__TO__TOP1_A_1: 
975  
976 
var idEvents5_Top1_2:int; 
977 
y_2:real; 
978 
let 
979  
980 
 transition trace : 
981 
POINT__To__Top1_A_1 
982 
(idEvents5_Top1_2, y_2) 
983 
= Top1_A_en(idEvents5_Top1_1, y_1, false); 
984 

985  
986 
(idEvents5_Top1, y) 
987 
= (idEvents5_Top1_2, y_2); 
988  
989 
add unused variables 
990 
(idEvents5_Top2, x, z) 
991 
= (idEvents5_Top2_1, x_1, z_1); 
992 

993  
994 
tel 
995  
996 
until true restart POINTEvents5_Top1 
997  
998  
999  
1000 
state TOP1_A__TO__TOP1_D_1: 
1001  
1002 
var idEvents5_Top1_2, idEvents5_Top1_3:int; 
1003 
y_2:real; 
1004 
idEvents5_Top2_2:int; 
1005 
x_2:real; 
1006 
z_2:real; 
1007 
let 
1008  
1009 
 transition trace : 
1010 
Top1_A__To__Top1_D_1 
1011 
(idEvents5_Top1_2) 
1012 
= Top1_A_ex(idEvents5_Top1_1, false); 
1013 

1014  
1015 
(idEvents5_Top2_2, x_2, z_2) 
1016 
= Top1_A__To__Top1_D_1_Transition_Action(idEvents5_Top2_1, x_1, F, z_1); 
1017 

1018  
1019 
(idEvents5_Top1_3, y_2) 
1020 
= Top1_D_en(idEvents5_Top1_2, y_1, false); 
1021 

1022  
1023 
(idEvents5_Top1, y, idEvents5_Top2, x, z) 
1024 
= (idEvents5_Top1_3, y_2, idEvents5_Top2_2, x_2, z_2); 
1025  
1026  
1027 
tel 
1028  
1029 
until true restart POINTEvents5_Top1 
1030  
1031  
1032  
1033 
state TOP1_E__TO__TOP1_A_1: 
1034  
1035 
var idEvents5_Top1_2, idEvents5_Top1_3:int; 
1036 
y_2:real; 
1037 
idEvents5_Top2_2:int; 
1038 
x_2:real; 
1039 
z_2:real; 
1040 
let 
1041  
1042 
 transition trace : 
1043 
Top1_E__To__Top1_A_1 
1044 
(idEvents5_Top1_2) 
1045 
= Top1_E_ex(idEvents5_Top1_1, false); 
1046 

1047  
1048 
(idEvents5_Top2_2, x_2, z_2) 
1049 
= Top1_E__To__Top1_A_1_Transition_Action(idEvents5_Top2_1, x_1, F, z_1); 
1050 

1051  
1052 
(idEvents5_Top1_3, y_2) 
1053 
= Top1_A_en(idEvents5_Top1_2, y_1, false); 
1054 

1055  
1056 
(idEvents5_Top1, y, idEvents5_Top2, x, z) 
1057 
= (idEvents5_Top1_3, y_2, idEvents5_Top2_2, x_2, z_2); 
1058  
1059  
1060 
tel 
1061  
1062 
until true restart POINTEvents5_Top1 
1063  
1064  
1065  
1066 
state TOP1_D__TO__TOP1_E_1: 
1067  
1068 
var idEvents5_Top1_2, idEvents5_Top1_3:int; 
1069 
y_2:real; 
1070 
idEvents5_Top2_2:int; 
1071 
x_2:real; 
1072 
z_2:real; 
1073 
let 
1074  
1075 
 transition trace : 
1076 
Top1_D__To__Top1_E_1 
1077 
(idEvents5_Top1_2) 
1078 
= Top1_D_ex(idEvents5_Top1_1, false); 
1079 

1080  
1081 
(idEvents5_Top2_2, x_2, z_2) 
1082 
= Top1_D__To__Top1_E_1_Transition_Action(idEvents5_Top2_1, x_1, F, z_1); 
1083 

1084  
1085 
(idEvents5_Top1_3, y_2) 
1086 
= Top1_E_en(idEvents5_Top1_2, y_1, false); 
1087 

1088  
1089 
(idEvents5_Top1, y, idEvents5_Top2, x, z) 
1090 
= (idEvents5_Top1_3, y_2, idEvents5_Top2_2, x_2, z_2); 
1091  
1092  
1093 
tel 
1094  
1095 
until true restart POINTEvents5_Top1 
1096  
1097  
1098  
1099 
state TOP1_A_IDL: 
1100  
1101 
let 
1102  
1103 

1104  
1105 
(idEvents5_Top1, y, idEvents5_Top2, x, z) 
1106 
= (idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, z_1); 
1107 

1108  
1109 
tel 
1110  
1111 
until true restart POINTEvents5_Top1 
1112  
1113  
1114  
1115 
state TOP1_E_IDL: 
1116  
1117 
let 
1118  
1119 

1120  
1121 
(idEvents5_Top1, y, idEvents5_Top2, x, z) 
1122 
= (idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, z_1); 
1123 

1124  
1125 
tel 
1126  
1127 
until true restart POINTEvents5_Top1 
1128  
1129  
1130  
1131 
state TOP1_D_IDL: 
1132  
1133 
let 
1134  
1135 

1136  
1137 
(idEvents5_Top1, y, idEvents5_Top2, x, z) 
1138 
= (idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, z_1); 
1139 

1140  
1141 
tel 
1142  
1143 
until true restart POINTEvents5_Top1 
1144  
1145  
1146  
1147 
tel 
1148  
1149  
1150 
***************************************************State :Events5_Events5 Automaton*************************************************** 
1151  
1152 
node Events5_Events5_node(idEvents5_Events5_1:int; 
1153 
idEvents5_Top1_1:int; 
1154 
y_1:real; 
1155 
idEvents5_Top2_1:int; 
1156 
x_1:real; 
1157 
E:bool; 
1158 
F:bool; 
1159 
z_1:real) 
1160  
1161 
returns (idEvents5_Events5:int; 
1162 
idEvents5_Top1:int; 
1163 
y:real; 
1164 
idEvents5_Top2:int; 
1165 
x:real; 
1166 
z:real); 
1167  
1168  
1169 
let 
1170  
1171 
automaton events5_events5 
1172  
1173 
state POINTEvents5_Events5: 
1174 
unless (idEvents5_Events5_1=0) restart EVENTS5_EVENTS5_PARALLEL_ENTRY 
1175 
unless true restart EVENTS5_EVENTS5_PARALLEL_IDL 
1176  
1177 
let 
1178  
1179 
(idEvents5_Events5, idEvents5_Top1, y, idEvents5_Top2, x, z) 
1180 
= (idEvents5_Events5_1, idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, z_1); 
1181 

1182  
1183 
tel 
1184  
1185  
1186  
1187 
state EVENTS5_EVENTS5_PARALLEL_ENTRY: 
1188  
1189 
var idEvents5_Events5_2, idEvents5_Events5_3:int; 
1190 
idEvents5_Top1_2:int; 
1191 
y_2:real; 
1192 
idEvents5_Top2_2:int; 
1193 
x_2:real; 
1194 
let 
1195  
1196 

1197 
(idEvents5_Top1_2, idEvents5_Events5_2, y_2) 
1198 
= Events5_Top1_en(idEvents5_Top1_1, idEvents5_Events5_1, y_1, false); 
1199  
1200 
(idEvents5_Top2_2, idEvents5_Events5_3, x_2) 
1201 
= Events5_Top2_en(idEvents5_Top2_1, idEvents5_Events5_2, x_1, false); 
1202  
1203  
1204 
(idEvents5_Events5, idEvents5_Top1, y, idEvents5_Top2, x) 
1205 
= (idEvents5_Events5_3, idEvents5_Top1_2, y_2, idEvents5_Top2_2, x_2); 
1206 

1207 
add unused variables 
1208 
(z) 
1209 
= (z_1); 
1210 

1211  
1212 
tel 
1213  
1214 
until true restart POINTEvents5_Events5 
1215  
1216  
1217  
1218 
state EVENTS5_EVENTS5_PARALLEL_IDL: 
1219  
1220 
var idEvents5_Top1_2:int; 
1221 
y_2:real; 
1222 
idEvents5_Top2_2, idEvents5_Top2_3:int; 
1223 
x_2, x_3:real; 
1224 
z_2:real; 
1225 
let 
1226  
1227 

1228  
1229 
(idEvents5_Top1_2, y_2, idEvents5_Top2_2, x_2, z_2) 
1230 
= if not (idEvents5_Top1_1= 0 ) then Events5_Top1_node(idEvents5_Top1_1, y_1, E, F, idEvents5_Top2_1, x_1, z_1) 
1231  
1232 
else (idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, z_1); 
1233  
1234 

1235  
1236 

1237  
1238 
(idEvents5_Top2_3, x_3) 
1239 
= if not (idEvents5_Top2_2= 0 ) then Events5_Top2_node(idEvents5_Top2_2, x_2, F) 
1240  
1241 
else (idEvents5_Top2_2, x_2); 
1242  
1243 

1244  
1245 

1246  
1247 
(idEvents5_Events5, idEvents5_Top1, y, idEvents5_Top2, x, z) 
1248 
= (idEvents5_Events5_1, idEvents5_Top1_2, y_2, idEvents5_Top2_3, x_3, z_2); 
1249 

1250  
1251 
tel 
1252  
1253 
until true restart POINTEvents5_Events5 
1254  
1255  
1256  
1257 
tel 
1258  
1259  
1260 
***************************************************State :Events5_Events5 Automaton*************************************************** 
1261  
1262 
node Events5_Events5(E:bool) 
1263  
1264 
returns (y:real; 
1265 
x:real; 
1266 
z:real); 
1267  
1268  
1269 
var y_1: real; 
1270  
1271 
x_1: real; 
1272  
1273 
z_1: real; 
1274  
1275 
F, F_1: bool; 
1276  
1277 
idEvents5_Events5, idEvents5_Events5_1: int; 
1278  
1279 
idEvents5_Top2, idEvents5_Top2_1: int; 
1280  
1281 
idEvents5_Top1, idEvents5_Top1_1: int; 
1282  
1283 
let 
1284  
1285 
y_1 = 0.0 > pre y; 
1286  
1287 
x_1 = 0.0 > pre x; 
1288  
1289 
z_1 = 0.0 > pre z; 
1290  
1291 
F_1 = false > pre F; 
1292  
1293 
idEvents5_Events5_1 = 0 > pre idEvents5_Events5; 
1294  
1295 
idEvents5_Top2_1 = 0 > pre idEvents5_Top2; 
1296  
1297 
idEvents5_Top1_1 = 0 > pre idEvents5_Top1; 
1298  
1299 

1300  
1301  
1302  
1303 
(idEvents5_Events5, idEvents5_Top1, y, idEvents5_Top2, x, z) 
1304 
= 
1305  
1306 
if E then Events5_Events5_node(idEvents5_Events5_1, idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, E, F, z_1) 
1307  
1308 
else (idEvents5_Events5_1, idEvents5_Top1_1, y_1, idEvents5_Top2_1, x_1, z_1); 
1309  
1310 

1311  
1312  
1313 
unused outputs 
1314 
F = false; 
1315  
1316 

1317  
1318 
tel 
1319  
1320  
1321  
1322 
node Events5 (E_1_1 : real) 
1323 
returns (y_1_1 : real; 
1324 
x_2_1 : real; 
1325 
z_3_1 : real); 
1326 
var 
1327 
Events5_1_1 : real; Events5_2_1 : real; Events5_3_1 : real; 
1328 
i_virtual_local : real; 
1329 
Events5E_1_1_event: bool; 
1330 
let 
1331 
Events5E_1_1_event = false > ((pre(E_1_1) > 0.0 and E_1_1 <= 0.0) or (pre(E_1_1) <= 0.0 and E_1_1 > 0.0)); 
1332 
(Events5_1_1, Events5_2_1, Events5_3_1) = Events5_Events5(Events5E_1_1_event); 
1333 
y_1_1 = Events5_1_1; 
1334 
x_2_1 = Events5_2_1; 
1335 
z_3_1 = Events5_3_1; 
1336 
i_virtual_local= 0.0 > 1.0; 
1337 
tel 
1338 