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

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9  
10  
11  
12 
node B_B1__To__B_B2_1_Transition_Action(c_1:int) 
13  
14 
returns (c:int); 
15  
16  
17 
var c_2:int; 
18  
19  
20 
let 
21  
22  
23  
24 
c_2 
25 
= c_1 + 1; 
26 

27  
28 
(c) 
29 
= (c_2); 
30 

31  
32 
tel 
33  
34  
35  
36  
37  
38  
39 
node B_B2__To__B_B1_1_Transition_Action(c_1:int) 
40  
41 
returns (c:int); 
42  
43  
44 
var c_2:int; 
45  
46  
47 
let 
48  
49  
50  
51 
c_2 
52 
= c_1 + 1; 
53 

54  
55 
(c) 
56 
= (c_2); 
57 

58  
59 
tel 
60  
61  
62  
63  
64  
65  
66  
67  
68  
69  
70  
71  
72  
73 
 Entry action for state :B2_B2a 
74 
node B2_B2a_en(idB_B2_1:int; 
75 
x:int; 
76 
b_1:int; 
77 
isInner:bool) 
78  
79 
returns (idB_B2:int; 
80 
b:int); 
81  
82  
83 
var idB_B2_2:int; 
84 
b_2:int; 
85  
86  
87 
let 
88  
89  
90  
91 
 set state as active 
92 
idB_B2_2 
93 
= 574; 
94 

95  
96 
b_2 
97 
= if (not isInner) then x+7 
98 
else b_1; 
99 

100  
101 
(idB_B2, b) 
102 
= (idB_B2_2, b_2); 
103 

104  
105 
tel 
106  
107  
108  
109  
110  
111 
 Exit action for state :B2_B2a 
112 
node B2_B2a_ex(idB_B2_1:int; 
113 
isInner:bool) 
114  
115 
returns (idB_B2:int); 
116  
117  
118 
var idB_B2_2:int; 
119  
120  
121 
let 
122  
123  
124  
125 
 set state as inactive 
126 
idB_B2_2 
127 
= if (not isInner) then 0 else idB_B2_1; 
128  
129  
130 
(idB_B2) 
131 
= (idB_B2_1); 
132 

133  
134 
tel 
135  
136  
137  
138  
139  
140  
141 
 Entry action for state :B2_B2b 
142 
node B2_B2b_en(idB_B2_1:int; 
143 
x:int; 
144 
b_1:int; 
145 
isInner:bool) 
146  
147 
returns (idB_B2:int; 
148 
b:int); 
149  
150  
151 
var idB_B2_2:int; 
152 
b_2:int; 
153  
154  
155 
let 
156  
157  
158  
159 
 set state as active 
160 
idB_B2_2 
161 
= 575; 
162 

163  
164 
b_2 
165 
= if (not isInner) then x+8 
166 
else b_1; 
167 

168  
169 
(idB_B2, b) 
170 
= (idB_B2_2, b_2); 
171 

172  
173 
tel 
174  
175  
176  
177  
178  
179 
 Exit action for state :B2_B2b 
180 
node B2_B2b_ex(idB_B2_1:int; 
181 
isInner:bool) 
182  
183 
returns (idB_B2:int); 
184  
185  
186 
var idB_B2_2:int; 
187  
188  
189 
let 
190  
191  
192  
193 
 set state as inactive 
194 
idB_B2_2 
195 
= if (not isInner) then 0 else idB_B2_1; 
196  
197  
198 
(idB_B2) 
199 
= (idB_B2_1); 
200 

201  
202 
tel 
203  
204  
205  
206  
207  
208  
209 
 Entry action for state :B_B2 
210 
node B_B2_en(idB_B2_1:int; 
211 
idEvents1_B_1:int; 
212 
b_1:int; 
213 
x:int; 
214 
isInner:bool) 
215  
216 
returns (idB_B2:int; 
217 
idEvents1_B:int; 
218 
b:int); 
219  
220  
221 
var idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5, idB_B2_6:int; 
222 
idEvents1_B_2, idEvents1_B_3, idEvents1_B_4:int; 
223 
b_2, b_3, b_4, b_5, b_6:int; 
224  
225  
226 
let 
227  
228  
229  
230 
 set state as active 
231 
idEvents1_B_2 
232 
= 573; 
233 

234  
235 

236 
 transition trace : 
237 
POINT__To__B2_B2a_1 
238 
(idB_B2_2, b_2) 
239 
= B2_B2a_en(idB_B2_1, x, b_1, false); 
240 

241  
242 
(idB_B2_3, idEvents1_B_3, b_3) 
243 
= 
244  
245 
if ( idB_B2_1 = 0) then 
246  
247 
(idB_B2_2, idEvents1_B_2, b_2) 
248  
249 
else(idB_B2_1, idEvents1_B_2, b_1); 
250  
251 

252  
253 
(idB_B2_4, b_4) 
254 
= 
255 
if ( idB_B2_1 = 574) then 
256 
B2_B2a_en(idB_B2_1, x, b_1, false) 
257 
else (idB_B2_1, b_1); 
258  
259 

260  
261 
(idB_B2_5, b_5) 
262 
= 
263 
if ( idB_B2_1 = 575) then 
264 
B2_B2b_en(idB_B2_1, x, b_1, false) 
265 
else (idB_B2_1, b_1); 
266  
267 

268  
269 
(idB_B2_6, idEvents1_B_4, b_6) 
270 
= 
271 
if ( idB_B2_1 = 0) then 
272 
(idB_B2_3, idEvents1_B_3, b_3) 
273 
else 
274 
if ( idB_B2_1 = 574) then 
275 
(idB_B2_4, idEvents1_B_3, b_4) 
276 
else 
277 
if ( idB_B2_1 = 575) then 
278 
(idB_B2_5, idEvents1_B_3, b_5) 
279 
else (idB_B2_1, idEvents1_B_2, b_1); 
280  
281  
282 
(idB_B2, idEvents1_B, b) 
283 
= (idB_B2_6, idEvents1_B_4, b_6); 
284 

285  
286 
tel 
287  
288  
289  
290  
291  
292 
 Exit action for state :B_B2 
293 
node B_B2_ex(idB_B2_1:int; 
294 
idEvents1_B_1:int; 
295 
isInner:bool) 
296  
297 
returns (idB_B2:int; 
298 
idEvents1_B:int); 
299  
300  
301 
var idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5:int; 
302 
idEvents1_B_2:int; 
303  
304  
305 
let 
306  
307  
308  
309 

310 
(idB_B2_2) 
311 
= 
312 
if ( idB_B2_1 = 574) then 
313 
B2_B2a_ex(idB_B2_1, false) 
314 
else (idB_B2_1); 
315  
316 

317  
318 
(idB_B2_3) 
319 
= 
320 
if ( idB_B2_1 = 575) then 
321 
B2_B2b_ex(idB_B2_1, false) 
322 
else (idB_B2_1); 
323  
324 

325  
326 
(idB_B2_4) 
327 
= 
328 
if ( idB_B2_1 = 574) then 
329 
(idB_B2_2) 
330 
else 
331 
if ( idB_B2_1 = 575) then 
332 
(idB_B2_3) 
333 
else (idB_B2_1); 
334  
335  
336 
 set state as inactive 
337 
idEvents1_B_2 
338 
= if (not isInner) then 0 else idEvents1_B_1; 
339  
340 
idB_B2_5 
341 
= 0; 
342 

343  
344 
(idB_B2, idEvents1_B) 
345 
= (idB_B2_5, idEvents1_B_1); 
346 

347  
348 
tel 
349  
350  
351  
352  
353  
354  
355 
 Entry action for state :B1_B1a 
356 
node B1_B1a_en(idB_B1_1:int; 
357 
x:int; 
358 
b_1:int; 
359 
isInner:bool) 
360  
361 
returns (idB_B1:int; 
362 
b:int); 
363  
364  
365 
var idB_B1_2:int; 
366 
b_2:int; 
367  
368  
369 
let 
370  
371  
372  
373 
 set state as active 
374 
idB_B1_2 
375 
= 577; 
376 

377  
378 
b_2 
379 
= if (not isInner) then x+5 
380 
else b_1; 
381 

382  
383 
(idB_B1, b) 
384 
= (idB_B1_2, b_2); 
385 

386  
387 
tel 
388  
389  
390  
391  
392  
393 
 Exit action for state :B1_B1a 
394 
node B1_B1a_ex(idB_B1_1:int; 
395 
isInner:bool) 
396  
397 
returns (idB_B1:int); 
398  
399  
400 
var idB_B1_2:int; 
401  
402  
403 
let 
404  
405  
406  
407 
 set state as inactive 
408 
idB_B1_2 
409 
= if (not isInner) then 0 else idB_B1_1; 
410  
411  
412 
(idB_B1) 
413 
= (idB_B1_1); 
414 

415  
416 
tel 
417  
418  
419  
420  
421  
422  
423 
 Entry action for state :B1_B1b 
424 
node B1_B1b_en(idB_B1_1:int; 
425 
x:int; 
426 
b_1:int; 
427 
isInner:bool) 
428  
429 
returns (idB_B1:int; 
430 
b:int); 
431  
432  
433 
var idB_B1_2:int; 
434 
b_2:int; 
435  
436  
437 
let 
438  
439  
440  
441 
 set state as active 
442 
idB_B1_2 
443 
= 578; 
444 

445  
446 
b_2 
447 
= if (not isInner) then x+6 
448 
else b_1; 
449 

450  
451 
(idB_B1, b) 
452 
= (idB_B1_2, b_2); 
453 

454  
455 
tel 
456  
457  
458  
459  
460  
461 
 Exit action for state :B1_B1b 
462 
node B1_B1b_ex(idB_B1_1:int; 
463 
isInner:bool) 
464  
465 
returns (idB_B1:int); 
466  
467  
468 
var idB_B1_2:int; 
469  
470  
471 
let 
472  
473  
474  
475 
 set state as inactive 
476 
idB_B1_2 
477 
= if (not isInner) then 0 else idB_B1_1; 
478  
479  
480 
(idB_B1) 
481 
= (idB_B1_1); 
482 

483  
484 
tel 
485  
486  
487  
488  
489  
490  
491 
 Entry action for state :B_B1 
492 
node B_B1_en(idB_B1_1:int; 
493 
idEvents1_B_1:int; 
494 
b_1:int; 
495 
x:int; 
496 
isInner:bool) 
497  
498 
returns (idB_B1:int; 
499 
idEvents1_B:int; 
500 
b:int); 
501  
502  
503 
var idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5, idB_B1_6:int; 
504 
idEvents1_B_2, idEvents1_B_3, idEvents1_B_4:int; 
505 
b_2, b_3, b_4, b_5, b_6:int; 
506  
507  
508 
let 
509  
510  
511  
512 
 set state as active 
