lustrectests / regression_tests / lustre_files / success / Stateflow / src_EventsOrderV2 / EventsOrderV2.lus @ eb639349
History  View  Annotate  Download (17.1 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  
17  
18 
 Entry action for state :A2_A2a 
19 
node A2_A2a_en(idA_A2_1:int; 
20 
a_1:int; 
21 
isInner:bool) 
22  
23 
returns (idA_A2:int; 
24 
a:int); 
25  
26  
27 
var idA_A2_2:int; 
28 
a_2:int; 
29  
30  
31 
let 
32  
33  
34  
35 
 set state as active 
36 
idA_A2_2 
37 
= 721; 
38 

39  
40 
a_2 
41 
= if (not isInner) then a_1 +3 
42 
else a_1; 
43 

44  
45 
(idA_A2, a) 
46 
= (idA_A2_2, a_2); 
47 

48  
49 
tel 
50  
51  
52  
53  
54  
55 
 Exit action for state :A2_A2a 
56 
node A2_A2a_ex(idA_A2_1:int; 
57 
isInner:bool) 
58  
59 
returns (idA_A2:int); 
60  
61  
62 
var idA_A2_2:int; 
63  
64  
65 
let 
66  
67  
68  
69 
 set state as inactive 
70 
idA_A2_2 
71 
= if (not isInner) then 0 else idA_A2_1; 
72  
73  
74 
(idA_A2) 
75 
= (idA_A2_1); 
76 

77  
78 
tel 
79  
80  
81  
82  
83  
84  
85 
 Entry action for state :A2_A2b 
86 
node A2_A2b_en(idA_A2_1:int; 
87 
a_1:int; 
88 
isInner:bool) 
89  
90 
returns (idA_A2:int; 
91 
a:int); 
92  
93  
94 
var idA_A2_2:int; 
95 
a_2:int; 
96  
97  
98 
let 
99  
100  
101  
102 
 set state as active 
103 
idA_A2_2 
104 
= 722; 
105 

106  
107 
a_2 
108 
= if (not isInner) then a_1 +4 
109 
else a_1; 
110 

111  
112 
(idA_A2, a) 
113 
= (idA_A2_2, a_2); 
114 

115  
116 
tel 
117  
118  
119  
120  
121  
122 
 Exit action for state :A2_A2b 
123 
node A2_A2b_ex(idA_A2_1:int; 
124 
isInner:bool) 
125  
126 
returns (idA_A2:int); 
127  
128  
129 
var idA_A2_2:int; 
130  
131  
132 
let 
133  
134  
135  
136 
 set state as inactive 
137 
idA_A2_2 
138 
= if (not isInner) then 0 else idA_A2_1; 
139  
140  
141 
(idA_A2) 
142 
= (idA_A2_1); 
143 

144  
145 
tel 
146  
147  
148  
149  
150  
151  
152 
 Entry action for state :A_A2 
153 
node A_A2_en(idA_A2_1:int; 
154 
idEvents1_A_1:int; 
155 
a_1:int; 
156 
isInner:bool) 
157  
158 
returns (idA_A2:int; 
159 
idEvents1_A:int; 
160 
a:int); 
161  
162  
163 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int; 
164 
idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int; 
165 
a_2, a_3, a_4, a_5, a_6:int; 
166  
167  
168 
let 
169  
170  
171  
172 
 set state as active 
173 
idEvents1_A_2 
174 
= 720; 
175 

176  
177 

178 
 transition trace : 
179 
POINT__To__A2_A2a_1 
180 
(idA_A2_2, a_2) 
181 
= A2_A2a_en(idA_A2_1, a_1, false); 
182 

183  
184 
(idA_A2_3, idEvents1_A_3, a_3) 
185 
= 
186  
187 
if ( idA_A2_1 = 0) then 
188  
189 
(idA_A2_2, idEvents1_A_2, a_2) 
190  
191 
else(idA_A2_1, idEvents1_A_2, a_1); 
192  
193 

194  
195 
(idA_A2_4, a_4) 
196 
= 
197 
if ( idA_A2_1 = 721) then 
198 
A2_A2a_en(idA_A2_1, a_1, false) 
199 
else (idA_A2_1, a_1); 
200  
201 

202  
203 
(idA_A2_5, a_5) 
204 
= 
205 
if ( idA_A2_1 = 722) then 
206 
A2_A2b_en(idA_A2_1, a_1, false) 
207 
else (idA_A2_1, a_1); 
208  
209 

210  
211 
(idA_A2_6, idEvents1_A_4, a_6) 
212 
= 
213 
if ( idA_A2_1 = 0) then 
214 
(idA_A2_3, idEvents1_A_3, a_3) 
215 
else 
216 
if ( idA_A2_1 = 721) then 
217 
(idA_A2_4, idEvents1_A_3, a_4) 
218 
else 
219 
if ( idA_A2_1 = 722) then 
220 
(idA_A2_5, idEvents1_A_3, a_5) 
221 
else (idA_A2_1, idEvents1_A_2, a_1); 
222  
223  
224 
(idA_A2, idEvents1_A, a) 
225 
= (idA_A2_6, idEvents1_A_4, a_6); 
226 

227  
228 
tel 
229  
230  
231  
232  
233  
234 
 Exit action for state :A_A2 
235 
node A_A2_ex(idA_A2_1:int; 
236 
idEvents1_A_1:int; 
237 
isInner:bool) 
238  
239 
returns (idA_A2:int; 
240 
idEvents1_A:int); 
241  
242  
243 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int; 
244 
idEvents1_A_2:int; 
245  
246  
247 
let 
248  
249  
250  
251 

252 
(idA_A2_2) 
253 
= 
254 
if ( idA_A2_1 = 721) then 
255 
A2_A2a_ex(idA_A2_1, false) 
256 
else (idA_A2_1); 
257  
258 

259  
260 
(idA_A2_3) 
261 
= 
262 
if ( idA_A2_1 = 722) then 
263 
A2_A2b_ex(idA_A2_1, false) 
264 
else (idA_A2_1); 
265  
266 

267  
268 
(idA_A2_4) 
269 
= 
270 
if ( idA_A2_1 = 721) then 
271 
(idA_A2_2) 
272 
else 
273 
if ( idA_A2_1 = 722) then 
274 
(idA_A2_3) 
275 
else (idA_A2_1); 
276  
277  
278 
 set state as inactive 
279 
idEvents1_A_2 
280 
= if (not isInner) then 0 else idEvents1_A_1; 
281  
282 
idA_A2_5 
283 
= 0; 
284 

285  
286 
(idA_A2, idEvents1_A) 
287 
= (idA_A2_5, idEvents1_A_1); 
288 

289  
290 
tel 
291  
292  
293  
294  
295  
296  
297 
 Entry action for state :A1_A1b 
298 
node A1_A1b_en(idA_A1_1:int; 
299 
a_1:int; 
300 
isInner:bool) 
301  
302 
returns (idA_A1:int; 
303 
a:int); 
304  
305  
306 
var idA_A1_2:int; 
307 
a_2:int; 
308  
309  
310 
let 
311  
312  
313  
314 
 set state as active 
315 
idA_A1_2 
316 
= 725; 
317 

318  
319 
a_2 
320 
= if (not isInner) then a_1 +2 
321 
else a_1; 
322 

323  
324 
(idA_A1, a) 
325 
= (idA_A1_2, a_2); 
326 

327  
328 
tel 
329  
330  
331  
332  
333  
334 
 Exit action for state :A1_A1b 
335 
node A1_A1b_ex(idA_A1_1:int; 
336 
isInner:bool) 
337  
338 
returns (idA_A1:int); 
339  
340  
341 
var idA_A1_2:int; 
342  
343  
344 
let 
345  
346  
347  
348 
 set state as inactive 
349 
idA_A1_2 
350 
= if (not isInner) then 0 else idA_A1_1; 
351  
352  
353 
(idA_A1) 
354 
= (idA_A1_1); 
355 

356  
357 
tel 
358  
359  
360  
361  
362  
363  
364 
 Entry action for state :A1_A1a 
365 
node A1_A1a_en(idA_A1_1:int; 
366 
a_1:int; 
367 
isInner:bool) 
368  
369 
returns (idA_A1:int; 
370 
a:int); 
371  
372  
373 
var idA_A1_2:int; 
374 
a_2:int; 
375  
376  
377 
let 
378  
379  
380  
381 
 set state as active 
382 
idA_A1_2 
383 
= 724; 
384 

385  
386 
a_2 
387 
= if (not isInner) then a_1 +1 
388 
else a_1; 
389 

390  
391 
(idA_A1, a) 
392 
= (idA_A1_2, a_2); 
393 

394  
395 
tel 
396  
397  
398  
399  
400  
401 
 Exit action for state :A1_A1a 
402 
node A1_A1a_ex(idA_A1_1:int; 
403 
isInner:bool) 
404  
405 
returns (idA_A1:int); 
406  
407  
408 
var idA_A1_2:int; 
409  
410  
411 
let 
412  
413  
414  
415 
 set state as inactive 
416 
idA_A1_2 
417 
= if (not isInner) then 0 else idA_A1_1; 
418  
419  
420 
(idA_A1) 
421 
= (idA_A1_1); 
422 

423  
424 
tel 
425  
426  
427  
428  
429  
430  
431 
 Entry action for state :A_A1 
432 
node A_A1_en(idA_A1_1:int; 
433 
idEvents1_A_1:int; 
434 
a_1:int; 
435 
isInner:bool) 
436  
437 
returns (idA_A1:int; 
438 
idEvents1_A:int; 
439 
a:int); 
440  
441  
442 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int; 
443 
idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int; 
444 
a_2, a_3, a_4, a_5, a_6:int; 
445  
446  
447 
let 
448  
449  
450  
451 
 set state as active 
452 
idEvents1_A_2 
453 
= 723; 
454 

455  
456 

457 
 transition trace : 
458 
POINT__To__A1_A1a_1 
459 
(idA_A1_2, a_2) 
460 
= A1_A1a_en(idA_A1_1, a_1, false); 
461 

462  
463 
(idA_A1_3, idEvents1_A_3, a_3) 
464 
= 
465  
466 
if ( idA_A1_1 = 0) then 
467  
468 
(idA_A1_2, idEvents1_A_2, a_2) 
469  
470 
else(idA_A1_1, idEvents1_A_2, a_1); 
471  
472 

473  
474 
(idA_A1_4, a_4) 
475 
= 
476 
if ( idA_A1_1 = 724) then 
477 
A1_A1a_en(idA_A1_1, a_1, false) 
478 
else (idA_A1_1, a_1); 
479  
480 

481  
482 
(idA_A1_5, a_5) 
483 
= 
484 
if ( idA_A1_1 = 725) then 
485 
A1_A1b_en(idA_A1_1, a_1, false) 
486 
else (idA_A1_1, a_1); 
487  
488 

489  
490 
(idA_A1_6, idEvents1_A_4, a_6) 
491 
= 
492 
if ( idA_A1_1 = 0) then 
493 
(idA_A1_3, idEvents1_A_3, a_3) 
494 
else 
495 
if ( idA_A1_1 = 724) then 
496 
(idA_A1_4, idEvents1_A_3, a_4) 
497 
else 
498 
if ( idA_A1_1 = 725) then 
499 
(idA_A1_5, idEvents1_A_3, a_5) 
500 
else (idA_A1_1, idEvents1_A_2, a_1); 
501  
502  
503 
(idA_A1, idEvents1_A, a) 
504 
= (idA_A1_6, idEvents1_A_4, a_6); 
505 

506  
507 
tel 
508  
509  
510  
511  
512  
513 
 Exit action for state :A_A1 
514 
node A_A1_ex(idA_A1_1:int; 
515 
idEvents1_A_1:int; 
516 
isInner:bool) 
517  
518 
returns (idA_A1:int; 
519 
idEvents1_A:int); 
520  
521  
522 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
523 
idEvents1_A_2:int; 
524  
525  
526 
let 
527  
528  
529  
530 

531 
(idA_A1_2) 
532 
= 
533 
if ( idA_A1_1 = 724) then 
534 
A1_A1a_ex(idA_A1_1, false) 
535 
else (idA_A1_1); 
536  
537 

538  
539 
(idA_A1_3) 
540 
= 
541 
if ( idA_A1_1 = 725) then 
542 
A1_A1b_ex(idA_A1_1, false) 
543 
else (idA_A1_1); 
544  
545 

546  
547 
(idA_A1_4) 
548 
= 
549 
if ( idA_A1_1 = 724) then 
550 
(idA_A1_2) 
551 
else 
552 
if ( idA_A1_1 = 725) then 
553 
(idA_A1_3) 
554 
else (idA_A1_1); 
555  
556  
557 
 set state as inactive 
558 
idEvents1_A_2 
559 
= if (not isInner) then 0 else idEvents1_A_1; 
560  
561 
idA_A1_5 
562 
= 0; 
563 

564  
565 
(idA_A1, idEvents1_A) 
566 
= (idA_A1_5, idEvents1_A_1); 
567 

568  
569 
tel 
570  
571  
572  
573  
574  
575  
576 
 Entry action for state :Events1_A 
577 
node Events1_A_en(idEvents1_A_1:int; 
578 
idEvents1_Events1_1:int; 
579 
a_1:int; 
580 
idA_A1_1:int; 
581 
idA_A2_1:int; 
582 
isInner:bool) 
583  
584 
returns (idEvents1_A:int; 
585 
idEvents1_Events1:int; 
586 
a:int; 
587 
idA_A1:int; 
588 
idA_A2:int); 
589  
590  
591 
var idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5, idEvents1_A_6:int; 
592 
idEvents1_Events1_2, idEvents1_Events1_3, idEvents1_Events1_4:int; 
593 
a_2, a_3, a_4, a_5, a_6:int; 
594 
idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
595 
idA_A2_2, idA_A2_3:int; 
596  
597  
598 
let 
599  
600  
601  
602 
 set state as active 
603 
idEvents1_Events1_2 
604 
= 719; 
605 

606  
607 

608 
 transition trace : 
609 
POINT__To__A_A1_1 
610 
(idA_A1_2, idEvents1_A_2, a_2) 
611 
= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false); 
612 

