lustrectests / regression_tests / lustre_files / success / Stateflow / src_Parallel3 / Parallel3.lus @ eb639349
History  View  Annotate  Download (69.3 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  
19  
20  
21  
22  
23  
24  
25  
26  
27  
28  
29  
30  
31  
32  
33  
34  
35  
36  
37  
38  
39  
40  
41  
42  
43  
44  
45 
 Entry action for state :B2_B2a 
46 
node B2_B2a_en(idB_B2_1:int; 
47 
x:int; 
48 
b_1:int; 
49 
isInner:bool) 
50  
51 
returns (idB_B2:int; 
52 
b:int); 
53  
54  
55 
var idB_B2_2:int; 
56 
b_2:int; 
57  
58  
59 
let 
60  
61  
62  
63 
 set state as active 
64 
idB_B2_2 
65 
= 1501; 
66 

67  
68 
b_2 
69 
= if (not isInner) then x+7 
70 
else b_1; 
71 

72  
73 
(idB_B2, b) 
74 
= (idB_B2_2, b_2); 
75 

76  
77 
tel 
78  
79  
80  
81  
82  
83 
 Exit action for state :B2_B2a 
84 
node B2_B2a_ex(idB_B2_1:int; 
85 
isInner:bool) 
86  
87 
returns (idB_B2:int); 
88  
89  
90 
var idB_B2_2:int; 
91  
92  
93 
let 
94  
95  
96  
97 
 set state as inactive 
98 
idB_B2_2 
99 
= if (not isInner) then 0 else idB_B2_1; 
100  
101  
102 
(idB_B2) 
103 
= (idB_B2_1); 
104 

105  
106 
tel 
107  
108  
109  
110  
111  
112  
113 
 Entry action for state :B2_B2b 
114 
node B2_B2b_en(idB_B2_1:int; 
115 
x:int; 
116 
b_1:int; 
117 
isInner:bool) 
118  
119 
returns (idB_B2:int; 
120 
b:int); 
121  
122  
123 
var idB_B2_2:int; 
124 
b_2:int; 
125  
126  
127 
let 
128  
129  
130  
131 
 set state as active 
132 
idB_B2_2 
133 
= 1502; 
134 

135  
136 
b_2 
137 
= if (not isInner) then x+8 
138 
else b_1; 
139 

140  
141 
(idB_B2, b) 
142 
= (idB_B2_2, b_2); 
143 

144  
145 
tel 
146  
147  
148  
149  
150  
151 
 Exit action for state :B2_B2b 
152 
node B2_B2b_ex(idB_B2_1:int; 
153 
isInner:bool) 
154  
155 
returns (idB_B2:int); 
156  
157  
158 
var idB_B2_2:int; 
159  
160  
161 
let 
162  
163  
164  
165 
 set state as inactive 
166 
idB_B2_2 
167 
= if (not isInner) then 0 else idB_B2_1; 
168  
169  
170 
(idB_B2) 
171 
= (idB_B2_1); 
172 

173  
174 
tel 
175  
176  
177  
178  
179  
180  
181 
 Entry action for state :B_B2 
182 
node B_B2_en(idB_B2_1:int; 
183 
idParallel3_B_1:int; 
184 
b_1:int; 
185 
x:int; 
186 
isInner:bool) 
187  
188 
returns (idB_B2:int; 
189 
idParallel3_B:int; 
190 
b:int); 
191  
192  
193 
var idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5, idB_B2_6:int; 
194 
idParallel3_B_2, idParallel3_B_3, idParallel3_B_4:int; 
195 
b_2, b_3, b_4, b_5, b_6:int; 
196  
197  
198 
let 
199  
200  
201  
202 
 set state as active 
203 
idParallel3_B_2 
204 
= 1500; 
205 

206  
207 

208 
 transition trace : 
209 
POINT__To__B2_B2a_1 
210 
(idB_B2_2, b_2) 
211 
= B2_B2a_en(idB_B2_1, x, b_1, false); 
212 

213  
214 
(idB_B2_3, idParallel3_B_3, b_3) 
215 
= 
216  
217 
if ( idB_B2_1 = 0) then 
218  
219 
(idB_B2_2, idParallel3_B_2, b_2) 
220  
221 
else(idB_B2_1, idParallel3_B_2, b_1); 
222  
223 

224  
225 
(idB_B2_4, b_4) 
226 
= 
227 
if ( idB_B2_1 = 1501) then 
228 
B2_B2a_en(idB_B2_1, x, b_1, false) 
229 
else (idB_B2_1, b_1); 
230  
231 

232  
233 
(idB_B2_5, b_5) 
234 
= 
235 
if ( idB_B2_1 = 1502) then 
236 
B2_B2b_en(idB_B2_1, x, b_1, false) 
237 
else (idB_B2_1, b_1); 
238  
239 

240  
241 
(idB_B2_6, idParallel3_B_4, b_6) 
242 
= 
243 
if ( idB_B2_1 = 0) then 
244 
(idB_B2_3, idParallel3_B_3, b_3) 
245 
else 
246 
if ( idB_B2_1 = 1501) then 
247 
(idB_B2_4, idParallel3_B_3, b_4) 
248 
else 
249 
if ( idB_B2_1 = 1502) then 
250 
(idB_B2_5, idParallel3_B_3, b_5) 
251 
else (idB_B2_1, idParallel3_B_2, b_1); 
252  
253  
254 
(idB_B2, idParallel3_B, b) 
255 
= (idB_B2_6, idParallel3_B_4, b_6); 
256 

257  
258 
tel 
259  
260  
261  
262  
263  
264 
 Exit action for state :B_B2 
265 
node B_B2_ex(idB_B2_1:int; 
266 
idParallel3_B_1:int; 
267 
isInner:bool) 
268  
269 
returns (idB_B2:int; 
270 
idParallel3_B:int); 
271  
272  
273 
var idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5:int; 
274 
idParallel3_B_2:int; 
275  
276  
277 
let 
278  
279  
280  
281 

282 
(idB_B2_2) 
283 
= 
284 
if ( idB_B2_1 = 1501) then 
285 
B2_B2a_ex(idB_B2_1, false) 
286 
else (idB_B2_1); 
287  
288 

289  
290 
(idB_B2_3) 
291 
= 
292 
if ( idB_B2_1 = 1502) then 
293 
B2_B2b_ex(idB_B2_1, false) 
294 
else (idB_B2_1); 
295  
296 

297  
298 
(idB_B2_4) 
299 
= 
300 
if ( idB_B2_1 = 1501) then 
301 
(idB_B2_2) 
302 
else 
303 
if ( idB_B2_1 = 1502) then 
304 
(idB_B2_3) 
305 
else (idB_B2_1); 
306  
307  
308 
 set state as inactive 
309 
idParallel3_B_2 
310 
= if (not isInner) then 0 else idParallel3_B_1; 
311  
312 
idB_B2_5 
313 
= 0; 
314 

315  
316 
(idB_B2, idParallel3_B) 
317 
= (idB_B2_5, idParallel3_B_1); 
318 

319  
320 
tel 
321  
322  
323  
324  
325  
326  
327 
 Entry action for state :B1_B1a 
328 
node B1_B1a_en(idB_B1_1:int; 
329 
x:int; 
330 
b_1:int; 
331 
isInner:bool) 
332  
333 
returns (idB_B1:int; 
334 
b:int); 
335  
336  
337 
var idB_B1_2:int; 
338 
b_2:int; 
339  
340  
341 
let 
342  
343  
344  
345 
 set state as active 
346 
idB_B1_2 
347 
= 1504; 
348 

349  
350 
b_2 
351 
= if (not isInner) then x+5 
352 
else b_1; 
353 

354  
355 
(idB_B1, b) 
356 
= (idB_B1_2, b_2); 
357 

358  
359 
tel 
360  
361  
362  
363  
364  
365 
 Exit action for state :B1_B1a 
366 
node B1_B1a_ex(idB_B1_1:int; 
367 
isInner:bool) 
368  
369 
returns (idB_B1:int); 
370  
371  
372 
var idB_B1_2:int; 
373  
374  
375 
let 
376  
377  
378  
379 
 set state as inactive 
380 
idB_B1_2 
381 
= if (not isInner) then 0 else idB_B1_1; 
382  
383  
384 
(idB_B1) 
385 
= (idB_B1_1); 
386 

387  
388 
tel 
389  
390  
391  
392  
393  
394  
395 
 Entry action for state :B1_B1b 
396 
node B1_B1b_en(idB_B1_1:int; 
397 
x:int; 
398 
b_1:int; 
399 
isInner:bool) 
400  
401 
returns (idB_B1:int; 
402 
b:int); 
403  
404  
405 
var idB_B1_2:int; 
406 
b_2:int; 
407  
408  
409 
let 
410  
411  
412  
413 
 set state as active 
414 
idB_B1_2 
415 
= 1505; 
416 

417  
418 
b_2 
419 
= if (not isInner) then x+6 
420 
else b_1; 
421 

422  
423 
(idB_B1, b) 
424 
= (idB_B1_2, b_2); 
425 

426  
427 
tel 
428  
429  
430  
431  
432  
433 
 Exit action for state :B1_B1b 
434 
node B1_B1b_ex(idB_B1_1:int; 
435 
isInner:bool) 
436  
437 
returns (idB_B1:int); 
438  
439  
440 
var idB_B1_2:int; 
441  
442  
443 
let 
444  
445  
446  
447 
 set state as inactive 
448 
idB_B1_2 
449 
= if (not isInner) then 0 else idB_B1_1; 
450  
451  
452 
(idB_B1) 
453 
= (idB_B1_1); 
454 

455  
456 
tel 
457  
458  
459  
460  
461  
462  
463 
 Entry action for state :B_B1 
464 
node B_B1_en(idB_B1_1:int; 
465 
idParallel3_B_1:int; 
466 
b_1:int; 
467 
x:int; 
468 
isInner:bool) 
469  
470 
returns (idB_B1:int; 
471 
idParallel3_B:int; 
472 
b:int); 
473  
474  
475 
var idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5, idB_B1_6:int; 
476 
idParallel3_B_2, idParallel3_B_3, idParallel3_B_4:int; 
477 
b_2, b_3, b_4, b_5, b_6:int; 
478  
479  
480 
let 
481  
482  
483  
484 
 set state as active 
485 
idParallel3_B_2 
486 
= 1503; 
487 

488  
489 

490 
 transition trace : 
491 
POINT__To__B1_B1a_1 
492 
(idB_B1_2, b_2) 
493 
= B1_B1a_en(idB_B1_1, x, b_1, false); 
494 

495  
496 
(idB_B1_3, idParallel3_B_3, b_3) 
497 
= 
498  
499 
if ( idB_B1_1 = 0) then 
500  
501 
(idB_B1_2, idParallel3_B_2, b_2) 
502  
503 
else(idB_B1_1, idParallel3_B_2, b_1); 
504  
505 

506  
507 
(idB_B1_4, b_4) 
508 
= 
509 
if ( idB_B1_1 = 1504) then 
510 
B1_B1a_en(idB_B1_1, x, b_1, false) 
511 
else (idB_B1_1, b_1); 
512  
513 

514  
515 
(idB_B1_5, b_5) 
516 
= 
517 
if ( idB_B1_1 = 1505) then 
518 
B1_B1b_en(idB_B1_1, x, b_1, false) 
519 
else (idB_B1_1, b_1); 
520  
521 

522  
523 
(idB_B1_6, idParallel3_B_4, b_6) 
524 
= 
525 
if ( idB_B1_1 = 0) then 
526 
(idB_B1_3, idParallel3_B_3, b_3) 
527 
else 
528 
if ( idB_B1_1 = 1504) then 
529 
(idB_B1_4, idParallel3_B_3, b_4) 
530 
else 
531 
if ( idB_B1_1 = 1505) then 
532 
(idB_B1_5, idParallel3_B_3, b_5) 
533 
else (idB_B1_1, idParallel3_B_2, b_1); 
534  
535  
536 
(idB_B1, idParallel3_B, b) 
537 
= (idB_B1_6, idParallel3_B_4, b_6); 
538 

539  
540 
tel 
541  
542  
543  
544  
545  
546 
 Exit action for state :B_B1 
547 
node B_B1_ex(idB_B1_1:int; 
548 
idParallel3_B_1:int; 
549 
isInner:bool) 
550  
551 
returns (idB_B1:int; 
552 
idParallel3_B:int); 
553  
554  
555 
var idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int; 
556 
idParallel3_B_2:int; 
557  
558  
559 
let 
560  
561  
562  
563 

564 
(idB_B1_2) 
565 
= 
566 
if ( idB_B1_1 = 1504) then 
567 
B1_B1a_ex(idB_B1_1, false) 
568 
else (idB_B1_1); 
569  
570 

571  
572 
(idB_B1_3) 
573 
= 
574 
if ( idB_B1_1 = 1505) then 
575 
B1_B1b_ex(idB_B1_1, false) 
576 
else (idB_B1_1); 
577  
578 

579  
580 
(idB_B1_4) 
581 
= 
582 
if ( idB_B1_1 = 1504) then 
583 
(idB_B1_2) 
584 
else 
585 
if ( idB_B1_1 = 1505) then 
586 
(idB_B1_3) 
587 
else (idB_B1_1); 
588  
589  
590 
 set state as inactive 
591 
idParallel3_B_2 
592 
= if (not isInner) then 0 else idParallel3_B_1; 
593  
594 
idB_B1_5 
595 
= 0; 
596 

597  
598 
(idB_B1, idParallel3_B) 
599 
= (idB_B1_5, idParallel3_B_1); 
600 

601  
602 
tel 
603  
604  
605  
606  
607  
608  
609 
 Entry action for state :Parallel3_B 
610 
node Parallel3_B_en(idParallel3_B_1:int; 
611 
idParallel3_Parallel3_1:int; 
612 
b_1:int; 
613 
idB_B1_1:int; 
614 
x:int; 
615 
idB_B2_1:int; 
616 
isInner:bool) 
617  
618 
returns (idParallel3_B:int; 
619 
idParallel3_Parallel3:int; 
620 
b:int; 
621 
idB_B1:int; 
622 
idB_B2:int); 
623  
624  
625 
var idParallel3_B_2, idParallel3_B_3, idParallel3_B_4, idParallel3_B_5, idParallel3_B_6:int; 
626 
idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int; 
627 
b_2, b_3, b_4, b_5, b_6:int; 
628 
idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int; 
629 
idB_B2_2, idB_B2_3:int; 
630  
631  
632 
let 
633  
634  
635  
636 
 set state as active 
637 
idParallel3_Parallel3_2 
638 
= 1499; 
639 

640  
641 

642 
 transition trace : 
643 
POINT__To__B_B1_1 
644 
(idB_B1_2, idParallel3_B_2, b_2) 
645 
= B_B1_en(idB_B1_1, idParallel3_B_1, b_1, x, false); 
646 

647  
648 
(idParallel3_B_3, idParallel3_Parallel3_3, b_3, idB_B1_3) 
649 
= 
650  
651 
if ( idParallel3_B_1 = 0) then 
652  
653 
(idParallel3_B_2, idParallel3_Parallel3_2, b_2, idB_B1_2) 
654  
655 
else(idParallel3_B_1, idParallel3_Parallel3_2, b_1, idB_B1_1); 
656  
657 

658  
659 
(idB_B2_2, idParallel3_B_4, b_4) 
660 
= 
661 
if ( idParallel3_B_1 = 1500) then 
662 
B_B2_en(idB_B2_1, idParallel3_B_1, b_1, x, false) 
663 
else (idB_B2_1, idParallel3_B_1, b_1); 
664  
665 

666  
667 
(idB_B1_4, idParallel3_B_5, b_5) 
668 
= 
669 
if ( idParallel3_B_1 = 1503) then 
670 
B_B1_en(idB_B1_1, idParallel3_B_1, b_1, x, false) 
671 
else (idB_B1_1, idParallel3_B_1, b_1); 
672  
673 

674  
675 
(idParallel3_B_6, idParallel3_Parallel3_4, b_6, idB_B1_5, idB_B2_3) 
676 
= 
677 
if ( idParallel3_B_1 = 0) then 
678 
(idParallel3_B_3, idParallel3_Parallel3_3, b_3, idB_B1_3, idB_B2_1) 
679 
else 
680 
if ( idParallel3_B_1 = 1500) then 
681 
(idParallel3_B_4, idParallel3_Parallel3_3, b_4, idB_B1_1, idB_B2_2) 
682 
else 
683 
if ( idParallel3_B_1 = 1503) then 
684 
(idParallel3_B_5, idParallel3_Parallel3_3, b_5, idB_B1_4, idB_B2_1) 
685 
else (idParallel3_B_1, idParallel3_Parallel3_2, b_1, idB_B1_1, idB_B2_1); 
686  
687  
688 
(idParallel3_B, idParallel3_Parallel3, b, idB_B1, idB_B2) 
689 
= (idParallel3_B_6, idParallel3_Parallel3_4, b_6, idB_B1_5, idB_B2_3); 
690 

691  
692 
tel 
693  
694  
695  
696  
697  
698 
 Exit action for state :Parallel3_B 
699 
node Parallel3_B_ex(idB_B2_1:int; 
700 
idParallel3_B_1:int; 
701 
idB_B1_1:int; 
702 
idParallel3_Parallel3_1:int; 
703 
isInner:bool) 
704  
705 
returns (idB_B2:int; 
706 
idParallel3_B:int; 
707 
idB_B1:int; 
708 
idParallel3_Parallel3:int); 
709  
710  
711 
var idB_B2_2, idB_B2_3:int; 
712 
idParallel3_B_2, idParallel3_B_3, idParallel3_B_4, idParallel3_B_5:int; 
713 
idB_B1_2, idB_B1_3:int; 
714 
idParallel3_Parallel3_2:int; 
715  
716  
717 
let 
718  
719  
720  
721 

722 
(idB_B2_2, idParallel3_B_2) 
723 
= 
724 
if ( idParallel3_B_1 = 1500) then 
725 
B_B2_ex(idB_B2_1, idParallel3_B_1, false) 
726 
else (idB_B2_1, idParallel3_B_1); 
727  
728 

729  
730 
(idB_B1_2, idParallel3_B_3) 
731 
= 
732 
if ( idParallel3_B_1 = 1503) then 
733 
B_B1_ex(idB_B1_1, idParallel3_B_1, false) 
734 
else (idB_B1_1, idParallel3_B_1); 
735  
736 

737  
738 
(idB_B2_3, idParallel3_B_4, idB_B1_3) 
739 
= 
740 
if ( idParallel3_B_1 = 1500) then 
741 
(idB_B2_2, idParallel3_B_2, idB_B1_1) 
742 
else 
743 
if ( idParallel3_B_1 = 1503) then 
744 
(idB_B2_1, idParallel3_B_3, idB_B1_2) 
745 
else (idB_B2_1, idParallel3_B_1, idB_B1_1); 
746  
747  
748 
 set state as inactive 
749 
idParallel3_Parallel3_2 
750 
= if (not isInner) then 0 else idParallel3_Parallel3_1; 
751  
752 
idParallel3_B_5 
753 
= 0; 
754 

755  
756 
(idB_B2, idParallel3_B, idB_B1, idParallel3_Parallel3) 
757 
= (idB_B2_3, idParallel3_B_5, idB_B1_3, idParallel3_Parallel3_1); 
758 

759  
760 
tel 
761  
762  
763  
764  
765  
766  
767 
 Entry action for state :D2_D2a 
768 
node D2_D2a_en(idD_D2_1:int; 
769 
y:int; 
770 
dd_1:int; 
771 
isInner:bool) 
772  
773 
returns (idD_D2:int; 
774 
dd:int); 
775  
776  
777 
var idD_D2_2:int; 
778 
dd_2:int; 
779  
780  
781 
let 
782  
783  
784  
785 
 set state as active 
786 
idD_D2_2 
787 
= 1515; 
788 

789  
790 
dd_2 
791 
= if (not isInner) then y+7 
792 
else dd_1; 
793 

794  
795 
(idD_D2, dd) 
796 
= (idD_D2_2, dd_2); 
797 

798  
799 
tel 
800  
801  
802  
803  
804  
805 
 Exit action for state :D2_D2a 
806 
node D2_D2a_ex(idD_D2_1:int; 
807 
isInner:bool) 
808  
809 
returns (idD_D2:int); 
810  
811  
812 
var idD_D2_2:int; 
813  
814  
815 
let 
816  
817  
818  
819 
 set state as inactive 
820 
idD_D2_2 
821 
= if (not isInner) then 0 else idD_D2_1; 
822  
823  
824 
(idD_D2) 
825 
= (idD_D2_1); 
826 

827  
828 
tel 
829  
830  
831  
832  
833  
834  
835 
 Entry action for state :D2_D2b 
836 
node D2_D2b_en(idD_D2_1:int; 
837 
y:int; 
838 
dd_1:int; 
839 
isInner:bool) 
840  
841 
returns (idD_D2:int; 
842 
dd:int); 
843  
844  
845 
var idD_D2_2:int; 
846 
dd_2:int; 
847  
848  
849 
let 
850  
851  
852  
853 
 set state as active 
854 
idD_D2_2 
855 
= 1516; 
856 

857  
858 
dd_2 
859 
= if (not isInner) then y+8 
860 
else dd_1; 
861 

862  
863 
(idD_D2, dd) 
864 
= (idD_D2_2, dd_2); 
865 

866  
867 
tel 
868  
869  
870  
871  
872  
873 
 Exit action for state :D2_D2b 
874 
node D2_D2b_ex(idD_D2_1:int; 
875 
isInner:bool) 
876  
877 
returns (idD_D2:int); 
878  
879  
880 
var idD_D2_2:int; 
881  
882  
883 
let 
884  
885  
886  
887 
 set state as inactive 
888 
idD_D2_2 
889 
= if (not isInner) then 0 else idD_D2_1; 
890  
891  
892 
(idD_D2) 
893 
= (idD_D2_1); 
894 

895  
896 
tel 
897  
898  
899  
900  
901  
902  
903 
 Entry action for state :D_D2 
904 
node D_D2_en(idD_D2_1:int; 
905 
idParallel3_D_1:int; 
906 
dd_1:int; 
907 
y:int; 
908 
isInner:bool) 
909  
910 
returns (idD_D2:int; 
911 
idParallel3_D:int; 
912 
dd:int); 
913  
914  
915 
var idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5, idD_D2_6:int; 
916 
idParallel3_D_2, idParallel3_D_3, idParallel3_D_4:int; 
917 
dd_2, dd_3, dd_4, dd_5, dd_6:int; 
918  
919  
920 
let 
921  
922  
923  
924 
 set state as active 
925 
idParallel3_D_2 
926 
= 1514; 
927 

928  
929 

930 
 transition trace : 
931 
POINT__To__D2_D2a_1 
932 
(idD_D2_2, dd_2) 
933 
= D2_D2a_en(idD_D2_1, y, dd_1, false); 
934 

935  
936 
(idD_D2_3, idParallel3_D_3, dd_3) 
937 
= 
938  
939 
if ( idD_D2_1 = 0) then 
940  
941 
(idD_D2_2, idParallel3_D_2, dd_2) 
942  
943 
else(idD_D2_1, idParallel3_D_2, dd_1); 
944  
945 

946  
947 
(idD_D2_4, dd_4) 
948 
= 
949 
if ( idD_D2_1 = 1515) then 
950 
D2_D2a_en(idD_D2_1, y, dd_1, false) 
951 
else (idD_D2_1, dd_1); 
952  
953 

954  
955 
(idD_D2_5, dd_5) 
956 
= 
957 
if ( idD_D2_1 = 1516) then 
958 
D2_D2b_en(idD_D2_1, y, dd_1, false) 
959 
else (idD_D2_1, dd_1); 
960  
961 

962  
963 
(idD_D2_6, idParallel3_D_4, dd_6) 
964 
= 
965 
if ( idD_D2_1 = 0) then 
966 
(idD_D2_3, idParallel3_D_3, dd_3) 
967 
else 
968 
if ( idD_D2_1 = 1515) then 
969 
(idD_D2_4, idParallel3_D_3, dd_4) 
970 
else 
971 
if ( idD_D2_1 = 1516) then 
972 
(idD_D2_5, idParallel3_D_3, dd_5) 
973 
else (idD_D2_1, idParallel3_D_2, dd_1); 
974  
975  
976 
(idD_D2, idParallel3_D, dd) 
977 
= (idD_D2_6, idParallel3_D_4, dd_6); 
978 

979  
980 
tel 
981  
982  
983  
984  
985  
986 
 Exit action for state :D_D2 
987 
node D_D2_ex(idD_D2_1:int; 
988 
idParallel3_D_1:int; 
989 
isInner:bool) 
990  
991 
returns (idD_D2:int; 
992 
idParallel3_D:int); 
993  
994  
995 
var idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5:int; 
996 
idParallel3_D_2:int; 
997  
998  
999 
let 
1000  
1001  
1002  
1003 

1004 
(idD_D2_2) 
1005 
= 
1006 
if ( idD_D2_1 = 1515) then 
1007 
D2_D2a_ex(idD_D2_1, false) 
1008 
else (idD_D2_1); 
1009  
1010 

1011  
1012 
(idD_D2_3) 
1013 
= 
1014 
if ( idD_D2_1 = 1516) then 
1015 
D2_D2b_ex(idD_D2_1, false) 
1016 
else (idD_D2_1); 
1017  
1018 

1019  
1020 
(idD_D2_4) 
1021 
= 
1022 
if ( idD_D2_1 = 1515) then 
1023 
(idD_D2_2) 
1024 
else 
1025 
if ( idD_D2_1 = 1516) then 
1026 
(idD_D2_3) 
1027 
else (idD_D2_1); 
1028  
1029  
1030 
 set state as inactive 
1031 
idParallel3_D_2 
1032 
= if (not isInner) then 0 else idParallel3_D_1; 
1033  
1034 
idD_D2_5 
1035 
= 0; 
1036 

1037  
1038 
(idD_D2, idParallel3_D) 
1039 
= (idD_D2_5, idParallel3_D_1); 
1040 

1041  
1042 
tel 
1043  
1044  
1045  
1046  
1047  
1048  
1049 
 Entry action for state :D1_D1a 
1050 
node D1_D1a_en(idD_D1_1:int; 
1051 
y:int; 
1052 
dd_1:int; 
1053 
isInner:bool) 
1054  
1055 
returns (idD_D1:int; 
1056 
dd:int); 
1057  
1058  
1059 
var idD_D1_2:int; 
1060 
dd_2:int; 
1061  
1062  
1063 
let 
1064  
1065  
1066  
1067 
 set state as active 
1068 
idD_D1_2 
1069 
= 1518; 
1070 

1071  
1072 
dd_2 
1073 
= if (not isInner) then y+5 
1074 
else dd_1; 
1075 

1076  
1077 
(idD_D1, dd) 
1078 
= (idD_D1_2, dd_2); 
1079 

1080  
1081 
tel 
1082  
1083  
1084  
1085  
1086  
1087 
 Exit action for state :D1_D1a 
1088 
node D1_D1a_ex(idD_D1_1:int; 
1089 
isInner:bool) 
1090  
1091 
returns (idD_D1:int); 
1092  
1093  
1094 
var idD_D1_2:int; 
1095  
1096  
1097 
let 
1098  
1099  
1100  
1101 
 set state as inactive 
1102 
idD_D1_2 
1103 
= if (not isInner) then 0 else idD_D1_1; 
1104  
1105  
1106 
(idD_D1) 
1107 
= (idD_D1_1); 
1108 

1109  
1110 
tel 
1111  
1112  
1113  
1114  
1115  
1116  
1117 
 Entry action for state :D1_D1b 
1118 
node D1_D1b_en(idD_D1_1:int; 
1119 
y:int; 
1120 
dd_1:int; 
1121 
isInner:bool) 
1122  
1123 
returns (idD_D1:int; 
1124 
dd:int); 
1125  
1126  
1127 
var idD_D1_2:int; 
1128 
dd_2:int; 
1129  
1130  
1131 
let 
1132  
1133  
1134  
1135 
 set state as active 
1136 
idD_D1_2 
1137 
= 1519; 
1138 

1139  
1140 
dd_2 
1141 
= if (not isInner) then y+6 
1142 
else dd_1; 
1143 

1144  
1145 
(idD_D1, dd) 
1146 
= (idD_D1_2, dd_2); 
1147 

1148  
1149 
tel 
1150  
1151  
1152  
1153  
1154  
1155 
 Exit action for state :D1_D1b 
1156 
node D1_D1b_ex(idD_D1_1:int; 
1157 
isInner:bool) 
1158  
1159 
returns (idD_D1:int); 
1160  
1161  
1162 
var idD_D1_2:int; 
1163  
1164  
1165 
let 
1166  
1167  
1168  
1169 
 set state as inactive 
1170 
idD_D1_2 
1171 
= if (not isInner) then 0 else idD_D1_1; 
1172  
1173  
1174 
(idD_D1) 
1175 
= (idD_D1_1); 
1176 

1177  
1178 
tel 
1179  
1180  
1181  
1182  
1183  
1184  
1185 
 Entry action for state :D_D1 
1186 
node D_D1_en(idD_D1_1:int; 
1187 
idParallel3_D_1:int; 
1188 
dd_1:int; 
1189 
y:int; 
1190 
isInner:bool) 
1191  
1192 
returns (idD_D1:int; 
1193 
idParallel3_D:int; 
1194 
dd:int); 
1195  
1196  
1197 
var idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5, idD_D1_6:int; 
1198 
idParallel3_D_2, idParallel3_D_3, idParallel3_D_4:int; 
1199 
dd_2, dd_3, dd_4, dd_5, dd_6:int; 
1200  
1201  
1202 
let 
1203  
1204  
1205  
1206 
 set state as active 
1207 
idParallel3_D_2 
1208 
= 1517; 
1209 

1210  
1211 

1212 
 transition trace : 
1213 
POINT__To__D1_D1a_1 
1214 
(idD_D1_2, dd_2) 
1215 
= D1_D1a_en(idD_D1_1, y, dd_1, false); 
1216 

1217  
1218 
(idD_D1_3, idParallel3_D_3, dd_3) 
1219 
= 
1220  
1221 
if ( idD_D1_1 = 0) then 
1222  
1223 
(idD_D1_2, idParallel3_D_2, dd_2) 
1224  
1225 
else(idD_D1_1, idParallel3_D_2, dd_1); 
1226  
1227 

1228  
1229 
(idD_D1_4, dd_4) 
1230 
= 
1231 
if ( idD_D1_1 = 1518) then 
1232 
D1_D1a_en(idD_D1_1, y, dd_1, false) 
1233 
else (idD_D1_1, dd_1); 
1234  
1235 

1236  
1237 
(idD_D1_5, dd_5) 
1238 
= 
1239 
if ( idD_D1_1 = 1519) then 
1240 
D1_D1b_en(idD_D1_1, y, dd_1, false) 
1241 
else (idD_D1_1, dd_1); 
1242  
1243 

1244  
1245 
(idD_D1_6, idParallel3_D_4, dd_6) 
1246 
= 
1247 
if ( idD_D1_1 = 0) then 
1248 
(idD_D1_3, idParallel3_D_3, dd_3) 
1249 
else 
1250 
if ( idD_D1_1 = 1518) then 
1251 
(idD_D1_4, idParallel3_D_3, dd_4) 
1252 
else 
1253 
if ( idD_D1_1 = 1519) then 
1254 
(idD_D1_5, idParallel3_D_3, dd_5) 
1255 
else (idD_D1_1, idParallel3_D_2, dd_1); 
1256  
1257  
1258 
(idD_D1, idParallel3_D, dd) 
1259 
= (idD_D1_6, idParallel3_D_4, dd_6); 
1260 

1261  
1262 
tel 
1263  
1264  
1265  
1266  
1267  
1268 
 Exit action for state :D_D1 
1269 
node D_D1_ex(idD_D1_1:int; 
1270 
idParallel3_D_1:int; 
1271 
isInner:bool) 
1272  
1273 
returns (idD_D1:int; 
1274 
idParallel3_D:int); 
1275  
1276  
1277 
var idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int; 
1278 
idParallel3_D_2:int; 
1279  
1280  
1281 
let 
1282  
1283  
1284  
1285 

1286 
(idD_D1_2) 
1287 
= 
1288 
if ( idD_D1_1 = 1518) then 
1289 
D1_D1a_ex(idD_D1_1, false) 
1290 
else (idD_D1_1); 
1291  
1292 

1293  
1294 
(idD_D1_3) 
1295 
= 
1296 
if ( idD_D1_1 = 1519) then 
1297 
D1_D1b_ex(idD_D1_1, false) 
1298 
else (idD_D1_1); 
1299  
1300 

1301  
1302 
(idD_D1_4) 
1303 
= 
1304 
if ( idD_D1_1 = 1518) then 
1305 
(idD_D1_2) 
1306 
else 
1307 
if ( idD_D1_1 = 1519) then 
1308 
(idD_D1_3) 
1309 
else (idD_D1_1); 
1310  
1311  
1312 
 set state as inactive 
1313 
idParallel3_D_2 
1314 
= if (not isInner) then 0 else idParallel3_D_1; 
1315  
1316 
idD_D1_5 
1317 
= 0; 
1318 

1319  
1320 
(idD_D1, idParallel3_D) 
1321 
= (idD_D1_5, idParallel3_D_1); 
1322 

1323  
1324 
tel 
1325  
1326  
1327  
1328  
1329  
1330  
1331 
 Entry action for state :Parallel3_D 
1332 
node Parallel3_D_en(idParallel3_D_1:int; 
1333 
idParallel3_Parallel3_1:int; 
1334 
dd_1:int; 
1335 
idD_D1_1:int; 
1336 
y:int; 
1337 
idD_D2_1:int; 
1338 
isInner:bool) 
1339  
1340 
returns (idParallel3_D:int; 
1341 
idParallel3_Parallel3:int; 
1342 
dd:int; 
1343 
idD_D1:int; 
1344 
idD_D2:int); 
1345  
1346  
1347 
var idParallel3_D_2, idParallel3_D_3, idParallel3_D_4, idParallel3_D_5, idParallel3_D_6:int; 
1348 
idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int; 
1349 
dd_2, dd_3, dd_4, dd_5, dd_6:int; 
1350 
idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int; 
1351 
idD_D2_2, idD_D2_3:int; 
1352  
1353  
1354 
let 
1355  
1356  
1357  
1358 
 set state as active 
1359 
idParallel3_Parallel3_2 
1360 
= 1513; 
1361 

1362  
1363 

1364 
 transition trace : 
1365 
POINT__To__D_D1_1 
1366 
(idD_D1_2, idParallel3_D_2, dd_2) 
1367 
= D_D1_en(idD_D1_1, idParallel3_D_1, dd_1, y, false); 
1368 

1369  
1370 
(idParallel3_D_3, idParallel3_Parallel3_3, dd_3, idD_D1_3) 
1371 
= 
1372  
1373 
if ( idParallel3_D_1 = 0) then 
1374  
1375 
(idParallel3_D_2, idParallel3_Parallel3_2, dd_2, idD_D1_2) 
1376  
1377 
else(idParallel3_D_1, idParallel3_Parallel3_2, dd_1, idD_D1_1); 
1378  
1379 

1380  
1381 
(idD_D2_2, idParallel3_D_4, dd_4) 
1382 
= 
1383 
if ( idParallel3_D_1 = 1514) then 
1384 
D_D2_en(idD_D2_1, idParallel3_D_1, dd_1, y, false) 
1385 
else (idD_D2_1, idParallel3_D_1, dd_1); 
1386  
1387 

1388  
1389 
(idD_D1_4, idParallel3_D_5, dd_5) 
1390 
= 
1391 
if ( idParallel3_D_1 = 1517) then 
1392 
D_D1_en(idD_D1_1, idParallel3_D_1, dd_1, y, false) 
1393 
else (idD_D1_1, idParallel3_D_1, dd_1); 
1394  
1395 

1396  
1397 
(idParallel3_D_6, idParallel3_Parallel3_4, dd_6, idD_D1_5, idD_D2_3) 
1398 
= 
1399 
if ( idParallel3_D_1 = 0) then 
1400 
(idParallel3_D_3, idParallel3_Parallel3_3, dd_3, idD_D1_3, idD_D2_1) 
1401 
else 
1402 
if ( idParallel3_D_1 = 1514) then 
1403 
(idParallel3_D_4, idParallel3_Parallel3_3, dd_4, idD_D1_1, idD_D2_2) 
1404 
else 
1405 
if ( idParallel3_D_1 = 1517) then 
1406 
(idParallel3_D_5, idParallel3_Parallel3_3, dd_5, idD_D1_4, idD_D2_1) 
1407 
else (idParallel3_D_1, idParallel3_Parallel3_2, dd_1, idD_D1_1, idD_D2_1); 
1408  
1409  
1410 
(idParallel3_D, idParallel3_Parallel3, dd, idD_D1, idD_D2) 
1411 
= (idParallel3_D_6, idParallel3_Parallel3_4, dd_6, idD_D1_5, idD_D2_3); 
1412 

1413  
1414 
tel 
1415  
1416  
1417  
1418  
1419  
1420 
 Exit action for state :Parallel3_D 
1421 
node Parallel3_D_ex(idD_D2_1:int; 
1422 
idParallel3_D_1:int; 
1423 
idD_D1_1:int; 
1424 
idParallel3_Parallel3_1:int; 
1425 
isInner:bool) 
1426  
1427 
returns (idD_D2:int; 
1428 
idParallel3_D:int; 
1429 
idD_D1:int; 
1430 
idParallel3_Parallel3:int); 
1431  
1432  
1433 
var idD_D2_2, idD_D2_3:int; 
1434 
idParallel3_D_2, idParallel3_D_3, idParallel3_D_4, idParallel3_D_5:int; 
1435 
idD_D1_2, idD_D1_3:int; 
1436 
idParallel3_Parallel3_2:int; 
1437  
1438  
1439 
let 
1440  
1441  
1442  
1443 

1444 
(idD_D2_2, idParallel3_D_2) 
1445 
= 
1446 
if ( idParallel3_D_1 = 1514) then 
1447 
D_D2_ex(idD_D2_1, idParallel3_D_1, false) 
1448 
else (idD_D2_1, idParallel3_D_1); 
1449  
1450 

1451  
1452 
(idD_D1_2, idParallel3_D_3) 
1453 
= 
1454 
if ( idParallel3_D_1 = 1517) then 
1455 
D_D1_ex(idD_D1_1, idParallel3_D_1, false) 
1456 
else (idD_D1_1, idParallel3_D_1); 
1457  
1458 

1459  
1460 
(idD_D2_3, idParallel3_D_4, idD_D1_3) 
1461 
= 
1462 
if ( idParallel3_D_1 = 1514) then 
1463 
(idD_D2_2, idParallel3_D_2, idD_D1_1) 
1464 
else 
1465 
if ( idParallel3_D_1 = 1517) then 
1466 
(idD_D2_1, idParallel3_D_3, idD_D1_2) 
1467 
else (idD_D2_1, idParallel3_D_1, idD_D1_1); 
1468  
1469  
1470 
 set state as inactive 
1471 
idParallel3_Parallel3_2 
1472 
= if (not isInner) then 0 else idParallel3_Parallel3_1; 
1473  
1474 
idParallel3_D_5 
1475 
= 0; 
1476 

1477  
1478 
(idD_D2, idParallel3_D, idD_D1, idParallel3_Parallel3) 
1479 
= (idD_D2_3, idParallel3_D_5, idD_D1_3, idParallel3_Parallel3_1); 
1480 

1481  
1482 
tel 
1483  
1484  
1485  
1486  
1487  
1488  
1489 
 Entry action for state :C2_C2a 
1490 
node C2_C2a_en(idC_C2_1:int; 
1491 
y:int; 
1492 
c_1:int; 
1493 
isInner:bool) 
1494  
1495 
returns (idC_C2:int; 
1496 
c:int); 
1497  
1498  
1499 
var idC_C2_2:int; 
1500 
c_2:int; 
1501  
1502  
1503 
let 
1504  
1505  
1506  
1507 
 set state as active 
1508 
idC_C2_2 
1509 
= 1508; 
1510 

1511  
1512 
c_2 
1513 
= if (not isInner) then y+3 
1514 
else c_1; 
1515 

1516  
1517 
(idC_C2, c) 
1518 
= (idC_C2_2, c_2); 
1519 

1520  
1521 
tel 
1522  
1523  
1524  
1525  
1526  
1527 
 Exit action for state :C2_C2a 
1528 
node C2_C2a_ex(idC_C2_1:int; 
1529 
isInner:bool) 
1530  
1531 
returns (idC_C2:int); 
1532  
1533  
1534 
var idC_C2_2:int; 
1535  
1536  
1537 
let 
1538  
1539  
1540  
1541 
 set state as inactive 
1542 
idC_C2_2 
1543 
= if (not isInner) then 0 else idC_C2_1; 
1544  
1545  
1546 
(idC_C2) 
1547 
= (idC_C2_1); 
1548 

1549  
1550 
tel 
1551  
1552  
1553  
1554  
1555  
1556  
1557 
 Entry action for state :C2_C2b 
1558 
node C2_C2b_en(idC_C2_1:int; 
1559 
y:int; 
1560 
c_1:int; 
1561 
isInner:bool) 
1562  
1563 
returns (idC_C2:int; 
1564 
c:int); 
1565  
1566  
1567 
var idC_C2_2:int; 
1568 
c_2:int; 
1569  
1570  
1571 
let 
1572  
1573  
1574  
1575 
 set state as active 
1576 
idC_C2_2 
1577 
= 1509; 
1578 

1579  
1580 
c_2 
1581 
= if (not isInner) then y+4 
1582 
else c_1; 
1583 

1584  
1585 
(idC_C2, c) 
1586 
= (idC_C2_2, c_2); 
1587 

1588  
1589 
tel 
1590  
1591  
1592  
1593  
1594  
1595 
 Exit action for state :C2_C2b 
1596 
node C2_C2b_ex(idC_C2_1:int; 
1597 
isInner:bool) 
1598  
1599 
returns (idC_C2:int); 
1600  
1601  
1602 
var idC_C2_2:int; 
1603  
1604  
1605 
let 
1606  
1607  
1608  
1609 
 set state as inactive 
1610 
idC_C2_2 
1611 
= if (not isInner) then 0 else idC_C2_1; 
1612  
1613  
1614 
(idC_C2) 
1615 
= (idC_C2_1); 
1616 

1617  
1618 
tel 
1619  
1620  
1621  
1622  
1623  
1624  
1625 
 Entry action for state :C_C2 
1626 
node C_C2_en(idC_C2_1:int; 
1627 
idParallel3_C_1:int; 
1628 
c_1:int; 
1629 
y:int; 
1630 
isInner:bool) 
1631  
1632 
returns (idC_C2:int; 
1633 
idParallel3_C:int; 
1634 
c:int); 
1635  
1636  
1637 
var idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5, idC_C2_6:int; 
1638 
idParallel3_C_2, idParallel3_C_3, idParallel3_C_4:int; 
1639 
c_2, c_3, c_4, c_5, c_6:int; 
1640  
1641  
1642 
let 
1643  
1644  
1645  
1646 
 set state as active 
1647 
idParallel3_C_2 
1648 
= 1507; 
1649 

1650  
1651 

1652 
 transition trace : 
1653 
POINT__To__C2_C2a_1 
1654 
(idC_C2_2, c_2) 
1655 
= C2_C2a_en(idC_C2_1, y, c_1, false); 
1656 

1657  
1658 
(idC_C2_3, idParallel3_C_3, c_3) 
1659 
= 
1660  
1661 
if ( idC_C2_1 = 0) then 
1662  
1663 
(idC_C2_2, idParallel3_C_2, c_2) 
1664  
1665 
else(idC_C2_1, idParallel3_C_2, c_1); 
1666  
1667 

1668  
1669 
(idC_C2_4, c_4) 
1670 
= 
1671 
if ( idC_C2_1 = 1508) then 
1672 
C2_C2a_en(idC_C2_1, y, c_1, false) 
1673 
else (idC_C2_1, c_1); 
1674  
1675 

1676  
1677 
(idC_C2_5, c_5) 
1678 
= 
1679 
if ( idC_C2_1 = 1509) then 
1680 
C2_C2b_en(idC_C2_1, y, c_1, false) 
1681 
else (idC_C2_1, c_1); 
1682  
1683 

1684  
1685 
(idC_C2_6, idParallel3_C_4, c_6) 
1686 
= 
1687 
if ( idC_C2_1 = 0) then 
1688 
(idC_C2_3, idParallel3_C_3, c_3) 
1689 
else 
1690 
if ( idC_C2_1 = 1508) then 
1691 
(idC_C2_4, idParallel3_C_3, c_4) 
1692 
else 
1693 
if ( idC_C2_1 = 1509) then 
1694 
(idC_C2_5, idParallel3_C_3, c_5) 
1695 
else (idC_C2_1, idParallel3_C_2, c_1); 
1696  
1697  
1698 
(idC_C2, idParallel3_C, c) 
1699 
= (idC_C2_6, idParallel3_C_4, c_6); 
1700 

1701  
1702 
tel 
1703  
1704  
1705  
1706  
1707  
1708 
 Exit action for state :C_C2 
1709 
node C_C2_ex(idC_C2_1:int; 
1710 
idParallel3_C_1:int; 
1711 
isInner:bool) 
1712  
1713 
returns (idC_C2:int; 
1714 
idParallel3_C:int); 
1715  
1716  
1717 
var idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5:int; 
1718 
idParallel3_C_2:int; 
1719  
1720  
1721 
let 
1722  
1723  
1724  
1725 

1726 
(idC_C2_2) 
1727 
= 
1728 
if ( idC_C2_1 = 1508) then 
1729 
C2_C2a_ex(idC_C2_1, false) 
1730 
else (idC_C2_1); 
1731  
1732 

1733  
1734 
(idC_C2_3) 
1735 
= 
1736 
if ( idC_C2_1 = 1509) then 
1737 
C2_C2b_ex(idC_C2_1, false) 
1738 
else (idC_C2_1); 
1739  
1740 

1741  
1742 
(idC_C2_4) 
1743 
= 
1744 
if ( idC_C2_1 = 1508) then 
1745 
(idC_C2_2) 
1746 
else 
1747 
if ( idC_C2_1 = 1509) then 
1748 
(idC_C2_3) 
1749 
else (idC_C2_1); 
1750  
1751  
1752 
 set state as inactive 
1753 
idParallel3_C_2 
1754 
= if (not isInner) then 0 else idParallel3_C_1; 
1755  
1756 
idC_C2_5 
1757 
= 0; 
1758 

1759  
1760 
(idC_C2, idParallel3_C) 
1761 
= (idC_C2_5, idParallel3_C_1); 
1762 

1763  
1764 
tel 
1765  
1766  
1767  
1768  
1769  
1770  
1771 
 Entry action for state :C1_C1a 
1772 
node C1_C1a_en(idC_C1_1:int; 
1773 
y:int; 
1774 
c_1:int; 
1775 
isInner:bool) 
1776  
1777 
returns (idC_C1:int; 
1778 
c:int); 
1779  
1780  
1781 
var idC_C1_2:int; 
1782 
c_2:int; 
1783  
1784  
1785 
let 
1786  
1787  
1788  
1789 
 set state as active 
1790 
idC_C1_2 
1791 
= 1511; 
1792 

1793  
1794 
c_2 
1795 
= if (not isInner) then y+1 
1796 
else c_1; 
1797 

1798  
1799 
(idC_C1, c) 
1800 
= (idC_C1_2, c_2); 
1801 

1802  
1803 
tel 
1804  
1805  
1806  
1807  
1808  
1809 
 Exit action for state :C1_C1a 
1810 
node C1_C1a_ex(idC_C1_1:int; 
1811 
isInner:bool) 
1812  
1813 
returns (idC_C1:int); 
1814  
1815  
1816 
var idC_C1_2:int; 
1817  
1818  
1819 
let 
1820  
1821  
1822  
1823 
 set state as inactive 
1824 
idC_C1_2 
1825 
= if (not isInner) then 0 else idC_C1_1; 
1826  
1827  
1828 
(idC_C1) 
1829 
= (idC_C1_1); 
1830 

1831  
1832 
tel 
1833  
1834  
1835  
1836  
1837  
1838  
1839 
 Entry action for state :C1_C1b 
1840 
node C1_C1b_en(idC_C1_1:int; 
1841 
y:int; 
1842 
c_1:int; 
1843 
isInner:bool) 
1844  
1845 
returns (idC_C1:int; 
1846 
c:int); 
1847  
1848  
1849 
var idC_C1_2:int; 
1850 
c_2:int; 
1851  
1852  
1853 
let 
1854  
1855  
1856  
1857 
 set state as active 
1858 
idC_C1_2 
1859 
= 1512; 
1860 

1861  
1862 
c_2 
1863 
= if (not isInner) then y+2 
1864 
else c_1; 
1865 

1866  
1867 
(idC_C1, c) 
1868 
= (idC_C1_2, c_2); 
1869 

1870  
1871 
tel 
1872  
1873  
1874  
1875  
1876  
1877 
 Exit action for state :C1_C1b 
1878 
node C1_C1b_ex(idC_C1_1:int; 
1879 
isInner:bool) 
1880  
1881 
returns (idC_C1:int); 
1882  
1883  
1884 
var idC_C1_2:int; 
1885  
1886  
1887 
let 
1888  
1889  
1890  
1891 
 set state as inactive 
1892 
idC_C1_2 
1893 
= if (not isInner) then 0 else idC_C1_1; 
1894  
1895  
1896 
(idC_C1) 
1897 
= (idC_C1_1); 
1898 

1899  
1900 
tel 
1901  
1902  
1903  
1904  
1905  
1906  
1907 
 Entry action for state :C_C1 
1908 
node C_C1_en(idC_C1_1:int; 
1909 
idParallel3_C_1:int; 
1910 
c_1:int; 
1911 
y:int; 
1912 
isInner:bool) 
1913  
1914 
returns (idC_C1:int; 
1915 
idParallel3_C:int; 
1916 
c:int); 
1917  
1918  
1919 
var idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5, idC_C1_6:int; 
1920 
idParallel3_C_2, idParallel3_C_3, idParallel3_C_4:int; 
1921 
c_2, c_3, c_4, c_5, c_6:int; 
1922  
1923  
1924 
let 
1925  
1926  
1927  
1928 
 set state as active 
1929 
idParallel3_C_2 
1930 
= 1510; 
1931 

1932  
1933 

1934 
 transition trace : 
1935 
POINT__To__C1_C1a_1 
1936 
(idC_C1_2, c_2) 
1937 
= C1_C1a_en(idC_C1_1, y, c_1, false); 
1938 

1939  
1940 
(idC_C1_3, idParallel3_C_3, c_3) 
1941 
= 
1942  
1943 
if ( idC_C1_1 = 0) then 
1944  
1945 
(idC_C1_2, idParallel3_C_2, c_2) 
1946  
1947 
else(idC_C1_1, idParallel3_C_2, c_1); 
1948  
1949 

1950  
1951 
(idC_C1_4, c_4) 
1952 
= 
1953 
if ( idC_C1_1 = 1511) then 
1954 
C1_C1a_en(idC_C1_1, y, c_1, false) 
1955 
else (idC_C1_1, c_1); 
1956  
1957 

1958  
1959 
(idC_C1_5, c_5) 
1960 
= 
1961 
if ( idC_C1_1 = 1512) then 
1962 
C1_C1b_en(idC_C1_1, y, c_1, false) 
1963 
else (idC_C1_1, c_1); 
1964  
1965 

1966  
1967 
(idC_C1_6, idParallel3_C_4, c_6) 
1968 
= 
1969 
if ( idC_C1_1 = 0) then 
1970 
(idC_C1_3, idParallel3_C_3, c_3) 
1971 
else 
1972 
if ( idC_C1_1 = 1511) then 
1973 
(idC_C1_4, idParallel3_C_3, c_4) 
1974 
else 
1975 
if ( idC_C1_1 = 1512) then 
1976 
(idC_C1_5, idParallel3_C_3, c_5) 
1977 
else (idC_C1_1, idParallel3_C_2, c_1); 
1978  
1979  
1980 
(idC_C1, idParallel3_C, c) 
1981 
= (idC_C1_6, idParallel3_C_4, c_6); 
1982 

1983  
1984 
tel 
1985  
1986  
1987  
1988  
1989  
1990 
 Exit action for state :C_C1 
1991 
node C_C1_ex(idC_C1_1:int; 
1992 
idParallel3_C_1:int; 
1993 
isInner:bool) 
1994  
1995 
returns (idC_C1:int; 
1996 
idParallel3_C:int); 
1997  
1998  
1999 
var idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int; 
2000 
idParallel3_C_2:int; 
2001  
2002  
2003 
let 
2004  
2005  
2006  
2007 

2008 
(idC_C1_2) 
2009 
= 
2010 
if ( idC_C1_1 = 1511) then 
2011 
C1_C1a_ex(idC_C1_1, false) 
2012 
else (idC_C1_1); 
2013  
2014 

2015  
2016 
(idC_C1_3) 
2017 
= 
2018 
if ( idC_C1_1 = 1512) then 
2019 
C1_C1b_ex(idC_C1_1, false) 
2020 
else (idC_C1_1); 
2021  
2022 

2023  
2024 
(idC_C1_4) 
2025 
= 
2026 
if ( idC_C1_1 = 1511) then 
2027 
(idC_C1_2) 
2028 
else 
2029 
if ( idC_C1_1 = 1512) then 
2030 
(idC_C1_3) 
2031 
else (idC_C1_1); 
2032  
2033  
2034 
 set state as inactive 
2035 
idParallel3_C_2 
2036 
= if (not isInner) then 0 else idParallel3_C_1; 
2037  
2038 
idC_C1_5 
2039 
= 0; 
2040 

2041  
2042 
(idC_C1, idParallel3_C) 
2043 
= (idC_C1_5, idParallel3_C_1); 
2044 

2045  
2046 
tel 
2047  
2048  
2049  
2050  
2051  
2052  
2053 
 Entry action for state :Parallel3_C 
2054 
node Parallel3_C_en(idParallel3_C_1:int; 
2055 
idParallel3_Parallel3_1:int; 
2056 
c_1:int; 
2057 
idC_C1_1:int; 
2058 
y:int; 
2059 
idC_C2_1:int; 
2060 
isInner:bool) 
2061  
2062 
returns (idParallel3_C:int; 
2063 
idParallel3_Parallel3:int; 
2064 
c:int; 
2065 
idC_C1:int; 
2066 
idC_C2:int); 
2067  
2068  
2069 
var idParallel3_C_2, idParallel3_C_3, idParallel3_C_4, idParallel3_C_5, idParallel3_C_6:int; 
2070 
idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int; 
2071 
c_2, c_3, c_4, c_5, c_6:int; 
2072 
idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int; 
2073 
idC_C2_2, idC_C2_3:int; 
2074  
2075  
2076 
let 
2077  
2078  
2079  
2080 
 set state as active 
2081 
idParallel3_Parallel3_2 
2082 
= 1506; 
2083 

2084  
2085 

2086 
 transition trace : 
2087 
POINT__To__C_C1_1 
2088 
(idC_C1_2, idParallel3_C_2, c_2) 
2089 
= C_C1_en(idC_C1_1, idParallel3_C_1, c_1, y, false); 
2090 

2091  
2092 
(idParallel3_C_3, idParallel3_Parallel3_3, c_3, idC_C1_3) 
2093 
= 
2094  
2095 
if ( idParallel3_C_1 = 0) then 
2096  
2097 
(idParallel3_C_2, idParallel3_Parallel3_2, c_2, idC_C1_2) 
2098  
2099 
else(idParallel3_C_1, idParallel3_Parallel3_2, c_1, idC_C1_1); 
2100  
2101 

2102  
2103 
(idC_C2_2, idParallel3_C_4, c_4) 
2104 
= 
2105 
if ( idParallel3_C_1 = 1507) then 
2106 
C_C2_en(idC_C2_1, idParallel3_C_1, c_1, y, false) 
2107 
else (idC_C2_1, idParallel3_C_1, c_1); 
2108  
2109 

2110  
2111 
(idC_C1_4, idParallel3_C_5, c_5) 
2112 
= 
2113 
if ( idParallel3_C_1 = 1510) then 
2114 
C_C1_en(idC_C1_1, idParallel3_C_1, c_1, y, false) 
2115 
else (idC_C1_1, idParallel3_C_1, c_1); 
2116  
2117 

2118  
2119 
(idParallel3_C_6, idParallel3_Parallel3_4, c_6, idC_C1_5, idC_C2_3) 
2120 
= 
2121 
if ( idParallel3_C_1 = 0) then 
2122 
(idParallel3_C_3, idParallel3_Parallel3_3, c_3, idC_C1_3, idC_C2_1) 
2123 
else 
2124 
if ( idParallel3_C_1 = 1507) then 
2125 
(idParallel3_C_4, idParallel3_Parallel3_3, c_4, idC_C1_1, idC_C2_2) 
2126 
else 
2127 
if ( idParallel3_C_1 = 1510) then 
2128 
(idParallel3_C_5, idParallel3_Parallel3_3, c_5, idC_C1_4, idC_C2_1) 
2129 
else (idParallel3_C_1, idParallel3_Parallel3_2, c_1, idC_C1_1, idC_C2_1); 
2130  
2131  
2132 
(idParallel3_C, idParallel3_Parallel3, c, idC_C1, idC_C2) 
2133 
= (idParallel3_C_6, idParallel3_Parallel3_4, c_6, idC_C1_5, idC_C2_3); 
2134 

2135  
2136 
tel 
2137  
2138  
2139  
2140  
2141  
2142 
 Exit action for state :Parallel3_C 
2143 
node Parallel3_C_ex(idC_C2_1:int; 
2144 
idParallel3_C_1:int; 
2145 
idC_C1_1:int; 
2146 
idParallel3_Parallel3_1:int; 
2147 
isInner:bool) 
2148  
2149 
returns (idC_C2:int; 
2150 
idParallel3_C:int; 
2151 
idC_C1:int; 
2152 
idParallel3_Parallel3:int); 
2153  
2154  
2155 
var idC_C2_2, idC_C2_3:int; 
2156 
idParallel3_C_2, idParallel3_C_3, idParallel3_C_4, idParallel3_C_5:int; 
2157 
idC_C1_2, idC_C1_3:int; 
2158 
idParallel3_Parallel3_2:int; 
2159  
2160  
2161 
let 
2162  
2163  
2164  
2165 

2166 
(idC_C2_2, idParallel3_C_2) 
2167 
= 
2168 
if ( idParallel3_C_1 = 1507) then 
2169 
C_C2_ex(idC_C2_1, idParallel3_C_1, false) 
2170 
else (idC_C2_1, idParallel3_C_1); 
2171  
2172 

2173  
2174 
(idC_C1_2, idParallel3_C_3) 
2175 
= 
2176 
if ( idParallel3_C_1 = 1510) then 
2177 
C_C1_ex(idC_C1_1, idParallel3_C_1, false) 
2178 
else (idC_C1_1, idParallel3_C_1); 
2179  
2180 

2181  
2182 
(idC_C2_3, idParallel3_C_4, idC_C1_3) 
2183 
= 
2184 
if ( idParallel3_C_1 = 1507) then 
2185 
(idC_C2_2, idParallel3_C_2, idC_C1_1) 
2186 
else 
2187 
if ( idParallel3_C_1 = 1510) then 
2188 
(idC_C2_1, idParallel3_C_3, idC_C1_2) 
2189 
else (idC_C2_1, idParallel3_C_1, idC_C1_1); 
2190  
2191  
2192 
 set state as inactive 
2193 
idParallel3_Parallel3_2 
2194 
= if (not isInner) then 0 else idParallel3_Parallel3_1; 
2195  
2196 
idParallel3_C_5 
2197 
= 0; 
2198 

2199  
2200 
(idC_C2, idParallel3_C, idC_C1, idParallel3_Parallel3) 
2201 
= (idC_C2_3, idParallel3_C_5, idC_C1_3, idParallel3_Parallel3_1); 
2202 

2203  
2204 
tel 
2205  
2206  
2207  
2208  
2209  
2210  
2211 
 Entry action for state :A2_A2a 
2212 
node A2_A2a_en(idA_A2_1:int; 
2213 
x:int; 
2214 
a_1:int; 
2215 
isInner:bool) 
2216  
2217 
returns (idA_A2:int; 
2218 
a:int); 
2219  
2220  
2221 
var idA_A2_2:int; 
2222 
a_2:int; 
2223  
2224  
2225 
let 
2226  
2227  
2228  
2229 
 set state as active 
2230 
idA_A2_2 
2231 
= 1497; 
2232 

2233  
2234 
a_2 
2235 
= if (not isInner) then x+3 
2236 
else a_1; 
2237 

2238  
2239 
(idA_A2, a) 
2240 
= (idA_A2_2, a_2); 
2241 

2242  
2243 
tel 
2244  
2245  
2246  
2247  
2248  
2249 
 Exit action for state :A2_A2a 
2250 
node A2_A2a_ex(idA_A2_1:int; 
2251 
isInner:bool) 
2252  
2253 
returns (idA_A2:int); 
2254  
2255  
2256 
var idA_A2_2:int; 
2257  
2258  
2259 
let 
2260  
2261  
2262  
2263 
 set state as inactive 
2264 
idA_A2_2 
2265 
= if (not isInner) then 0 else idA_A2_1; 
2266  
2267  
2268 
(idA_A2) 
2269 
= (idA_A2_1); 
2270 

2271  
2272 
tel 
2273  
2274  
2275  
2276  
2277  
2278  
2279 
 Entry action for state :A2_A2b 
2280 
node A2_A2b_en(idA_A2_1:int; 
2281 
x:int; 
2282 
a_1:int; 
2283 
isInner:bool) 
2284  
2285 
returns (idA_A2:int; 
2286 
a:int); 
2287  
2288  
2289 
var idA_A2_2:int; 
2290 
a_2:int; 
2291  
2292  
2293 
let 
2294  
2295  
2296  
2297 
 set state as active 
2298 
idA_A2_2 
2299 
= 1498; 
2300 

2301  
2302 
a_2 
2303 
= if (not isInner) then x+4 
2304 
else a_1; 
2305 

2306  
2307 
(idA_A2, a) 
2308 
= (idA_A2_2, a_2); 
2309 

2310  
2311 
tel 
2312  
2313  
2314  
2315  
2316  
2317 
 Exit action for state :A2_A2b 
2318 
node A2_A2b_ex(idA_A2_1:int; 
2319 
isInner:bool) 
2320  
2321 
returns (idA_A2:int); 
2322  
2323  
2324 
var idA_A2_2:int; 
2325  
2326  
2327 
let 
2328  
2329  
2330  
2331 
 set state as inactive 
2332 
idA_A2_2 
2333 
= if (not isInner) then 0 else idA_A2_1; 
2334  
2335  
2336 
(idA_A2) 
2337 
= (idA_A2_1); 
2338 

2339  
2340 
tel 
2341  
2342  
2343  
2344  
2345  
2346  
2347 
 Entry action for state :A_A2 
2348 
node A_A2_en(idA_A2_1:int; 
2349 
idParallel3_A_1:int; 
2350 
a_1:int; 
2351 
x:int; 
2352 
isInner:bool) 
2353  
2354 
returns (idA_A2:int; 
2355 
idParallel3_A:int; 
2356 
a:int); 
2357  
2358  
2359 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int; 
2360 
idParallel3_A_2, idParallel3_A_3, idParallel3_A_4:int; 
2361 
a_2, a_3, a_4, a_5, a_6:int; 
2362  
2363  
2364 
let 
2365  
2366  
2367  
2368 
 set state as active 
2369 
idParallel3_A_2 
2370 
= 1496; 
2371 

2372  
2373 

2374 
 transition trace : 
2375 
POINT__To__A2_A2a_1 
2376 
(idA_A2_2, a_2) 
2377 
= A2_A2a_en(idA_A2_1, x, a_1, false); 
2378 

2379  
2380 
(idA_A2_3, idParallel3_A_3, a_3) 
2381 
= 
2382  
2383 
if ( idA_A2_1 = 0) then 
2384  
2385 
(idA_A2_2, idParallel3_A_2, a_2) 
2386  
2387 
else(idA_A2_1, idParallel3_A_2, a_1); 
2388  
2389 

2390  
2391 
(idA_A2_4, a_4) 
2392 
= 
2393 
if ( idA_A2_1 = 1497) then 
2394 
A2_A2a_en(idA_A2_1, x, a_1, false) 
2395 
else (idA_A2_1, a_1); 
2396  
2397 

2398  
2399 
(idA_A2_5, a_5) 
2400 
= 
2401 
if ( idA_A2_1 = 1498) then 
2402 
A2_A2b_en(idA_A2_1, x, a_1, false) 
2403 
else (idA_A2_1, a_1); 
2404  
2405 

2406  
2407 
(idA_A2_6, idParallel3_A_4, a_6) 
2408 
= 
2409 
if ( idA_A2_1 = 0) then 
2410 
(idA_A2_3, idParallel3_A_3, a_3) 
2411 
else 
2412 
if ( idA_A2_1 = 1497) then 
2413 
(idA_A2_4, idParallel3_A_3, a_4) 
2414 
else 
2415 
if ( idA_A2_1 = 1498) then 
2416 
(idA_A2_5, idParallel3_A_3, a_5) 
2417 
else (idA_A2_1, idParallel3_A_2, a_1); 
2418  
2419  
2420 
(idA_A2, idParallel3_A, a) 
2421 
= (idA_A2_6, idParallel3_A_4, a_6); 
2422 

2423  
2424 
tel 
2425  
2426  
2427  
2428  
2429  
2430 
 Exit action for state :A_A2 
2431 
node A_A2_ex(idA_A2_1:int; 
2432 
idParallel3_A_1:int; 
2433 
isInner:bool) 
2434  
2435 
returns (idA_A2:int; 
2436 
idParallel3_A:int); 
2437  
2438  
2439 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int; 
2440 
idParallel3_A_2:int; 
2441  
2442  
2443 
let 
2444  
2445  
2446  
2447 

2448 
(idA_A2_2) 
2449 
= 
2450 
if ( idA_A2_1 = 1497) then 
2451 
A2_A2a_ex(idA_A2_1, false) 
2452 
else (idA_A2_1); 
2453  
2454 

2455  
2456 
(idA_A2_3) 
2457 
= 
2458 
if ( idA_A2_1 = 1498) then 
2459 
A2_A2b_ex(idA_A2_1, false) 
2460 
else (idA_A2_1); 
2461  
2462 

2463  
2464 
(idA_A2_4) 
2465 
= 
2466 
if ( idA_A2_1 = 1497) then 
2467 
(idA_A2_2) 
2468 
else 
2469 
if ( idA_A2_1 = 1498) then 
2470 
(idA_A2_3) 
2471 
else (idA_A2_1); 
2472  
2473  
2474 
 set state as inactive 
2475 
idParallel3_A_2 
2476 
= if (not isInner) then 0 else idParallel3_A_1; 
2477  
2478 
idA_A2_5 
2479 
= 0; 
2480 

2481  
2482 
(idA_A2, idParallel3_A) 
2483 
= (idA_A2_5, idParallel3_A_1); 
2484 

2485  
2486 
tel 
2487  
2488  
2489  
2490  
2491  
2492  
2493 
 Entry action for state :A1_A1a 
2494 
node A1_A1a_en(idA_A1_1:int; 
2495 
x:int; 
2496 
a_1:int; 
2497 
isInner:bool) 
2498  
2499 
returns (idA_A1:int; 
2500 
a:int); 
2501  
2502  
2503 
var idA_A1_2:int; 
2504 
a_2:int; 
2505  
2506  
2507 
let 
2508  
2509  
2510  
2511 
 set state as active 
2512 
idA_A1_2 
2513 
= 1494; 
2514 

2515  
2516 
a_2 
2517 
= if (not isInner) then x+1 
2518 
else a_1; 
2519 

2520  
2521 
(idA_A1, a) 
2522 
= (idA_A1_2, a_2); 
2523 

2524  
2525 
tel 
2526  
2527  
2528  
2529  
2530  
2531 
 Exit action for state :A1_A1a 
2532 
node A1_A1a_ex(idA_A1_1:int; 
2533 
isInner:bool) 
2534  
2535 
returns (idA_A1:int); 
2536  
2537  
2538 
var idA_A1_2:int; 
2539  
2540  
2541 
let 
2542  
2543  
2544  
2545 
 set state as inactive 
2546 
idA_A1_2 
2547 
= if (not isInner) then 0 else idA_A1_1; 
2548  
2549  
2550 
(idA_A1) 
2551 
= (idA_A1_1); 
2552 

2553  
2554 
tel 
2555  
2556  
2557  
2558  
2559  
2560  
2561 
 Entry action for state :A1_A1b 
2562 
node A1_A1b_en(idA_A1_1:int; 
2563 
x:int; 
2564 
a_1:int; 
2565 
isInner:bool) 
2566  
2567 
returns (idA_A1:int; 
2568 
a:int); 
2569  
2570  
2571 
var idA_A1_2:int; 
2572 
a_2:int; 
2573  
2574  
2575 
let 
2576  
2577  
2578  
2579 
 set state as active 
2580 
idA_A1_2 
2581 
= 1495; 
2582 

2583  
2584 
a_2 
2585 
= if (not isInner) then x+2 
2586 
else a_1; 
2587 

2588  
2589 
(idA_A1, a) 
2590 
= (idA_A1_2, a_2); 
2591 

2592  
2593 
tel 
2594  
2595  
2596  
2597  
2598  
2599 
 Exit action for state :A1_A1b 
2600 
node A1_A1b_ex(idA_A1_1:int; 
2601 
isInner:bool) 
2602  
2603 
returns (idA_A1:int); 
2604  
2605  
2606 
var idA_A1_2:int; 
2607  
2608  
2609 
let 
2610  
2611  
2612  
2613 
 set state as inactive 
2614 
idA_A1_2 
2615 
= if (not isInner) then 0 else idA_A1_1; 
2616  
2617  
2618 
(idA_A1) 
2619 
= (idA_A1_1); 
2620 

2621  
2622 
tel 
2623  
2624  
2625  
2626  
2627  
2628  
2629 
 Entry action for state :A_A1 
2630 
node A_A1_en(idA_A1_1:int; 
2631 
idParallel3_A_1:int; 
2632 
a_1:int; 
2633 
x:int; 
2634 
isInner:bool) 
2635  
2636 
returns (idA_A1:int; 
2637 
idParallel3_A:int; 
2638 
a:int); 
2639  
2640  
2641 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int; 
2642 
idParallel3_A_2, idParallel3_A_3, idParallel3_A_4:int; 
2643 
a_2, a_3, a_4, a_5, a_6:int; 
2644  
2645  
2646 
let 
2647  
2648  
2649  
2650 
 set state as active 
2651 
idParallel3_A_2 
2652 
= 1493; 
2653 

2654  
2655 

2656 
 transition trace : 
2657 
POINT__To__A1_A1a_1 
2658 
(idA_A1_2, a_2) 
2659 
= A1_A1a_en(idA_A1_1, x, a_1, false); 
2660 

2661  
2662 
(idA_A1_3, idParallel3_A_3, a_3) 
2663 
= 
2664  
2665 
if ( idA_A1_1 = 0) then 
2666  
2667 
(idA_A1_2, idParallel3_A_2, a_2) 
2668  
2669 
else(idA_A1_1, idParallel3_A_2, a_1); 
2670  
2671 

2672  
2673 
(idA_A1_4, a_4) 
2674 
= 
2675 
if ( idA_A1_1 = 1494) then 
2676 
A1_A1a_en(idA_A1_1, x, a_1, false) 
2677 
else (idA_A1_1, a_1); 
2678  
2679 

2680  
2681 
(idA_A1_5, a_5) 
2682 
= 
2683 
if ( idA_A1_1 = 1495) then 
2684 
A1_A1b_en(idA_A1_1, x, a_1, false) 
2685 
else (idA_A1_1, a_1); 
2686  
2687 

2688  
2689 
(idA_A1_6, idParallel3_A_4, a_6) 
2690 
= 
2691 
if ( idA_A1_1 = 0) then 
2692 
(idA_A1_3, idParallel3_A_3, a_3) 
2693 
else 
2694 
if ( idA_A1_1 = 1494) then 
2695 
(idA_A1_4, idParallel3_A_3, a_4) 
2696 
else 
2697 
if ( idA_A1_1 = 1495) then 
2698 
(idA_A1_5, idParallel3_A_3, a_5) 
2699 
else (idA_A1_1, idParallel3_A_2, a_1); 
2700  
2701  
2702 
(idA_A1, idParallel3_A, a) 
2703 
= (idA_A1_6, idParallel3_A_4, a_6); 
2704 

2705  
2706 
tel 
2707  
2708  
2709  
2710  
2711  
2712 
 Exit action for state :A_A1 
2713 
node A_A1_ex(idA_A1_1:int; 
2714 
idParallel3_A_1:int; 
2715 
isInner:bool) 
2716  
2717 
returns (idA_A1:int; 
2718 
idParallel3_A:int); 
2719  
2720  
2721 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
2722 
idParallel3_A_2:int; 
2723  
2724  
2725 
let 
2726  
2727  
2728  
2729 

2730 
(idA_A1_2) 
2731 
= 
2732 
if ( idA_A1_1 = 1494) then 
2733 
A1_A1a_ex(idA_A1_1, false) 
2734 
else (idA_A1_1); 
2735  
2736 

2737  
2738 
(idA_A1_3) 
2739 
= 
2740 
if ( idA_A1_1 = 1495) then 
2741 
A1_A1b_ex(idA_A1_1, false) 
2742 
else (idA_A1_1); 
2743  
2744 

2745  
2746 
(idA_A1_4) 
2747 
= 
2748 
if ( idA_A1_1 = 1494) then 
2749 
(idA_A1_2) 
2750 
else 
2751 
if ( idA_A1_1 = 1495) then 
2752 
(idA_A1_3) 
2753 
else (idA_A1_1); 
2754  
2755  
2756 
 set state as inactive 
2757 
idParallel3_A_2 
2758 
= if (not isInner) then 0 else idParallel3_A_1; 
2759  
2760 
idA_A1_5 
2761 
= 0; 
2762 

2763  
2764 
(idA_A1, idParallel3_A) 
2765 
= (idA_A1_5, idParallel3_A_1); 
2766 

2767  
2768 
tel 
2769  
2770  
2771  
2772  
2773  
2774  
2775 
 Entry action for state :Parallel3_A 
2776 
node Parallel3_A_en(idParallel3_A_1:int; 
2777 
idParallel3_Parallel3_1:int; 
2778 
a_1:int; 
2779 
idA_A1_1:int; 
2780 
x:int; 
2781 
idA_A2_1:int; 
2782 
isInner:bool) 
2783  
2784 
returns (idParallel3_A:int; 
2785 
idParallel3_Parallel3:int; 
2786 
a:int; 
2787 
idA_A1:int; 
2788 
idA_A2:int); 
2789  
2790  
2791 
var idParallel3_A_2, idParallel3_A_3, idParallel3_A_4, idParallel3_A_5, idParallel3_A_6:int; 
2792 
idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int; 
2793 
a_2, a_3, a_4, a_5, a_6:int; 
2794 
idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
2795 
idA_A2_2, idA_A2_3:int; 
2796  
2797  
2798 
let 
2799  
2800  
2801  
2802 
 set state as active 
2803 
idParallel3_Parallel3_2 
2804 
= 1492; 
2805 

2806  
2807 

2808 
 transition trace : 
2809 
POINT__To__A_A1_1 
2810 
(idA_A1_2, idParallel3_A_2, a_2) 
2811 
= A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false); 
2812 