513 
idEvents1_B_2 
514 
= 576; 
515 

516  
517 

518 
 transition trace : 
519 
POINT__To__B1_B1a_1 
520 
(idB_B1_2, b_2) 
521 
= B1_B1a_en(idB_B1_1, x, b_1, false); 
522 

523  
524 
(idB_B1_3, idEvents1_B_3, b_3) 
525 
= 
526  
527 
if ( idB_B1_1 = 0) then 
528  
529 
(idB_B1_2, idEvents1_B_2, b_2) 
530  
531 
else(idB_B1_1, idEvents1_B_2, b_1); 
532  
533 

534  
535 
(idB_B1_4, b_4) 
536 
= 
537 
if ( idB_B1_1 = 577) then 
538 
B1_B1a_en(idB_B1_1, x, b_1, false) 
539 
else (idB_B1_1, b_1); 
540  
541 

542  
543 
(idB_B1_5, b_5) 
544 
= 
545 
if ( idB_B1_1 = 578) then 
546 
B1_B1b_en(idB_B1_1, x, b_1, false) 
547 
else (idB_B1_1, b_1); 
548  
549 

550  
551 
(idB_B1_6, idEvents1_B_4, b_6) 
552 
= 
553 
if ( idB_B1_1 = 0) then 
554 
(idB_B1_3, idEvents1_B_3, b_3) 
555 
else 
556 
if ( idB_B1_1 = 577) then 
557 
(idB_B1_4, idEvents1_B_3, b_4) 
558 
else 
559 
if ( idB_B1_1 = 578) then 
560 
(idB_B1_5, idEvents1_B_3, b_5) 
561 
else (idB_B1_1, idEvents1_B_2, b_1); 
562  
563  
564 
(idB_B1, idEvents1_B, b) 
565 
= (idB_B1_6, idEvents1_B_4, b_6); 
566 

567  
568 
tel 
569  
570  
571  
572  
573  
574 
 Exit action for state :B_B1 
575 
node B_B1_ex(idB_B1_1:int; 
576 
idEvents1_B_1:int; 
577 
isInner:bool) 
578  
579 
returns (idB_B1:int; 
580 
idEvents1_B:int); 
581  
582  
583 
var idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int; 
584 
idEvents1_B_2:int; 
585  
586  
587 
let 
588  
589  
590  
591 

592 
(idB_B1_2) 
593 
= 
594 
if ( idB_B1_1 = 577) then 
595 
B1_B1a_ex(idB_B1_1, false) 
596 
else (idB_B1_1); 
597  
598 

599  
600 
(idB_B1_3) 
601 
= 
602 
if ( idB_B1_1 = 578) then 
603 
B1_B1b_ex(idB_B1_1, false) 
604 
else (idB_B1_1); 
605  
606 

607  
608 
(idB_B1_4) 
609 
= 
610 
if ( idB_B1_1 = 577) then 
611 
(idB_B1_2) 
612 
else 
613 
if ( idB_B1_1 = 578) then 
614 
(idB_B1_3) 
615 
else (idB_B1_1); 
616  
617  
618 
 set state as inactive 
619 
idEvents1_B_2 
620 
= if (not isInner) then 0 else idEvents1_B_1; 
621  
622 
idB_B1_5 
623 
= 0; 
624 

625  
626 
(idB_B1, idEvents1_B) 
627 
= (idB_B1_5, idEvents1_B_1); 
628 

629  
630 
tel 
631  
632  
633  
634  
635  
636  
637 
 Entry action for state :Events1_B 
638 
node Events1_B_en(idEvents1_B_1:int; 
639 
idEvents1_Events1_1:int; 
640 
b_1:int; 
641 
idB_B1_1:int; 
642 
x:int; 
643 
idB_B2_1:int; 
644 
isInner:bool) 
645  
646 
returns (idEvents1_B:int; 
647 
idEvents1_Events1:int; 
648 
b:int; 
649 
idB_B1:int; 
650 
idB_B2:int); 
651  
652  
653 
var idEvents1_B_2, idEvents1_B_3, idEvents1_B_4, idEvents1_B_5, idEvents1_B_6:int; 
654 
idEvents1_Events1_2, idEvents1_Events1_3, idEvents1_Events1_4:int; 
655 
b_2, b_3, b_4, b_5, b_6:int; 
656 
idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int; 
657 
idB_B2_2, idB_B2_3:int; 
658  
659  
660 
let 
661  
662  
663  
664 
 set state as active 
665 
idEvents1_Events1_2 
666 
= 572; 
667 

668  
669 

670 
 transition trace : 
671 
POINT__To__B_B1_1 
672 
(idB_B1_2, idEvents1_B_2, b_2) 
673 
= B_B1_en(idB_B1_1, idEvents1_B_1, b_1, x, false); 
674 

675  
676 
(idEvents1_B_3, idEvents1_Events1_3, b_3, idB_B1_3) 
677 
= 
678  
679 
if ( idEvents1_B_1 = 0) then 
680  
681 
(idEvents1_B_2, idEvents1_Events1_2, b_2, idB_B1_2) 
682  
683 
else(idEvents1_B_1, idEvents1_Events1_2, b_1, idB_B1_1); 
684  
685 

686  
687 
(idB_B2_2, idEvents1_B_4, b_4) 
688 
= 
689 
if ( idEvents1_B_1 = 573) then 
690 
B_B2_en(idB_B2_1, idEvents1_B_1, b_1, x, false) 
691 
else (idB_B2_1, idEvents1_B_1, b_1); 
692  
693 

694  
695 
(idB_B1_4, idEvents1_B_5, b_5) 
696 
= 
697 
if ( idEvents1_B_1 = 576) then 
698 
B_B1_en(idB_B1_1, idEvents1_B_1, b_1, x, false) 
699 
else (idB_B1_1, idEvents1_B_1, b_1); 
700  
701 

702  
703 
(idEvents1_B_6, idEvents1_Events1_4, b_6, idB_B1_5, idB_B2_3) 
704 
= 
705 
if ( idEvents1_B_1 = 0) then 
706 
(idEvents1_B_3, idEvents1_Events1_3, b_3, idB_B1_3, idB_B2_1) 
707 
else 
708 
if ( idEvents1_B_1 = 573) then 
709 
(idEvents1_B_4, idEvents1_Events1_3, b_4, idB_B1_1, idB_B2_2) 
710 
else 
711 
if ( idEvents1_B_1 = 576) then 
712 
(idEvents1_B_5, idEvents1_Events1_3, b_5, idB_B1_4, idB_B2_1) 
713 
else (idEvents1_B_1, idEvents1_Events1_2, b_1, idB_B1_1, idB_B2_1); 
714  
715  
716 
(idEvents1_B, idEvents1_Events1, b, idB_B1, idB_B2) 
717 
= (idEvents1_B_6, idEvents1_Events1_4, b_6, idB_B1_5, idB_B2_3); 
718 

719  
720 
tel 
721  
722  
723  
724  
725  
726 
 Exit action for state :Events1_B 
727 
node Events1_B_ex(idB_B2_1:int; 
728 
idEvents1_B_1:int; 
729 
idB_B1_1:int; 
730 
idEvents1_Events1_1:int; 
731 
isInner:bool) 
732  
733 
returns (idB_B2:int; 
734 
idEvents1_B:int; 
735 
idB_B1:int; 
736 
idEvents1_Events1:int); 
737  
738  
739 
var idB_B2_2, idB_B2_3:int; 
740 
idEvents1_B_2, idEvents1_B_3, idEvents1_B_4, idEvents1_B_5:int; 
741 
idB_B1_2, idB_B1_3:int; 
742 
idEvents1_Events1_2:int; 
743  
744  
745 
let 
746  
747  
748  
749 

750 
(idB_B2_2, idEvents1_B_2) 
751 
= 
752 
if ( idEvents1_B_1 = 573) then 
753 
B_B2_ex(idB_B2_1, idEvents1_B_1, false) 
754 
else (idB_B2_1, idEvents1_B_1); 
755  
756 

757  
758 
(idB_B1_2, idEvents1_B_3) 
759 
= 
760 
if ( idEvents1_B_1 = 576) then 
761 
B_B1_ex(idB_B1_1, idEvents1_B_1, false) 
762 
else (idB_B1_1, idEvents1_B_1); 
763  
764 

765  
766 
(idB_B2_3, idEvents1_B_4, idB_B1_3) 
767 
= 
768 
if ( idEvents1_B_1 = 573) then 
769 
(idB_B2_2, idEvents1_B_2, idB_B1_1) 
770 
else 
771 
if ( idEvents1_B_1 = 576) then 
772 
(idB_B2_1, idEvents1_B_3, idB_B1_2) 
773 
else (idB_B2_1, idEvents1_B_1, idB_B1_1); 
774  
775  
776 
 set state as inactive 
777 
idEvents1_Events1_2 
778 
= if (not isInner) then 0 else idEvents1_Events1_1; 
779  
780 
idEvents1_B_5 
781 
= 0; 
782 

783  
784 
(idB_B2, idEvents1_B, idB_B1, idEvents1_Events1) 
785 
= (idB_B2_3, idEvents1_B_5, idB_B1_3, idEvents1_Events1_1); 
786 

787  
788 
tel 
789  
790  
791  
792  
793  
794  
795 
 Entry action for state :A2_A2a 
796 
node A2_A2a_en(idA_A2_1:int; 
797 
x:int; 
798 
a_1:int; 
799 
isInner:bool) 
800  
801 
returns (idA_A2:int; 
802 
a:int); 
803  
804  
805 
var idA_A2_2:int; 
806 
a_2:int; 
807  
808  
809 
let 
810  
811  
812  
813 
 set state as active 
814 
idA_A2_2 
815 
= 567; 
816 

817  
818 
a_2 
819 
= if (not isInner) then x+3 
820 
else a_1; 
821 

822  
823 
(idA_A2, a) 
824 
= (idA_A2_2, a_2); 
825 

826  
827 
tel 
828  
829  
830  
831  
832  
833 
 Exit action for state :A2_A2a 
834 
node A2_A2a_ex(idA_A2_1:int; 
835 
isInner:bool) 
836  
837 
returns (idA_A2:int); 
838  
839  
840 
var idA_A2_2:int; 
841  
842  
843 
let 
844  
845  
846  
847 
 set state as inactive 
848 
idA_A2_2 
849 
= if (not isInner) then 0 else idA_A2_1; 
850  
851  
852 
(idA_A2) 
853 
= (idA_A2_1); 
854 