613  
614 
(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3) 
615 
= 
616  
617 
if ( idEvents1_A_1 = 0) then 
618  
619 
(idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2) 
620  
621 
else(idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1); 
622  
623 

624  
625 
(idA_A2_2, idEvents1_A_4, a_4) 
626 
= 
627 
if ( idEvents1_A_1 = 720) then 
628 
A_A2_en(idA_A2_1, idEvents1_A_1, a_1, false) 
629 
else (idA_A2_1, idEvents1_A_1, a_1); 
630  
631 

632  
633 
(idA_A1_4, idEvents1_A_5, a_5) 
634 
= 
635 
if ( idEvents1_A_1 = 723) then 
636 
A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false) 
637 
else (idA_A1_1, idEvents1_A_1, a_1); 
638  
639 

640  
641 
(idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3) 
642 
= 
643 
if ( idEvents1_A_1 = 0) then 
644 
(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_1) 
645 
else 
646 
if ( idEvents1_A_1 = 720) then 
647 
(idEvents1_A_4, idEvents1_Events1_3, a_4, idA_A1_1, idA_A2_2) 
648 
else 
649 
if ( idEvents1_A_1 = 723) then 
650 
(idEvents1_A_5, idEvents1_Events1_3, a_5, idA_A1_4, idA_A2_1) 
651 
else (idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1, idA_A2_1); 
652  
653  
654 
(idEvents1_A, idEvents1_Events1, a, idA_A1, idA_A2) 
655 
= (idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3); 
656 