2813  
2814 
(idParallel3_A_3, idParallel3_Parallel3_3, a_3, idA_A1_3) 
2815 
= 
2816  
2817 
if ( idParallel3_A_1 = 0) then 
2818  
2819 
(idParallel3_A_2, idParallel3_Parallel3_2, a_2, idA_A1_2) 
2820  
2821 
else(idParallel3_A_1, idParallel3_Parallel3_2, a_1, idA_A1_1); 
2822  
2823 

2824  
2825 
(idA_A1_4, idParallel3_A_4, a_4) 
2826 
= 
2827 
if ( idParallel3_A_1 = 1493) then 
2828 
A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false) 
2829 
else (idA_A1_1, idParallel3_A_1, a_1); 
2830  
2831 

2832  
2833 
(idA_A2_2, idParallel3_A_5, a_5) 
2834 
= 
2835 
if ( idParallel3_A_1 = 1496) then 
2836 
A_A2_en(idA_A2_1, idParallel3_A_1, a_1, x, false) 
2837 
else (idA_A2_1, idParallel3_A_1, a_1); 
2838  
2839 

2840  
2841 
(idParallel3_A_6, idParallel3_Parallel3_4, a_6, idA_A1_5, idA_A2_3) 
2842 
= 
2843 
if ( idParallel3_A_1 = 0) then 
2844 
(idParallel3_A_3, idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_1) 
2845 
else 
2846 
if ( idParallel3_A_1 = 1493) then 
2847 
(idParallel3_A_4, idParallel3_Parallel3_3, a_4, idA_A1_4, idA_A2_1) 
2848 
else 
2849 
if ( idParallel3_A_1 = 1496) then 
2850 
(idParallel3_A_5, idParallel3_Parallel3_3, a_5, idA_A1_1, idA_A2_2) 
2851 
else (idParallel3_A_1, idParallel3_Parallel3_2, a_1, idA_A1_1, idA_A2_1); 
2852  
2853  
2854 
(idParallel3_A, idParallel3_Parallel3, a, idA_A1, idA_A2) 
2855 
= (idParallel3_A_6, idParallel3_Parallel3_4, a_6, idA_A1_5, idA_A2_3); 
2856 