855  
856 
tel 
857  
858  
859  
860  
861  
862  
863 
 Entry action for state :A2_A2b 
864 
node A2_A2b_en(idA_A2_1:int; 
865 
x:int; 
866 
a_1:int; 
867 
isInner:bool) 
868  
869 
returns (idA_A2:int; 
870 
a:int); 
871  
872  
873 
var idA_A2_2:int; 
874 
a_2:int; 
875  
876  
877 
let 
878  
879  
880  
881 
 set state as active 
882 
idA_A2_2 
883 
= 568; 
884 

885  
886 
a_2 
887 
= if (not isInner) then x+4 
888 
else a_1; 
889 

890  
891 
(idA_A2, a) 
892 
= (idA_A2_2, a_2); 
893 

894  
895 
tel 
896  
897  
898  
899  
900  
901 
 Exit action for state :A2_A2b 
902 
node A2_A2b_ex(idA_A2_1:int; 
903 
isInner:bool) 
904  
905 
returns (idA_A2:int); 
906  
907  
908 
var idA_A2_2:int; 
909  
910  
911 
let 
912  
913  
914  
915 
 set state as inactive 
916 
idA_A2_2 
917 
= if (not isInner) then 0 else idA_A2_1; 
918  
919  
920 
(idA_A2) 
921 
= (idA_A2_1); 
922 

923  
924 
tel 
925  
926  
927  
928  
929  
930  
931 
 Entry action for state :A_A2 
932 
node A_A2_en(idA_A2_1:int; 
933 
idEvents1_A_1:int; 
934 
a_1:int; 
935 
x:int; 
936 
isInner:bool) 
937  
938 
returns (idA_A2:int; 
939 
idEvents1_A:int; 
940 
a:int); 
941  
942  
943 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int; 
944 
idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int; 
945 
a_2, a_3, a_4, a_5, a_6:int; 
946  
947  
948 
let 
949  
950  
951  
952 
 set state as active 
953 
idEvents1_A_2 
954 
= 566; 
955 

956  
957 

958 
 transition trace : 
959 
POINT__To__A2_A2a_1 
960 
(idA_A2_2, a_2) 
961 
= A2_A2a_en(idA_A2_1, x, a_1, false); 
962 

963  
964 
(idA_A2_3, idEvents1_A_3, a_3) 
965 
= 
966  
967 
if ( idA_A2_1 = 0) then 
968  
969 
(idA_A2_2, idEvents1_A_2, a_2) 
970  
971 
else(idA_A2_1, idEvents1_A_2, a_1); 
972  
973 

974  
975 
(idA_A2_4, a_4) 
976 
= 
977 
if ( idA_A2_1 = 567) then 
978 
A2_A2a_en(idA_A2_1, x, a_1, false) 
979 
else (idA_A2_1, a_1); 
980  
981 

982  
983 
(idA_A2_5, a_5) 
984 
= 
985 
if ( idA_A2_1 = 568) then 
986 
A2_A2b_en(idA_A2_1, x, a_1, false) 
987 
else (idA_A2_1, a_1); 
988  
989 

990  
991 
(idA_A2_6, idEvents1_A_4, a_6) 
992 
= 
993 
if ( idA_A2_1 = 0) then 
994 
(idA_A2_3, idEvents1_A_3, a_3) 
995 
else 
996 
if ( idA_A2_1 = 567) then 
997 
(idA_A2_4, idEvents1_A_3, a_4) 
998 
else 
999 
if ( idA_A2_1 = 568) then 
1000 
(idA_A2_5, idEvents1_A_3, a_5) 
1001 
else (idA_A2_1, idEvents1_A_2, a_1); 
1002  
1003  
1004 
(idA_A2, idEvents1_A, a) 
1005 
= (idA_A2_6, idEvents1_A_4, a_6); 
1006 

1007  
1008 
tel 
1009  
1010  
1011  
1012  
1013  
1014 
 Exit action for state :A_A2 
1015 
node A_A2_ex(idA_A2_1:int; 
1016 
idEvents1_A_1:int; 
1017 
isInner:bool) 
1018  
1019 
returns (idA_A2:int; 
1020 
idEvents1_A:int); 
1021  
1022  
1023 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int; 
1024 
idEvents1_A_2:int; 
1025  
1026  
1027 
let 
1028  
1029  
1030  
1031 

1032 
(idA_A2_2) 
1033 
= 
1034 
if ( idA_A2_1 = 567) then 
1035 
A2_A2a_ex(idA_A2_1, false) 
1036 
else (idA_A2_1); 
1037  
1038 

1039  
1040 
(idA_A2_3) 
1041 
= 
1042 
if ( idA_A2_1 = 568) then 
1043 
A2_A2b_ex(idA_A2_1, false) 
1044 
else (idA_A2_1); 
1045  
1046 

1047  
1048 
(idA_A2_4) 
1049 
= 
1050 
if ( idA_A2_1 = 567) then 
1051 
(idA_A2_2) 
1052 
else 
1053 
if ( idA_A2_1 = 568) then 
1054 
(idA_A2_3) 
1055 
else (idA_A2_1); 
1056  
1057  
1058 
 set state as inactive 
1059 
idEvents1_A_2 
1060 
= if (not isInner) then 0 else idEvents1_A_1; 
1061  
1062 
idA_A2_5 
1063 
= 0; 
1064 

1065  
1066 
(idA_A2, idEvents1_A) 
1067 
= (idA_A2_5, idEvents1_A_1); 
1068 

1069  
1070 
tel 
1071  
1072  
1073  
1074  
1075  
1076  
1077 
 Entry action for state :A1_A1a 
1078 
node A1_A1a_en(idA_A1_1:int; 
1079 
x:int; 
1080 
a_1:int; 
1081 
isInner:bool) 
1082  
1083 
returns (idA_A1:int; 
1084 
a:int); 
1085  
1086  
1087 
var idA_A1_2:int; 
1088 
a_2:int; 
1089  
1090  
1091 
let 
1092  
1093  
1094  
1095 
 set state as active 
1096 
idA_A1_2 
1097 
= 570; 
1098 

1099  
1100 
a_2 
1101 
= if (not isInner) then x+1 
1102 
else a_1; 
1103 

1104  
1105 
(idA_A1, a) 
1106 
= (idA_A1_2, a_2); 
1107 

1108  
1109 
tel 
1110  
1111  
1112  
1113  
1114  
1115 
 Exit action for state :A1_A1a 
1116 
node A1_A1a_ex(idA_A1_1:int; 
1117 
isInner:bool) 
1118  
1119 
returns (idA_A1:int); 
1120  
1121  
1122 
var idA_A1_2:int; 
1123  
1124  
1125 
let 
1126  
1127  
1128  
1129 
 set state as inactive 
1130 
idA_A1_2 
1131 
= if (not isInner) then 0 else idA_A1_1; 
1132  
1133  
1134 
(idA_A1) 
1135 
= (idA_A1_1); 
1136 

1137  
1138 
tel 
1139  
1140  
1141  
1142  
1143  
1144  
1145 
 Entry action for state :A1_A1b 
1146 
node A1_A1b_en(idA_A1_1:int; 
1147 
x:int; 
1148 
a_1:int; 
1149 
isInner:bool) 
1150  
1151 
returns (idA_A1:int; 
1152 
a:int); 
1153  
1154  
1155 
var idA_A1_2:int; 
1156 
a_2:int; 
1157  
1158  
1159 
let 
1160  
1161  
1162  
1163 
 set state as active 
1164 
idA_A1_2 
1165 
= 571; 
1166 

1167  
1168 
a_2 
1169 
= if (not isInner) then x+2 
1170 
else a_1; 
1171 

1172  
1173 
(idA_A1, a) 
1174 
= (idA_A1_2, a_2); 
1175 

1176  
1177 
tel 
1178  
1179  
1180  
1181  
1182  
1183 
 Exit action for state :A1_A1b 
1184 
node A1_A1b_ex(idA_A1_1:int; 
1185 
isInner:bool) 
1186  
1187 
returns (idA_A1:int); 
1188  
1189  
1190 
var idA_A1_2:int; 
1191  
1192  
1193 
let 
1194  
1195  
1196  
1197 
 set state as inactive 
1198 
idA_A1_2 
1199 
= if (not isInner) then 0 else idA_A1_1; 
1200  
1201  
1202 
(idA_A1) 
1203 
= (idA_A1_1); 
1204 

1205  
1206 
tel 
1207  
1208  
1209  
1210  
1211  
1212  
1213 
 Entry action for state :A_A1 
1214 
node A_A1_en(idA_A1_1:int; 
1215 
idEvents1_A_1:int; 
1216 
a_1:int; 
1217 
x:int; 
1218 
isInner:bool) 
1219  
1220 
returns (idA_A1:int; 
1221 
idEvents1_A:int; 
1222 
a:int); 
1223  
1224  
1225 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int; 
1226 
idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int; 
1227 
a_2, a_3, a_4, a_5, a_6:int; 
1228  
1229  
1230 
let 
1231  
1232  
1233  
1234 
 set state as active 
1235 
idEvents1_A_2 
1236 
= 569; 
1237 

1238  
1239 

1240 
 transition trace : 
1241 
POINT__To__A1_A1a_1 
1242 
(idA_A1_2, a_2) 
1243 
= A1_A1a_en(idA_A1_1, x, a_1, false); 
1244 

1245  
1246 
(idA_A1_3, idEvents1_A_3, a_3) 
1247 
= 
1248  
1249 
if ( idA_A1_1 = 0) then 
1250  
1251 
(idA_A1_2, idEvents1_A_2, a_2) 
1252  
1253 
else(idA_A1_1, idEvents1_A_2, a_1); 
1254  
1255 

1256  
1257 
(idA_A1_4, a_4) 
1258 
= 
1259 
if ( idA_A1_1 = 570) then 
1260 
A1_A1a_en(idA_A1_1, x, a_1, false) 
1261 
else (idA_A1_1, a_1); 
1262  
1263 

1264  
1265 
(idA_A1_5, a_5) 
1266 
= 
1267 
if ( idA_A1_1 = 571) then 
1268 
A1_A1b_en(idA_A1_1, x, a_1, false) 
1269 
else (idA_A1_1, a_1); 
1270  
1271 

1272  
1273 
(idA_A1_6, idEvents1_A_4, a_6) 
1274 
= 
1275 
if ( idA_A1_1 = 0) then 
1276 
(idA_A1_3, idEvents1_A_3, a_3) 
1277 
else 
1278 
if ( idA_A1_1 = 570) then 
1279 
(idA_A1_4, idEvents1_A_3, a_4) 
1280 
else 
1281 
if ( idA_A1_1 = 571) then 
1282 
(idA_A1_5, idEvents1_A_3, a_5) 
1283 
else (idA_A1_1, idEvents1_A_2, a_1); 
1284  
1285  
1286 
(idA_A1, idEvents1_A, a) 
1287 
= (idA_A1_6, idEvents1_A_4, a_6); 
1288 