657  
658 
tel 
659  
660  
661  
662  
663  
664 
 Exit action for state :Events1_A 
665 
node Events1_A_ex(idA_A2_1:int; 
666 
idEvents1_A_1:int; 
667 
idA_A1_1:int; 
668 
idEvents1_Events1_1:int; 
669 
isInner:bool) 
670  
671 
returns (idA_A2:int; 
672 
idEvents1_A:int; 
673 
idA_A1:int; 
674 
idEvents1_Events1:int); 
675  
676  
677 
var idA_A2_2, idA_A2_3:int; 
678 
idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5:int; 
679 
idA_A1_2, idA_A1_3:int; 
680 
idEvents1_Events1_2:int; 
681  
682  
683 
let 
684  
685  
686  
687 

688 
(idA_A2_2, idEvents1_A_2) 
689 
= 
690 
if ( idEvents1_A_1 = 720) then 
691 
A_A2_ex(idA_A2_1, idEvents1_A_1, false) 
692 
else (idA_A2_1, idEvents1_A_1); 
693  
694 

695  
696 
(idA_A1_2, idEvents1_A_3) 
697 
= 
698 
if ( idEvents1_A_1 = 723) then 
699 
A_A1_ex(idA_A1_1, idEvents1_A_1, false) 
700 
else (idA_A1_1, idEvents1_A_1); 
701  
702 