2857  
2858 
tel 
2859  
2860  
2861  
2862  
2863  
2864 
 Exit action for state :Parallel3_A 
2865 
node Parallel3_A_ex(idA_A1_1:int; 
2866 
idParallel3_A_1:int; 
2867 
idA_A2_1:int; 
2868 
idParallel3_Parallel3_1:int; 
2869 
isInner:bool) 
2870  
2871 
returns (idA_A1:int; 
2872 
idParallel3_A:int; 
2873 
idA_A2:int; 
2874 
idParallel3_Parallel3:int); 
2875  
2876  
2877 
var idA_A1_2, idA_A1_3:int; 
2878 
idParallel3_A_2, idParallel3_A_3, idParallel3_A_4, idParallel3_A_5:int; 
2879 
idA_A2_2, idA_A2_3:int; 
2880 
idParallel3_Parallel3_2:int; 
2881  
2882  
2883 
let 
2884  
2885  
2886  
2887 

2888 
(idA_A1_2, idParallel3_A_2) 
2889 
= 
2890 
if ( idParallel3_A_1 = 1493) then 
2891 
A_A1_ex(idA_A1_1, idParallel3_A_1, false) 
2892 
else (idA_A1_1, idParallel3_A_1); 
2893  
2894 

2895  
2896 
(idA_A2_2, idParallel3_A_3) 
2897 
= 
2898 
if ( idParallel3_A_1 = 1496) then 
2899 
A_A2_ex(idA_A2_1, idParallel3_A_1, false) 
2900 
else (idA_A2_1, idParallel3_A_1); 
2901  
2902 