1289  
1290 
tel 
1291  
1292  
1293  
1294  
1295  
1296 
 Exit action for state :A_A1 
1297 
node A_A1_ex(idA_A1_1:int; 
1298 
idEvents1_A_1:int; 
1299 
isInner:bool) 
1300  
1301 
returns (idA_A1:int; 
1302 
idEvents1_A:int); 
1303  
1304  
1305 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
1306 
idEvents1_A_2:int; 
1307  
1308  
1309 
let 
1310  
1311  
1312  
1313 

1314 
(idA_A1_2) 
1315 
= 
1316 
if ( idA_A1_1 = 570) then 
1317 
A1_A1a_ex(idA_A1_1, false) 
1318 
else (idA_A1_1); 
1319  
1320 

1321  
1322 
(idA_A1_3) 
1323 
= 
1324 
if ( idA_A1_1 = 571) then 
1325 
A1_A1b_ex(idA_A1_1, false) 
1326 
else (idA_A1_1); 
1327  
1328 

1329  
1330 
(idA_A1_4) 
1331 
= 
1332 
if ( idA_A1_1 = 570) then 
1333 
(idA_A1_2) 
1334 
else 
1335 
if ( idA_A1_1 = 571) then 
1336 
(idA_A1_3) 
1337 
else (idA_A1_1); 
1338  
1339  
1340 
 set state as inactive 
1341 
idEvents1_A_2 
1342 
= if (not isInner) then 0 else idEvents1_A_1; 
1343  
1344 
idA_A1_5 
1345 
= 0; 
1346 

1347  
1348 
(idA_A1, idEvents1_A) 
1349 
= (idA_A1_5, idEvents1_A_1); 
1350 

1351  
1352 
tel 
1353  
1354  
1355  
1356  
1357  
1358  
1359 
 Entry action for state :Events1_A 
1360 
node Events1_A_en(idEvents1_A_1:int; 
1361 
idEvents1_Events1_1:int; 
1362 
a_1:int; 
1363 
idA_A1_1:int; 
1364 
x:int; 
1365 
idA_A2_1:int; 
1366 
isInner:bool) 
1367  
1368 
returns (idEvents1_A:int; 
1369 
idEvents1_Events1:int; 
1370 
a:int; 
1371 
idA_A1:int; 
1372 
idA_A2:int); 
1373  
1374  
1375 
var idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5, idEvents1_A_6:int; 
1376 
idEvents1_Events1_2, idEvents1_Events1_3, idEvents1_Events1_4:int; 
1377 
a_2, a_3, a_4, a_5, a_6:int; 
1378 
idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
1379 
idA_A2_2, idA_A2_3:int; 
1380  
1381  
1382 
let 
1383  
1384  
1385  
1386 
 set state as active 
1387 
idEvents1_Events1_2 
1388 
= 565; 
1389 

1390  
1391 

1392 
 transition trace : 
1393 
POINT__To__A_A1_1 
1394 
(idA_A1_2, idEvents1_A_2, a_2) 
1395 
= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, x, false); 
1396 

1397  
1398 
(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3) 
1399 
= 
1400  
1401 
if ( idEvents1_A_1 = 0) then 
1402  
1403 
(idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2) 
1404  
1405 
else(idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1); 
1406  
1407 

1408  
1409 
(idA_A2_2, idEvents1_A_4, a_4) 
1410 
= 
1411 
if ( idEvents1_A_1 = 566) then 
1412 
A_A2_en(idA_A2_1, idEvents1_A_1, a_1, x, false) 
1413 
else (idA_A2_1, idEvents1_A_1, a_1); 
1414  
1415 

1416  
1417 
(idA_A1_4, idEvents1_A_5, a_5) 
1418 
= 
1419 
if ( idEvents1_A_1 = 569) then 
1420 
A_A1_en(idA_A1_1, idEvents1_A_1, a_1, x, false) 
1421 
else (idA_A1_1, idEvents1_A_1, a_1); 
1422  
1423 

1424  
1425 
(idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3) 
1426 
= 
1427 
if ( idEvents1_A_1 = 0) then 
1428 
(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_1) 
1429 
else 
1430 
if ( idEvents1_A_1 = 566) then 
1431 
(idEvents1_A_4, idEvents1_Events1_3, a_4, idA_A1_1, idA_A2_2) 
1432 
else 
1433 
if ( idEvents1_A_1 = 569) then 
1434 
(idEvents1_A_5, idEvents1_Events1_3, a_5, idA_A1_4, idA_A2_1) 
1435 
else (idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1, idA_A2_1); 
1436  
1437  
1438 
(idEvents1_A, idEvents1_Events1, a, idA_A1, idA_A2) 
1439 
= (idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3); 
1440 

1441  
1442 
tel 
1443  
1444  
1445  
1446  
1447  
1448 
 Exit action for state :Events1_A 
1449 
node Events1_A_ex(idA_A2_1:int; 
1450 
idEvents1_A_1:int; 
1451 
idA_A1_1:int; 
1452 
idEvents1_Events1_1:int; 
1453 
isInner:bool) 
1454  
1455 
returns (idA_A2:int; 
1456 
idEvents1_A:int; 
1457 
idA_A1:int; 
1458 
idEvents1_Events1:int); 
1459  
1460  
1461 
var idA_A2_2, idA_A2_3:int; 
1462 
idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5:int; 
1463 
idA_A1_2, idA_A1_3:int; 
1464 
idEvents1_Events1_2:int; 
1465  
1466  
1467 
let 
1468  
1469  
1470  
1471 

1472 
(idA_A2_2, idEvents1_A_2) 
1473 
= 
1474 
if ( idEvents1_A_1 = 566) then 
1475 
A_A2_ex(idA_A2_1, idEvents1_A_1, false) 
1476 
else (idA_A2_1, idEvents1_A_1); 
1477  
1478 

1479  
1480 
(idA_A1_2, idEvents1_A_3) 
1481 
= 
1482 
if ( idEvents1_A_1 = 569) then 
1483 
A_A1_ex(idA_A1_1, idEvents1_A_1, false) 
1484 
else (idA_A1_1, idEvents1_A_1); 
1485  
1486 

1487  
1488 
(idA_A2_3, idEvents1_A_4, idA_A1_3) 
1489 
= 
1490 
if ( idEvents1_A_1 = 566) then 
1491 
(idA_A2_2, idEvents1_A_2, idA_A1_1) 
1492 
else 
1493 
if ( idEvents1_A_1 = 569) then 
1494 
(idA_A2_1, idEvents1_A_3, idA_A1_2) 
1495 
else (idA_A2_1, idEvents1_A_1, idA_A1_1); 
1496  
1497  
1498 
 set state as inactive 
1499 
idEvents1_Events1_2 
1500 
= if (not isInner) then 0 else idEvents1_Events1_1; 
1501  
1502 
idEvents1_A_5 
1503 
= 0; 
1504 

1505  
1506 
(idA_A2, idEvents1_A, idA_A1, idEvents1_Events1) 
1507 
= (idA_A2_3, idEvents1_A_5, idA_A1_3, idEvents1_Events1_1); 
1508 

1509  
1510 
tel 
1511  
1512  
1513 
***************************************************State :B_B2 Automaton*************************************************** 
1514  
1515 
node B_B2_node(idB_B2_1:int; 
1516 
b_1:int; 
1517 
x:int; 
1518 
S1:bool; 
1519 
R1:bool) 
1520  
1521 
returns (idB_B2:int; 
1522 
b:int); 
1523  
1524  
1525 
let 
1526  
1527 
automaton b_b2 
1528  
1529 
state POINTB_B2: 
1530 
unless (idB_B2_1=0) restart POINT__TO__B2_B2A_1 
1531  
1532  
1533  
1534 
unless (idB_B2_1=574) and S1 restart B2_B2A__TO__B2_B2B_1 
1535  
1536  
1537  
1538 
unless (idB_B2_1=575) and R1 restart B2_B2B__TO__B2_B2A_1 
1539  
1540  
1541  
1542 
unless (idB_B2_1=574) restart B2_B2A_IDL 
1543  
1544 
unless (idB_B2_1=575) restart B2_B2B_IDL 
1545  
1546 
let 
1547  
1548 
(idB_B2, b) 
1549 
= (idB_B2_1, b_1); 
1550 

1551  
1552 
tel 
1553  
1554  
1555  
1556 
state POINT__TO__B2_B2A_1: 
1557  
1558 
var idB_B2_2:int; 
1559 
b_2:int; 
1560 
let 
1561  
1562 
 transition trace : 
1563 
POINT__To__B2_B2a_1 
1564 
(idB_B2_2, b_2) 
1565 
= B2_B2a_en(idB_B2_1, x, b_1, false); 
1566 

1567  
1568 
(idB_B2, b) 
1569 
= (idB_B2_2, b_2); 
1570  
1571  
1572 
tel 
1573  
1574 
until true restart POINTB_B2 
1575  
1576  
1577  
1578 
state B2_B2A__TO__B2_B2B_1: 
1579  
1580 
var idB_B2_2, idB_B2_3:int; 
1581 
b_2:int; 
1582 
let 
1583  
1584 
 transition trace : 
1585 
B2_B2a__To__B2_B2b_1 
1586 
(idB_B2_2) 
1587 
= B2_B2a_ex(idB_B2_1, false); 
1588 

1589  
1590 
(idB_B2_3, b_2) 
1591 
= B2_B2b_en(idB_B2_2, x, b_1, false); 
1592 

1593  
1594 
(idB_B2, b) 
1595 
= (idB_B2_3, b_2); 
1596  
1597  
1598 
tel 
1599  
1600 
until true restart POINTB_B2 
1601  
1602  
1603  
1604 
state B2_B2B__TO__B2_B2A_1: 
1605  
1606 
var idB_B2_2, idB_B2_3:int; 
1607 
b_2:int; 
1608 
let 
1609  
1610 
 transition trace : 
1611 
B2_B2b__To__B2_B2a_1 
1612 
(idB_B2_2) 
1613 
= B2_B2b_ex(idB_B2_1, false); 
1614 

1615  
1616 
(idB_B2_3, b_2) 
1617 
= B2_B2a_en(idB_B2_2, x, b_1, false); 
1618 

1619  
1620 
(idB_B2, b) 
1621 
= (idB_B2_3, b_2); 
1622  
1623  
1624 
tel 
1625  
1626 
until true restart POINTB_B2 
1627  
1628  
1629  
1630 
state B2_B2A_IDL: 
1631  
1632 
let 
1633  
1634 