703  
704 
(idA_A2_3, idEvents1_A_4, idA_A1_3) 
705 
= 
706 
if ( idEvents1_A_1 = 720) then 
707 
(idA_A2_2, idEvents1_A_2, idA_A1_1) 
708 
else 
709 
if ( idEvents1_A_1 = 723) then 
710 
(idA_A2_1, idEvents1_A_3, idA_A1_2) 
711 
else (idA_A2_1, idEvents1_A_1, idA_A1_1); 
712  
713  
714 
 set state as inactive 
715 
idEvents1_Events1_2 
716 
= if (not isInner) then 0 else idEvents1_Events1_1; 
717  
718 
idEvents1_A_5 
719 
= 0; 
720 

721  
722 
(idA_A2, idEvents1_A, idA_A1, idEvents1_Events1) 
723 
= (idA_A2_3, idEvents1_A_5, idA_A1_3, idEvents1_Events1_1); 
724 

725  
726 
tel 
727  
728  
729 
***************************************************State :A_A2 Automaton*************************************************** 
730  
731 
node A_A2_node(idA_A2_1:int; 
732 
a_1:int; 
733 
S:bool; 
734 
R:bool) 
735  
736 
returns (idA_A2:int; 
737 
a:int); 
738  
739  
740 
let 
741  
742 
automaton a_a2 
743  
744 
state POINTA_A2: 
745 
unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1 
746  
747  
748  
749 
unless (idA_A2_1=721) and ( S ) restart A2_A2A__TO__A2_A2B_1 
750  
751  
752  
753 
unless (idA_A2_1=722) and ( R ) restart A2_A2B__TO__A2_A2A_1 
754  
755  
756  
757 
unless (idA_A2_1=721) restart A2_A2A_IDL 
758  
759 
unless (idA_A2_1=722) restart A2_A2B_IDL 
760  
761 
let 
762  
763 
(idA_A2, a) 
764 
= (idA_A2_1, a_1); 
765 