2903  
2904 
(idA_A1_3, idParallel3_A_4, idA_A2_3) 
2905 
= 
2906 
if ( idParallel3_A_1 = 1493) then 
2907 
(idA_A1_2, idParallel3_A_2, idA_A2_1) 
2908 
else 
2909 
if ( idParallel3_A_1 = 1496) then 
2910 
(idA_A1_1, idParallel3_A_3, idA_A2_2) 
2911 
else (idA_A1_1, idParallel3_A_1, idA_A2_1); 
2912  
2913  
2914 
 set state as inactive 
2915 
idParallel3_Parallel3_2 
2916 
= if (not isInner) then 0 else idParallel3_Parallel3_1; 
2917  
2918 
idParallel3_A_5 
2919 
= 0; 
2920 

2921  
2922 
(idA_A1, idParallel3_A, idA_A2, idParallel3_Parallel3) 
2923 
= (idA_A1_3, idParallel3_A_5, idA_A2_3, idParallel3_Parallel3_1); 
2924 

2925  
2926 
tel 
2927  
2928  
2929 
***************************************************State :B_B2 Automaton*************************************************** 
2930  
2931 
node B_B2_node(idB_B2_1:int; 
2932 
b_1:int; 
2933 
x:int; 
2934 
S:bool; 
2935 
R:bool) 
2936  
2937 
returns (idB_B2:int; 
2938 
b:int); 
2939  
2940  
2941 
let 
2942  
2943 
automaton b_b2 
2944  
2945 
state POINTB_B2: 
2946 
unless (idB_B2_1=0) restart POINT__TO__B2_B2A_1 
2947  
2948  
2949  
2950 
unless (idB_B2_1=1501) and S restart B2_B2A__TO__B2_B2B_1 
2951  
2952  
2953  
2954 
unless (idB_B2_1=1502) and R restart B2_B2B__TO__B2_B2A_1 
2955  
2956  
2957  
2958 
unless (idB_B2_1=1501) restart B2_B2A_IDL 
2959  
2960 
unless (idB_B2_1=1502) restart B2_B2B_IDL 
2961  
2962 
let 
2963  
2964 
(idB_B2, b) 
2965 
= (idB_B2_1, b_1); 
2966 