1635  
1636 
(idB_B2, b) 
1637 
= (idB_B2_1, b_1); 
1638 

1639  
1640 
tel 
1641  
1642 
until true restart POINTB_B2 
1643  
1644  
1645  
1646 
state B2_B2B_IDL: 
1647  
1648 
let 
1649  
1650 

1651  
1652 
(idB_B2, b) 
1653 
= (idB_B2_1, b_1); 
1654 

1655  
1656 
tel 
1657  
1658 
until true restart POINTB_B2 
1659  
1660  
1661  
1662 
tel 
1663  
1664  
1665 
***************************************************State :B_B1 Automaton*************************************************** 
1666  
1667 
node B_B1_node(idB_B1_1:int; 
1668 
b_1:int; 
1669 
x:int; 
1670 
S1:bool; 
1671 
R1:bool) 
1672  
1673 
returns (idB_B1:int; 
1674 
b:int); 
1675  
1676  
1677 
let 
1678  
1679 
automaton b_b1 
1680  
1681 
state POINTB_B1: 
1682 
unless (idB_B1_1=0) restart POINT__TO__B1_B1A_1 
1683  
1684  
1685  
1686 
unless (idB_B1_1=577) and S1 restart B1_B1A__TO__B1_B1B_1 
1687  
1688  
1689  
1690 
unless (idB_B1_1=578) and R1 restart B1_B1B__TO__B1_B1A_1 
1691  
1692  
1693  
1694 
unless (idB_B1_1=577) restart B1_B1A_IDL 
1695  
1696 
unless (idB_B1_1=578) restart B1_B1B_IDL 
1697  
1698 
let 
1699  
1700 
(idB_B1, b) 
1701 
= (idB_B1_1, b_1); 
1702 

1703  
1704 
tel 
1705  
1706  
1707  
1708 
state POINT__TO__B1_B1A_1: 
1709  
1710 
var idB_B1_2:int; 
1711 
b_2:int; 
1712 
let 
1713  
1714 
 transition trace : 
1715 
POINT__To__B1_B1a_1 
1716 
(idB_B1_2, b_2) 
1717 
= B1_B1a_en(idB_B1_1, x, b_1, false); 
1718 

1719  
1720 
(idB_B1, b) 
1721 
= (idB_B1_2, b_2); 
1722  
1723  
1724 
tel 
1725  
1726 
until true restart POINTB_B1 
1727  
1728  
1729  
1730 
state B1_B1A__TO__B1_B1B_1: 
1731  
1732 
var idB_B1_2, idB_B1_3:int; 
1733 
b_2:int; 
1734 
let 
1735  
1736 
 transition trace : 
1737 
B1_B1a__To__B1_B1b_1 
1738 
(idB_B1_2) 
1739 
= B1_B1a_ex(idB_B1_1, false); 
1740 

1741  
1742 
(idB_B1_3, b_2) 
1743 
= B1_B1b_en(idB_B1_2, x, b_1, false); 
1744 

1745  
1746 
(idB_B1, b) 
1747 
= (idB_B1_3, b_2); 
1748  
1749  
1750 
tel 
1751  
1752 
until true restart POINTB_B1 
1753  
1754  
1755  
1756 
state B1_B1B__TO__B1_B1A_1: 
1757  
1758 
var idB_B1_2, idB_B1_3:int; 
1759 
b_2:int; 
1760 
let 
1761  
1762 
 transition trace : 
1763 
B1_B1b__To__B1_B1a_1 
1764 
(idB_B1_2) 
1765 
= B1_B1b_ex(idB_B1_1, false); 
1766 

1767  
1768 
(idB_B1_3, b_2) 
1769 
= B1_B1a_en(idB_B1_2, x, b_1, false); 
1770 

1771  
1772 
(idB_B1, b) 
1773 
= (idB_B1_3, b_2); 
1774  
1775  
1776 
tel 
1777  
1778 
until true restart POINTB_B1 
1779  
1780  
1781  
1782 
state B1_B1A_IDL: 
1783  
1784 
let 
1785  
1786 

1787  
1788 
(idB_B1, b) 
1789 
= (idB_B1_1, b_1); 
1790 

1791  
1792 
tel 
1793  
1794 
until true restart POINTB_B1 
1795  
1796  
1797  
1798 
state B1_B1B_IDL: 
1799  
1800 
let 
1801  
1802 

1803  
1804 
(idB_B1, b) 
1805 
= (idB_B1_1, b_1); 
1806 

1807  
1808 
tel 
1809  
1810 
until true restart POINTB_B1 
1811  
1812  
1813  
1814 
tel 
1815  
1816  
1817 
***************************************************State :Events1_B Automaton*************************************************** 
1818  
1819 
node Events1_B_node(idEvents1_B_1:int; 
1820 
b_1:int; 
1821 
idB_B1_1:int; 
1822 
x:int; 
1823 
T1:bool; 
1824 
idB_B2_1:int; 
1825 
c_1:int; 
1826 
R1:bool; 
1827 
S1:bool) 
1828  
1829 
returns (idEvents1_B:int; 
1830 
b:int; 
1831 
idB_B1:int; 
1832 
idB_B2:int; 
1833 
c:int); 
1834  
1835  
1836 
let 
1837  
1838 
automaton events1_b 
1839  
1840 
state POINTEvents1_B: 
1841 
unless (idEvents1_B_1=0) restart POINT__TO__B_B1_1 
1842  
1843  
1844  
1845 
unless (idEvents1_B_1=573) and T1 restart B_B2__TO__B_B1_1 
1846  
1847  
1848  
1849 
unless (idEvents1_B_1=576) and T1 restart B_B1__TO__B_B2_1 
1850  
1851  
1852  
1853 
unless (idEvents1_B_1=573) restart B_B2_IDL 
1854  
1855 
unless (idEvents1_B_1=576) restart B_B1_IDL 
1856  
1857 
let 
1858  
1859 
(idEvents1_B, b, idB_B1, idB_B2, c) 
1860 
= (idEvents1_B_1, b_1, idB_B1_1, idB_B2_1, c_1); 
1861 

1862  
1863 
tel 
1864  
1865  
1866  
1867 
state POINT__TO__B_B1_1: 
1868  
1869 
var idEvents1_B_2:int; 
1870 
b_2:int; 
1871 
idB_B1_2:int; 
1872 
let 
1873  
1874 
 transition trace : 
1875 
POINT__To__B_B1_1 
1876 
(idB_B1_2, idEvents1_B_2, b_2) 
1877 
= B_B1_en(idB_B1_1, idEvents1_B_1, b_1, x, false); 
1878 

1879  
1880 
(idEvents1_B, b, idB_B1) 
1881 
= (idEvents1_B_2, b_2, idB_B1_2); 
1882  
1883 
add unused variables 
1884 
(c, idB_B2) 
1885 
= (c_1, idB_B2_1); 
1886 

1887  
1888 
tel 
1889  
1890 
until true restart POINTEvents1_B 
1891  
1892  
1893  
1894 
state B_B2__TO__B_B1_1: 
1895  
1896 
var idEvents1_B_2, idEvents1_B_3:int; 
1897 
b_2:int; 
1898 
idB_B1_2:int; 
1899 
idB_B2_2:int; 
1900 
c_2:int; 
1901 
let 
1902  
1903 
 transition trace : 
1904 
B_B2__To__B_B1_1 
1905 
(idB_B2_2, idEvents1_B_2) 
1906 
= B_B2_ex(idB_B2_1, idEvents1_B_1, false); 
1907 

1908  
1909 
(c_2) 
1910 
= B_B2__To__B_B1_1_Transition_Action(c_1); 
1911 

1912  
1913 
(idB_B1_2, idEvents1_B_3, b_2) 
1914 
= B_B1_en(idB_B1_1, idEvents1_B_2, b_1, x, false); 
1915 

1916  
1917 
(idEvents1_B, b, idB_B1, idB_B2, c) 
1918 
= (idEvents1_B_3, b_2, idB_B1_2, idB_B2_2, c_2); 
1919  
1920  
1921 
tel 
1922  
1923 
until true restart POINTEvents1_B 
1924  
1925  
1926  
1927 
state B_B1__TO__B_B2_1: 
1928  
1929 
var idEvents1_B_2, idEvents1_B_3:int; 
1930 
b_2:int; 
1931 
idB_B1_2:int; 
1932 
idB_B2_2:int; 
1933 
c_2:int; 
1934 
let 
1935  
1936 
 transition trace : 
1937 
B_B1__To__B_B2_1 
1938 
(idB_B1_2, idEvents1_B_2) 
1939 
= B_B1_ex(idB_B1_1, idEvents1_B_1, false); 
1940 

1941  
1942 
(c_2) 
1943 
= B_B1__To__B_B2_1_Transition_Action(c_1); 
1944 

1945  
1946 
(idB_B2_2, idEvents1_B_3, b_2) 
1947 
= B_B2_en(idB_B2_1, idEvents1_B_2, b_1, x, false); 
1948 

1949  
1950 
(idEvents1_B, b, idB_B1, idB_B2, c) 
1951 
= (idEvents1_B_3, b_2, idB_B1_2, idB_B2_2, c_2); 
1952  
1953  
1954 
tel 
1955  
1956 
until true restart POINTEvents1_B 
1957  
1958  
1959  
1960 
state B_B2_IDL: 
1961  
1962 
var b_2:int; 
1963 
idB_B2_2:int; 
1964 
let 
1965  
1966 

1967 
(idB_B2_2, b_2) 
1968 
= B_B2_node(idB_B2_1, b_1, x, S1, R1); 
1969  
1970 

1971  
1972  
1973 
(idEvents1_B, b, idB_B1, idB_B2, c) 
1974 
= (idEvents1_B_1, b_2, idB_B1_1, idB_B2_2, c_1); 
1975 

1976  
1977 
tel 
1978  
1979 
until true restart POINTEvents1_B 
1980  
1981  
1982  
1983 
state B_B1_IDL: 
1984  
1985 
var b_2:int; 
1986 
idB_B1_2:int; 
1987 
let 
1988  
1989 

1990 
(idB_B1_2, b_2) 
1991 
= B_B1_node(idB_B1_1, b_1, x, S1, R1); 
1992  
1993 

1994  
1995  
1996 
(idEvents1_B, b, idB_B1, idB_B2, c) 
1997 
= (idEvents1_B_1, b_2, idB_B1_2, idB_B2_1, c_1); 
1998 