766  
767 
tel 
768  
769  
770  
771 
state POINT__TO__A2_A2A_1: 
772  
773 
var idA_A2_2:int; 
774 
a_2:int; 
775 
let 
776  
777 
 transition trace : 
778 
POINT__To__A2_A2a_1 
779 
(idA_A2_2, a_2) 
780 
= A2_A2a_en(idA_A2_1, a_1, false); 
781 

782  
783 
(idA_A2, a) 
784 
= (idA_A2_2, a_2); 
785  
786  
787 
tel 
788  
789 
until true restart POINTA_A2 
790  
791  
792  
793 
state A2_A2A__TO__A2_A2B_1: 
794  
795 
var idA_A2_2, idA_A2_3:int; 
796 
a_2:int; 
797 
let 
798  
799 
 transition trace : 
800 
A2_A2a__To__A2_A2b_1 
801 
(idA_A2_2) 
802 
= A2_A2a_ex(idA_A2_1, false); 
803 

804  
805 
(idA_A2_3, a_2) 
806 
= A2_A2b_en(idA_A2_2, a_1, false); 
807 

808  
809 
(idA_A2, a) 
810 
= (idA_A2_3, a_2); 
811  
812  
813 
tel 
814  
815 
until true restart POINTA_A2 
816  
817  
818  
819 
state A2_A2B__TO__A2_A2A_1: 
820  
821 
var idA_A2_2, idA_A2_3:int; 
822 
a_2:int; 
823 
let 
824  
825 
 transition trace : 
826 
A2_A2b__To__A2_A2a_1 
827 
(idA_A2_2) 
828 
= A2_A2b_ex(idA_A2_1, false); 
829 

830  
831 
(idA_A2_3, a_2) 
832 
= A2_A2a_en(idA_A2_2, a_1, false); 
833 

834  
835 
(idA_A2, a) 
836 
= (idA_A2_3, a_2); 
837  
838  
839 
tel 
840  
841 
until true restart POINTA_A2 
842  
843  
844  
845 
state A2_A2A_IDL: 
846  
847 
let 
848  
849 

850  
851 
(idA_A2, a) 
852 
= (idA_A2_1, a_1); 
853 

854  
855 
tel 
856  
857 
until true restart POINTA_A2 
858  
859  
860  
861 
state A2_A2B_IDL: 
862  
863 
let 
864  
865 

866  
867 
(idA_A2, a) 
868 
= (idA_A2_1, a_1); 
869 