2967  
2968 
tel 
2969  
2970  
2971  
2972 
state POINT__TO__B2_B2A_1: 
2973  
2974 
var idB_B2_2:int; 
2975 
b_2:int; 
2976 
let 
2977  
2978 
 transition trace : 
2979 
POINT__To__B2_B2a_1 
2980 
(idB_B2_2, b_2) 
2981 
= B2_B2a_en(idB_B2_1, x, b_1, false); 
2982 

2983  
2984 
(idB_B2, b) 
2985 
= (idB_B2_2, b_2); 
2986  
2987  
2988 
tel 
2989  
2990 
until true restart POINTB_B2 
2991  
2992  
2993  
2994 
state B2_B2A__TO__B2_B2B_1: 
2995  
2996 
var idB_B2_2, idB_B2_3:int; 
2997 
b_2:int; 
2998 
let 
2999  
3000 
 transition trace : 
3001 
B2_B2a__To__B2_B2b_1 
3002 
(idB_B2_2) 
3003 
= B2_B2a_ex(idB_B2_1, false); 
3004 

3005  
3006 
(idB_B2_3, b_2) 
3007 
= B2_B2b_en(idB_B2_2, x, b_1, false); 
3008 

3009  
3010 
(idB_B2, b) 
3011 
= (idB_B2_3, b_2); 
3012  
3013  
3014 
tel 
3015  
3016 
until true restart POINTB_B2 
3017  
3018  
3019  
3020 
state B2_B2B__TO__B2_B2A_1: 
3021  
3022 
var idB_B2_2, idB_B2_3:int; 
3023 
b_2:int; 
3024 
let 
3025  
3026 
 transition trace : 
3027 
B2_B2b__To__B2_B2a_1 
3028 
(idB_B2_2) 
3029 
= B2_B2b_ex(idB_B2_1, false); 
3030 

3031  
3032 
(idB_B2_3, b_2) 
3033 
= B2_B2a_en(idB_B2_2, x, b_1, false); 
3034 

3035  
3036 
(idB_B2, b) 
3037 
= (idB_B2_3, b_2); 
3038  
3039  
3040 
tel 
3041  
3042 
until true restart POINTB_B2 
3043  
3044  
3045  
3046 
state B2_B2A_IDL: 
3047  
3048 
let 
3049  
3050 

3051  
3052 
(idB_B2, b) 
3053 
= (idB_B2_1, b_1); 
3054 

3055  
3056 
tel 
3057  
3058 
until true restart POINTB_B2 
3059  
3060  
3061  
3062 
state B2_B2B_IDL: 
3063  
3064 
let 
3065  
3066 

3067  
3068 
(idB_B2, b) 
3069 
= (idB_B2_1, b_1); 
3070 

3071  
3072 
tel 
3073  
3074 
until true restart POINTB_B2 
3075  
3076  
3077  
3078 
tel 
3079  
3080  
3081 
***************************************************State :B_B1 Automaton*************************************************** 
3082  
3083 
node B_B1_node(idB_B1_1:int; 
3084 
b_1:int; 
3085 
x:int; 
3086 
S:bool; 
3087 
R:bool) 
3088  
3089 
returns (idB_B1:int; 
3090 
b:int); 
3091  
3092  
3093 
let 
3094  
3095 
automaton b_b1 
3096  
3097 
state POINTB_B1: 
3098 
unless (idB_B1_1=0) restart POINT__TO__B1_B1A_1 
3099  
3100  
3101  
3102 
unless (idB_B1_1=1504) and S restart B1_B1A__TO__B1_B1B_1 
3103  
3104  
3105  
3106 
unless (idB_B1_1=1505) and R restart B1_B1B__TO__B1_B1A_1 
3107  
3108  
3109  
3110 
unless (idB_B1_1=1504) restart B1_B1A_IDL 
3111  
3112 
unless (idB_B1_1=1505) restart B1_B1B_IDL 
3113  
3114 
let 
3115  
3116 
(idB_B1, b) 
3117 
= (idB_B1_1, b_1); 
3118 

3119  
3120 
tel 
3121  
3122  
3123  
3124 
state POINT__TO__B1_B1A_1: 
3125  
3126 
var idB_B1_2:int; 
3127 
b_2:int; 
3128 
let 
3129  
3130 
 transition trace : 
3131 
POINT__To__B1_B1a_1 
3132 
(idB_B1_2, b_2) 
3133 
= B1_B1a_en(idB_B1_1, x, b_1, false); 
3134 

3135  
3136 
(idB_B1, b) 
3137 
= (idB_B1_2, b_2); 
3138  
3139  
3140 
tel 
3141  
3142 
until true restart POINTB_B1 
3143  
3144  
3145  
3146 
state B1_B1A__TO__B1_B1B_1: 
3147  
3148 
var idB_B1_2, idB_B1_3:int; 
3149 
b_2:int; 
3150 
let 
3151  
3152 
 transition trace : 
3153 
B1_B1a__To__B1_B1b_1 
3154 
(idB_B1_2) 
3155 
= B1_B1a_ex(idB_B1_1, false); 
3156 

3157  
3158 
(idB_B1_3, b_2) 
3159 
= B1_B1b_en(idB_B1_2, x, b_1, false); 
3160 

3161  
3162 
(idB_B1, b) 
3163 
= (idB_B1_3, b_2); 
3164  
3165  
3166 
tel 
3167  
3168 
until true restart POINTB_B1 
3169  
3170  
3171  
3172 
state B1_B1B__TO__B1_B1A_1: 
3173  
3174 
var idB_B1_2, idB_B1_3:int; 
3175 
b_2:int; 
3176 
let 
3177  
3178 
 transition trace : 
3179 
B1_B1b__To__B1_B1a_1 
3180 
(idB_B1_2) 
3181 
= B1_B1b_ex(idB_B1_1, false); 
3182 

3183  
3184 
(idB_B1_3, b_2) 
3185 
= B1_B1a_en(idB_B1_2, x, b_1, false); 
3186 

3187  
3188 
(idB_B1, b) 
3189 
= (idB_B1_3, b_2); 
3190  
3191  
3192 
tel 
3193  
3194 
until true restart POINTB_B1 
3195  
3196  
3197  
3198 
state B1_B1A_IDL: 
3199  
3200 
let 
3201  
3202 

3203  
3204 
(idB_B1, b) 
3205 
= (idB_B1_1, b_1); 
3206 

3207  
3208 
tel 
3209  
3210 
until true restart POINTB_B1 
3211  
3212  
3213  
3214 
state B1_B1B_IDL: 
3215  
3216 
let 
3217  
3218 

3219  
3220 
(idB_B1, b) 
3221 
= (idB_B1_1, b_1); 
3222 

3223  
3224 
tel 
3225  
3226 
until true restart POINTB_B1 
3227  
3228  
3229  
3230 
tel 
3231  
3232  
3233 
***************************************************State :Parallel3_B Automaton*************************************************** 
3234  
3235 
node Parallel3_B_node(idParallel3_B_1:int; 
3236 
b_1:int; 
3237 
idB_B1_1:int; 
3238 
x:int; 
3239 
T:bool; 
3240 
idB_B2_1:int; 
3241 
R:bool; 
3242 
S:bool) 
3243  
3244 
returns (idParallel3_B:int; 
3245 
b:int; 
3246 
idB_B1:int; 
3247 
idB_B2:int); 
3248  
3249  
3250 
let 
3251  
3252 
automaton parallel3_b 
3253  
3254 
state POINTParallel3_B: 
3255 
unless (idParallel3_B_1=0) restart POINT__TO__B_B1_1 
3256  
3257  
3258  
3259 
unless (idParallel3_B_1=1500) and T restart B_B2__TO__B_B1_1 
3260  
3261  
3262  
3263 
unless (idParallel3_B_1=1503) and T restart B_B1__TO__B_B2_1 
3264  
3265  
3266  
3267 
unless (idParallel3_B_1=1500) restart B_B2_IDL 
3268  
3269 
unless (idParallel3_B_1=1503) restart B_B1_IDL 
3270  
3271 
let 
3272  
3273 
(idParallel3_B, b, idB_B1, idB_B2) 
3274 
= (idParallel3_B_1, b_1, idB_B1_1, idB_B2_1); 
3275 

3276  
3277 
tel 
3278  
3279  
3280  
3281 
state POINT__TO__B_B1_1: 
3282  
3283 
var idParallel3_B_2:int; 
3284 
b_2:int; 
3285 
idB_B1_2:int; 
3286 
let 
3287  
3288 
 transition trace : 
3289 
POINT__To__B_B1_1 
3290 
(idB_B1_2, idParallel3_B_2, b_2) 
3291 
= B_B1_en(idB_B1_1, idParallel3_B_1, b_1, x, false); 
3292 

3293  
3294 
(idParallel3_B, b, idB_B1) 
3295 
= (idParallel3_B_2, b_2, idB_B1_2); 
3296  
3297 
add unused variables 
3298 
(idB_B2) 
3299 
= (idB_B2_1); 
3300 

3301  
3302 
tel 
3303  
3304 
until true restart POINTParallel3_B 
3305  
3306  
3307  
3308 
state B_B2__TO__B_B1_1: 
3309  
3310 
var idParallel3_B_2, idParallel3_B_3:int; 
3311 
b_2:int; 
3312 
idB_B1_2:int; 
3313 
idB_B2_2:int; 
3314 
let 
3315  
3316 
 transition trace : 
3317 
B_B2__To__B_B1_1 
3318 
(idB_B2_2, idParallel3_B_2) 
3319 
= B_B2_ex(idB_B2_1, idParallel3_B_1, false); 
3320 

3321  
3322 
(idB_B1_2, idParallel3_B_3, b_2) 
3323 
= B_B1_en(idB_B1_1, idParallel3_B_2, b_1, x, false); 
3324 

3325  
3326 
(idParallel3_B, b, idB_B1, idB_B2) 
3327 
= (idParallel3_B_3, b_2, idB_B1_2, idB_B2_2); 
3328  
3329  
3330 
tel 
3331  
3332 
until true restart POINTParallel3_B 
3333  
3334  
3335  
3336 
state B_B1__TO__B_B2_1: 
3337  
3338 
var idParallel3_B_2, idParallel3_B_3:int; 
3339 
b_2:int; 
3340 
idB_B1_2:int; 
3341 
idB_B2_2:int; 
3342 
let 
3343  
3344 
 transition trace : 
3345 
B_B1__To__B_B2_1 
3346 
(idB_B1_2, idParallel3_B_2) 
3347 
= B_B1_ex(idB_B1_1, idParallel3_B_1, false); 
3348 