1999  
2000 
tel 
2001  
2002 
until true restart POINTEvents1_B 
2003  
2004  
2005  
2006 
tel 
2007  
2008  
2009  
2010  
2011  
2012  
2013 
node A2_A2a__To__A2_A2b_1_Transition_Action(idEvents1_B_1:int; 
2014 
b_1:int; 
2015 
idB_B1_1:int; 
2016 
x:int; 
2017 
T1:bool; 
2018 
idB_B2_1:int; 
2019 
c_1:int; 
2020 
R1:bool; 
2021 
S1:bool) 
2022  
2023 
returns (idEvents1_B:int; 
2024 
b:int; 
2025 
idB_B1:int; 
2026 
idB_B2:int; 
2027 
c:int); 
2028  
2029  
2030 
var idEvents1_B_2:int; 
2031 
b_2:int; 
2032 
idB_B1_2:int; 
2033 
idB_B2_2:int; 
2034 
c_2:int; 
2035  
2036  
2037 
let 
2038  
2039  
2040  
2041 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2042 
= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, true); 
2043 

2044  
2045 
(idEvents1_B, b, idB_B1, idB_B2, c) 
2046 
= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2); 
2047 

2048  
2049 
tel 
2050  
2051  
2052  
2053  
2054  
2055  
2056 
node A2_A2b__To__A2_A2a_1_Transition_Action(idEvents1_B_1:int; 
2057 
b_1:int; 
2058 
idB_B1_1:int; 
2059 
x:int; 
2060 
T1:bool; 
2061 
idB_B2_1:int; 
2062 
c_1:int; 
2063 
R1:bool; 
2064 
S1:bool) 
2065  
2066 
returns (idEvents1_B:int; 
2067 
b:int; 
2068 
idB_B1:int; 
2069 
idB_B2:int; 
2070 
c:int); 
2071  
2072  
2073 
var idEvents1_B_2:int; 
2074 
b_2:int; 
2075 
idB_B1_2:int; 
2076 
idB_B2_2:int; 
2077 
c_2:int; 
2078  
2079  
2080 
let 
2081  
2082  
2083  
2084 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2085 
= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, true, S1); 
2086 

2087  
2088 
(idEvents1_B, b, idB_B1, idB_B2, c) 
2089 
= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2); 
2090 