870  
871 
tel 
872  
873 
until true restart POINTA_A2 
874  
875  
876  
877 
tel 
878  
879  
880 
***************************************************State :A_A1 Automaton*************************************************** 
881  
882 
node A_A1_node(idA_A1_1:int; 
883 
a_1:int; 
884 
S:bool; 
885 
R:bool) 
886  
887 
returns (idA_A1:int; 
888 
a:int); 
889  
890  
891 
let 
892  
893 
automaton a_a1 
894  
895 
state POINTA_A1: 
896 
unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1 
897  
898  
899  
900 
unless (idA_A1_1=724) and ( S ) restart A1_A1A__TO__A1_A1B_1 
901  
902  
903  
904 
unless (idA_A1_1=725) and ( R ) restart A1_A1B__TO__A1_A1A_1 
905  
906  
907  
908 
unless (idA_A1_1=724) restart A1_A1A_IDL 
909  
910 
unless (idA_A1_1=725) restart A1_A1B_IDL 
911  
912 
let 
913  
914 
(idA_A1, a) 
915 
= (idA_A1_1, a_1); 
916 

917  
918 
tel 
919  
920  
921  
922 
state POINT__TO__A1_A1A_1: 
923  
924 
var idA_A1_2:int; 
925 
a_2:int; 
926 
let 
927  
928 
 transition trace : 
929 
POINT__To__A1_A1a_1 
930 
(idA_A1_2, a_2) 
931 
= A1_A1a_en(idA_A1_1, a_1, false); 
932 

933  
934 
(idA_A1, a) 
935 
= (idA_A1_2, a_2); 
936  
937  
938 
tel 
939  
940 
until true restart POINTA_A1 
941  
942  
943  
944 
state A1_A1A__TO__A1_A1B_1: 
945  
946 
var idA_A1_2, idA_A1_3:int; 
947 
a_2:int; 
948 
let 
949  
950 
 transition trace : 
951 
A1_A1a__To__A1_A1b_1 
952 
(idA_A1_2) 
953 
= A1_A1a_ex(idA_A1_1, false); 
954 

955  
956 
(idA_A1_3, a_2) 
957 
= A1_A1b_en(idA_A1_2, a_1, false); 
958 

959  
960 
(idA_A1, a) 
961 
= (idA_A1_3, a_2); 
962  
963  
964 
tel 
965  
966 
until true restart POINTA_A1 
967  
968  
969  
970 
state A1_A1B__TO__A1_A1A_1: 
971  
972 
var idA_A1_2, idA_A1_3:int; 
973 
a_2:int; 
974 
let 
975  
976 
 transition trace : 
977 
A1_A1b__To__A1_A1a_1 
978 
(idA_A1_2) 
979 
= A1_A1b_ex(idA_A1_1, false); 
980 

981  
982 
(idA_A1_3, a_2) 
983 
= A1_A1a_en(idA_A1_2, a_1, false); 
984 

985  
986 
(idA_A1, a) 
987 
= (idA_A1_3, a_2); 
988  
989  
990 
tel 
991  
992 
until true restart POINTA_A1 
993  
994  
995  
996 
state A1_A1A_IDL: 
997  
998 
let 
999  
1000 

1001  
1002 
(idA_A1, a) 
1003 
= (idA_A1_1, a_1); 
1004 

1005  
1006 
tel 
1007  
1008 
until true restart POINTA_A1 
1009  
1010  
1011  
1012 
state A1_A1B_IDL: 
1013  
1014 
let 
1015  
1016 

1017  
1018 
(idA_A1, a) 
1019 
= (idA_A1_1, a_1); 
1020 

1021  
1022 
tel 
1023  
1024 
until true restart POINTA_A1 
1025  
1026  
1027  
1028 
tel 
1029  
1030  
1031 
***************************************************State :Events1_A Automaton*************************************************** 
1032  
1033 
node Events1_A_node(idEvents1_A_1:int; 
1034 
a_1:int; 
1035 
idA_A1_1:int; 
1036 
T:bool; 
1037 
idA_A2_1:int; 
1038 
R:bool; 
1039 
S:bool) 
1040  
1041 
returns (idEvents1_A:int; 
1042 
a:int; 
1043 
idA_A1:int; 
1044 
idA_A2:int); 
1045  
1046  
1047 
let 
1048  
1049 
automaton events1_a 
1050  
1051 
state POINTEvents1_A: 
1052 
unless (idEvents1_A_1=0) restart POINT__TO__A_A1_1 
1053  
1054  
1055  
1056 
unless (idEvents1_A_1=720) and ( T ) restart A_A2__TO__A_A1_1 
1057  
1058  
1059  
1060 
unless (idEvents1_A_1=723) and ( T ) restart A_A1__TO__A_A2_1 
1061  
1062  
1063  
1064 
unless (idEvents1_A_1=720) restart A_A2_IDL 
1065  
1066 
unless (idEvents1_A_1=723) restart A_A1_IDL 
1067  
1068 
let 
1069  
1070 
(idEvents1_A, a, idA_A1, idA_A2) 
1071 
= (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1); 
1072 