3349  
3350 
(idB_B2_2, idParallel3_B_3, b_2) 
3351 
= B_B2_en(idB_B2_1, idParallel3_B_2, b_1, x, false); 
3352 

3353  
3354 
(idParallel3_B, b, idB_B1, idB_B2) 
3355 
= (idParallel3_B_3, b_2, idB_B1_2, idB_B2_2); 
3356  
3357  
3358 
tel 
3359  
3360 
until true restart POINTParallel3_B 
3361  
3362  
3363  
3364 
state B_B2_IDL: 
3365  
3366 
var b_2:int; 
3367 
idB_B2_2:int; 
3368 
let 
3369  
3370 

3371 
(idB_B2_2, b_2) 
3372 
= B_B2_node(idB_B2_1, b_1, x, S, R); 
3373  
3374 

3375  
3376  
3377 
(idParallel3_B, b, idB_B1, idB_B2) 
3378 
= (idParallel3_B_1, b_2, idB_B1_1, idB_B2_2); 
3379 

3380  
3381 
tel 
3382  
3383 
until true restart POINTParallel3_B 
3384  
3385  
3386  
3387 
state B_B1_IDL: 
3388  
3389 
var b_2:int; 
3390 
idB_B1_2:int; 
3391 
let 
3392  
3393 

3394 
(idB_B1_2, b_2) 
3395 
= B_B1_node(idB_B1_1, b_1, x, S, R); 
3396  
3397 

3398  
3399  
3400 
(idParallel3_B, b, idB_B1, idB_B2) 
3401 
= (idParallel3_B_1, b_2, idB_B1_2, idB_B2_1); 
3402 

3403  
3404 
tel 
3405  
3406 
until true restart POINTParallel3_B 
3407  
3408  
3409  
3410 
tel 
3411  
3412  
3413 
***************************************************State :D_D2 Automaton*************************************************** 
3414  
3415 
node D_D2_node(idD_D2_1:int; 
3416 
dd_1:int; 
3417 
y:int; 
3418 
S:bool; 
3419 
R:bool) 
3420  
3421 
returns (idD_D2:int; 
3422 
dd:int); 
3423  
3424  
3425 
let 
3426  
3427 
automaton d_d2 
3428  
3429 
state POINTD_D2: 
3430 
unless (idD_D2_1=0) restart POINT__TO__D2_D2A_1 
3431  
3432  
3433  
3434 
unless (idD_D2_1=1515) and S restart D2_D2A__TO__D2_D2B_1 
3435  
3436  
3437  
3438 
unless (idD_D2_1=1516) and R restart D2_D2B__TO__D2_D2A_1 
3439  
3440  
3441  
3442 
unless (idD_D2_1=1515) restart D2_D2A_IDL 
3443  
3444 
unless (idD_D2_1=1516) restart D2_D2B_IDL 
3445  
3446 
let 
3447  
3448 
(idD_D2, dd) 
3449 
= (idD_D2_1, dd_1); 
3450 

3451  
3452 
tel 
3453  
3454  
3455  
3456 
state POINT__TO__D2_D2A_1: 
3457  
3458 
var idD_D2_2:int; 
3459 
dd_2:int; 
3460 
let 
3461  
3462 
 transition trace : 
3463 
POINT__To__D2_D2a_1 
3464 
(idD_D2_2, dd_2) 
3465 
= D2_D2a_en(idD_D2_1, y, dd_1, false); 
3466 

3467  
3468 
(idD_D2, dd) 
3469 
= (idD_D2_2, dd_2); 
3470  
3471  
3472 
tel 
3473  
3474 
until true restart POINTD_D2 
3475  
3476  
3477  
3478 
state D2_D2A__TO__D2_D2B_1: 
3479  
3480 
var idD_D2_2, idD_D2_3:int; 
3481 
dd_2:int; 
3482 
let 
3483  
3484 
 transition trace : 
3485 
D2_D2a__To__D2_D2b_1 
3486 
(idD_D2_2) 
3487 
= D2_D2a_ex(idD_D2_1, false); 
3488 

3489  
3490 
(idD_D2_3, dd_2) 
3491 
= D2_D2b_en(idD_D2_2, y, dd_1, false); 
3492 

3493  
3494 
(idD_D2, dd) 
3495 
= (idD_D2_3, dd_2); 
3496  
3497  
3498 
tel 
3499  
3500 
until true restart POINTD_D2 
3501  
3502  
3503  
3504 
state D2_D2B__TO__D2_D2A_1: 
3505  
3506 
var idD_D2_2, idD_D2_3:int; 
3507 
dd_2:int; 
3508 
let 
3509  
3510 
 transition trace : 
3511 
D2_D2b__To__D2_D2a_1 
3512 
(idD_D2_2) 
3513 
= D2_D2b_ex(idD_D2_1, false); 
3514 

3515  
3516 
(idD_D2_3, dd_2) 
3517 
= D2_D2a_en(idD_D2_2, y, dd_1, false); 
3518 

3519  
3520 
(idD_D2, dd) 
3521 
= (idD_D2_3, dd_2); 
3522  
3523  
3524 
tel 
3525  
3526 
until true restart POINTD_D2 
3527  
3528  
3529  
3530 
state D2_D2A_IDL: 
3531  
3532 
let 
3533  
3534 

3535  
3536 
(idD_D2, dd) 
3537 
= (idD_D2_1, dd_1); 
3538 

3539  
3540 
tel 
3541  
3542 
until true restart POINTD_D2 
3543  
3544  
3545  
3546 
state D2_D2B_IDL: 
3547  
3548 
let 
3549  
3550 

3551  
3552 
(idD_D2, dd) 
3553 
= (idD_D2_1, dd_1); 
3554 

3555  
3556 
tel 
3557  
3558 
until true restart POINTD_D2 
3559  
3560  
3561  
3562 
tel 
3563  
3564  
3565 
***************************************************State :D_D1 Automaton*************************************************** 
3566  
3567 
node D_D1_node(idD_D1_1:int; 
3568 
dd_1:int; 
3569 
y:int; 
3570 
S:bool; 
3571 
R:bool) 
3572  
3573 
returns (idD_D1:int; 
3574 
dd:int); 
3575  
3576  
3577 
let 
3578  
3579 
automaton d_d1 
3580  
3581 
state POINTD_D1: 
3582 
unless (idD_D1_1=0) restart POINT__TO__D1_D1A_1 
3583  
3584  
3585  
3586 
unless (idD_D1_1=1518) and S restart D1_D1A__TO__D1_D1B_1 
3587  
3588  
3589  
3590 
unless (idD_D1_1=1519) and R restart D1_D1B__TO__D1_D1A_1 
3591  
3592  
3593  
3594 
unless (idD_D1_1=1518) restart D1_D1A_IDL 
3595  
3596 
unless (idD_D1_1=1519) restart D1_D1B_IDL 
3597  
3598 
let 
3599  
3600 
(idD_D1, dd) 
3601 
= (idD_D1_1, dd_1); 
3602 

3603  
3604 
tel 
3605  
3606  
3607  
3608 
state POINT__TO__D1_D1A_1: 
3609  
3610 
var idD_D1_2:int; 
3611 
dd_2:int; 
3612 
let 
3613  
3614 
 transition trace : 
3615 
POINT__To__D1_D1a_1 
3616 
(idD_D1_2, dd_2) 
3617 
= D1_D1a_en(idD_D1_1, y, dd_1, false); 
3618 

3619  
3620 
(idD_D1, dd) 
3621 
= (idD_D1_2, dd_2); 
3622  
3623  
3624 
tel 
3625  
3626 
until true restart POINTD_D1 
3627  
3628  
3629  
3630 
state D1_D1A__TO__D1_D1B_1: 
3631  
3632 
var idD_D1_2, idD_D1_3:int; 
3633 
dd_2:int; 
3634 
let 
3635  
3636 
 transition trace : 
3637 
D1_D1a__To__D1_D1b_1 
3638 
(idD_D1_2) 
3639 
= D1_D1a_ex(idD_D1_1, false); 
3640 

3641  
3642 
(idD_D1_3, dd_2) 
3643 
= D1_D1b_en(idD_D1_2, y, dd_1, false); 
3644 

3645  
3646 
(idD_D1, dd) 
3647 
= (idD_D1_3, dd_2); 
3648  
3649  
3650 
tel 
3651  
3652 
until true restart POINTD_D1 
3653  
3654  
3655  
3656 
state D1_D1B__TO__D1_D1A_1: 
3657  
3658 
var idD_D1_2, idD_D1_3:int; 
3659 
dd_2:int; 
3660 
let 
3661  
3662 
 transition trace : 
3663 
D1_D1b__To__D1_D1a_1 
3664 
(idD_D1_2) 
3665 
= D1_D1b_ex(idD_D1_1, false); 
3666 

3667  
3668 
(idD_D1_3, dd_2) 
3669 
= D1_D1a_en(idD_D1_2, y, dd_1, false); 
3670 

3671  
3672 
(idD_D1, dd) 
3673 
= (idD_D1_3, dd_2); 
3674  
3675  
3676 
tel 
3677  
3678 
until true restart POINTD_D1 
3679  
3680  
3681  
3682 
state D1_D1A_IDL: 
3683  
3684 
let 
3685  
3686 

3687  
3688 
(idD_D1, dd) 
3689 
= (idD_D1_1, dd_1); 
3690 

3691  
3692 
tel 
3693  
3694 
until true restart POINTD_D1 
3695  
3696  
3697  
3698 
state D1_D1B_IDL: 
3699  
3700 
let 
3701  
3702 

3703  
3704 
(idD_D1, dd) 
3705 
= (idD_D1_1, dd_1); 
3706 

3707  
3708 
tel 
3709  
3710 
until true restart POINTD_D1 
3711  
3712  
3713  
3714 
tel 
3715  
3716  
3717 
***************************************************State :Parallel3_D Automaton*************************************************** 
3718  
3719 
node Parallel3_D_node(idParallel3_D_1:int; 
3720 
dd_1:int; 
3721 
idD_D1_1:int; 
3722 
y:int; 
3723 
T:bool; 
3724 
idD_D2_1:int; 
3725 
R:bool; 
3726 
S:bool) 
3727  
3728 
returns (idParallel3_D:int; 
3729 
dd:int; 
3730 
idD_D1:int; 
3731 
idD_D2:int); 
3732  
3733  
3734 
let 
3735  
3736 
automaton parallel3_d 
3737  
3738 
state POINTParallel3_D: 
3739 
unless (idParallel3_D_1=0) restart POINT__TO__D_D1_1 
3740  
3741  
3742  
3743 
unless (idParallel3_D_1=1514) and T restart D_D2__TO__D_D1_1 
3744  
3745  
3746  
3747 
unless (idParallel3_D_1=1517) and T restart D_D1__TO__D_D2_1 
3748  
3749  
3750  
3751 
unless (idParallel3_D_1=1514) restart D_D2_IDL 
3752  
3753 
unless (idParallel3_D_1=1517) restart D_D1_IDL 
3754  
3755 
let 
3756  
3757 
(idParallel3_D, dd, idD_D1, idD_D2) 
3758 
= (idParallel3_D_1, dd_1, idD_D1_1, idD_D2_1); 
3759 

3760  
3761 
tel 
3762  
3763  
3764  
3765 
state POINT__TO__D_D1_1: 
3766  
3767 
var idParallel3_D_2:int; 
3768 
dd_2:int; 
3769 
idD_D1_2:int; 
3770 
let 
3771  
3772 
 transition trace : 
3773 
POINT__To__D_D1_1 
3774 
(idD_D1_2, idParallel3_D_2, dd_2) 
3775 
= D_D1_en(idD_D1_1, idParallel3_D_1, dd_1, y, false); 
3776 

3777  
3778 
(idParallel3_D, dd, idD_D1) 
3779 
= (idParallel3_D_2, dd_2, idD_D1_2); 
3780  
3781 
add unused variables 
3782 
(idD_D2) 
3783 
= (idD_D2_1); 
3784 

3785  
3786 
tel 
3787  
3788 
until true restart POINTParallel3_D 
3789  
3790  
3791  
3792 
state D_D2__TO__D_D1_1: 
3793  
3794 
var idParallel3_D_2, idParallel3_D_3:int; 
3795 
dd_2:int; 
3796 
idD_D1_2:int; 
3797 
idD_D2_2:int; 
3798 
let 
3799  
3800 
 transition trace : 
3801 
D_D2__To__D_D1_1 
3802 
(idD_D2_2, idParallel3_D_2) 
3803 
= D_D2_ex(idD_D2_1, idParallel3_D_1, false); 
3804 

3805  
3806 
(idD_D1_2, idParallel3_D_3, dd_2) 
3807 
= D_D1_en(idD_D1_1, idParallel3_D_2, dd_1, y, false); 
3808 

3809  
3810 
(idParallel3_D, dd, idD_D1, idD_D2) 
3811 
= (idParallel3_D_3, dd_2, idD_D1_2, idD_D2_2); 
3812  
3813  
3814 
tel 
3815  
3816 
until true restart POINTParallel3_D 
3817  
3818  
3819  
3820 
state D_D1__TO__D_D2_1: 
3821  
3822 
var idParallel3_D_2, idParallel3_D_3:int; 
3823 
dd_2:int; 
3824 
idD_D1_2:int; 
3825 
idD_D2_2:int; 
3826 
let 
3827  
3828 
 transition trace : 
3829 
D_D1__To__D_D2_1 
3830 
(idD_D1_2, idParallel3_D_2) 
3831 
= D_D1_ex(idD_D1_1, idParallel3_D_1, false); 
3832 

3833  
3834 
(idD_D2_2, idParallel3_D_3, dd_2) 
3835 
= D_D2_en(idD_D2_1, idParallel3_D_2, dd_1, y, false); 
3836 

3837  
3838 
(idParallel3_D, dd, idD_D1, idD_D2) 
3839 
= (idParallel3_D_3, dd_2, idD_D1_2, idD_D2_2); 
3840  
3841  
3842 
tel 
3843  
3844 
until true restart POINTParallel3_D 
3845  
3846  
3847  
3848 
state D_D2_IDL: 
3849  
3850 
var dd_2:int; 
3851 
idD_D2_2:int; 
3852 
let 
3853  
3854 

3855 
(idD_D2_2, dd_2) 
3856 
= D_D2_node(idD_D2_1, dd_1, y, S, R); 
3857  
3858 

3859  
3860  
3861 
(idParallel3_D, dd, idD_D1, idD_D2) 
3862 
= (idParallel3_D_1, dd_2, idD_D1_1, idD_D2_2); 
3863 

3864  
3865 
tel 
3866  
3867 
until true restart POINTParallel3_D 
3868  
3869  
3870  
3871 
state D_D1_IDL: 
3872  
3873 
var dd_2:int; 
3874 
idD_D1_2:int; 
3875 
let 
3876  
3877 

3878 
(idD_D1_2, dd_2) 
3879 
= D_D1_node(idD_D1_1, dd_1, y, S, R); 
3880  
3881 

3882  
3883  
3884 
(idParallel3_D, dd, idD_D1, idD_D2) 
3885 
= (idParallel3_D_1, dd_2, idD_D1_2, idD_D2_1); 
3886 

3887  
3888 
tel 
3889  
3890 
until true restart POINTParallel3_D 
3891  
3892  
3893  
3894 
tel 
3895  
3896  
3897 
***************************************************State :C_C2 Automaton*************************************************** 
3898  
3899 
node C_C2_node(idC_C2_1:int; 
3900 
c_1:int; 
3901 
y:int; 
3902 
S:bool; 
3903 
R:bool) 
3904  
3905 
returns (idC_C2:int; 
3906 
c:int); 
3907  
3908  
3909 
let 
3910  
3911 
automaton c_c2 
3912  
3913 
state POINTC_C2: 
3914 
unless (idC_C2_1=0) restart POINT__TO__C2_C2A_1 
3915  
3916  
3917  
3918 
unless (idC_C2_1=1508) and S restart C2_C2A__TO__C2_C2B_1 
3919  
3920  
3921  
3922 
unless (idC_C2_1=1509) and R restart C2_C2B__TO__C2_C2A_1 
3923  
3924  
3925  
3926 
unless (idC_C2_1=1508) restart C2_C2A_IDL 
3927  
3928 
unless (idC_C2_1=1509) restart C2_C2B_IDL 
3929  
3930 
let 
3931  
3932 
(idC_C2, c) 
3933 
= (idC_C2_1, c_1); 
3934 

3935  
3936 
tel 
3937  
3938  
3939  
3940 
state POINT__TO__C2_C2A_1: 
3941  
3942 
var idC_C2_2:int; 
3943 
c_2:int; 
3944 
let 
3945  
3946 
 transition trace : 
3947 
POINT__To__C2_C2a_1 
3948 
(idC_C2_2, c_2) 
3949 
= C2_C2a_en(idC_C2_1, y, c_1, false); 
3950 

3951  
3952 
(idC_C2, c) 
3953 
= (idC_C2_2, c_2); 
3954  
3955  
3956 
tel 
3957  
3958 
until true restart POINTC_C2 
3959  
3960  
3961  
3962 
state C2_C2A__TO__C2_C2B_1: 
3963  
3964 
var idC_C2_2, idC_C2_3:int; 
3965 
c_2:int; 
3966 
let 
3967  
3968 
 transition trace : 
3969 
C2_C2a__To__C2_C2b_1 
3970 
(idC_C2_2) 
3971 
= C2_C2a_ex(idC_C2_1, false); 
3972 

3973  
3974 
(idC_C2_3, c_2) 
3975 
= C2_C2b_en(idC_C2_2, y, c_1, false); 
3976 

3977  
3978 
(idC_C2, c) 
3979 
= (idC_C2_3, c_2); 
3980  
3981  
3982 
tel 
3983  
3984 
until true restart POINTC_C2 
3985  
3986  
3987  
3988 
state C2_C2B__TO__C2_C2A_1: 
3989  
3990 
var idC_C2_2, idC_C2_3:int; 
3991 
c_2:int; 
3992 
let 
3993  
3994 
 transition trace : 
3995 
C2_C2b__To__C2_C2a_1 
3996 
(idC_C2_2) 
3997 
= C2_C2b_ex(idC_C2_1, false); 
3998 

3999  
4000 
(idC_C2_3, c_2) 
4001 
= C2_C2a_en(idC_C2_2, y, c_1, false); 
4002 

4003  
4004 
(idC_C2, c) 
4005 
= (idC_C2_3, c_2); 
4006  
4007  
4008 
tel 
4009  
4010 
until true restart POINTC_C2 
4011  
4012  
4013  
4014 
state C2_C2A_IDL: 
4015  
4016 
let 
4017  
4018 