2091  
2092 
tel 
2093  
2094  
2095 
***************************************************State :A_A2 Automaton*************************************************** 
2096  
2097 
node A_A2_node(idA_A2_1:int; 
2098 
a_1:int; 
2099 
x:int; 
2100 
S:bool; 
2101 
R1:bool; 
2102 
S1:bool; 
2103 
T1:bool; 
2104 
b_1:int; 
2105 
c_1:int; 
2106 
idB_B1_1:int; 
2107 
idB_B2_1:int; 
2108 
idEvents1_B_1:int; 
2109 
R:bool) 
2110  
2111 
returns (idA_A2:int; 
2112 
a:int; 
2113 
b:int; 
2114 
c:int; 
2115 
idB_B1:int; 
2116 
idB_B2:int; 
2117 
idEvents1_B:int); 
2118  
2119  
2120 
let 
2121  
2122 
automaton a_a2 
2123  
2124 
state POINTA_A2: 
2125 
unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1 
2126  
2127  
2128  
2129 
unless (idA_A2_1=567) and S restart A2_A2A__TO__A2_A2B_1 
2130  
2131  
2132  
2133 
unless (idA_A2_1=568) and R restart A2_A2B__TO__A2_A2A_1 
2134  
2135  
2136  
2137 
unless (idA_A2_1=567) restart A2_A2A_IDL 
2138  
2139 
unless (idA_A2_1=568) restart A2_A2B_IDL 
2140  
2141 
let 
2142  
2143 
(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2144 
= (idA_A2_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2145 

2146  
2147 
tel 
2148  
2149  
2150  
2151 
state POINT__TO__A2_A2A_1: 
2152  
2153 
var idA_A2_2:int; 
2154 
a_2:int; 
2155 
let 
2156  
2157 
 transition trace : 
2158 
POINT__To__A2_A2a_1 
2159 
(idA_A2_2, a_2) 
2160 
= A2_A2a_en(idA_A2_1, x, a_1, false); 
2161 

2162  
2163 
(idA_A2, a) 
2164 
= (idA_A2_2, a_2); 
2165  
2166 
add unused variables 
2167 
(b, c, idB_B1, idB_B2, idEvents1_B) 
2168 
= (b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2169 

2170  
2171 
tel 
2172  
2173 
until true restart POINTA_A2 
2174  
2175  
2176  
2177 
state A2_A2A__TO__A2_A2B_1: 
2178  
2179 
var idA_A2_2, idA_A2_3:int; 
2180 
a_2:int; 
2181 
b_2:int; 
2182 
c_2:int; 
2183 
idB_B1_2:int; 
2184 
idB_B2_2:int; 
2185 
idEvents1_B_2:int; 
2186 
let 
2187  
2188 
 transition trace : 
2189 
A2_A2a__To__A2_A2b_1 
2190 
(idA_A2_2) 
2191 
= A2_A2a_ex(idA_A2_1, false); 
2192 

2193  
2194 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2195 
= A2_A2a__To__A2_A2b_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1); 
2196 

2197  
2198 
(idA_A2_3, a_2) 
2199 
= A2_A2b_en(idA_A2_2, x, a_1, false); 
2200 

2201  
2202 
(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2203 
= (idA_A2_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2204  
2205  
2206 
tel 
2207  
2208 
until true restart POINTA_A2 
2209  
2210  
2211  
2212 
state A2_A2B__TO__A2_A2A_1: 
2213  
2214 
var idA_A2_2, idA_A2_3:int; 
2215 
a_2:int; 
2216 
b_2:int; 
2217 
c_2:int; 
2218 
idB_B1_2:int; 
2219 
idB_B2_2:int; 
2220 
idEvents1_B_2:int; 
2221 
let 
2222  
2223 
 transition trace : 
2224 
A2_A2b__To__A2_A2a_1 
2225 
(idA_A2_2) 
2226 
= A2_A2b_ex(idA_A2_1, false); 
2227 

2228  
2229 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2230 
= A2_A2b__To__A2_A2a_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1); 
2231 

2232  
2233 
(idA_A2_3, a_2) 
2234 
= A2_A2a_en(idA_A2_2, x, a_1, false); 
2235 

2236  
2237 
(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2238 
= (idA_A2_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2239  
2240  
2241 
tel 
2242  
2243 
until true restart POINTA_A2 
2244  
2245  
2246  
2247 
state A2_A2A_IDL: 
2248  
2249 
let 
2250  
2251 

2252  
2253 
(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2254 
= (idA_A2_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2255 

2256  
2257 
tel 
2258  
2259 
until true restart POINTA_A2 
2260  
2261  
2262  
2263 
state A2_A2B_IDL: 
2264  
2265 
let 
2266  
2267 

2268  
2269 
(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2270 
= (idA_A2_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2271 

2272  
2273 
tel 
2274  
2275 
until true restart POINTA_A2 
2276  
2277  
2278  
2279 
tel 
2280  
2281  
2282  
2283  
2284  
2285  
2286 
node A1_A1a__To__A1_A1b_1_Transition_Action(idEvents1_B_1:int; 
2287 
b_1:int; 
2288 
idB_B1_1:int; 
2289 
x:int; 
2290 
T1:bool; 
2291 
idB_B2_1:int; 
2292 
c_1:int; 
2293 
R1:bool; 
2294 
S1:bool) 
2295  
2296 
returns (idEvents1_B:int; 
2297 
b:int; 
2298 
idB_B1:int; 
2299 
idB_B2:int; 
2300 
c:int); 
2301  
2302  
2303 
var idEvents1_B_2:int; 
2304 
b_2:int; 
2305 
idB_B1_2:int; 
2306 
idB_B2_2:int; 
2307 
c_2:int; 
2308  
2309  
2310 
let 
2311  
2312  
2313  
2314 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2315 
= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, true); 
2316 

2317  
2318 
(idEvents1_B, b, idB_B1, idB_B2, c) 
2319 
= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2); 
2320 

2321  
2322 
tel 
2323  
2324  
2325  
2326  
2327  
2328  
2329 
node A1_A1b__To__A1_A1a_1_Transition_Action(idEvents1_B_1:int; 
2330 
b_1:int; 
2331 
idB_B1_1:int; 
2332 
x:int; 
2333 
T1:bool; 
2334 
idB_B2_1:int; 
2335 
c_1:int; 
2336 
R1:bool; 
2337 
S1:bool) 
2338  
2339 
returns (idEvents1_B:int; 
2340 
b:int; 
2341 
idB_B1:int; 
2342 
idB_B2:int; 
2343 
c:int); 
2344  
2345  
2346 
var idEvents1_B_2:int; 
2347 
b_2:int; 
2348 
idB_B1_2:int; 
2349 
idB_B2_2:int; 
2350 
c_2:int; 
2351  
2352  
2353 
let 
2354  
2355  
2356  
2357 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2358 
= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, true, S1); 
2359 

2360  
2361 
(idEvents1_B, b, idB_B1, idB_B2, c) 
2362 
= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2); 
2363 

2364  
2365 
tel 
2366  
2367  
2368 
***************************************************State :A_A1 Automaton*************************************************** 
2369  
2370 
node A_A1_node(idA_A1_1:int; 
2371 
a_1:int; 
2372 
x:int; 
2373 
S:bool; 
2374 
R1:bool; 
2375 
S1:bool; 
2376 
T1:bool; 
2377 
b_1:int; 
2378 
c_1:int; 
2379 
idB_B1_1:int; 
2380 
idB_B2_1:int; 
2381 
idEvents1_B_1:int; 
2382 
R:bool) 
2383  
2384 
returns (idA_A1:int; 
2385 
a:int; 
2386 
b:int; 
2387 
c:int; 
2388 
idB_B1:int; 
2389 
idB_B2:int; 
2390 
idEvents1_B:int); 
2391  
2392  
2393 
let 
2394  
2395 
automaton a_a1 
2396  
2397 
state POINTA_A1: 
2398 
unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1 
2399  
2400  
2401  
2402 
unless (idA_A1_1=570) and S restart A1_A1A__TO__A1_A1B_1 
2403  
2404  
2405  
2406 
unless (idA_A1_1=571) and R restart A1_A1B__TO__A1_A1A_1 
2407  
2408  
2409  
2410 
unless (idA_A1_1=570) restart A1_A1A_IDL 
2411  
2412 
unless (idA_A1_1=571) restart A1_A1B_IDL 
2413  
2414 
let 
2415  
2416 
(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2417 
= (idA_A1_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2418 

2419  
2420 
tel 
2421  
2422  
2423  
2424 
state POINT__TO__A1_A1A_1: 
2425  
2426 
var idA_A1_2:int; 
2427 
a_2:int; 
2428 
let 
2429  
2430 
 transition trace : 
2431 
POINT__To__A1_A1a_1 
2432 
(idA_A1_2, a_2) 
2433 
= A1_A1a_en(idA_A1_1, x, a_1, false); 
2434 

2435  
2436 
(idA_A1, a) 
2437 
= (idA_A1_2, a_2); 
2438  
2439 
add unused variables 
2440 
(b, c, idB_B1, idB_B2, idEvents1_B) 
2441 
= (b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2442 

2443  
2444 
tel 
2445  
2446 
until true restart POINTA_A1 
2447  
2448  
2449  
2450 
state A1_A1A__TO__A1_A1B_1: 
2451  
2452 
var idA_A1_2, idA_A1_3:int; 
2453 
a_2:int; 
2454 
b_2:int; 
2455 
c_2:int; 
2456 
idB_B1_2:int; 
2457 
idB_B2_2:int; 
2458 
idEvents1_B_2:int; 
2459 
let 
2460  
2461 
 transition trace : 
2462 
A1_A1a__To__A1_A1b_1 
2463 
(idA_A1_2) 
2464 
= A1_A1a_ex(idA_A1_1, false); 
2465 

2466  
2467 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2468 
= A1_A1a__To__A1_A1b_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1); 
2469 

2470  
2471 
(idA_A1_3, a_2) 
2472 
= A1_A1b_en(idA_A1_2, x, a_1, false); 
2473 

2474  
2475 
(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2476 
= (idA_A1_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2477  
2478  
2479 
tel 
2480  
2481 
until true restart POINTA_A1 
2482  
2483  
2484  
2485 
state A1_A1B__TO__A1_A1A_1: 
2486  
2487 
var idA_A1_2, idA_A1_3:int; 
2488 
a_2:int; 
2489 
b_2:int; 
2490 
c_2:int; 
2491 
idB_B1_2:int; 
2492 
idB_B2_2:int; 
2493 
idEvents1_B_2:int; 
2494 
let 
2495  
2496 
 transition trace : 
2497 
A1_A1b__To__A1_A1a_1 
2498 
(idA_A1_2) 
2499 
= A1_A1b_ex(idA_A1_1, false); 
2500 

2501  
2502 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2503 
= A1_A1b__To__A1_A1a_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1); 
2504 

2505  
2506 
(idA_A1_3, a_2) 
2507 
= A1_A1a_en(idA_A1_2, x, a_1, false); 
2508 

2509  
2510 
(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2511 
= (idA_A1_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2512  
2513  
2514 
tel 
2515  
2516 
until true restart POINTA_A1 
2517  
2518  
2519  
2520 
state A1_A1A_IDL: 
2521  
2522 
let 
2523  
2524 

2525  
2526 
(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2527 
= (idA_A1_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2528 

2529  
2530 
tel 
2531  
2532 
until true restart POINTA_A1 
2533  
2534  
2535  
2536 
state A1_A1B_IDL: 
2537  
2538 
let 
2539  
2540 

2541  
2542 
(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2543 
= (idA_A1_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2544 

2545  
2546 
tel 
2547  
2548 
until true restart POINTA_A1 
2549  
2550  
2551  
2552 
tel 
2553  
2554  
2555  
2556  
2557  
2558  
2559 
node A_A2__To__A_A1_1_Transition_Action(idEvents1_B_1:int; 
2560 
b_1:int; 
2561 
idB_B1_1:int; 
2562 
x:int; 
2563 
T1:bool; 
2564 
idB_B2_1:int; 
2565 
c_1:int; 
2566 
R1:bool; 
2567 
S1:bool) 
2568  
2569 
returns (idEvents1_B:int; 
2570 
b:int; 
2571 
idB_B1:int; 
2572 
idB_B2:int; 
2573 
c:int); 
2574  
2575  
2576 
var idEvents1_B_2:int; 
2577 
b_2:int; 
2578 
idB_B1_2:int; 
2579 
idB_B2_2:int; 
2580 
c_2:int; 
2581  
2582  
2583 
let 
2584  
2585  
2586  
2587 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2588 
= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, true, idB_B2_1, c_1, R1, S1); 
2589 

2590  
2591 
(idEvents1_B, b, idB_B1, idB_B2, c) 
2592 
= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2); 
2593 

2594  
2595 
tel 
2596  
2597  
2598  
2599  
2600  
2601  
2602 
node A_A1__To__A_A2_1_Transition_Action(idEvents1_B_1:int; 
2603 
b_1:int; 
2604 
idB_B1_1:int; 
2605 
x:int; 
2606 
T1:bool; 
2607 
idB_B2_1:int; 
2608 
c_1:int; 
2609 
R1:bool; 
2610 
S1:bool) 
2611  
2612 
returns (idEvents1_B:int; 
2613 
b:int; 
2614 
idB_B1:int; 
2615 
idB_B2:int; 
2616 
c:int); 
2617  
2618  
2619 
var idEvents1_B_2:int; 
2620 
b_2:int; 
2621 
idB_B1_2:int; 
2622 
idB_B2_2:int; 
2623 
c_2:int; 
2624  
2625  
2626 
let 
2627  
2628  
2629  
2630 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2631 
= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, true, idB_B2_1, c_1, R1, S1); 
2632 

2633  
2634 
(idEvents1_B, b, idB_B1, idB_B2, c) 
2635 
= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2); 
2636 

2637  
2638 
tel 
2639  
2640  
2641 
***************************************************State :Events1_A Automaton*************************************************** 
2642  
2643 
node Events1_A_node(idEvents1_A_1:int; 
2644 
a_1:int; 
2645 
idA_A1_1:int; 
2646 
x:int; 
2647 
T:bool; 
2648 
idA_A2_1:int; 
2649 
R1:bool; 
2650 
S1:bool; 
2651 
T1:bool; 
2652 
b_1:int; 
2653 
c_1:int; 
2654 
idB_B1_1:int; 
2655 
idB_B2_1:int; 
2656 
idEvents1_B_1:int; 
2657 
R:bool; 
2658 
S:bool) 
2659  
2660 
returns (idEvents1_A:int; 
2661 
a:int; 
2662 
idA_A1:int; 
2663 
idA_A2:int; 
2664 
b:int; 
2665 
c:int; 
2666 
idB_B1:int; 
2667 
idB_B2:int; 
2668 
idEvents1_B:int); 
2669  
2670  
2671 
let 
2672  
2673 
automaton events1_a 
2674  
2675 
state POINTEvents1_A: 
2676 
unless (idEvents1_A_1=0) restart POINT__TO__A_A1_1 
2677  
2678  
2679  
2680 
unless (idEvents1_A_1=566) and T restart A_A2__TO__A_A1_1 
2681  
2682  
2683  
2684 
unless (idEvents1_A_1=569) and T restart A_A1__TO__A_A2_1 
2685  
2686  
2687  
2688 
unless (idEvents1_A_1=566) restart A_A2_IDL 
2689  
2690 
unless (idEvents1_A_1=569) restart A_A1_IDL 
2691  
2692 
let 
2693  
2694 
(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2695 
= (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2696 

2697  
2698 
tel 
2699  
2700  
2701  
2702 
state POINT__TO__A_A1_1: 
2703  
2704 
var idEvents1_A_2:int; 
2705 
a_2:int; 
2706 
idA_A1_2:int; 
2707 
let 
2708  
2709 
 transition trace : 
2710 
POINT__To__A_A1_1 
2711 
(idA_A1_2, idEvents1_A_2, a_2) 
2712 
= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, x, false); 
2713 

2714  
2715 
(idEvents1_A, a, idA_A1) 
2716 
= (idEvents1_A_2, a_2, idA_A1_2); 
2717  
2718 
add unused variables 
2719 
(b, c, idA_A2, idB_B1, idB_B2, idEvents1_B) 
2720 
= (b_1, c_1, idA_A2_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2721 

2722  
2723 
tel 
2724  
2725 
until true restart POINTEvents1_A 
2726  
2727  
2728  
2729 
state A_A2__TO__A_A1_1: 
2730  
2731 
var idEvents1_A_2, idEvents1_A_3:int; 
2732 
a_2:int; 
2733 
idA_A1_2:int; 
2734 
idA_A2_2:int; 
2735 
b_2:int; 
2736 
c_2:int; 
2737 
idB_B1_2:int; 
2738 
idB_B2_2:int; 
2739 
idEvents1_B_2:int; 
2740 
let 
2741  
2742 
 transition trace : 
2743 
A_A2__To__A_A1_1 
2744 
(idA_A2_2, idEvents1_A_2) 
2745 
= A_A2_ex(idA_A2_1, idEvents1_A_1, false); 
2746 

2747  
2748 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2749 
= A_A2__To__A_A1_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1); 
2750 

2751  
2752 
(idA_A1_2, idEvents1_A_3, a_2) 
2753 
= A_A1_en(idA_A1_1, idEvents1_A_2, a_1, x, false); 
2754 

2755  
2756 
(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2757 
= (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2758  
2759  
2760 
tel 
2761  
2762 
until true restart POINTEvents1_A 
2763  
2764  
2765  
2766 
state A_A1__TO__A_A2_1: 
2767  
2768 
var idEvents1_A_2, idEvents1_A_3:int; 
2769 
a_2:int; 
2770 
idA_A1_2:int; 
2771 
idA_A2_2:int; 
2772 
b_2:int; 
2773 
c_2:int; 
2774 
idB_B1_2:int; 
2775 
idB_B2_2:int; 
2776 
idEvents1_B_2:int; 
2777 
let 
2778  
2779 
 transition trace : 
2780 
A_A1__To__A_A2_1 
2781 
(idA_A1_2, idEvents1_A_2) 
2782 
= A_A1_ex(idA_A1_1, idEvents1_A_1, false); 
2783 

2784  
2785 
(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2786 
= A_A1__To__A_A2_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1); 
2787 

2788  
2789 
(idA_A2_2, idEvents1_A_3, a_2) 
2790 
= A_A2_en(idA_A2_1, idEvents1_A_2, a_1, x, false); 
2791 

2792  
2793 
(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2794 
= (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2795  
2796  
2797 
tel 
2798  
2799 
until true restart POINTEvents1_A 
2800  
2801  
2802  
2803 
state A_A2_IDL: 
2804  
2805 
var a_2:int; 
2806 
idA_A2_2:int; 
2807 
b_2:int; 
2808 
c_2:int; 
2809 
idB_B1_2:int; 
2810 
idB_B2_2:int; 
2811 
idEvents1_B_2:int; 
2812 
let 
2813  
2814 

2815 
(idA_A2_2, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2) 
2816 
= A_A2_node(idA_A2_1, a_1, x, S, R1, S1, T1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R); 
2817  
2818 

2819  
2820  
2821 
(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2822 
= (idEvents1_A_1, a_2, idA_A1_1, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2823 

2824  
2825 
tel 
2826  
2827 
until true restart POINTEvents1_A 
2828  
2829  
2830  
2831 
state A_A1_IDL: 
2832  
2833 
var a_2:int; 
2834 
idA_A1_2:int; 
2835 
b_2:int; 
2836 
c_2:int; 
2837 
idB_B1_2:int; 
2838 
idB_B2_2:int; 
2839 
idEvents1_B_2:int; 
2840 
let 
2841  
2842 

2843 
(idA_A1_2, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2) 
2844 
= A_A1_node(idA_A1_1, a_1, x, S, R1, S1, T1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R); 
2845  
2846 

2847  
2848  
2849 
(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2850 
= (idEvents1_A_1, a_2, idA_A1_2, idA_A2_1, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2851 

2852  
2853 
tel 
2854  
2855 
until true restart POINTEvents1_A 
2856  
2857  
2858  
2859 
tel 
2860  
2861  
2862 
***************************************************State :Events1_Events1 Automaton*************************************************** 
2863  
2864 
node Events1_Events1_node(idEvents1_Events1_1:int; 
2865 
a_1:int; 
2866 
idA_A1_1:int; 
2867 
idA_A2_1:int; 
2868 
idEvents1_A_1:int; 
2869 
x:int; 
2870 
b_1:int; 
2871 
idB_B1_1:int; 
2872 
idB_B2_1:int; 
2873 
idEvents1_B_1:int; 
2874 
R:bool; 
2875 
R1:bool; 
2876 
S:bool; 
2877 
S1:bool; 
2878 
T:bool; 
2879 
T1:bool; 
2880 
c_1:int) 
2881  
2882 
returns (idEvents1_Events1:int; 
2883 
a:int; 
2884 
idA_A1:int; 
2885 
idA_A2:int; 
2886 
idEvents1_A:int; 
2887 
b:int; 
2888 
idB_B1:int; 
2889 
idB_B2:int; 
2890 
idEvents1_B:int; 
2891 
c:int); 
2892  
2893  
2894 
let 
2895  
2896 
automaton events1_events1 
2897  
2898 
state POINTEvents1_Events1: 
2899 
unless (idEvents1_Events1_1=0) restart EVENTS1_EVENTS1_PARALLEL_ENTRY 
2900 
unless true restart EVENTS1_EVENTS1_PARALLEL_IDL 
2901  
2902 
let 
2903  
2904 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B, c) 
2905 
= (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, b_1, idB_B1_1, idB_B2_1, idEvents1_B_1, c_1); 
2906 

2907  
2908 
tel 
2909  
2910  
2911  
2912 
state EVENTS1_EVENTS1_PARALLEL_ENTRY: 
2913  
2914 
var idEvents1_Events1_2, idEvents1_Events1_3:int; 
2915 
a_2:int; 
2916 
idA_A1_2:int; 
2917 
idA_A2_2:int; 
2918 
idEvents1_A_2:int; 
2919 
b_2:int; 
2920 
idB_B1_2:int; 
2921 
idB_B2_2:int; 
2922 
idEvents1_B_2:int; 
2923 
let 
2924  
2925 

2926 
(idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2) 
2927 
= Events1_A_en(idEvents1_A_1, idEvents1_Events1_1, a_1, idA_A1_1, x, idA_A2_1, false); 
2928  
2929 
(idEvents1_B_2, idEvents1_Events1_3, b_2, idB_B1_2, idB_B2_2) 
2930 
= Events1_B_en(idEvents1_B_1, idEvents1_Events1_2, b_1, idB_B1_1, x, idB_B2_1, false); 
2931  
2932  
2933 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B) 
2934 
= (idEvents1_Events1_3, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2); 
2935 

2936 
add unused variables 
2937 
(c) 
2938 
= (c_1); 
2939 

2940  
2941 
tel 
2942  
2943 
until true restart POINTEvents1_Events1 
2944  
2945  
2946  
2947 
state EVENTS1_EVENTS1_PARALLEL_IDL: 
2948  
2949 
var a_2:int; 
2950 
idA_A1_2:int; 
2951 
idA_A2_2:int; 
2952 
idEvents1_A_2:int; 
2953 
b_2, b_3:int; 
2954 
idB_B1_2, idB_B1_3:int; 
2955 
idB_B2_2, idB_B2_3:int; 
2956 
idEvents1_B_2, idEvents1_B_3:int; 
2957 
c_2, c_3:int; 
2958 
let 
2959  
2960 

2961  
2962 
(idEvents1_A_2, a_2, idA_A1_2, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2) 
2963 
= if not (idEvents1_A_1= 0 ) then Events1_A_node(idEvents1_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R1, S1, T1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R, S) 
2964  
2965 
else (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1); 
2966  
2967 

2968  
2969 

2970  
2971 
(idEvents1_B_3, b_3, idB_B1_3, idB_B2_3, c_3) 
2972 
= if not (idEvents1_B_2= 0 ) then Events1_B_node(idEvents1_B_2, b_2, idB_B1_2, x, T1, idB_B2_2, c_2, R1, S1) 
2973  
2974 
else (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2); 
2975  
2976 

2977  
2978 

2979  
2980 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B, c) 
2981 
= (idEvents1_Events1_1, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, c_3); 
2982 

2983  
2984 
tel 
2985  
2986 
until true restart POINTEvents1_Events1 
2987  
2988  
2989  
2990 
tel 
2991  
2992  
2993 
***************************************************State :Events1_Events1 Automaton*************************************************** 
2994  
2995 
node Events1_Events1(x:int; 
2996 
R:bool; 
2997 
S:bool; 
2998 
T:bool) 
2999  
3000 
returns (a:int; 
3001 
b:int; 
3002 
c:int); 
3003  
3004  
3005 
var a_1: int; 
3006  
3007 
b_1: int; 
3008  
3009 
c_1: int; 
3010  
3011 
R1, R1_1: bool; 
3012  
3013 
S1, S1_1: bool; 
3014  
3015 
T1, T1_1: bool; 
3016  
3017 
idEvents1_Events1, idEvents1_Events1_1: int; 
3018  
3019 
idB_B2, idB_B2_1: int; 
3020  
3021 
idB_B1, idB_B1_1: int; 
3022  
3023 
idEvents1_B, idEvents1_B_1: int; 
3024  
3025 
idA_A2, idA_A2_1: int; 
3026  
3027 
idA_A1, idA_A1_1: int; 
3028  
3029 
idEvents1_A, idEvents1_A_1: int; 
3030  
3031 
idEvents1_Events1_2, idEvents1_Events1_3:int; 
3032 
a_2, a_3:int; 
3033 
idA_A1_2, idA_A1_3:int; 
3034 
idA_A2_2, idA_A2_3:int; 
3035 
idEvents1_A_2, idEvents1_A_3:int; 
3036 
b_2, b_3:int; 
3037 
idB_B1_2, idB_B1_3:int; 
3038 
idB_B2_2, idB_B2_3:int; 
3039 
idEvents1_B_2, idEvents1_B_3:int; 
3040 
c_2, c_3:int; 
3041 
let 
3042  
3043 
a_1 = 0 > pre a; 
3044  
3045 
b_1 = 0 > pre b; 
3046  
3047 
c_1 = 0 > pre c; 
3048  
3049 
R1_1 = false > pre R1; 
3050  
3051 
S1_1 = false > pre S1; 
3052  
3053 
T1_1 = false > pre T1; 
3054  
3055 
idEvents1_Events1_1 = 0 > pre idEvents1_Events1; 
3056  
3057 
idB_B2_1 = 0 > pre idB_B2; 
3058  
3059 
idB_B1_1 = 0 > pre idB_B1; 
3060  
3061 
idEvents1_B_1 = 0 > pre idEvents1_B; 
3062  
3063 
idA_A2_1 = 0 > pre idA_A2; 
3064  
3065 
idA_A1_1 = 0 > pre idA_A1; 
3066  
3067 
idEvents1_A_1 = 0 > pre idEvents1_A; 
3068  
3069 

3070  
3071  
3072  
3073 
(idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2, c_2) 
3074 
= 
3075  
3076 
if R then Events1_Events1_node(idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, x, b_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R, R1, false, S1, false, T1, c_1) 
3077  
3078 
else (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, b_1, idB_B1_1, idB_B2_1, idEvents1_B_1, c_1); 
3079  
3080 

3081  
3082  
3083  
3084 
(idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, c_3) 
3085 
= 
3086  
3087 
if S then Events1_Events1_node(idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, x, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2, false, R1, S, S1, false, T1, c_2) 
3088  
3089 
else (idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2, c_2); 
3090  
3091 

3092  
3093  
3094  
3095 
(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B, c) 
3096 
= 
3097  
3098 
if T then Events1_Events1_node(idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3, x, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, false, R1, false, S1, T, T1, c_3) 
3099  
3100 
else (idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, c_3); 
3101  
3102 

3103  
3104  
3105 
unused outputs 
3106 
R1 = false; 
3107  
3108 
S1 = false; 
3109  
3110 
T1 = false; 
3111  
3112 

3113  
3114 
tel 
3115  
3116  
3117  
3118 
node Events1 (x_1_1 : int; R_1_1 : real; S_1_1 : real; T_1_1 : real) 
3119 
returns (a_1_1 : int; 
3120 
b_2_1 : int; 
3121 
c_3_1 : int); 
3122 
var 
3123 
Events1_1_1 : int; Events1_2_1 : int; Events1_3_1 : int; 
3124 
Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real; 
3125 
i_virtual_local : real; 
3126 
Events1Mux_1_1_event: bool; 
3127 
Events1Mux_1_2_event: bool; 
3128 
Events1Mux_1_3_event: bool; 
3129 
let 
3130 
Events1Mux_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)); 
3131 
Events1Mux_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)); 
3132 
Events1Mux_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)); 
3133 
(Events1_1_1, Events1_2_1, Events1_3_1) = Events1_Events1(x_1_1, Events1Mux_1_1_event, Events1Mux_1_2_event, Events1Mux_1_3_event); 
3134 
Mux_1_1 = R_1_1 ; 
3135 
Mux_1_2 = S_1_1 ; 
3136 
Mux_1_3 = T_1_1 ; 
3137 
a_1_1 = Events1_1_1; 
3138 
b_2_1 = Events1_2_1; 
3139 
c_3_1 = Events1_3_1; 
3140 
i_virtual_local= 0.0 > 1.0; 
3141 
tel 
3142 