1073  
1074 
tel 
1075  
1076  
1077  
1078 
state POINT__TO__A_A1_1: 
1079  
1080 
var idEvents1_A_2:int; 
1081 
a_2:int; 
1082 
idA_A1_2:int; 
1083 
let 
1084  
1085 
 transition trace : 
1086 
POINT__To__A_A1_1 
1087 
(idA_A1_2, idEvents1_A_2, a_2) 
1088 
= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false); 
1089 

1090  
1091 
(idEvents1_A, a, idA_A1) 
1092 
= (idEvents1_A_2, a_2, idA_A1_2); 
1093  
1094 
add unused variables 
1095 
(idA_A2) 
1096 
= (idA_A2_1); 
1097 

1098  
1099 
tel 
1100  
1101 
until true restart POINTEvents1_A 
1102  
1103  
1104  
1105 
state A_A2__TO__A_A1_1: 
1106  
1107 
var idEvents1_A_2, idEvents1_A_3:int; 
1108 
a_2:int; 
1109 
idA_A1_2:int; 
1110 
idA_A2_2:int; 
1111 
let 
1112  
1113 
 transition trace : 
1114 
A_A2__To__A_A1_1 
1115 
(idA_A2_2, idEvents1_A_2) 
1116 
= A_A2_ex(idA_A2_1, idEvents1_A_1, false); 
1117 

1118  
1119 
(idA_A1_2, idEvents1_A_3, a_2) 
1120 
= A_A1_en(idA_A1_1, idEvents1_A_2, a_1, false); 
1121 

1122  
1123 
(idEvents1_A, a, idA_A1, idA_A2) 
1124 
= (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2); 
1125  
1126  
1127 
tel 
1128  
1129 
until true restart POINTEvents1_A 
1130  
1131  
1132  
1133 
state A_A1__TO__A_A2_1: 
1134  
1135 
var idEvents1_A_2, idEvents1_A_3:int; 
1136 
a_2:int; 
1137 
idA_A1_2:int; 
1138 
idA_A2_2:int; 
1139 
let 
1140  
1141 
 transition trace : 
1142 
A_A1__To__A_A2_1 
1143 
(idA_A1_2, idEvents1_A_2) 
1144 
= A_A1_ex(idA_A1_1, idEvents1_A_1, false); 
1145 

1146  
1147 
(idA_A2_2, idEvents1_A_3, a_2) 
1148 
= A_A2_en(idA_A2_1, idEvents1_A_2, a_1, false); 
1149 

1150  
1151 
(idEvents1_A, a, idA_A1, idA_A2) 
1152 
= (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2); 
1153  
1154  
1155 
tel 
1156  
1157 
until true restart POINTEvents1_A 
1158  
1159  
1160  
1161 
state A_A2_IDL: 
1162  
1163 
var a_2:int; 
1164 
idA_A2_2:int; 
1165 
let 
1166  
1167 

1168 
(idA_A2_2, a_2) 
1169 
= A_A2_node(idA_A2_1, a_1, S, R); 
1170  
1171 

1172  
1173  
1174 
(idEvents1_A, a, idA_A1, idA_A2) 
1175 
= (idEvents1_A_1, a_2, idA_A1_1, idA_A2_2); 
1176 

1177  
1178 
tel 
1179  
1180 
until true restart POINTEvents1_A 
1181  
1182  
1183  
1184 
state A_A1_IDL: 
1185  
1186 
var a_2:int; 
1187 
idA_A1_2:int; 
1188 
let 
1189  
1190 

1191 
(idA_A1_2, a_2) 
1192 
= A_A1_node(idA_A1_1, a_1, S, R); 
1193  
1194 

1195  
1196  
1197 
(idEvents1_A, a, idA_A1, idA_A2) 
1198 
= (idEvents1_A_1, a_2, idA_A1_2, idA_A2_1); 
1199 