4019  
4020 
(idC_C2, c) 
4021 
= (idC_C2_1, c_1); 
4022 

4023  
4024 
tel 
4025  
4026 
until true restart POINTC_C2 
4027  
4028  
4029  
4030 
state C2_C2B_IDL: 
4031  
4032 
let 
4033  
4034 

4035  
4036 
(idC_C2, c) 
4037 
= (idC_C2_1, c_1); 
4038 

4039  
4040 
tel 
4041  
4042 
until true restart POINTC_C2 
4043  
4044  
4045  
4046 
tel 
4047  
4048  
4049 
***************************************************State :C_C1 Automaton*************************************************** 
4050  
4051 
node C_C1_node(idC_C1_1:int; 
4052 
c_1:int; 
4053 
y:int; 
4054 
S:bool; 
4055 
R:bool) 
4056  
4057 
returns (idC_C1:int; 
4058 
c:int); 
4059  
4060  
4061 
let 
4062  
4063 
automaton c_c1 
4064  
4065 
state POINTC_C1: 
4066 
unless (idC_C1_1=0) restart POINT__TO__C1_C1A_1 
4067  
4068  
4069  
4070 
unless (idC_C1_1=1511) and S restart C1_C1A__TO__C1_C1B_1 
4071  
4072  
4073  
4074 
unless (idC_C1_1=1512) and R restart C1_C1B__TO__C1_C1A_1 
4075  
4076  
4077  
4078 
unless (idC_C1_1=1511) restart C1_C1A_IDL 
4079  
4080 
unless (idC_C1_1=1512) restart C1_C1B_IDL 
4081  
4082 
let 
4083  
4084 
(idC_C1, c) 
4085 
= (idC_C1_1, c_1); 
4086 

4087  
4088 
tel 
4089  
4090  
4091  
4092 
state POINT__TO__C1_C1A_1: 
4093  
4094 
var idC_C1_2:int; 
4095 
c_2:int; 
4096 
let 
4097  
4098 
 transition trace : 
4099 
POINT__To__C1_C1a_1 
4100 
(idC_C1_2, c_2) 
4101 
= C1_C1a_en(idC_C1_1, y, c_1, false); 
4102 

4103  
4104 
(idC_C1, c) 
4105 
= (idC_C1_2, c_2); 
4106  
4107  
4108 
tel 
4109  
4110 
until true restart POINTC_C1 
4111  
4112  
4113  
4114 
state C1_C1A__TO__C1_C1B_1: 
4115  
4116 
var idC_C1_2, idC_C1_3:int; 
4117 
c_2:int; 
4118 
let 
4119  
4120 
 transition trace : 
4121 
C1_C1a__To__C1_C1b_1 
4122 
(idC_C1_2) 
4123 
= C1_C1a_ex(idC_C1_1, false); 
4124 

4125  
4126 
(idC_C1_3, c_2) 
4127 
= C1_C1b_en(idC_C1_2, y, c_1, false); 
4128 

4129  
4130 
(idC_C1, c) 
4131 
= (idC_C1_3, c_2); 
4132  
4133  
4134 
tel 
4135  
4136 
until true restart POINTC_C1 
4137  
4138  
4139  
4140 
state C1_C1B__TO__C1_C1A_1: 
4141  
4142 
var idC_C1_2, idC_C1_3:int; 
4143 
c_2:int; 
4144 
let 
4145  
4146 
 transition trace : 
4147 
C1_C1b__To__C1_C1a_1 
4148 
(idC_C1_2) 
4149 
= C1_C1b_ex(idC_C1_1, false); 
4150 

4151  
4152 
(idC_C1_3, c_2) 
4153 
= C1_C1a_en(idC_C1_2, y, c_1, false); 
4154 

4155  
4156 
(idC_C1, c) 
4157 
= (idC_C1_3, c_2); 
4158  
4159  
4160 
tel 
4161  
4162 
until true restart POINTC_C1 
4163  
4164  
4165  
4166 
state C1_C1A_IDL: 
4167  
4168 
let 
4169  
4170 

4171  
4172 
(idC_C1, c) 
4173 
= (idC_C1_1, c_1); 
4174 

4175  
4176 
tel 
4177  
4178 
until true restart POINTC_C1 
4179  
4180  
4181  
4182 
state C1_C1B_IDL: 
4183  
4184 
let 
4185  
4186 

4187  
4188 
(idC_C1, c) 
4189 
= (idC_C1_1, c_1); 
4190 

4191  
4192 
tel 
4193  
4194 
until true restart POINTC_C1 
4195  
4196  
4197  
4198 
tel 
4199  
4200  
4201 
***************************************************State :Parallel3_C Automaton*************************************************** 
4202  
4203 
node Parallel3_C_node(idParallel3_C_1:int; 
4204 
c_1:int; 
4205 
idC_C1_1:int; 
4206 
y:int; 
4207 
T:bool; 
4208 
idC_C2_1:int; 
4209 
R:bool; 
4210 
S:bool) 
4211  
4212 
returns (idParallel3_C:int; 
4213 
c:int; 
4214 
idC_C1:int; 
4215 
idC_C2:int); 
4216  
4217  
4218 
let 
4219  
4220 
automaton parallel3_c 
4221  
4222 
state POINTParallel3_C: 
4223 
unless (idParallel3_C_1=0) restart POINT__TO__C_C1_1 
4224  
4225  
4226  
4227 
unless (idParallel3_C_1=1507) and T restart C_C2__TO__C_C1_1 
4228  
4229  
4230  
4231 
unless (idParallel3_C_1=1510) and T restart C_C1__TO__C_C2_1 
4232  
4233  
4234  
4235 
unless (idParallel3_C_1=1507) restart C_C2_IDL 
4236  
4237 
unless (idParallel3_C_1=1510) restart C_C1_IDL 
4238  
4239 
let 
4240  
4241 
(idParallel3_C, c, idC_C1, idC_C2) 
4242 
= (idParallel3_C_1, c_1, idC_C1_1, idC_C2_1); 
4243 

4244  
4245 
tel 
4246  
4247  
4248  
4249 
state POINT__TO__C_C1_1: 
4250  
4251 
var idParallel3_C_2:int; 
4252 
c_2:int; 
4253 
idC_C1_2:int; 
4254 
let 
4255  
4256 
 transition trace : 
4257 
POINT__To__C_C1_1 
4258 
(idC_C1_2, idParallel3_C_2, c_2) 
4259 
= C_C1_en(idC_C1_1, idParallel3_C_1, c_1, y, false); 
4260 

4261  
4262 
(idParallel3_C, c, idC_C1) 
4263 
= (idParallel3_C_2, c_2, idC_C1_2); 
4264  
4265 
add unused variables 
4266 
(idC_C2) 
4267 
= (idC_C2_1); 
4268 

4269  
4270 
tel 
4271  
4272 
until true restart POINTParallel3_C 
4273  
4274  
4275  
4276 
state C_C2__TO__C_C1_1: 
4277  
4278 
var idParallel3_C_2, idParallel3_C_3:int; 
4279 
c_2:int; 
4280 
idC_C1_2:int; 
4281 
idC_C2_2:int; 
4282 
let 
4283  
4284 
 transition trace : 
4285 
C_C2__To__C_C1_1 
4286 
(idC_C2_2, idParallel3_C_2) 
4287 
= C_C2_ex(idC_C2_1, idParallel3_C_1, false); 
4288 

4289  
4290 
(idC_C1_2, idParallel3_C_3, c_2) 
4291 
= C_C1_en(idC_C1_1, idParallel3_C_2, c_1, y, false); 
4292 

4293  
4294 
(idParallel3_C, c, idC_C1, idC_C2) 
4295 
= (idParallel3_C_3, c_2, idC_C1_2, idC_C2_2); 
4296  
4297  
4298 
tel 
4299  
4300 
until true restart POINTParallel3_C 
4301  
4302  
4303  
4304 
state C_C1__TO__C_C2_1: 
4305  
4306 
var idParallel3_C_2, idParallel3_C_3:int; 
4307 
c_2:int; 
4308 
idC_C1_2:int; 
4309 
idC_C2_2:int; 
4310 
let 
4311  
4312 
 transition trace : 
4313 
C_C1__To__C_C2_1 
4314 
(idC_C1_2, idParallel3_C_2) 
4315 
= C_C1_ex(idC_C1_1, idParallel3_C_1, false); 
4316 

4317  
4318 
(idC_C2_2, idParallel3_C_3, c_2) 
4319 
= C_C2_en(idC_C2_1, idParallel3_C_2, c_1, y, false); 
4320 

4321  
4322 
(idParallel3_C, c, idC_C1, idC_C2) 
4323 
= (idParallel3_C_3, c_2, idC_C1_2, idC_C2_2); 
4324  
4325  
4326 
tel 
4327  
4328 
until true restart POINTParallel3_C 
4329  
4330  
4331  
4332 
state C_C2_IDL: 
4333  
4334 
var c_2:int; 
4335 
idC_C2_2:int; 
4336 
let 
4337  
4338 

4339 
(idC_C2_2, c_2) 
4340 
= C_C2_node(idC_C2_1, c_1, y, S, R); 
4341  
4342 

4343  
4344  
4345 
(idParallel3_C, c, idC_C1, idC_C2) 
4346 
= (idParallel3_C_1, c_2, idC_C1_1, idC_C2_2); 
4347 

4348  
4349 
tel 
4350  
4351 
until true restart POINTParallel3_C 
4352  
4353  
4354  
4355 
state C_C1_IDL: 
4356  
4357 
var c_2:int; 
4358 
idC_C1_2:int; 
4359 
let 
4360  
4361 

4362 
(idC_C1_2, c_2) 
4363 
= C_C1_node(idC_C1_1, c_1, y, S, R); 
4364  
4365 

4366  
4367  
4368 
(idParallel3_C, c, idC_C1, idC_C2) 
4369 
= (idParallel3_C_1, c_2, idC_C1_2, idC_C2_1); 
4370 

4371  
4372 
tel 
4373  
4374 
until true restart POINTParallel3_C 
4375  
4376  
4377  
4378 
tel 
4379  
4380  
4381 
***************************************************State :A_A2 Automaton*************************************************** 
4382  
4383 
node A_A2_node(idA_A2_1:int; 
4384 
a_1:int; 
4385 
x:int; 
4386 
S:bool; 
4387 
R:bool) 
4388  
4389 
returns (idA_A2:int; 
4390 
a:int); 
4391  
4392  
4393 
let 
4394  
4395 
automaton a_a2 
4396  
4397 
state POINTA_A2: 
4398 
unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1 
4399  
4400  
4401  
4402 
unless (idA_A2_1=1497) and S restart A2_A2A__TO__A2_A2B_1 
4403  
4404  
4405  
4406 
unless (idA_A2_1=1498) and R restart A2_A2B__TO__A2_A2A_1 
4407  
4408  
4409  
4410 
unless (idA_A2_1=1497) restart A2_A2A_IDL 
4411  
4412 
unless (idA_A2_1=1498) restart A2_A2B_IDL 
4413  
4414 
let 
4415  
4416 
(idA_A2, a) 
4417 
= (idA_A2_1, a_1); 
4418 

4419  
4420 
tel 
4421  
4422  
4423  
4424 
state POINT__TO__A2_A2A_1: 
4425  
4426 
var idA_A2_2:int; 
4427 
a_2:int; 
4428 
let 
4429  
4430 
 transition trace : 
4431 
POINT__To__A2_A2a_1 
4432 
(idA_A2_2, a_2) 
4433 
= A2_A2a_en(idA_A2_1, x, a_1, false); 
4434 

4435  
4436 
(idA_A2, a) 
4437 
= (idA_A2_2, a_2); 
4438  
4439  
4440 
tel 
4441  
4442 
until true restart POINTA_A2 
4443  
4444  
4445  
4446 
state A2_A2A__TO__A2_A2B_1: 
4447  
4448 
var idA_A2_2, idA_A2_3:int; 
4449 
a_2:int; 
4450 
let 
4451  
4452 
 transition trace : 
4453 
A2_A2a__To__A2_A2b_1 
4454 
(idA_A2_2) 
4455 
= A2_A2a_ex(idA_A2_1, false); 
4456 

4457  
4458 
(idA_A2_3, a_2) 
4459 
= A2_A2b_en(idA_A2_2, x, a_1, false); 
4460 

4461  
4462 
(idA_A2, a) 
4463 
= (idA_A2_3, a_2); 
4464  
4465  
4466 
tel 
4467  
4468 
until true restart POINTA_A2 
4469  
4470  
4471  
4472 
state A2_A2B__TO__A2_A2A_1: 
4473  
4474 
var idA_A2_2, idA_A2_3:int; 
4475 
a_2:int; 
4476 
let 
4477  
4478 
 transition trace : 
4479 
A2_A2b__To__A2_A2a_1 
4480 
(idA_A2_2) 
4481 
= A2_A2b_ex(idA_A2_1, false); 
4482 

4483  
4484 
(idA_A2_3, a_2) 
4485 
= A2_A2a_en(idA_A2_2, x, a_1, false); 
4486 

4487  
4488 
(idA_A2, a) 
4489 
= (idA_A2_3, a_2); 
4490  
4491  
4492 
tel 
4493  
4494 
until true restart POINTA_A2 
4495  
4496  
4497  
4498 
state A2_A2A_IDL: 
4499  
4500 
let 
4501  
4502 

4503  
4504 
(idA_A2, a) 
4505 
= (idA_A2_1, a_1); 
4506 

4507  
4508 
tel 
4509  
4510 
until true restart POINTA_A2 
4511  
4512  
4513  
4514 
state A2_A2B_IDL: 
4515  
4516 
let 
4517  
4518 

4519  
4520 
(idA_A2, a) 
4521 
= (idA_A2_1, a_1); 
4522 

4523  
4524 
tel 
4525  
4526 
until true restart POINTA_A2 
4527  
4528  
4529  
4530 
tel 
4531  
4532  
4533 
***************************************************State :A_A1 Automaton*************************************************** 
4534  
4535 
node A_A1_node(idA_A1_1:int; 
4536 
a_1:int; 
4537 
x:int; 
4538 
S:bool; 
4539 
R:bool) 
4540  
4541 
returns (idA_A1:int; 
4542 
a:int); 
4543  
4544  
4545 
let 
4546  
4547 
automaton a_a1 
4548  
4549 
state POINTA_A1: 
4550 
unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1 
4551  
4552  
4553  
4554 
unless (idA_A1_1=1494) and S restart A1_A1A__TO__A1_A1B_1 
4555  
4556  
4557  
4558 
unless (idA_A1_1=1495) and R restart A1_A1B__TO__A1_A1A_1 
4559  
4560  
4561  
4562 
unless (idA_A1_1=1494) restart A1_A1A_IDL 
4563  
4564 
unless (idA_A1_1=1495) restart A1_A1B_IDL 
4565  
4566 
let 
4567  
4568 
(idA_A1, a) 
4569 
= (idA_A1_1, a_1); 
4570 

4571  
4572 
tel 
4573  
4574  
4575  
4576 
state POINT__TO__A1_A1A_1: 
4577  
4578 
var idA_A1_2:int; 
4579 
a_2:int; 
4580 
let 
4581  
4582 
 transition trace : 
4583 
POINT__To__A1_A1a_1 
4584 
(idA_A1_2, a_2) 
4585 
= A1_A1a_en(idA_A1_1, x, a_1, false); 
4586 

4587  
4588 
(idA_A1, a) 
4589 
= (idA_A1_2, a_2); 
4590  
4591  
4592 
tel 
4593  
4594 
until true restart POINTA_A1 
4595  
4596  
4597  
4598 
state A1_A1A__TO__A1_A1B_1: 
4599  
4600 
var idA_A1_2, idA_A1_3:int; 
4601 
a_2:int; 
4602 
let 
4603  
4604 
 transition trace : 
4605 
A1_A1a__To__A1_A1b_1 
4606 
(idA_A1_2) 
4607 
= A1_A1a_ex(idA_A1_1, false); 
4608 

4609  
4610 
(idA_A1_3, a_2) 
4611 
= A1_A1b_en(idA_A1_2, x, a_1, false); 
4612 

4613  
4614 
(idA_A1, a) 
4615 
= (idA_A1_3, a_2); 
4616  
4617  
4618 
tel 
4619  
4620 
until true restart POINTA_A1 
4621  
4622  
4623  
4624 
state A1_A1B__TO__A1_A1A_1: 
4625  
4626 
var idA_A1_2, idA_A1_3:int; 
4627 
a_2:int; 
4628 
let 
4629  
4630 
 transition trace : 
4631 
A1_A1b__To__A1_A1a_1 
4632 
(idA_A1_2) 
4633 
= A1_A1b_ex(idA_A1_1, false); 
4634 

4635  
4636 
(idA_A1_3, a_2) 
4637 
= A1_A1a_en(idA_A1_2, x, a_1, false); 
4638 

4639  
4640 
(idA_A1, a) 
4641 
= (idA_A1_3, a_2); 
4642  
4643  
4644 
tel 
4645  
4646 
until true restart POINTA_A1 
4647  
4648  
4649  
4650 
state A1_A1A_IDL: 
4651  
4652 
let 
4653  
4654 

4655  
4656 
(idA_A1, a) 
4657 
= (idA_A1_1, a_1); 
4658 

4659  
4660 
tel 
4661  
4662 
until true restart POINTA_A1 
4663  
4664  
4665  
4666 
state A1_A1B_IDL: 
4667  
4668 
let 
4669  
4670 

4671  
4672 
(idA_A1, a) 
4673 
= (idA_A1_1, a_1); 
4674 

4675  
4676 
tel 
4677  
4678 
until true restart POINTA_A1 
4679  
4680  
4681  
4682 
tel 
4683  
4684  
4685 
***************************************************State :Parallel3_A Automaton*************************************************** 
4686  
4687 
node Parallel3_A_node(idParallel3_A_1:int; 
4688 
a_1:int; 
4689 
idA_A1_1:int; 
4690 
x:int; 
4691 
T:bool; 
4692 
idA_A2_1:int; 
4693 
R:bool; 
4694 
S:bool) 
4695  
4696 
returns (idParallel3_A:int; 
4697 
a:int; 
4698 
idA_A1:int; 
4699 
idA_A2:int); 
4700  
4701  
4702 
let 
4703  
4704 
automaton parallel3_a 
4705  
4706 
state POINTParallel3_A: 
4707 
unless (idParallel3_A_1=0) restart POINT__TO__A_A1_1 
4708  
4709  
4710  
4711 
unless (idParallel3_A_1=1493) and T restart A_A1__TO__A_A2_1 
4712  
4713  
4714  
4715 
unless (idParallel3_A_1=1496) and T restart A_A2__TO__A_A1_1 
4716  
4717  
4718  
4719 
unless (idParallel3_A_1=1493) restart A_A1_IDL 
4720  
4721 
unless (idParallel3_A_1=1496) restart A_A2_IDL 
4722  
4723 
let 
4724  
4725 
(idParallel3_A, a, idA_A1, idA_A2) 
4726 
= (idParallel3_A_1, a_1, idA_A1_1, idA_A2_1); 
4727 

4728  
4729 
tel 
4730  
4731  
4732  
4733 
state POINT__TO__A_A1_1: 
4734  
4735 
var idParallel3_A_2:int; 
4736 
a_2:int; 
4737 
idA_A1_2:int; 
4738 
let 
4739  
4740 
 transition trace : 
4741 
POINT__To__A_A1_1 
4742 
(idA_A1_2, idParallel3_A_2, a_2) 
4743 
= A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false); 
4744 

4745  
4746 
(idParallel3_A, a, idA_A1) 
4747 
= (idParallel3_A_2, a_2, idA_A1_2); 
4748  
4749 
add unused variables 
4750 
(idA_A2) 
4751 
= (idA_A2_1); 
4752 

4753  
4754 
tel 
4755  
4756 
until true restart POINTParallel3_A 
4757  
4758  
4759  
4760 
state A_A1__TO__A_A2_1: 
4761  
4762 
var idParallel3_A_2, idParallel3_A_3:int; 
4763 
a_2:int; 
4764 
idA_A1_2:int; 
4765 
idA_A2_2:int; 
4766 
let 
4767  
4768 
 transition trace : 
4769 
A_A1__To__A_A2_1 
4770 
(idA_A1_2, idParallel3_A_2) 
4771 
= A_A1_ex(idA_A1_1, idParallel3_A_1, false); 
4772 

4773  
4774 
(idA_A2_2, idParallel3_A_3, a_2) 
4775 
= A_A2_en(idA_A2_1, idParallel3_A_2, a_1, x, false); 
4776 

4777  
4778 
(idParallel3_A, a, idA_A1, idA_A2) 
4779 
= (idParallel3_A_3, a_2, idA_A1_2, idA_A2_2); 
4780  
4781  
4782 
tel 
4783  
4784 
until true restart POINTParallel3_A 
4785  
4786  
4787  
4788 
state A_A2__TO__A_A1_1: 
4789  
4790 
var idParallel3_A_2, idParallel3_A_3:int; 
4791 
a_2:int; 
4792 
idA_A1_2:int; 
4793 
idA_A2_2:int; 
4794 
let 
4795  
4796 
 transition trace : 
4797 
A_A2__To__A_A1_1 
4798 
(idA_A2_2, idParallel3_A_2) 
4799 
= A_A2_ex(idA_A2_1, idParallel3_A_1, false); 
4800 

4801  
4802 
(idA_A1_2, idParallel3_A_3, a_2) 
4803 
= A_A1_en(idA_A1_1, idParallel3_A_2, a_1, x, false); 
4804 

4805  
4806 
(idParallel3_A, a, idA_A1, idA_A2) 
4807 
= (idParallel3_A_3, a_2, idA_A1_2, idA_A2_2); 
4808  
4809  
4810 
tel 
4811  
4812 
until true restart POINTParallel3_A 
4813  
4814  
4815  
4816 
state A_A1_IDL: 
4817  
4818 
var a_2:int; 
4819 
idA_A1_2:int; 
4820 
let 
4821  
4822 

4823 
(idA_A1_2, a_2) 
4824 
= A_A1_node(idA_A1_1, a_1, x, S, R); 
4825  
4826 

4827  
4828  
4829 
(idParallel3_A, a, idA_A1, idA_A2) 
4830 
= (idParallel3_A_1, a_2, idA_A1_2, idA_A2_1); 
4831 

4832  
4833 
tel 
4834  
4835 
until true restart POINTParallel3_A 
4836  
4837  
4838  
4839 
state A_A2_IDL: 
4840  
4841 
var a_2:int; 
4842 
idA_A2_2:int; 
4843 
let 
4844  
4845 

4846 
(idA_A2_2, a_2) 
4847 
= A_A2_node(idA_A2_1, a_1, x, S, R); 
4848  
4849 

4850  
4851  
4852 
(idParallel3_A, a, idA_A1, idA_A2) 
4853 
= (idParallel3_A_1, a_2, idA_A1_1, idA_A2_2); 
4854 

4855  
4856 
tel 
4857  
4858 
until true restart POINTParallel3_A 
4859  
4860  
4861  
4862 
tel 
4863  
4864  
4865 
***************************************************State :Parallel3_Parallel3 Automaton*************************************************** 
4866  
4867 
node Parallel3_Parallel3_node(idParallel3_Parallel3_1:int; 
4868 
a_1:int; 
4869 
idA_A1_1:int; 
4870 
idA_A2_1:int; 
4871 
idParallel3_A_1:int; 
4872 
x:int; 
4873 
b_1:int; 
4874 
idB_B1_1:int; 
4875 
idB_B2_1:int; 
4876 
idParallel3_B_1:int; 
4877 
c_1:int; 
4878 
idC_C1_1:int; 
4879 
idC_C2_1:int; 
4880 
idParallel3_C_1:int; 
4881 
y:int; 
4882 
dd_1:int; 
4883 
idD_D1_1:int; 
4884 
idD_D2_1:int; 
4885 
idParallel3_D_1:int; 
4886 
R:bool; 
4887 
S:bool; 
4888 
T:bool) 
4889  
4890 
returns (idParallel3_Parallel3:int; 
4891 
a:int; 
4892 
idA_A1:int; 
4893 
idA_A2:int; 
4894 
idParallel3_A:int; 
4895 
b:int; 
4896 
idB_B1:int; 
4897 
idB_B2:int; 
4898 
idParallel3_B:int; 
4899 
c:int; 
4900 
idC_C1:int; 
4901 
idC_C2:int; 
4902 
idParallel3_C:int; 
4903 
dd:int; 
4904 
idD_D1:int; 
4905 
idD_D2:int; 
4906 
idParallel3_D:int); 
4907  
4908  
4909 
let 
4910  
4911 
automaton parallel3_parallel3 
4912  
4913 
state POINTParallel3_Parallel3: 
4914 
unless (idParallel3_Parallel3_1=0) restart PARALLEL3_PARALLEL3_PARALLEL_ENTRY 
4915 
unless true restart PARALLEL3_PARALLEL3_PARALLEL_IDL 
4916  
4917 
let 
4918  
4919 
(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D) 
4920 
= (idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, idC_C1_1, idC_C2_1, idParallel3_C_1, dd_1, idD_D1_1, idD_D2_1, idParallel3_D_1); 
4921 

4922  
4923 
tel 
4924  
4925  
4926  
4927 
state PARALLEL3_PARALLEL3_PARALLEL_ENTRY: 
4928  
4929 
var idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4, idParallel3_Parallel3_5:int; 
4930 
a_2:int; 
4931 
idA_A1_2:int; 
4932 
idA_A2_2:int; 
4933 
idParallel3_A_2:int; 
4934 
b_2:int; 
4935 
idB_B1_2:int; 
4936 
idB_B2_2:int; 
4937 
idParallel3_B_2:int; 
4938 
c_2:int; 
4939 
idC_C1_2:int; 
4940 
idC_C2_2:int; 
4941 
idParallel3_C_2:int; 
4942 
dd_2:int; 
4943 
idD_D1_2:int; 
4944 
idD_D2_2:int; 
4945 
idParallel3_D_2:int; 
4946 
let 
4947  
4948 

4949 
(idParallel3_A_2, idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2) 
4950 
= Parallel3_A_en(idParallel3_A_1, idParallel3_Parallel3_1, a_1, idA_A1_1, x, idA_A2_1, false); 
4951  
4952 
(idParallel3_B_2, idParallel3_Parallel3_3, b_2, idB_B1_2, idB_B2_2) 
4953 
= Parallel3_B_en(idParallel3_B_1, idParallel3_Parallel3_2, b_1, idB_B1_1, x, idB_B2_1, false); 
4954  
4955 
(idParallel3_C_2, idParallel3_Parallel3_4, c_2, idC_C1_2, idC_C2_2) 
4956 
= Parallel3_C_en(idParallel3_C_1, idParallel3_Parallel3_3, c_1, idC_C1_1, y, idC_C2_1, false); 
4957  
4958 
(idParallel3_D_2, idParallel3_Parallel3_5, dd_2, idD_D1_2, idD_D2_2) 
4959 
= Parallel3_D_en(idParallel3_D_1, idParallel3_Parallel3_4, dd_1, idD_D1_1, y, idD_D2_1, false); 
4960  
4961  
4962 
(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D) 
4963 
= (idParallel3_Parallel3_5, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2); 
4964 

4965  
4966 
tel 
4967  
4968 
until true restart POINTParallel3_Parallel3 
4969  
4970  
4971  
4972 
state PARALLEL3_PARALLEL3_PARALLEL_IDL: 
4973  
4974 
var a_2:int; 
4975 
idA_A1_2:int; 
4976 
idA_A2_2:int; 
4977 
idParallel3_A_2:int; 
4978 
b_2:int; 
4979 
idB_B1_2:int; 
4980 
idB_B2_2:int; 
4981 
idParallel3_B_2:int; 
4982 
c_2:int; 
4983 
idC_C1_2:int; 
4984 
idC_C2_2:int; 
4985 
idParallel3_C_2:int; 
4986 
dd_2:int; 
4987 
idD_D1_2:int; 
4988 
idD_D2_2:int; 
4989 
idParallel3_D_2:int; 
4990 
let 
4991  
4992 

4993  
4994 
(idParallel3_A_2, a_2, idA_A1_2, idA_A2_2) 
4995 
= if not (idParallel3_A_1= 0 ) then Parallel3_A_node(idParallel3_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R, S) 
4996  
4997 
else (idParallel3_A_1, a_1, idA_A1_1, idA_A2_1); 
4998  
4999 

5000  
5001 

5002  
5003 
(idParallel3_B_2, b_2, idB_B1_2, idB_B2_2) 
5004 
= if not (idParallel3_B_1= 0 ) then Parallel3_B_node(idParallel3_B_1, b_1, idB_B1_1, x, T, idB_B2_1, R, S) 
5005  
5006 
else (idParallel3_B_1, b_1, idB_B1_1, idB_B2_1); 
5007  
5008 

5009  
5010 

5011  
5012 
(idParallel3_C_2, c_2, idC_C1_2, idC_C2_2) 
5013 
= if not (idParallel3_C_1= 0 ) then Parallel3_C_node(idParallel3_C_1, c_1, idC_C1_1, y, T, idC_C2_1, R, S) 
5014  
5015 
else (idParallel3_C_1, c_1, idC_C1_1, idC_C2_1); 
5016  
5017 

5018  
5019 

5020  
5021 
(idParallel3_D_2, dd_2, idD_D1_2, idD_D2_2) 
5022 
= if not (idParallel3_D_1= 0 ) then Parallel3_D_node(idParallel3_D_1, dd_1, idD_D1_1, y, T, idD_D2_1, R, S) 
5023  
5024 
else (idParallel3_D_1, dd_1, idD_D1_1, idD_D2_1); 
5025  
5026 

5027  
5028 

5029  
5030 
(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D) 
5031 
= (idParallel3_Parallel3_1, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2); 
5032 

5033  
5034 
tel 
5035  
5036 
until true restart POINTParallel3_Parallel3 
5037  
5038  
5039  
5040 
tel 
5041  
5042  
5043 
***************************************************State :Parallel3_Parallel3 Automaton*************************************************** 
5044  
5045 
node Parallel3_Parallel3(x:int; 
5046 
y:int; 
5047 
R:bool; 
5048 
S:bool; 
5049 
T:bool) 
5050  
5051 
returns (a:int; 
5052 
b:int; 
5053 
dd:int; 
5054 
c:int); 
5055  
5056  
5057 
var a_1: int; 
5058  
5059 
b_1: int; 
5060  
5061 
dd_1: int; 
5062  
5063 
c_1: int; 
5064  
5065 
idParallel3_Parallel3, idParallel3_Parallel3_1: int; 
5066  
5067 
idB_B2, idB_B2_1: int; 
5068  
5069 
idB_B1, idB_B1_1: int; 
5070  
5071 
idParallel3_B, idParallel3_B_1: int; 
5072  
5073 
idD_D2, idD_D2_1: int; 
5074  
5075 
idD_D1, idD_D1_1: int; 
5076  
5077 
idParallel3_D, idParallel3_D_1: int; 
5078  
5079 
idC_C2, idC_C2_1: int; 
5080  
5081 
idC_C1, idC_C1_1: int; 
5082  
5083 
idParallel3_C, idParallel3_C_1: int; 
5084  
5085 
idA_A2, idA_A2_1: int; 
5086  
5087 
idA_A1, idA_A1_1: int; 
5088  
5089 
idParallel3_A, idParallel3_A_1: int; 
5090  
5091 
idParallel3_Parallel3_2, idParallel3_Parallel3_3:int; 
5092 
a_2, a_3:int; 
5093 
idA_A1_2, idA_A1_3:int; 
5094 
idA_A2_2, idA_A2_3:int; 
5095 
idParallel3_A_2, idParallel3_A_3:int; 
5096 
b_2, b_3:int; 
5097 
idB_B1_2, idB_B1_3:int; 
5098 
idB_B2_2, idB_B2_3:int; 
5099 
idParallel3_B_2, idParallel3_B_3:int; 
5100 
c_2, c_3:int; 
5101 
idC_C1_2, idC_C1_3:int; 
5102 
idC_C2_2, idC_C2_3:int; 
5103 
idParallel3_C_2, idParallel3_C_3:int; 
5104 
dd_2, dd_3:int; 
5105 
idD_D1_2, idD_D1_3:int; 
5106 
idD_D2_2, idD_D2_3:int; 
5107 
idParallel3_D_2, idParallel3_D_3:int; 
5108 
let 
5109  
5110 
a_1 = 0 > pre a; 
5111  
5112 
b_1 = 0 > pre b; 
5113  
5114 
dd_1 = 0 > pre dd; 
5115  
5116 
c_1 = 0 > pre c; 
5117  
5118 
idParallel3_Parallel3_1 = 0 > pre idParallel3_Parallel3; 
5119  
5120 
idB_B2_1 = 0 > pre idB_B2; 
5121  
5122 
idB_B1_1 = 0 > pre idB_B1; 
5123  
5124 
idParallel3_B_1 = 0 > pre idParallel3_B; 
5125  
5126 
idD_D2_1 = 0 > pre idD_D2; 
5127  
5128 
idD_D1_1 = 0 > pre idD_D1; 
5129  
5130 
idParallel3_D_1 = 0 > pre idParallel3_D; 
5131  
5132 
idC_C2_1 = 0 > pre idC_C2; 
5133  
5134 
idC_C1_1 = 0 > pre idC_C1; 
5135  
5136 
idParallel3_C_1 = 0 > pre idParallel3_C; 
5137  
5138 
idA_A2_1 = 0 > pre idA_A2; 
5139  
5140 
idA_A1_1 = 0 > pre idA_A1; 
5141  
5142 
idParallel3_A_1 = 0 > pre idParallel3_A; 
5143  
5144 

5145  
5146  
5147  
5148 
(idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2) 
5149 
= 
5150  
5151 
if R then Parallel3_Parallel3_node(idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, x, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, idC_C1_1, idC_C2_1, idParallel3_C_1, y, dd_1, idD_D1_1, idD_D2_1, idParallel3_D_1, R, false, false) 
5152  
5153 
else (idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, idC_C1_1, idC_C2_1, idParallel3_C_1, dd_1, idD_D1_1, idD_D2_1, idParallel3_D_1); 
5154  
5155 

5156  
5157  
5158  
5159 
(idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, idC_C1_3, idC_C2_3, idParallel3_C_3, dd_3, idD_D1_3, idD_D2_3, idParallel3_D_3) 
5160 
= 
5161  
5162 
if S then Parallel3_Parallel3_node(idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, x, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, y, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2, false, S, false) 
5163  
5164 
else (idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2); 
5165  
5166 

5167  
5168  
5169  
5170 
(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D) 
5171 
= 
5172  
5173 
if T then Parallel3_Parallel3_node(idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, x, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, idC_C1_3, idC_C2_3, idParallel3_C_3, y, dd_3, idD_D1_3, idD_D2_3, idParallel3_D_3, false, false, T) 
5174  
5175 
else (idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, idC_C1_3, idC_C2_3, idParallel3_C_3, dd_3, idD_D1_3, idD_D2_3, idParallel3_D_3); 
5176  
5177 

5178  
5179  
5180 
unused outputs 
5181 

5182  
5183 
tel 
5184  
5185  
5186  
5187 
node Parallel3 (x_1_1 : int; R_1_1 : real; y_1_1 : int; S_1_1 : real; T_1_1 : real) 
5188 
returns (a_1_1 : int; 
5189 
b_2_1 : int; 
5190 
dd_3_1 : int; 
5191 
c_4_1 : int); 
5192 
var 
5193 
Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real; 
5194 
Parallel3_1_1 : int; Parallel3_2_1 : int; Parallel3_3_1 : int; Parallel3_4_1 : int; 
5195 
i_virtual_local : real; 
5196 
Parallel3Mux_1_1_event: bool; 
5197 
Parallel3Mux_1_2_event: bool; 
5198 
Parallel3Mux_1_3_event: bool; 
5199 
let 
5200 
Mux_1_1 = R_1_1 ; 
5201 
Mux_1_2 = S_1_1 ; 
5202 
Mux_1_3 = T_1_1 ; 
5203 
Parallel3Mux_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)); 
5204 
Parallel3Mux_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)); 
5205 
Parallel3Mux_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)); 
5206 
(Parallel3_1_1, Parallel3_2_1, Parallel3_3_1, Parallel3_4_1) = Parallel3_Parallel3(x_1_1, y_1_1, Parallel3Mux_1_1_event, Parallel3Mux_1_2_event, Parallel3Mux_1_3_event); 
5207 
a_1_1 = Parallel3_1_1; 
5208 
b_2_1 = Parallel3_2_1; 
5209 
dd_3_1 = Parallel3_3_1; 
5210 
c_4_1 = Parallel3_4_1; 
5211 
i_virtual_local= 0.0 > 1.0; 
5212 
tel 
5213 