1200  
1201 
tel 
1202  
1203 
until true restart POINTEvents1_A 
1204  
1205  
1206  
1207 
tel 
1208  
1209  
1210 
***************************************************State :Events1_Events1 Automaton*************************************************** 
1211  
1212 
node Events1_Events1_node(idEvents1_Events1_1:int; 
1213 
a_1:int; 
1214 
idA_A1_1:int; 
1215 
idA_A2_1:int; 
1216 
idEvents1_A_1:int; 
1217 
R:bool; 
1218 
S:bool; 
1219 
T:bool) 
1220  
1221 
returns (idEvents1_Events1:int; 
1222 
a:int; 
1223 
idA_A1:int; 
1224 
idA_A2:int; 
1225 
idEvents1_A:int); 
1226  
1227  
1228 
let 
1229  
1230 
automaton events1_events1 
1231  
1232 
state POINTEvents1_Events1: 
1233 
unless (idEvents1_Events1_1=0) restart POINT__TO__EVENTS1_A_1 
1234  
1235  
1236  
1237 
unless true restart EVENTS1_EVENTS1_PARALLEL_IDL 
1238  
1239 
let 
1240  
1241 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A) 
1242 
= (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1); 
1243 

1244  
1245 
tel 
1246  
1247  
1248  
1249 
state POINT__TO__EVENTS1_A_1: 
1250  
1251 
var idEvents1_Events1_2:int; 
1252 
a_2:int; 
1253 
idA_A1_2:int; 
1254 
idA_A2_2:int; 
1255 
idEvents1_A_2:int; 
1256 
let 
1257  
1258 
 transition trace : 
1259 
POINT__To__Events1_A_1 
1260 
(idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2) 
1261 
= Events1_A_en(idEvents1_A_1, idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, false); 
1262 

1263  
1264 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A) 
1265 
= (idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2); 
1266  
1267  
1268 
tel 
1269  
1270 
until true restart POINTEvents1_Events1 
1271  
1272  
1273  
1274 
state EVENTS1_EVENTS1_PARALLEL_IDL: 
1275  
1276 
var a_2:int; 
1277 
idA_A1_2:int; 
1278 
idA_A2_2:int; 
1279 
idEvents1_A_2:int; 
1280 
let 
1281  
1282 

1283  
1284 
(idEvents1_A_2, a_2, idA_A1_2, idA_A2_2) 
1285 
= if not (idEvents1_A_1= 0 ) then Events1_A_node(idEvents1_A_1, a_1, idA_A1_1, T, idA_A2_1, R, S) 
1286  
1287 
else (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1); 
1288  
1289 

1290  
1291 

1292  
1293 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A) 
1294 
= (idEvents1_Events1_1, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2); 
1295 

1296  
1297 
tel 
1298  
1299 
until true restart POINTEvents1_Events1 
1300  
1301  
1302  
1303 
tel 
1304  
1305  
1306 
***************************************************State :Events1_Events1 Automaton*************************************************** 
1307  
1308 
node EventsOrderV2_Events1(R:bool; 
1309 
S:bool; 
1310 
T:bool) 
1311  
1312 
returns (a:int); 
1313  
1314  
1315 
var a_1: int; 
1316  
1317 
idEvents1_Events1, idEvents1_Events1_1: int; 
1318  
1319 
idA_A2, idA_A2_1: int; 
1320  
1321 
idA_A1, idA_A1_1: int; 
1322  
1323 
idEvents1_A, idEvents1_A_1: int; 
1324  
1325 
let 
1326  
1327 
a_1 = 0 > pre a; 
1328  
1329 
idEvents1_Events1_1 = 0 > pre idEvents1_Events1; 
1330  
1331 
idA_A2_1 = 0 > pre idA_A2; 
1332  
1333 
idA_A1_1 = 0 > pre idA_A1; 
1334  
1335 
idEvents1_A_1 = 0 > pre idEvents1_A; 
1336  
1337 

1338  
1339  
1340  
1341 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A) 
1342 
= Events1_Events1_node(idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, R, S, T); 
1343  
1344  
1345 
unused outputs 
1346 

1347  
1348 
tel 
1349  
1350  
1351  
1352 
node EventsOrderV2 (R_1_1 : bool; S_1_1 : bool; T_1_1 : bool) 
1353 
returns (a_1_1 : int); 
1354 
var 
1355 
Events1_1_1 : int; 
1356 
i_virtual_local : real; 
1357 
let 
1358 
Events1_1_1 = EventsOrderV2_Events1(R_1_1, S_1_1, T_1_1); 
1359 
a_1_1 = Events1_1_1; 
1360 
i_virtual_local= 0.0 > 1.0; 
1361 
tel 
1362 