lustrectests / regression_tests / lustre_files / success / Stateflow / src_Parallel4 / Parallel4.lus @ eb639349
History  View  Annotate  Download (82.2 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  
46 
 Entry action for state :B2_B2a 
47 
node B2_B2a_en(idB_B2_1:int; 
48 
a_1:int; 
49 
b_1:int; 
50 
isInner:bool) 
51  
52 
returns (idB_B2:int; 
53 
a:int; 
54 
b:int); 
55  
56  
57 
var idB_B2_2:int; 
58 
b_2:int; 
59  
60  
61 
let 
62  
63  
64  
65 
 set state as active 
66 
idB_B2_2 
67 
= 1655; 
68 

69  
70 
b_2 
71 
= if (not isInner) then a_1 +7 
72 
else b_1; 
73 

74  
75 
(idB_B2, a, b) 
76 
= (idB_B2_2, a_1, b_2); 
77 

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

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

138  
139 
b_2 
140 
= if (not isInner) then a_1 +8 
141 
else b_1; 
142 

143  
144 
(idB_B2, a, b) 
145 
= (idB_B2_2, a_1, b_2); 
146 

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

176  
177 
tel 
178  
179  
180  
181  
182  
183  
184 
 Entry action for state :B_B2 
185 
node B_B2_en(idB_B2_1:int; 
186 
idParallel4_B_1:int; 
187 
a_1:int; 
188 
b_1:int; 
189 
isInner:bool) 
190  
191 
returns (idB_B2:int; 
192 
idParallel4_B:int; 
193 
a:int; 
194 
b:int); 
195  
196  
197 
var idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5, idB_B2_6:int; 
198 
idParallel4_B_2, idParallel4_B_3, idParallel4_B_4:int; 
199 
a_2, a_3, a_4, a_5, a_6:int; 
200 
b_2, b_3, b_4, b_5, b_6:int; 
201  
202  
203 
let 
204  
205  
206  
207 
 set state as active 
208 
idParallel4_B_2 
209 
= 1654; 
210 

211  
212 

213 
 transition trace : 
214 
POINT__To__B2_B2a_1 
215 
(idB_B2_2, a_2, b_2) 
216 
= B2_B2a_en(idB_B2_1, a_1, b_1, false); 
217 

218  
219 
(idB_B2_3, idParallel4_B_3, a_3, b_3) 
220 
= 
221  
222 
if ( idB_B2_1 = 0) then 
223  
224 
(idB_B2_2, idParallel4_B_2, a_2, b_2) 
225  
226 
else(idB_B2_1, idParallel4_B_2, a_1, b_1); 
227  
228 

229  
230 
(idB_B2_4, a_4, b_4) 
231 
= 
232 
if ( idB_B2_1 = 1655) then 
233 
B2_B2a_en(idB_B2_1, a_1, b_1, false) 
234 
else (idB_B2_1, a_1, b_1); 
235  
236 

237  
238 
(idB_B2_5, a_5, b_5) 
239 
= 
240 
if ( idB_B2_1 = 1656) then 
241 
B2_B2b_en(idB_B2_1, a_1, b_1, false) 
242 
else (idB_B2_1, a_1, b_1); 
243  
244 

245  
246 
(idB_B2_6, idParallel4_B_4, a_6, b_6) 
247 
= 
248 
if ( idB_B2_1 = 0) then 
249 
(idB_B2_3, idParallel4_B_3, a_3, b_3) 
250 
else 
251 
if ( idB_B2_1 = 1655) then 
252 
(idB_B2_4, idParallel4_B_3, a_4, b_4) 
253 
else 
254 
if ( idB_B2_1 = 1656) then 
255 
(idB_B2_5, idParallel4_B_3, a_5, b_5) 
256 
else (idB_B2_1, idParallel4_B_2, a_1, b_1); 
257  
258  
259 
(idB_B2, idParallel4_B, a, b) 
260 
= (idB_B2_6, idParallel4_B_4, a_6, b_6); 
261 

262  
263 
tel 
264  
265  
266  
267  
268  
269 
 Exit action for state :B_B2 
270 
node B_B2_ex(idB_B2_1:int; 
271 
idParallel4_B_1:int; 
272 
isInner:bool) 
273  
274 
returns (idB_B2:int; 
275 
idParallel4_B:int); 
276  
277  
278 
var idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5:int; 
279 
idParallel4_B_2:int; 
280  
281  
282 
let 
283  
284  
285  
286 

287 
(idB_B2_2) 
288 
= 
289 
if ( idB_B2_1 = 1655) then 
290 
B2_B2a_ex(idB_B2_1, false) 
291 
else (idB_B2_1); 
292  
293 

294  
295 
(idB_B2_3) 
296 
= 
297 
if ( idB_B2_1 = 1656) then 
298 
B2_B2b_ex(idB_B2_1, false) 
299 
else (idB_B2_1); 
300  
301 

302  
303 
(idB_B2_4) 
304 
= 
305 
if ( idB_B2_1 = 1655) then 
306 
(idB_B2_2) 
307 
else 
308 
if ( idB_B2_1 = 1656) then 
309 
(idB_B2_3) 
310 
else (idB_B2_1); 
311  
312  
313 
 set state as inactive 
314 
idParallel4_B_2 
315 
= if (not isInner) then 0 else idParallel4_B_1; 
316  
317 
idB_B2_5 
318 
= 0; 
319 

320  
321 
(idB_B2, idParallel4_B) 
322 
= (idB_B2_5, idParallel4_B_1); 
323 

324  
325 
tel 
326  
327  
328  
329  
330  
331  
332 
 Entry action for state :B1_B1a 
333 
node B1_B1a_en(idB_B1_1:int; 
334 
a_1:int; 
335 
b_1:int; 
336 
isInner:bool) 
337  
338 
returns (idB_B1:int; 
339 
a:int; 
340 
b:int); 
341  
342  
343 
var idB_B1_2:int; 
344 
b_2:int; 
345  
346  
347 
let 
348  
349  
350  
351 
 set state as active 
352 
idB_B1_2 
353 
= 1658; 
354 

355  
356 
b_2 
357 
= if (not isInner) then a_1 +5 
358 
else b_1; 
359 

360  
361 
(idB_B1, a, b) 
362 
= (idB_B1_2, a_1, b_2); 
363 

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

393  
394 
tel 
395  
396  
397  
398  
399  
400  
401 
 Entry action for state :B1_B1b 
402 
node B1_B1b_en(idB_B1_1:int; 
403 
a_1:int; 
404 
b_1:int; 
405 
isInner:bool) 
406  
407 
returns (idB_B1:int; 
408 
a:int; 
409 
b:int); 
410  
411  
412 
var idB_B1_2:int; 
413 
b_2:int; 
414  
415  
416 
let 
417  
418  
419  
420 
 set state as active 
421 
idB_B1_2 
422 
= 1659; 
423 

424  
425 
b_2 
426 
= if (not isInner) then a_1 +6 
427 
else b_1; 
428 

429  
430 
(idB_B1, a, b) 
431 
= (idB_B1_2, a_1, b_2); 
432 

433  
434 
tel 
435  
436  
437  
438  
439  
440 
 Exit action for state :B1_B1b 
441 
node B1_B1b_ex(idB_B1_1:int; 
442 
isInner:bool) 
443  
444 
returns (idB_B1:int); 
445  
446  
447 
var idB_B1_2:int; 
448  
449  
450 
let 
451  
452  
453  
454 
 set state as inactive 
455 
idB_B1_2 
456 
= if (not isInner) then 0 else idB_B1_1; 
457  
458  
459 
(idB_B1) 
460 
= (idB_B1_1); 
461 

462  
463 
tel 
464  
465  
466  
467  
468  
469  
470 
 Entry action for state :B_B1 
471 
node B_B1_en(idB_B1_1:int; 
472 
idParallel4_B_1:int; 
473 
a_1:int; 
474 
b_1:int; 
475 
isInner:bool) 
476  
477 
returns (idB_B1:int; 
478 
idParallel4_B:int; 
479 
a:int; 
480 
b:int); 
481  
482  
483 
var idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5, idB_B1_6:int; 
484 
idParallel4_B_2, idParallel4_B_3, idParallel4_B_4:int; 
485 
a_2, a_3, a_4, a_5, a_6:int; 
486 
b_2, b_3, b_4, b_5, b_6:int; 
487  
488  
489 
let 
490  
491  
492  
493 
 set state as active 
494 
idParallel4_B_2 
495 
= 1657; 
496 

497  
498 

499 
 transition trace : 
500 
POINT__To__B1_B1a_1 
501 
(idB_B1_2, a_2, b_2) 
502 
= B1_B1a_en(idB_B1_1, a_1, b_1, false); 
503 

504  
505 
(idB_B1_3, idParallel4_B_3, a_3, b_3) 
506 
= 
507  
508 
if ( idB_B1_1 = 0) then 
509  
510 
(idB_B1_2, idParallel4_B_2, a_2, b_2) 
511  
512 
else(idB_B1_1, idParallel4_B_2, a_1, b_1); 
513  
514 

515  
516 
(idB_B1_4, a_4, b_4) 
517 
= 
518 
if ( idB_B1_1 = 1658) then 
519 
B1_B1a_en(idB_B1_1, a_1, b_1, false) 
520 
else (idB_B1_1, a_1, b_1); 
521  
522 

523  
524 
(idB_B1_5, a_5, b_5) 
525 
= 
526 
if ( idB_B1_1 = 1659) then 
527 
B1_B1b_en(idB_B1_1, a_1, b_1, false) 
528 
else (idB_B1_1, a_1, b_1); 
529  
530 

531  
532 
(idB_B1_6, idParallel4_B_4, a_6, b_6) 
533 
= 
534 
if ( idB_B1_1 = 0) then 
535 
(idB_B1_3, idParallel4_B_3, a_3, b_3) 
536 
else 
537 
if ( idB_B1_1 = 1658) then 
538 
(idB_B1_4, idParallel4_B_3, a_4, b_4) 
539 
else 
540 
if ( idB_B1_1 = 1659) then 
541 
(idB_B1_5, idParallel4_B_3, a_5, b_5) 
542 
else (idB_B1_1, idParallel4_B_2, a_1, b_1); 
543  
544  
545 
(idB_B1, idParallel4_B, a, b) 
546 
= (idB_B1_6, idParallel4_B_4, a_6, b_6); 
547 

548  
549 
tel 
550  
551  
552  
553  
554  
555 
 Exit action for state :B_B1 
556 
node B_B1_ex(idB_B1_1:int; 
557 
idParallel4_B_1:int; 
558 
isInner:bool) 
559  
560 
returns (idB_B1:int; 
561 
idParallel4_B:int); 
562  
563  
564 
var idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int; 
565 
idParallel4_B_2:int; 
566  
567  
568 
let 
569  
570  
571  
572 

573 
(idB_B1_2) 
574 
= 
575 
if ( idB_B1_1 = 1658) then 
576 
B1_B1a_ex(idB_B1_1, false) 
577 
else (idB_B1_1); 
578  
579 

580  
581 
(idB_B1_3) 
582 
= 
583 
if ( idB_B1_1 = 1659) then 
584 
B1_B1b_ex(idB_B1_1, false) 
585 
else (idB_B1_1); 
586  
587 

588  
589 
(idB_B1_4) 
590 
= 
591 
if ( idB_B1_1 = 1658) then 
592 
(idB_B1_2) 
593 
else 
594 
if ( idB_B1_1 = 1659) then 
595 
(idB_B1_3) 
596 
else (idB_B1_1); 
597  
598  
599 
 set state as inactive 
600 
idParallel4_B_2 
601 
= if (not isInner) then 0 else idParallel4_B_1; 
602  
603 
idB_B1_5 
604 
= 0; 
605 

606  
607 
(idB_B1, idParallel4_B) 
608 
= (idB_B1_5, idParallel4_B_1); 
609 

610  
611 
tel 
612  
613  
614  
615  
616  
617  
618 
 Entry action for state :Parallel4_B 
619 
node Parallel4_B_en(idParallel4_B_1:int; 
620 
idParallel4_Parallel4_1:int; 
621 
a_1:int; 
622 
b_1:int; 
623 
idB_B1_1:int; 
624 
idB_B2_1:int; 
625 
isInner:bool) 
626  
627 
returns (idParallel4_B:int; 
628 
idParallel4_Parallel4:int; 
629 
a:int; 
630 
b:int; 
631 
idB_B1:int; 
632 
idB_B2:int); 
633  
634  
635 
var idParallel4_B_2, idParallel4_B_3, idParallel4_B_4, idParallel4_B_5, idParallel4_B_6:int; 
636 
idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4:int; 
637 
a_2, a_3, a_4, a_5, a_6:int; 
638 
b_2, b_3, b_4, b_5, b_6:int; 
639 
idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int; 
640 
idB_B2_2, idB_B2_3:int; 
641  
642  
643 
let 
644  
645  
646  
647 
 set state as active 
648 
idParallel4_Parallel4_2 
649 
= 1653; 
650 

651  
652 

653 
 transition trace : 
654 
POINT__To__B_B1_1 
655 
(idB_B1_2, idParallel4_B_2, a_2, b_2) 
656 
= B_B1_en(idB_B1_1, idParallel4_B_1, a_1, b_1, false); 
657 

658  
659 
(idParallel4_B_3, idParallel4_Parallel4_3, a_3, b_3, idB_B1_3) 
660 
= 
661  
662 
if ( idParallel4_B_1 = 0) then 
663  
664 
(idParallel4_B_2, idParallel4_Parallel4_2, a_2, b_2, idB_B1_2) 
665  
666 
else(idParallel4_B_1, idParallel4_Parallel4_2, a_1, b_1, idB_B1_1); 
667  
668 

669  
670 
(idB_B2_2, idParallel4_B_4, a_4, b_4) 
671 
= 
672 
if ( idParallel4_B_1 = 1654) then 
673 
B_B2_en(idB_B2_1, idParallel4_B_1, a_1, b_1, false) 
674 
else (idB_B2_1, idParallel4_B_1, a_1, b_1); 
675  
676 

677  
678 
(idB_B1_4, idParallel4_B_5, a_5, b_5) 
679 
= 
680 
if ( idParallel4_B_1 = 1657) then 
681 
B_B1_en(idB_B1_1, idParallel4_B_1, a_1, b_1, false) 
682 
else (idB_B1_1, idParallel4_B_1, a_1, b_1); 
683  
684 

685  
686 
(idParallel4_B_6, idParallel4_Parallel4_4, a_6, b_6, idB_B1_5, idB_B2_3) 
687 
= 
688 
if ( idParallel4_B_1 = 0) then 
689 
(idParallel4_B_3, idParallel4_Parallel4_3, a_3, b_3, idB_B1_3, idB_B2_1) 
690 
else 
691 
if ( idParallel4_B_1 = 1654) then 
692 
(idParallel4_B_4, idParallel4_Parallel4_3, a_4, b_4, idB_B1_1, idB_B2_2) 
693 
else 
694 
if ( idParallel4_B_1 = 1657) then 
695 
(idParallel4_B_5, idParallel4_Parallel4_3, a_5, b_5, idB_B1_4, idB_B2_1) 
696 
else (idParallel4_B_1, idParallel4_Parallel4_2, a_1, b_1, idB_B1_1, idB_B2_1); 
697  
698  
699 
(idParallel4_B, idParallel4_Parallel4, a, b, idB_B1, idB_B2) 
700 
= (idParallel4_B_6, idParallel4_Parallel4_4, a_6, b_6, idB_B1_5, idB_B2_3); 
701 

702  
703 
tel 
704  
705  
706  
707  
708  
709 
 Exit action for state :Parallel4_B 
710 
node Parallel4_B_ex(idB_B2_1:int; 
711 
idParallel4_B_1:int; 
712 
idB_B1_1:int; 
713 
idParallel4_Parallel4_1:int; 
714 
isInner:bool) 
715  
716 
returns (idB_B2:int; 
717 
idParallel4_B:int; 
718 
idB_B1:int; 
719 
idParallel4_Parallel4:int); 
720  
721  
722 
var idB_B2_2, idB_B2_3:int; 
723 
idParallel4_B_2, idParallel4_B_3, idParallel4_B_4, idParallel4_B_5:int; 
724 
idB_B1_2, idB_B1_3:int; 
725 
idParallel4_Parallel4_2:int; 
726  
727  
728 
let 
729  
730  
731  
732 

733 
(idB_B2_2, idParallel4_B_2) 
734 
= 
735 
if ( idParallel4_B_1 = 1654) then 
736 
B_B2_ex(idB_B2_1, idParallel4_B_1, false) 
737 
else (idB_B2_1, idParallel4_B_1); 
738  
739 

740  
741 
(idB_B1_2, idParallel4_B_3) 
742 
= 
743 
if ( idParallel4_B_1 = 1657) then 
744 
B_B1_ex(idB_B1_1, idParallel4_B_1, false) 
745 
else (idB_B1_1, idParallel4_B_1); 
746  
747 

748  
749 
(idB_B2_3, idParallel4_B_4, idB_B1_3) 
750 
= 
751 
if ( idParallel4_B_1 = 1654) then 
752 
(idB_B2_2, idParallel4_B_2, idB_B1_1) 
753 
else 
754 
if ( idParallel4_B_1 = 1657) then 
755 
(idB_B2_1, idParallel4_B_3, idB_B1_2) 
756 
else (idB_B2_1, idParallel4_B_1, idB_B1_1); 
757  
758  
759 
 set state as inactive 
760 
idParallel4_Parallel4_2 
761 
= if (not isInner) then 0 else idParallel4_Parallel4_1; 
762  
763 
idParallel4_B_5 
764 
= 0; 
765 

766  
767 
(idB_B2, idParallel4_B, idB_B1, idParallel4_Parallel4) 
768 
= (idB_B2_3, idParallel4_B_5, idB_B1_3, idParallel4_Parallel4_1); 
769 

770  
771 
tel 
772  
773  
774  
775  
776  
777  
778 
 Entry action for state :D2_D2a 
779 
node D2_D2a_en(idD_D2_1:int; 
780 
c_1:int; 
781 
dd_1:int; 
782 
isInner:bool) 
783  
784 
returns (idD_D2:int; 
785 
c:int; 
786 
dd:int); 
787  
788  
789 
var idD_D2_2:int; 
790 
dd_2:int; 
791  
792  
793 
let 
794  
795  
796  
797 
 set state as active 
798 
idD_D2_2 
799 
= 1669; 
800 

801  
802 
dd_2 
803 
= if (not isInner) then c_1 +7 
804 
else dd_1; 
805 

806  
807 
(idD_D2, c, dd) 
808 
= (idD_D2_2, c_1, dd_2); 
809 

810  
811 
tel 
812  
813  
814  
815  
816  
817 
 Exit action for state :D2_D2a 
818 
node D2_D2a_ex(idD_D2_1:int; 
819 
isInner:bool) 
820  
821 
returns (idD_D2:int); 
822  
823  
824 
var idD_D2_2:int; 
825  
826  
827 
let 
828  
829  
830  
831 
 set state as inactive 
832 
idD_D2_2 
833 
= if (not isInner) then 0 else idD_D2_1; 
834  
835  
836 
(idD_D2) 
837 
= (idD_D2_1); 
838 

839  
840 
tel 
841  
842  
843  
844  
845  
846  
847 
 Entry action for state :D2_D2b 
848 
node D2_D2b_en(idD_D2_1:int; 
849 
c_1:int; 
850 
dd_1:int; 
851 
isInner:bool) 
852  
853 
returns (idD_D2:int; 
854 
c:int; 
855 
dd:int); 
856  
857  
858 
var idD_D2_2:int; 
859 
dd_2:int; 
860  
861  
862 
let 
863  
864  
865  
866 
 set state as active 
867 
idD_D2_2 
868 
= 1670; 
869 

870  
871 
dd_2 
872 
= if (not isInner) then c_1 +8 
873 
else dd_1; 
874 

875  
876 
(idD_D2, c, dd) 
877 
= (idD_D2_2, c_1, dd_2); 
878 

879  
880 
tel 
881  
882  
883  
884  
885  
886 
 Exit action for state :D2_D2b 
887 
node D2_D2b_ex(idD_D2_1:int; 
888 
isInner:bool) 
889  
890 
returns (idD_D2:int); 
891  
892  
893 
var idD_D2_2:int; 
894  
895  
896 
let 
897  
898  
899  
900 
 set state as inactive 
901 
idD_D2_2 
902 
= if (not isInner) then 0 else idD_D2_1; 
903  
904  
905 
(idD_D2) 
906 
= (idD_D2_1); 
907 

908  
909 
tel 
910  
911  
912  
913  
914  
915  
916 
 Entry action for state :D_D2 
917 
node D_D2_en(idD_D2_1:int; 
918 
idCD_D_1:int; 
919 
c_1:int; 
920 
dd_1:int; 
921 
isInner:bool) 
922  
923 
returns (idD_D2:int; 
924 
idCD_D:int; 
925 
c:int; 
926 
dd:int); 
927  
928  
929 
var idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5, idD_D2_6:int; 
930 
idCD_D_2, idCD_D_3, idCD_D_4:int; 
931 
c_2, c_3, c_4, c_5, c_6:int; 
932 
dd_2, dd_3, dd_4, dd_5, dd_6:int; 
933  
934  
935 
let 
936  
937  
938  
939 
 set state as active 
940 
idCD_D_2 
941 
= 1668; 
942 

943  
944 

945 
 transition trace : 
946 
POINT__To__D2_D2a_1 
947 
(idD_D2_2, c_2, dd_2) 
948 
= D2_D2a_en(idD_D2_1, c_1, dd_1, false); 
949 

950  
951 
(idD_D2_3, idCD_D_3, c_3, dd_3) 
952 
= 
953  
954 
if ( idD_D2_1 = 0) then 
955  
956 
(idD_D2_2, idCD_D_2, c_2, dd_2) 
957  
958 
else(idD_D2_1, idCD_D_2, c_1, dd_1); 
959  
960 

961  
962 
(idD_D2_4, c_4, dd_4) 
963 
= 
964 
if ( idD_D2_1 = 1669) then 
965 
D2_D2a_en(idD_D2_1, c_1, dd_1, false) 
966 
else (idD_D2_1, c_1, dd_1); 
967  
968 

969  
970 
(idD_D2_5, c_5, dd_5) 
971 
= 
972 
if ( idD_D2_1 = 1670) then 
973 
D2_D2b_en(idD_D2_1, c_1, dd_1, false) 
974 
else (idD_D2_1, c_1, dd_1); 
975  
976 

977  
978 
(idD_D2_6, idCD_D_4, c_6, dd_6) 
979 
= 
980 
if ( idD_D2_1 = 0) then 
981 
(idD_D2_3, idCD_D_3, c_3, dd_3) 
982 
else 
983 
if ( idD_D2_1 = 1669) then 
984 
(idD_D2_4, idCD_D_3, c_4, dd_4) 
985 
else 
986 
if ( idD_D2_1 = 1670) then 
987 
(idD_D2_5, idCD_D_3, c_5, dd_5) 
988 
else (idD_D2_1, idCD_D_2, c_1, dd_1); 
989  
990  
991 
(idD_D2, idCD_D, c, dd) 
992 
= (idD_D2_6, idCD_D_4, c_6, dd_6); 
993 

994  
995 
tel 
996  
997  
998  
999  
1000  
1001 
 Exit action for state :D_D2 
1002 
node D_D2_ex(idD_D2_1:int; 
1003 
idCD_D_1:int; 
1004 
isInner:bool) 
1005  
1006 
returns (idD_D2:int; 
1007 
idCD_D:int); 
1008  
1009  
1010 
var idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5:int; 
1011 
idCD_D_2:int; 
1012  
1013  
1014 
let 
1015  
1016  
1017  
1018 

1019 
(idD_D2_2) 
1020 
= 
1021 
if ( idD_D2_1 = 1669) then 
1022 
D2_D2a_ex(idD_D2_1, false) 
1023 
else (idD_D2_1); 
1024  
1025 

1026  
1027 
(idD_D2_3) 
1028 
= 
1029 
if ( idD_D2_1 = 1670) then 
1030 
D2_D2b_ex(idD_D2_1, false) 
1031 
else (idD_D2_1); 
1032  
1033 

1034  
1035 
(idD_D2_4) 
1036 
= 
1037 
if ( idD_D2_1 = 1669) then 
1038 
(idD_D2_2) 
1039 
else 
1040 
if ( idD_D2_1 = 1670) then 
1041 
(idD_D2_3) 
1042 
else (idD_D2_1); 
1043  
1044  
1045 
 set state as inactive 
1046 
idCD_D_2 
1047 
= if (not isInner) then 0 else idCD_D_1; 
1048  
1049 
idD_D2_5 
1050 
= 0; 
1051 

1052  
1053 
(idD_D2, idCD_D) 
1054 
= (idD_D2_5, idCD_D_1); 
1055 

1056  
1057 
tel 
1058  
1059  
1060  
1061  
1062  
1063  
1064 
 Entry action for state :D1_D1a 
1065 
node D1_D1a_en(idD_D1_1:int; 
1066 
c_1:int; 
1067 
dd_1:int; 
1068 
isInner:bool) 
1069  
1070 
returns (idD_D1:int; 
1071 
c:int; 
1072 
dd:int); 
1073  
1074  
1075 
var idD_D1_2:int; 
1076 
dd_2:int; 
1077  
1078  
1079 
let 
1080  
1081  
1082  
1083 
 set state as active 
1084 
idD_D1_2 
1085 
= 1672; 
1086 

1087  
1088 
dd_2 
1089 
= if (not isInner) then c_1 +5 
1090 
else dd_1; 
1091 

1092  
1093 
(idD_D1, c, dd) 
1094 
= (idD_D1_2, c_1, dd_2); 
1095 

1096  
1097 
tel 
1098  
1099  
1100  
1101  
1102  
1103 
 Exit action for state :D1_D1a 
1104 
node D1_D1a_ex(idD_D1_1:int; 
1105 
isInner:bool) 
1106  
1107 
returns (idD_D1:int); 
1108  
1109  
1110 
var idD_D1_2:int; 
1111  
1112  
1113 
let 
1114  
1115  
1116  
1117 
 set state as inactive 
1118 
idD_D1_2 
1119 
= if (not isInner) then 0 else idD_D1_1; 
1120  
1121  
1122 
(idD_D1) 
1123 
= (idD_D1_1); 
1124 

1125  
1126 
tel 
1127  
1128  
1129  
1130  
1131  
1132  
1133 
 Entry action for state :D1_D1b 
1134 
node D1_D1b_en(idD_D1_1:int; 
1135 
c_1:int; 
1136 
dd_1:int; 
1137 
isInner:bool) 
1138  
1139 
returns (idD_D1:int; 
1140 
c:int; 
1141 
dd:int); 
1142  
1143  
1144 
var idD_D1_2:int; 
1145 
dd_2:int; 
1146  
1147  
1148 
let 
1149  
1150  
1151  
1152 
 set state as active 
1153 
idD_D1_2 
1154 
= 1673; 
1155 

1156  
1157 
dd_2 
1158 
= if (not isInner) then c_1 +6 
1159 
else dd_1; 
1160 

1161  
1162 
(idD_D1, c, dd) 
1163 
= (idD_D1_2, c_1, dd_2); 
1164 

1165  
1166 
tel 
1167  
1168  
1169  
1170  
1171  
1172 
 Exit action for state :D1_D1b 
1173 
node D1_D1b_ex(idD_D1_1:int; 
1174 
isInner:bool) 
1175  
1176 
returns (idD_D1:int); 
1177  
1178  
1179 
var idD_D1_2:int; 
1180  
1181  
1182 
let 
1183  
1184  
1185  
1186 
 set state as inactive 
1187 
idD_D1_2 
1188 
= if (not isInner) then 0 else idD_D1_1; 
1189  
1190  
1191 
(idD_D1) 
1192 
= (idD_D1_1); 
1193 

1194  
1195 
tel 
1196  
1197  
1198  
1199  
1200  
1201  
1202 
 Entry action for state :D_D1 
1203 
node D_D1_en(idD_D1_1:int; 
1204 
idCD_D_1:int; 
1205 
c_1:int; 
1206 
dd_1:int; 
1207 
isInner:bool) 
1208  
1209 
returns (idD_D1:int; 
1210 
idCD_D:int; 
1211 
c:int; 
1212 
dd:int); 
1213  
1214  
1215 
var idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5, idD_D1_6:int; 
1216 
idCD_D_2, idCD_D_3, idCD_D_4:int; 
1217 
c_2, c_3, c_4, c_5, c_6:int; 
1218 
dd_2, dd_3, dd_4, dd_5, dd_6:int; 
1219  
1220  
1221 
let 
1222  
1223  
1224  
1225 
 set state as active 
1226 
idCD_D_2 
1227 
= 1671; 
1228 

1229  
1230 

1231 
 transition trace : 
1232 
POINT__To__D1_D1a_1 
1233 
(idD_D1_2, c_2, dd_2) 
1234 
= D1_D1a_en(idD_D1_1, c_1, dd_1, false); 
1235 

1236  
1237 
(idD_D1_3, idCD_D_3, c_3, dd_3) 
1238 
= 
1239  
1240 
if ( idD_D1_1 = 0) then 
1241  
1242 
(idD_D1_2, idCD_D_2, c_2, dd_2) 
1243  
1244 
else(idD_D1_1, idCD_D_2, c_1, dd_1); 
1245  
1246 

1247  
1248 
(idD_D1_4, c_4, dd_4) 
1249 
= 
1250 
if ( idD_D1_1 = 1672) then 
1251 
D1_D1a_en(idD_D1_1, c_1, dd_1, false) 
1252 
else (idD_D1_1, c_1, dd_1); 
1253  
1254 

1255  
1256 
(idD_D1_5, c_5, dd_5) 
1257 
= 
1258 
if ( idD_D1_1 = 1673) then 
1259 
D1_D1b_en(idD_D1_1, c_1, dd_1, false) 
1260 
else (idD_D1_1, c_1, dd_1); 
1261  
1262 

1263  
1264 
(idD_D1_6, idCD_D_4, c_6, dd_6) 
1265 
= 
1266 
if ( idD_D1_1 = 0) then 
1267 
(idD_D1_3, idCD_D_3, c_3, dd_3) 
1268 
else 
1269 
if ( idD_D1_1 = 1672) then 
1270 
(idD_D1_4, idCD_D_3, c_4, dd_4) 
1271 
else 
1272 
if ( idD_D1_1 = 1673) then 
1273 
(idD_D1_5, idCD_D_3, c_5, dd_5) 
1274 
else (idD_D1_1, idCD_D_2, c_1, dd_1); 
1275  
1276  
1277 
(idD_D1, idCD_D, c, dd) 
1278 
= (idD_D1_6, idCD_D_4, c_6, dd_6); 
1279 

1280  
1281 
tel 
1282  
1283  
1284  
1285  
1286  
1287 
 Exit action for state :D_D1 
1288 
node D_D1_ex(idD_D1_1:int; 
1289 
idCD_D_1:int; 
1290 
isInner:bool) 
1291  
1292 
returns (idD_D1:int; 
1293 
idCD_D:int); 
1294  
1295  
1296 
var idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int; 
1297 
idCD_D_2:int; 
1298  
1299  
1300 
let 
1301  
1302  
1303  
1304 

1305 
(idD_D1_2) 
1306 
= 
1307 
if ( idD_D1_1 = 1672) then 
1308 
D1_D1a_ex(idD_D1_1, false) 
1309 
else (idD_D1_1); 
1310  
1311 

1312  
1313 
(idD_D1_3) 
1314 
= 
1315 
if ( idD_D1_1 = 1673) then 
1316 
D1_D1b_ex(idD_D1_1, false) 
1317 
else (idD_D1_1); 
1318  
1319 

1320  
1321 
(idD_D1_4) 
1322 
= 
1323 
if ( idD_D1_1 = 1672) then 
1324 
(idD_D1_2) 
1325 
else 
1326 
if ( idD_D1_1 = 1673) then 
1327 
(idD_D1_3) 
1328 
else (idD_D1_1); 
1329  
1330  
1331 
 set state as inactive 
1332 
idCD_D_2 
1333 
= if (not isInner) then 0 else idCD_D_1; 
1334  
1335 
idD_D1_5 
1336 
= 0; 
1337 

1338  
1339 
(idD_D1, idCD_D) 
1340 
= (idD_D1_5, idCD_D_1); 
1341 

1342  
1343 
tel 
1344  
1345  
1346  
1347  
1348  
1349  
1350 
 Entry action for state :CD_D 
1351 
node CD_D_en(idCD_D_1:int; 
1352 
idParallel4_CD_1:int; 
1353 
c_1:int; 
1354 
dd_1:int; 
1355 
idD_D1_1:int; 
1356 
idD_D2_1:int; 
1357 
isInner:bool) 
1358  
1359 
returns (idCD_D:int; 
1360 
idParallel4_CD:int; 
1361 
c:int; 
1362 
dd:int; 
1363 
idD_D1:int; 
1364 
idD_D2:int); 
1365  
1366  
1367 
var idCD_D_2, idCD_D_3, idCD_D_4, idCD_D_5, idCD_D_6:int; 
1368 
idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4:int; 
1369 
c_2, c_3, c_4, c_5, c_6:int; 
1370 
dd_2, dd_3, dd_4, dd_5, dd_6:int; 
1371 
idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int; 
1372 
idD_D2_2, idD_D2_3:int; 
1373  
1374  
1375 
let 
1376  
1377  
1378  
1379 
 set state as active 
1380 
idParallel4_CD_2 
1381 
= 1667; 
1382 

1383  
1384 

1385 
 transition trace : 
1386 
POINT__To__D_D1_1 
1387 
(idD_D1_2, idCD_D_2, c_2, dd_2) 
1388 
= D_D1_en(idD_D1_1, idCD_D_1, c_1, dd_1, false); 
1389 

1390  
1391 
(idCD_D_3, idParallel4_CD_3, c_3, dd_3, idD_D1_3) 
1392 
= 
1393  
1394 
if ( idCD_D_1 = 0) then 
1395  
1396 
(idCD_D_2, idParallel4_CD_2, c_2, dd_2, idD_D1_2) 
1397  
1398 
else(idCD_D_1, idParallel4_CD_2, c_1, dd_1, idD_D1_1); 
1399  
1400 

1401  
1402 
(idD_D2_2, idCD_D_4, c_4, dd_4) 
1403 
= 
1404 
if ( idCD_D_1 = 1668) then 
1405 
D_D2_en(idD_D2_1, idCD_D_1, c_1, dd_1, false) 
1406 
else (idD_D2_1, idCD_D_1, c_1, dd_1); 
1407  
1408 

1409  
1410 
(idD_D1_4, idCD_D_5, c_5, dd_5) 
1411 
= 
1412 
if ( idCD_D_1 = 1671) then 
1413 
D_D1_en(idD_D1_1, idCD_D_1, c_1, dd_1, false) 
1414 
else (idD_D1_1, idCD_D_1, c_1, dd_1); 
1415  
1416 

1417  
1418 
(idCD_D_6, idParallel4_CD_4, c_6, dd_6, idD_D1_5, idD_D2_3) 
1419 
= 
1420 
if ( idCD_D_1 = 0) then 
1421 
(idCD_D_3, idParallel4_CD_3, c_3, dd_3, idD_D1_3, idD_D2_1) 
1422 
else 
1423 
if ( idCD_D_1 = 1668) then 
1424 
(idCD_D_4, idParallel4_CD_3, c_4, dd_4, idD_D1_1, idD_D2_2) 
1425 
else 
1426 
if ( idCD_D_1 = 1671) then 
1427 
(idCD_D_5, idParallel4_CD_3, c_5, dd_5, idD_D1_4, idD_D2_1) 
1428 
else (idCD_D_1, idParallel4_CD_2, c_1, dd_1, idD_D1_1, idD_D2_1); 
1429  
1430  
1431 
(idCD_D, idParallel4_CD, c, dd, idD_D1, idD_D2) 
1432 
= (idCD_D_6, idParallel4_CD_4, c_6, dd_6, idD_D1_5, idD_D2_3); 
1433 

1434  
1435 
tel 
1436  
1437  
1438  
1439  
1440  
1441 
 Exit action for state :CD_D 
1442 
node CD_D_ex(idD_D2_1:int; 
1443 
idCD_D_1:int; 
1444 
idD_D1_1:int; 
1445 
idParallel4_CD_1:int; 
1446 
isInner:bool) 
1447  
1448 
returns (idD_D2:int; 
1449 
idCD_D:int; 
1450 
idD_D1:int; 
1451 
idParallel4_CD:int); 
1452  
1453  
1454 
var idD_D2_2, idD_D2_3:int; 
1455 
idCD_D_2, idCD_D_3, idCD_D_4, idCD_D_5:int; 
1456 
idD_D1_2, idD_D1_3:int; 
1457 
idParallel4_CD_2:int; 
1458  
1459  
1460 
let 
1461  
1462  
1463  
1464 

1465 
(idD_D2_2, idCD_D_2) 
1466 
= 
1467 
if ( idCD_D_1 = 1668) then 
1468 
D_D2_ex(idD_D2_1, idCD_D_1, false) 
1469 
else (idD_D2_1, idCD_D_1); 
1470  
1471 

1472  
1473 
(idD_D1_2, idCD_D_3) 
1474 
= 
1475 
if ( idCD_D_1 = 1671) then 
1476 
D_D1_ex(idD_D1_1, idCD_D_1, false) 
1477 
else (idD_D1_1, idCD_D_1); 
1478  
1479 

1480  
1481 
(idD_D2_3, idCD_D_4, idD_D1_3) 
1482 
= 
1483 
if ( idCD_D_1 = 1668) then 
1484 
(idD_D2_2, idCD_D_2, idD_D1_1) 
1485 
else 
1486 
if ( idCD_D_1 = 1671) then 
1487 
(idD_D2_1, idCD_D_3, idD_D1_2) 
1488 
else (idD_D2_1, idCD_D_1, idD_D1_1); 
1489  
1490  
1491 
 set state as inactive 
1492 
idParallel4_CD_2 
1493 
= if (not isInner) then 0 else idParallel4_CD_1; 
1494  
1495 
idCD_D_5 
1496 
= 0; 
1497 

1498  
1499 
(idD_D2, idCD_D, idD_D1, idParallel4_CD) 
1500 
= (idD_D2_3, idCD_D_5, idD_D1_3, idParallel4_CD_1); 
1501 

1502  
1503 
tel 
1504  
1505  
1506  
1507  
1508  
1509  
1510 
 Entry action for state :C2_C2a 
1511 
node C2_C2a_en(idC_C2_1:int; 
1512 
b_1:int; 
1513 
c_1:int; 
1514 
isInner:bool) 
1515  
1516 
returns (idC_C2:int; 
1517 
b:int; 
1518 
c:int); 
1519  
1520  
1521 
var idC_C2_2:int; 
1522 
c_2:int; 
1523  
1524  
1525 
let 
1526  
1527  
1528  
1529 
 set state as active 
1530 
idC_C2_2 
1531 
= 1662; 
1532 

1533  
1534 
c_2 
1535 
= if (not isInner) then b_1 +3 
1536 
else c_1; 
1537 

1538  
1539 
(idC_C2, b, c) 
1540 
= (idC_C2_2, b_1, c_2); 
1541 

1542  
1543 
tel 
1544  
1545  
1546  
1547  
1548  
1549 
 Exit action for state :C2_C2a 
1550 
node C2_C2a_ex(idC_C2_1:int; 
1551 
isInner:bool) 
1552  
1553 
returns (idC_C2:int); 
1554  
1555  
1556 
var idC_C2_2:int; 
1557  
1558  
1559 
let 
1560  
1561  
1562  
1563 
 set state as inactive 
1564 
idC_C2_2 
1565 
= if (not isInner) then 0 else idC_C2_1; 
1566  
1567  
1568 
(idC_C2) 
1569 
= (idC_C2_1); 
1570 

1571  
1572 
tel 
1573  
1574  
1575  
1576  
1577  
1578  
1579 
 Entry action for state :C2_C2b 
1580 
node C2_C2b_en(idC_C2_1:int; 
1581 
b_1:int; 
1582 
c_1:int; 
1583 
isInner:bool) 
1584  
1585 
returns (idC_C2:int; 
1586 
b:int; 
1587 
c:int); 
1588  
1589  
1590 
var idC_C2_2:int; 
1591 
c_2:int; 
1592  
1593  
1594 
let 
1595  
1596  
1597  
1598 
 set state as active 
1599 
idC_C2_2 
1600 
= 1663; 
1601 

1602  
1603 
c_2 
1604 
= if (not isInner) then b_1 +4 
1605 
else c_1; 
1606 

1607  
1608 
(idC_C2, b, c) 
1609 
= (idC_C2_2, b_1, c_2); 
1610 

1611  
1612 
tel 
1613  
1614  
1615  
1616  
1617  
1618 
 Exit action for state :C2_C2b 
1619 
node C2_C2b_ex(idC_C2_1:int; 
1620 
isInner:bool) 
1621  
1622 
returns (idC_C2:int); 
1623  
1624  
1625 
var idC_C2_2:int; 
1626  
1627  
1628 
let 
1629  
1630  
1631  
1632 
 set state as inactive 
1633 
idC_C2_2 
1634 
= if (not isInner) then 0 else idC_C2_1; 
1635  
1636  
1637 
(idC_C2) 
1638 
= (idC_C2_1); 
1639 

1640  
1641 
tel 
1642  
1643  
1644  
1645  
1646  
1647  
1648 
 Entry action for state :C_C2 
1649 
node C_C2_en(idC_C2_1:int; 
1650 
idCD_C_1:int; 
1651 
b_1:int; 
1652 
c_1:int; 
1653 
isInner:bool) 
1654  
1655 
returns (idC_C2:int; 
1656 
idCD_C:int; 
1657 
b:int; 
1658 
c:int); 
1659  
1660  
1661 
var idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5, idC_C2_6:int; 
1662 
idCD_C_2, idCD_C_3, idCD_C_4:int; 
1663 
b_2, b_3, b_4, b_5, b_6:int; 
1664 
c_2, c_3, c_4, c_5, c_6:int; 
1665  
1666  
1667 
let 
1668  
1669  
1670  
1671 
 set state as active 
1672 
idCD_C_2 
1673 
= 1661; 
1674 

1675  
1676 

1677 
 transition trace : 
1678 
POINT__To__C2_C2a_1 
1679 
(idC_C2_2, b_2, c_2) 
1680 
= C2_C2a_en(idC_C2_1, b_1, c_1, false); 
1681 

1682  
1683 
(idC_C2_3, idCD_C_3, b_3, c_3) 
1684 
= 
1685  
1686 
if ( idC_C2_1 = 0) then 
1687  
1688 
(idC_C2_2, idCD_C_2, b_2, c_2) 
1689  
1690 
else(idC_C2_1, idCD_C_2, b_1, c_1); 
1691  
1692 

1693  
1694 
(idC_C2_4, b_4, c_4) 
1695 
= 
1696 
if ( idC_C2_1 = 1662) then 
1697 
C2_C2a_en(idC_C2_1, b_1, c_1, false) 
1698 
else (idC_C2_1, b_1, c_1); 
1699  
1700 

1701  
1702 
(idC_C2_5, b_5, c_5) 
1703 
= 
1704 
if ( idC_C2_1 = 1663) then 
1705 
C2_C2b_en(idC_C2_1, b_1, c_1, false) 
1706 
else (idC_C2_1, b_1, c_1); 
1707  
1708 

1709  
1710 
(idC_C2_6, idCD_C_4, b_6, c_6) 
1711 
= 
1712 
if ( idC_C2_1 = 0) then 
1713 
(idC_C2_3, idCD_C_3, b_3, c_3) 
1714 
else 
1715 
if ( idC_C2_1 = 1662) then 
1716 
(idC_C2_4, idCD_C_3, b_4, c_4) 
1717 
else 
1718 
if ( idC_C2_1 = 1663) then 
1719 
(idC_C2_5, idCD_C_3, b_5, c_5) 
1720 
else (idC_C2_1, idCD_C_2, b_1, c_1); 
1721  
1722  
1723 
(idC_C2, idCD_C, b, c) 
1724 
= (idC_C2_6, idCD_C_4, b_6, c_6); 
1725 

1726  
1727 
tel 
1728  
1729  
1730  
1731  
1732  
1733 
 Exit action for state :C_C2 
1734 
node C_C2_ex(idC_C2_1:int; 
1735 
idCD_C_1:int; 
1736 
isInner:bool) 
1737  
1738 
returns (idC_C2:int; 
1739 
idCD_C:int); 
1740  
1741  
1742 
var idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5:int; 
1743 
idCD_C_2:int; 
1744  
1745  
1746 
let 
1747  
1748  
1749  
1750 

1751 
(idC_C2_2) 
1752 
= 
1753 
if ( idC_C2_1 = 1662) then 
1754 
C2_C2a_ex(idC_C2_1, false) 
1755 
else (idC_C2_1); 
1756  
1757 

1758  
1759 
(idC_C2_3) 
1760 
= 
1761 
if ( idC_C2_1 = 1663) then 
1762 
C2_C2b_ex(idC_C2_1, false) 
1763 
else (idC_C2_1); 
1764  
1765 

1766  
1767 
(idC_C2_4) 
1768 
= 
1769 
if ( idC_C2_1 = 1662) then 
1770 
(idC_C2_2) 
1771 
else 
1772 
if ( idC_C2_1 = 1663) then 
1773 
(idC_C2_3) 
1774 
else (idC_C2_1); 
1775  
1776  
1777 
 set state as inactive 
1778 
idCD_C_2 
1779 
= if (not isInner) then 0 else idCD_C_1; 
1780  
1781 
idC_C2_5 
1782 
= 0; 
1783 

1784  
1785 
(idC_C2, idCD_C) 
1786 
= (idC_C2_5, idCD_C_1); 
1787 

1788  
1789 
tel 
1790  
1791  
1792  
1793  
1794  
1795  
1796 
 Entry action for state :C1_C1a 
1797 
node C1_C1a_en(idC_C1_1:int; 
1798 
b_1:int; 
1799 
c_1:int; 
1800 
isInner:bool) 
1801  
1802 
returns (idC_C1:int; 
1803 
b:int; 
1804 
c:int); 
1805  
1806  
1807 
var idC_C1_2:int; 
1808 
c_2:int; 
1809  
1810  
1811 
let 
1812  
1813  
1814  
1815 
 set state as active 
1816 
idC_C1_2 
1817 
= 1665; 
1818 

1819  
1820 
c_2 
1821 
= if (not isInner) then b_1 +1 
1822 
else c_1; 
1823 

1824  
1825 
(idC_C1, b, c) 
1826 
= (idC_C1_2, b_1, c_2); 
1827 

1828  
1829 
tel 
1830  
1831  
1832  
1833  
1834  
1835 
 Exit action for state :C1_C1a 
1836 
node C1_C1a_ex(idC_C1_1:int; 
1837 
isInner:bool) 
1838  
1839 
returns (idC_C1:int); 
1840  
1841  
1842 
var idC_C1_2:int; 
1843  
1844  
1845 
let 
1846  
1847  
1848  
1849 
 set state as inactive 
1850 
idC_C1_2 
1851 
= if (not isInner) then 0 else idC_C1_1; 
1852  
1853  
1854 
(idC_C1) 
1855 
= (idC_C1_1); 
1856 

1857  
1858 
tel 
1859  
1860  
1861  
1862  
1863  
1864  
1865 
 Entry action for state :C1_C1b 
1866 
node C1_C1b_en(idC_C1_1:int; 
1867 
b_1:int; 
1868 
c_1:int; 
1869 
isInner:bool) 
1870  
1871 
returns (idC_C1:int; 
1872 
b:int; 
1873 
c:int); 
1874  
1875  
1876 
var idC_C1_2:int; 
1877 
c_2:int; 
1878  
1879  
1880 
let 
1881  
1882  
1883  
1884 
 set state as active 
1885 
idC_C1_2 
1886 
= 1666; 
1887 

1888  
1889 
c_2 
1890 
= if (not isInner) then b_1 +2 
1891 
else c_1; 
1892 

1893  
1894 
(idC_C1, b, c) 
1895 
= (idC_C1_2, b_1, c_2); 
1896 

1897  
1898 
tel 
1899  
1900  
1901  
1902  
1903  
1904 
 Exit action for state :C1_C1b 
1905 
node C1_C1b_ex(idC_C1_1:int; 
1906 
isInner:bool) 
1907  
1908 
returns (idC_C1:int); 
1909  
1910  
1911 
var idC_C1_2:int; 
1912  
1913  
1914 
let 
1915  
1916  
1917  
1918 
 set state as inactive 
1919 
idC_C1_2 
1920 
= if (not isInner) then 0 else idC_C1_1; 
1921  
1922  
1923 
(idC_C1) 
1924 
= (idC_C1_1); 
1925 

1926  
1927 
tel 
1928  
1929  
1930  
1931  
1932  
1933  
1934 
 Entry action for state :C_C1 
1935 
node C_C1_en(idC_C1_1:int; 
1936 
idCD_C_1:int; 
1937 
b_1:int; 
1938 
c_1:int; 
1939 
isInner:bool) 
1940  
1941 
returns (idC_C1:int; 
1942 
idCD_C:int; 
1943 
b:int; 
1944 
c:int); 
1945  
1946  
1947 
var idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5, idC_C1_6:int; 
1948 
idCD_C_2, idCD_C_3, idCD_C_4:int; 
1949 
b_2, b_3, b_4, b_5, b_6:int; 
1950 
c_2, c_3, c_4, c_5, c_6:int; 
1951  
1952  
1953 
let 
1954  
1955  
1956  
1957 
 set state as active 
1958 
idCD_C_2 
1959 
= 1664; 
1960 

1961  
1962 

1963 
 transition trace : 
1964 
POINT__To__C1_C1a_1 
1965 
(idC_C1_2, b_2, c_2) 
1966 
= C1_C1a_en(idC_C1_1, b_1, c_1, false); 
1967 

1968  
1969 
(idC_C1_3, idCD_C_3, b_3, c_3) 
1970 
= 
1971  
1972 
if ( idC_C1_1 = 0) then 
1973  
1974 
(idC_C1_2, idCD_C_2, b_2, c_2) 
1975  
1976 
else(idC_C1_1, idCD_C_2, b_1, c_1); 
1977  
1978 

1979  
1980 
(idC_C1_4, b_4, c_4) 
1981 
= 
1982 
if ( idC_C1_1 = 1665) then 
1983 
C1_C1a_en(idC_C1_1, b_1, c_1, false) 
1984 
else (idC_C1_1, b_1, c_1); 
1985  
1986 

1987  
1988 
(idC_C1_5, b_5, c_5) 
1989 
= 
1990 
if ( idC_C1_1 = 1666) then 
1991 
C1_C1b_en(idC_C1_1, b_1, c_1, false) 
1992 
else (idC_C1_1, b_1, c_1); 
1993  
1994 

1995  
1996 
(idC_C1_6, idCD_C_4, b_6, c_6) 
1997 
= 
1998 
if ( idC_C1_1 = 0) then 
1999 
(idC_C1_3, idCD_C_3, b_3, c_3) 
2000 
else 
2001 
if ( idC_C1_1 = 1665) then 
2002 
(idC_C1_4, idCD_C_3, b_4, c_4) 
2003 
else 
2004 
if ( idC_C1_1 = 1666) then 
2005 
(idC_C1_5, idCD_C_3, b_5, c_5) 
2006 
else (idC_C1_1, idCD_C_2, b_1, c_1); 
2007  
2008  
2009 
(idC_C1, idCD_C, b, c) 
2010 
= (idC_C1_6, idCD_C_4, b_6, c_6); 
2011 

2012  
2013 
tel 
2014  
2015  
2016  
2017  
2018  
2019 
 Exit action for state :C_C1 
2020 
node C_C1_ex(idC_C1_1:int; 
2021 
idCD_C_1:int; 
2022 
isInner:bool) 
2023  
2024 
returns (idC_C1:int; 
2025 
idCD_C:int); 
2026  
2027  
2028 
var idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int; 
2029 
idCD_C_2:int; 
2030  
2031  
2032 
let 
2033  
2034  
2035  
2036 

2037 
(idC_C1_2) 
2038 
= 
2039 
if ( idC_C1_1 = 1665) then 
2040 
C1_C1a_ex(idC_C1_1, false) 
2041 
else (idC_C1_1); 
2042  
2043 

2044  
2045 
(idC_C1_3) 
2046 
= 
2047 
if ( idC_C1_1 = 1666) then 
2048 
C1_C1b_ex(idC_C1_1, false) 
2049 
else (idC_C1_1); 
2050  
2051 

2052  
2053 
(idC_C1_4) 
2054 
= 
2055 
if ( idC_C1_1 = 1665) then 
2056 
(idC_C1_2) 
2057 
else 
2058 
if ( idC_C1_1 = 1666) then 
2059 
(idC_C1_3) 
2060 
else (idC_C1_1); 
2061  
2062  
2063 
 set state as inactive 
2064 
idCD_C_2 
2065 
= if (not isInner) then 0 else idCD_C_1; 
2066  
2067 
idC_C1_5 
2068 
= 0; 
2069 

2070  
2071 
(idC_C1, idCD_C) 
2072 
= (idC_C1_5, idCD_C_1); 
2073 

2074  
2075 
tel 
2076  
2077  
2078  
2079  
2080  
2081  
2082 
 Entry action for state :CD_C 
2083 
node CD_C_en(idCD_C_1:int; 
2084 
idParallel4_CD_1:int; 
2085 
b_1:int; 
2086 
c_1:int; 
2087 
idC_C1_1:int; 
2088 
idC_C2_1:int; 
2089 
isInner:bool) 
2090  
2091 
returns (idCD_C:int; 
2092 
idParallel4_CD:int; 
2093 
b:int; 
2094 
c:int; 
2095 
idC_C1:int; 
2096 
idC_C2:int); 
2097  
2098  
2099 
var idCD_C_2, idCD_C_3, idCD_C_4, idCD_C_5, idCD_C_6:int; 
2100 
idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4:int; 
2101 
b_2, b_3, b_4, b_5, b_6:int; 
2102 
c_2, c_3, c_4, c_5, c_6:int; 
2103 
idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int; 
2104 
idC_C2_2, idC_C2_3:int; 
2105  
2106  
2107 
let 
2108  
2109  
2110  
2111 
 set state as active 
2112 
idParallel4_CD_2 
2113 
= 1660; 
2114 

2115  
2116 

2117 
 transition trace : 
2118 
POINT__To__C_C1_1 
2119 
(idC_C1_2, idCD_C_2, b_2, c_2) 
2120 
= C_C1_en(idC_C1_1, idCD_C_1, b_1, c_1, false); 
2121 

2122  
2123 
(idCD_C_3, idParallel4_CD_3, b_3, c_3, idC_C1_3) 
2124 
= 
2125  
2126 
if ( idCD_C_1 = 0) then 
2127  
2128 
(idCD_C_2, idParallel4_CD_2, b_2, c_2, idC_C1_2) 
2129  
2130 
else(idCD_C_1, idParallel4_CD_2, b_1, c_1, idC_C1_1); 
2131  
2132 

2133  
2134 
(idC_C2_2, idCD_C_4, b_4, c_4) 
2135 
= 
2136 
if ( idCD_C_1 = 1661) then 
2137 
C_C2_en(idC_C2_1, idCD_C_1, b_1, c_1, false) 
2138 
else (idC_C2_1, idCD_C_1, b_1, c_1); 
2139  
2140 

2141  
2142 
(idC_C1_4, idCD_C_5, b_5, c_5) 
2143 
= 
2144 
if ( idCD_C_1 = 1664) then 
2145 
C_C1_en(idC_C1_1, idCD_C_1, b_1, c_1, false) 
2146 
else (idC_C1_1, idCD_C_1, b_1, c_1); 
2147  
2148 

2149  
2150 
(idCD_C_6, idParallel4_CD_4, b_6, c_6, idC_C1_5, idC_C2_3) 
2151 
= 
2152 
if ( idCD_C_1 = 0) then 
2153 
(idCD_C_3, idParallel4_CD_3, b_3, c_3, idC_C1_3, idC_C2_1) 
2154 
else 
2155 
if ( idCD_C_1 = 1661) then 
2156 
(idCD_C_4, idParallel4_CD_3, b_4, c_4, idC_C1_1, idC_C2_2) 
2157 
else 
2158 
if ( idCD_C_1 = 1664) then 
2159 
(idCD_C_5, idParallel4_CD_3, b_5, c_5, idC_C1_4, idC_C2_1) 
2160 
else (idCD_C_1, idParallel4_CD_2, b_1, c_1, idC_C1_1, idC_C2_1); 
2161  
2162  
2163 
(idCD_C, idParallel4_CD, b, c, idC_C1, idC_C2) 
2164 
= (idCD_C_6, idParallel4_CD_4, b_6, c_6, idC_C1_5, idC_C2_3); 
2165 

2166  
2167 
tel 
2168  
2169  
2170  
2171  
2172  
2173 
 Exit action for state :CD_C 
2174 
node CD_C_ex(idC_C2_1:int; 
2175 
idCD_C_1:int; 
2176 
idC_C1_1:int; 
2177 
idParallel4_CD_1:int; 
2178 
isInner:bool) 
2179  
2180 
returns (idC_C2:int; 
2181 
idCD_C:int; 
2182 
idC_C1:int; 
2183 
idParallel4_CD:int); 
2184  
2185  
2186 
var idC_C2_2, idC_C2_3:int; 
2187 
idCD_C_2, idCD_C_3, idCD_C_4, idCD_C_5:int; 
2188 
idC_C1_2, idC_C1_3:int; 
2189 
idParallel4_CD_2:int; 
2190  
2191  
2192 
let 
2193  
2194  
2195  
2196 

2197 
(idC_C2_2, idCD_C_2) 
2198 
= 
2199 
if ( idCD_C_1 = 1661) then 
2200 
C_C2_ex(idC_C2_1, idCD_C_1, false) 
2201 
else (idC_C2_1, idCD_C_1); 
2202  
2203 

2204  
2205 
(idC_C1_2, idCD_C_3) 
2206 
= 
2207 
if ( idCD_C_1 = 1664) then 
2208 
C_C1_ex(idC_C1_1, idCD_C_1, false) 
2209 
else (idC_C1_1, idCD_C_1); 
2210  
2211 

2212  
2213 
(idC_C2_3, idCD_C_4, idC_C1_3) 
2214 
= 
2215 
if ( idCD_C_1 = 1661) then 
2216 
(idC_C2_2, idCD_C_2, idC_C1_1) 
2217 
else 
2218 
if ( idCD_C_1 = 1664) then 
2219 
(idC_C2_1, idCD_C_3, idC_C1_2) 
2220 
else (idC_C2_1, idCD_C_1, idC_C1_1); 
2221  
2222  
2223 
 set state as inactive 
2224 
idParallel4_CD_2 
2225 
= if (not isInner) then 0 else idParallel4_CD_1; 
2226  
2227 
idCD_C_5 
2228 
= 0; 
2229 

2230  
2231 
(idC_C2, idCD_C, idC_C1, idParallel4_CD) 
2232 
= (idC_C2_3, idCD_C_5, idC_C1_3, idParallel4_CD_1); 
2233 

2234  
2235 
tel 
2236  
2237  
2238  
2239  
2240  
2241  
2242 
 Entry action for state :Parallel4_CD 
2243 
node Parallel4_CD_en(idParallel4_CD_1:int; 
2244 
idParallel4_Parallel4_1:int; 
2245 
b_1:int; 
2246 
c_1:int; 
2247 
idCD_C_1:int; 
2248 
idC_C1_1:int; 
2249 
idC_C2_1:int; 
2250 
dd_1:int; 
2251 
idCD_D_1:int; 
2252 
idD_D1_1:int; 
2253 
idD_D2_1:int; 
2254 
isInner:bool) 
2255  
2256 
returns (idParallel4_CD:int; 
2257 
idParallel4_Parallel4:int; 
2258 
b:int; 
2259 
c:int; 
2260 
idCD_C:int; 
2261 
idC_C1:int; 
2262 
idC_C2:int; 
2263 
dd:int; 
2264 
idCD_D:int; 
2265 
idD_D1:int; 
2266 
idD_D2:int); 
2267  
2268  
2269 
var idParallel4_CD_2, idParallel4_CD_3:int; 
2270 
idParallel4_Parallel4_2:int; 
2271 
b_2:int; 
2272 
c_2, c_3:int; 
2273 
idCD_C_2:int; 
2274 
idC_C1_2:int; 
2275 
idC_C2_2:int; 
2276 
dd_2:int; 
2277 
idCD_D_2:int; 
2278 
idD_D1_2:int; 
2279 
idD_D2_2:int; 
2280  
2281  
2282 
let 
2283  
2284  
2285  
2286 
 set state as active 
2287 
idParallel4_Parallel4_2 
2288 
= 1674; 
2289 

2290  
2291 

2292 
(idCD_C_2, idParallel4_CD_2, b_2, c_2, idC_C1_2, idC_C2_2) 
2293 
= CD_C_en(idCD_C_1, idParallel4_CD_1, b_1, c_1, idC_C1_1, idC_C2_1, false); 
2294  
2295 
(idCD_D_2, idParallel4_CD_3, c_3, dd_2, idD_D1_2, idD_D2_2) 
2296 
= CD_D_en(idCD_D_1, idParallel4_CD_2, c_2, dd_1, idD_D1_1, idD_D2_1, false); 
2297  
2298  
2299 
(idParallel4_CD, idParallel4_Parallel4, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
2300 
= (idParallel4_CD_3, idParallel4_Parallel4_2, b_2, c_3, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2); 
2301 

2302  
2303 
tel 
2304  
2305  
2306  
2307  
2308  
2309 
 Exit action for state :Parallel4_CD 
2310 
node Parallel4_CD_ex(idD_D2_1:int; 
2311 
idCD_D_1:int; 
2312 
idD_D1_1:int; 
2313 
idParallel4_CD_1:int; 
2314 
idCD_C_1:int; 
2315 
idC_C1_1:int; 
2316 
idC_C2_1:int; 
2317 
idParallel4_Parallel4_1:int; 
2318 
isInner:bool) 
2319  
2320 
returns (idD_D2:int; 
2321 
idCD_D:int; 
2322 
idD_D1:int; 
2323 
idParallel4_CD:int; 
2324 
idCD_C:int; 
2325 
idC_C1:int; 
2326 
idC_C2:int; 
2327 
idParallel4_Parallel4:int); 
2328  
2329  
2330 
var idD_D2_2:int; 
2331 
idCD_D_2:int; 
2332 
idD_D1_2:int; 
2333 
idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4:int; 
2334 
idCD_C_2:int; 
2335 
idC_C1_2:int; 
2336 
idC_C2_2:int; 
2337 
idParallel4_Parallel4_2:int; 
2338  
2339  
2340 
let 
2341  
2342  
2343  
2344 

2345 
(idD_D2_2, idCD_D_2, idD_D1_2, idParallel4_CD_2) 
2346 
= CD_D_ex(idD_D2_1, idCD_D_1, idD_D1_1, idParallel4_CD_1, false); 
2347  
2348 
(idC_C2_2, idCD_C_2, idC_C1_2, idParallel4_CD_3) 
2349 
= CD_C_ex(idC_C2_1, idCD_C_1, idC_C1_1, idParallel4_CD_2, false); 
2350  
2351  
2352 
 set state as inactive 
2353 
idParallel4_Parallel4_2 
2354 
= if (not isInner) then 0 else idParallel4_Parallel4_1; 
2355  
2356 
idParallel4_CD_4 
2357 
= 0; 
2358 

2359  
2360 
(idD_D2, idCD_D, idD_D1, idParallel4_CD, idCD_C, idC_C1, idC_C2, idParallel4_Parallel4) 
2361 
= (idD_D2_2, idCD_D_2, idD_D1_2, idParallel4_CD_4, idCD_C_2, idC_C1_2, idC_C2_2, idParallel4_Parallel4_1); 
2362 

2363  
2364 
tel 
2365  
2366  
2367  
2368  
2369  
2370  
2371 
 Entry action for state :A2_A2a 
2372 
node A2_A2a_en(idA_A2_1:int; 
2373 
x:int; 
2374 
a_1:int; 
2375 
isInner:bool) 
2376  
2377 
returns (idA_A2:int; 
2378 
a:int); 
2379  
2380  
2381 
var idA_A2_2:int; 
2382 
a_2:int; 
2383  
2384  
2385 
let 
2386  
2387  
2388  
2389 
 set state as active 
2390 
idA_A2_2 
2391 
= 1651; 
2392 

2393  
2394 
a_2 
2395 
= if (not isInner) then x+3 
2396 
else a_1; 
2397 

2398  
2399 
(idA_A2, a) 
2400 
= (idA_A2_2, a_2); 
2401 

2402  
2403 
tel 
2404  
2405  
2406  
2407  
2408  
2409 
 Exit action for state :A2_A2a 
2410 
node A2_A2a_ex(idA_A2_1:int; 
2411 
isInner:bool) 
2412  
2413 
returns (idA_A2:int); 
2414  
2415  
2416 
var idA_A2_2:int; 
2417  
2418  
2419 
let 
2420  
2421  
2422  
2423 
 set state as inactive 
2424 
idA_A2_2 
2425 
= if (not isInner) then 0 else idA_A2_1; 
2426  
2427  
2428 
(idA_A2) 
2429 
= (idA_A2_1); 
2430 

2431  
2432 
tel 
2433  
2434  
2435  
2436  
2437  
2438  
2439 
 Entry action for state :A2_A2b 
2440 
node A2_A2b_en(idA_A2_1:int; 
2441 
x:int; 
2442 
a_1:int; 
2443 
isInner:bool) 
2444  
2445 
returns (idA_A2:int; 
2446 
a:int); 
2447  
2448  
2449 
var idA_A2_2:int; 
2450 
a_2:int; 
2451  
2452  
2453 
let 
2454  
2455  
2456  
2457 
 set state as active 
2458 
idA_A2_2 
2459 
= 1652; 
2460 

2461  
2462 
a_2 
2463 
= if (not isInner) then x+4 
2464 
else a_1; 
2465 

2466  
2467 
(idA_A2, a) 
2468 
= (idA_A2_2, a_2); 
2469 

2470  
2471 
tel 
2472  
2473  
2474  
2475  
2476  
2477 
 Exit action for state :A2_A2b 
2478 
node A2_A2b_ex(idA_A2_1:int; 
2479 
isInner:bool) 
2480  
2481 
returns (idA_A2:int); 
2482  
2483  
2484 
var idA_A2_2:int; 
2485  
2486  
2487 
let 
2488  
2489  
2490  
2491 
 set state as inactive 
2492 
idA_A2_2 
2493 
= if (not isInner) then 0 else idA_A2_1; 
2494  
2495  
2496 
(idA_A2) 
2497 
= (idA_A2_1); 
2498 

2499  
2500 
tel 
2501  
2502  
2503  
2504  
2505  
2506  
2507 
 Entry action for state :A_A2 
2508 
node A_A2_en(idA_A2_1:int; 
2509 
idParallel4_A_1:int; 
2510 
a_1:int; 
2511 
x:int; 
2512 
isInner:bool) 
2513  
2514 
returns (idA_A2:int; 
2515 
idParallel4_A:int; 
2516 
a:int); 
2517  
2518  
2519 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int; 
2520 
idParallel4_A_2, idParallel4_A_3, idParallel4_A_4:int; 
2521 
a_2, a_3, a_4, a_5, a_6:int; 
2522  
2523  
2524 
let 
2525  
2526  
2527  
2528 
 set state as active 
2529 
idParallel4_A_2 
2530 
= 1650; 
2531 

2532  
2533 

2534 
 transition trace : 
2535 
POINT__To__A2_A2a_1 
2536 
(idA_A2_2, a_2) 
2537 
= A2_A2a_en(idA_A2_1, x, a_1, false); 
2538 

2539  
2540 
(idA_A2_3, idParallel4_A_3, a_3) 
2541 
= 
2542  
2543 
if ( idA_A2_1 = 0) then 
2544  
2545 
(idA_A2_2, idParallel4_A_2, a_2) 
2546  
2547 
else(idA_A2_1, idParallel4_A_2, a_1); 
2548  
2549 

2550  
2551 
(idA_A2_4, a_4) 
2552 
= 
2553 
if ( idA_A2_1 = 1651) then 
2554 
A2_A2a_en(idA_A2_1, x, a_1, false) 
2555 
else (idA_A2_1, a_1); 
2556  
2557 

2558  
2559 
(idA_A2_5, a_5) 
2560 
= 
2561 
if ( idA_A2_1 = 1652) then 
2562 
A2_A2b_en(idA_A2_1, x, a_1, false) 
2563 
else (idA_A2_1, a_1); 
2564  
2565 

2566  
2567 
(idA_A2_6, idParallel4_A_4, a_6) 
2568 
= 
2569 
if ( idA_A2_1 = 0) then 
2570 
(idA_A2_3, idParallel4_A_3, a_3) 
2571 
else 
2572 
if ( idA_A2_1 = 1651) then 
2573 
(idA_A2_4, idParallel4_A_3, a_4) 
2574 
else 
2575 
if ( idA_A2_1 = 1652) then 
2576 
(idA_A2_5, idParallel4_A_3, a_5) 
2577 
else (idA_A2_1, idParallel4_A_2, a_1); 
2578  
2579  
2580 
(idA_A2, idParallel4_A, a) 
2581 
= (idA_A2_6, idParallel4_A_4, a_6); 
2582 

2583  
2584 
tel 
2585  
2586  
2587  
2588  
2589  
2590 
 Exit action for state :A_A2 
2591 
node A_A2_ex(idA_A2_1:int; 
2592 
idParallel4_A_1:int; 
2593 
isInner:bool) 
2594  
2595 
returns (idA_A2:int; 
2596 
idParallel4_A:int); 
2597  
2598  
2599 
var idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int; 
2600 
idParallel4_A_2:int; 
2601  
2602  
2603 
let 
2604  
2605  
2606  
2607 

2608 
(idA_A2_2) 
2609 
= 
2610 
if ( idA_A2_1 = 1651) then 
2611 
A2_A2a_ex(idA_A2_1, false) 
2612 
else (idA_A2_1); 
2613  
2614 

2615  
2616 
(idA_A2_3) 
2617 
= 
2618 
if ( idA_A2_1 = 1652) then 
2619 
A2_A2b_ex(idA_A2_1, false) 
2620 
else (idA_A2_1); 
2621  
2622 

2623  
2624 
(idA_A2_4) 
2625 
= 
2626 
if ( idA_A2_1 = 1651) then 
2627 
(idA_A2_2) 
2628 
else 
2629 
if ( idA_A2_1 = 1652) then 
2630 
(idA_A2_3) 
2631 
else (idA_A2_1); 
2632  
2633  
2634 
 set state as inactive 
2635 
idParallel4_A_2 
2636 
= if (not isInner) then 0 else idParallel4_A_1; 
2637  
2638 
idA_A2_5 
2639 
= 0; 
2640 

2641  
2642 
(idA_A2, idParallel4_A) 
2643 
= (idA_A2_5, idParallel4_A_1); 
2644 

2645  
2646 
tel 
2647  
2648  
2649  
2650  
2651  
2652  
2653 
 Entry action for state :A1_A1a 
2654 
node A1_A1a_en(idA_A1_1:int; 
2655 
x:int; 
2656 
a_1:int; 
2657 
isInner:bool) 
2658  
2659 
returns (idA_A1:int; 
2660 
a:int); 
2661  
2662  
2663 
var idA_A1_2:int; 
2664 
a_2:int; 
2665  
2666  
2667 
let 
2668  
2669  
2670  
2671 
 set state as active 
2672 
idA_A1_2 
2673 
= 1648; 
2674 

2675  
2676 
a_2 
2677 
= if (not isInner) then x+1 
2678 
else a_1; 
2679 

2680  
2681 
(idA_A1, a) 
2682 
= (idA_A1_2, a_2); 
2683 

2684  
2685 
tel 
2686  
2687  
2688  
2689  
2690  
2691 
 Exit action for state :A1_A1a 
2692 
node A1_A1a_ex(idA_A1_1:int; 
2693 
isInner:bool) 
2694  
2695 
returns (idA_A1:int); 
2696  
2697  
2698 
var idA_A1_2:int; 
2699  
2700  
2701 
let 
2702  
2703  
2704  
2705 
 set state as inactive 
2706 
idA_A1_2 
2707 
= if (not isInner) then 0 else idA_A1_1; 
2708  
2709  
2710 
(idA_A1) 
2711 
= (idA_A1_1); 
2712 

2713  
2714 
tel 
2715  
2716  
2717  
2718  
2719  
2720  
2721 
 Entry action for state :A1_A1b 
2722 
node A1_A1b_en(idA_A1_1:int; 
2723 
x:int; 
2724 
a_1:int; 
2725 
isInner:bool) 
2726  
2727 
returns (idA_A1:int; 
2728 
a:int); 
2729  
2730  
2731 
var idA_A1_2:int; 
2732 
a_2:int; 
2733  
2734  
2735 
let 
2736  
2737  
2738  
2739 
 set state as active 
2740 
idA_A1_2 
2741 
= 1649; 
2742 

2743  
2744 
a_2 
2745 
= if (not isInner) then x+2 
2746 
else a_1; 
2747 

2748  
2749 
(idA_A1, a) 
2750 
= (idA_A1_2, a_2); 
2751 

2752  
2753 
tel 
2754  
2755  
2756  
2757  
2758  
2759 
 Exit action for state :A1_A1b 
2760 
node A1_A1b_ex(idA_A1_1:int; 
2761 
isInner:bool) 
2762  
2763 
returns (idA_A1:int); 
2764  
2765  
2766 
var idA_A1_2:int; 
2767  
2768  
2769 
let 
2770  
2771  
2772  
2773 
 set state as inactive 
2774 
idA_A1_2 
2775 
= if (not isInner) then 0 else idA_A1_1; 
2776  
2777  
2778 
(idA_A1) 
2779 
= (idA_A1_1); 
2780 

2781  
2782 
tel 
2783  
2784  
2785  
2786  
2787  
2788  
2789 
 Entry action for state :A_A1 
2790 
node A_A1_en(idA_A1_1:int; 
2791 
idParallel4_A_1:int; 
2792 
a_1:int; 
2793 
x:int; 
2794 
isInner:bool) 
2795  
2796 
returns (idA_A1:int; 
2797 
idParallel4_A:int; 
2798 
a:int); 
2799  
2800  
2801 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int; 
2802 
idParallel4_A_2, idParallel4_A_3, idParallel4_A_4:int; 
2803 
a_2, a_3, a_4, a_5, a_6:int; 
2804  
2805  
2806 
let 
2807  
2808  
2809  
2810 
 set state as active 
2811 
idParallel4_A_2 
2812 
= 1647; 
2813 

2814  
2815 

2816 
 transition trace : 
2817 
POINT__To__A1_A1a_1 
2818 
(idA_A1_2, a_2) 
2819 
= A1_A1a_en(idA_A1_1, x, a_1, false); 
2820 

2821  
2822 
(idA_A1_3, idParallel4_A_3, a_3) 
2823 
= 
2824  
2825 
if ( idA_A1_1 = 0) then 
2826  
2827 
(idA_A1_2, idParallel4_A_2, a_2) 
2828  
2829 
else(idA_A1_1, idParallel4_A_2, a_1); 
2830  
2831 

2832  
2833 
(idA_A1_4, a_4) 
2834 
= 
2835 
if ( idA_A1_1 = 1648) then 
2836 
A1_A1a_en(idA_A1_1, x, a_1, false) 
2837 
else (idA_A1_1, a_1); 
2838  
2839 

2840  
2841 
(idA_A1_5, a_5) 
2842 
= 
2843 
if ( idA_A1_1 = 1649) then 
2844 
A1_A1b_en(idA_A1_1, x, a_1, false) 
2845 
else (idA_A1_1, a_1); 
2846  
2847 

2848  
2849 
(idA_A1_6, idParallel4_A_4, a_6) 
2850 
= 
2851 
if ( idA_A1_1 = 0) then 
2852 
(idA_A1_3, idParallel4_A_3, a_3) 
2853 
else 
2854 
if ( idA_A1_1 = 1648) then 
2855 
(idA_A1_4, idParallel4_A_3, a_4) 
2856 
else 
2857 
if ( idA_A1_1 = 1649) then 
2858 
(idA_A1_5, idParallel4_A_3, a_5) 
2859 
else (idA_A1_1, idParallel4_A_2, a_1); 
2860  
2861  
2862 
(idA_A1, idParallel4_A, a) 
2863 
= (idA_A1_6, idParallel4_A_4, a_6); 
2864 

2865  
2866 
tel 
2867  
2868  
2869  
2870  
2871  
2872 
 Exit action for state :A_A1 
2873 
node A_A1_ex(idA_A1_1:int; 
2874 
idParallel4_A_1:int; 
2875 
isInner:bool) 
2876  
2877 
returns (idA_A1:int; 
2878 
idParallel4_A:int); 
2879  
2880  
2881 
var idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
2882 
idParallel4_A_2:int; 
2883  
2884  
2885 
let 
2886  
2887  
2888  
2889 

2890 
(idA_A1_2) 
2891 
= 
2892 
if ( idA_A1_1 = 1648) then 
2893 
A1_A1a_ex(idA_A1_1, false) 
2894 
else (idA_A1_1); 
2895  
2896 

2897  
2898 
(idA_A1_3) 
2899 
= 
2900 
if ( idA_A1_1 = 1649) then 
2901 
A1_A1b_ex(idA_A1_1, false) 
2902 
else (idA_A1_1); 
2903  
2904 

2905  
2906 
(idA_A1_4) 
2907 
= 
2908 
if ( idA_A1_1 = 1648) then 
2909 
(idA_A1_2) 
2910 
else 
2911 
if ( idA_A1_1 = 1649) then 
2912 
(idA_A1_3) 
2913 
else (idA_A1_1); 
2914  
2915  
2916 
 set state as inactive 
2917 
idParallel4_A_2 
2918 
= if (not isInner) then 0 else idParallel4_A_1; 
2919  
2920 
idA_A1_5 
2921 
= 0; 
2922 

2923  
2924 
(idA_A1, idParallel4_A) 
2925 
= (idA_A1_5, idParallel4_A_1); 
2926 

2927  
2928 
tel 
2929  
2930  
2931  
2932  
2933  
2934  
2935 
 Entry action for state :Parallel4_A 
2936 
node Parallel4_A_en(idParallel4_A_1:int; 
2937 
idParallel4_Parallel4_1:int; 
2938 
a_1:int; 
2939 
idA_A1_1:int; 
2940 
x:int; 
2941 
idA_A2_1:int; 
2942 
isInner:bool) 
2943  
2944 
returns (idParallel4_A:int; 
2945 
idParallel4_Parallel4:int; 
2946 
a:int; 
2947 
idA_A1:int; 
2948 
idA_A2:int); 
2949  
2950  
2951 
var idParallel4_A_2, idParallel4_A_3, idParallel4_A_4, idParallel4_A_5, idParallel4_A_6:int; 
2952 
idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4:int; 
2953 
a_2, a_3, a_4, a_5, a_6:int; 
2954 
idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int; 
2955 
idA_A2_2, idA_A2_3:int; 
2956  
2957  
2958 
let 
2959  
2960  
2961  
2962 
 set state as active 
2963 
idParallel4_Parallel4_2 
2964 
= 1646; 
2965 

2966  
2967 

2968 
 transition trace : 
2969 
POINT__To__A_A1_1 
2970 
(idA_A1_2, idParallel4_A_2, a_2) 
2971 
= A_A1_en(idA_A1_1, idParallel4_A_1, a_1, x, false); 
2972 

2973  
2974 
(idParallel4_A_3, idParallel4_Parallel4_3, a_3, idA_A1_3) 
2975 
= 
2976  
2977 
if ( idParallel4_A_1 = 0) then 
2978  
2979 
(idParallel4_A_2, idParallel4_Parallel4_2, a_2, idA_A1_2) 
2980  
2981 
else(idParallel4_A_1, idParallel4_Parallel4_2, a_1, idA_A1_1); 
2982  
2983 

2984  
2985 
(idA_A2_2, idParallel4_A_4, a_4) 
2986 
= 
2987 
if ( idParallel4_A_1 = 1650) then 
2988 
A_A2_en(idA_A2_1, idParallel4_A_1, a_1, x, false) 
2989 
else (idA_A2_1, idParallel4_A_1, a_1); 
2990  
2991 

2992  
2993 
(idA_A1_4, idParallel4_A_5, a_5) 
2994 
= 
2995 
if ( idParallel4_A_1 = 1647) then 
2996 
A_A1_en(idA_A1_1, idParallel4_A_1, a_1, x, false) 
2997 
else (idA_A1_1, idParallel4_A_1, a_1); 
2998  
2999 

3000  
3001 
(idParallel4_A_6, idParallel4_Parallel4_4, a_6, idA_A1_5, idA_A2_3) 
3002 
= 
3003 
if ( idParallel4_A_1 = 0) then 
3004 
(idParallel4_A_3, idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_1) 
3005 
else 
3006 
if ( idParallel4_A_1 = 1650) then 
3007 
(idParallel4_A_4, idParallel4_Parallel4_3, a_4, idA_A1_1, idA_A2_2) 
3008 
else 
3009 
if ( idParallel4_A_1 = 1647) then 
3010 
(idParallel4_A_5, idParallel4_Parallel4_3, a_5, idA_A1_4, idA_A2_1) 
3011 
else (idParallel4_A_1, idParallel4_Parallel4_2, a_1, idA_A1_1, idA_A2_1); 
3012  
3013  
3014 
(idParallel4_A, idParallel4_Parallel4, a, idA_A1, idA_A2) 
3015 
= (idParallel4_A_6, idParallel4_Parallel4_4, a_6, idA_A1_5, idA_A2_3); 
3016 

3017  
3018 
tel 
3019  
3020  
3021  
3022  
3023  
3024 
 Exit action for state :Parallel4_A 
3025 
node Parallel4_A_ex(idA_A2_1:int; 
3026 
idParallel4_A_1:int; 
3027 
idA_A1_1:int; 
3028 
idParallel4_Parallel4_1:int; 
3029 
isInner:bool) 
3030  
3031 
returns (idA_A2:int; 
3032 
idParallel4_A:int; 
3033 
idA_A1:int; 
3034 
idParallel4_Parallel4:int); 
3035  
3036  
3037 
var idA_A2_2, idA_A2_3:int; 
3038 
idParallel4_A_2, idParallel4_A_3, idParallel4_A_4, idParallel4_A_5:int; 
3039 
idA_A1_2, idA_A1_3:int; 
3040 
idParallel4_Parallel4_2:int; 
3041  
3042  
3043 
let 
3044  
3045  
3046  
3047 

3048 
(idA_A2_2, idParallel4_A_2) 
3049 
= 
3050 
if ( idParallel4_A_1 = 1650) then 
3051 
A_A2_ex(idA_A2_1, idParallel4_A_1, false) 
3052 
else (idA_A2_1, idParallel4_A_1); 
3053  
3054 

3055  
3056 
(idA_A1_2, idParallel4_A_3) 
3057 
= 
3058 
if ( idParallel4_A_1 = 1647) then 
3059 
A_A1_ex(idA_A1_1, idParallel4_A_1, false) 
3060 
else (idA_A1_1, idParallel4_A_1); 
3061  
3062 

3063  
3064 
(idA_A2_3, idParallel4_A_4, idA_A1_3) 
3065 
= 
3066 
if ( idParallel4_A_1 = 1650) then 
3067 
(idA_A2_2, idParallel4_A_2, idA_A1_1) 
3068 
else 
3069 
if ( idParallel4_A_1 = 1647) then 
3070 
(idA_A2_1, idParallel4_A_3, idA_A1_2) 
3071 
else (idA_A2_1, idParallel4_A_1, idA_A1_1); 
3072  
3073  
3074 
 set state as inactive 
3075 
idParallel4_Parallel4_2 
3076 
= if (not isInner) then 0 else idParallel4_Parallel4_1; 
3077  
3078 
idParallel4_A_5 
3079 
= 0; 
3080 

3081  
3082 
(idA_A2, idParallel4_A, idA_A1, idParallel4_Parallel4) 
3083 
= (idA_A2_3, idParallel4_A_5, idA_A1_3, idParallel4_Parallel4_1); 
3084 

3085  
3086 
tel 
3087  
3088  
3089 
***************************************************State :B_B2 Automaton*************************************************** 
3090  
3091 
node B_B2_node(idB_B2_1:int; 
3092 
a_1:int; 
3093 
b_1:int; 
3094 
S:bool; 
3095 
R:bool) 
3096  
3097 
returns (idB_B2:int; 
3098 
a:int; 
3099 
b:int); 
3100  
3101  
3102 
let 
3103  
3104 
automaton b_b2 
3105  
3106 
state POINTB_B2: 
3107 
unless (idB_B2_1=0) restart POINT__TO__B2_B2A_1 
3108  
3109  
3110  
3111 
unless (idB_B2_1=1655) and S restart B2_B2A__TO__B2_B2B_1 
3112  
3113  
3114  
3115 
unless (idB_B2_1=1656) and R restart B2_B2B__TO__B2_B2A_1 
3116  
3117  
3118  
3119 
unless (idB_B2_1=1655) restart B2_B2A_IDL 
3120  
3121 
unless (idB_B2_1=1656) restart B2_B2B_IDL 
3122  
3123 
let 
3124  
3125 
(idB_B2, a, b) 
3126 
= (idB_B2_1, a_1, b_1); 
3127 

3128  
3129 
tel 
3130  
3131  
3132  
3133 
state POINT__TO__B2_B2A_1: 
3134  
3135 
var idB_B2_2:int; 
3136 
a_2:int; 
3137 
b_2:int; 
3138 
let 
3139  
3140 
 transition trace : 
3141 
POINT__To__B2_B2a_1 
3142 
(idB_B2_2, a_2, b_2) 
3143 
= B2_B2a_en(idB_B2_1, a_1, b_1, false); 
3144 

3145  
3146 
(idB_B2, a, b) 
3147 
= (idB_B2_2, a_2, b_2); 
3148  
3149  
3150 
tel 
3151  
3152 
until true restart POINTB_B2 
3153  
3154  
3155  
3156 
state B2_B2A__TO__B2_B2B_1: 
3157  
3158 
var idB_B2_2, idB_B2_3:int; 
3159 
a_2:int; 
3160 
b_2:int; 
3161 
let 
3162  
3163 
 transition trace : 
3164 
B2_B2a__To__B2_B2b_1 
3165 
(idB_B2_2) 
3166 
= B2_B2a_ex(idB_B2_1, false); 
3167 

3168  
3169 
(idB_B2_3, a_2, b_2) 
3170 
= B2_B2b_en(idB_B2_2, a_1, b_1, false); 
3171 

3172  
3173 
(idB_B2, a, b) 
3174 
= (idB_B2_3, a_2, b_2); 
3175  
3176  
3177 
tel 
3178  
3179 
until true restart POINTB_B2 
3180  
3181  
3182  
3183 
state B2_B2B__TO__B2_B2A_1: 
3184  
3185 
var idB_B2_2, idB_B2_3:int; 
3186 
a_2:int; 
3187 
b_2:int; 
3188 
let 
3189  
3190 
 transition trace : 
3191 
B2_B2b__To__B2_B2a_1 
3192 
(idB_B2_2) 
3193 
= B2_B2b_ex(idB_B2_1, false); 
3194 

3195  
3196 
(idB_B2_3, a_2, b_2) 
3197 
= B2_B2a_en(idB_B2_2, a_1, b_1, false); 
3198 

3199  
3200 
(idB_B2, a, b) 
3201 
= (idB_B2_3, a_2, b_2); 
3202  
3203  
3204 
tel 
3205  
3206 
until true restart POINTB_B2 
3207  
3208  
3209  
3210 
state B2_B2A_IDL: 
3211  
3212 
let 
3213  
3214 

3215  
3216 
(idB_B2, a, b) 
3217 
= (idB_B2_1, a_1, b_1); 
3218 

3219  
3220 
tel 
3221  
3222 
until true restart POINTB_B2 
3223  
3224  
3225  
3226 
state B2_B2B_IDL: 
3227  
3228 
let 
3229  
3230 

3231  
3232 
(idB_B2, a, b) 
3233 
= (idB_B2_1, a_1, b_1); 
3234 

3235  
3236 
tel 
3237  
3238 
until true restart POINTB_B2 
3239  
3240  
3241  
3242 
tel 
3243  
3244  
3245 
***************************************************State :B_B1 Automaton*************************************************** 
3246  
3247 
node B_B1_node(idB_B1_1:int; 
3248 
a_1:int; 
3249 
b_1:int; 
3250 
S:bool; 
3251 
R:bool) 
3252  
3253 
returns (idB_B1:int; 
3254 
a:int; 
3255 
b:int); 
3256  
3257  
3258 
let 
3259  
3260 
automaton b_b1 
3261  
3262 
state POINTB_B1: 
3263 
unless (idB_B1_1=0) restart POINT__TO__B1_B1A_1 
3264  
3265  
3266  
3267 
unless (idB_B1_1=1658) and S restart B1_B1A__TO__B1_B1B_1 
3268  
3269  
3270  
3271 
unless (idB_B1_1=1659) and R restart B1_B1B__TO__B1_B1A_1 
3272  
3273  
3274  
3275 
unless (idB_B1_1=1658) restart B1_B1A_IDL 
3276  
3277 
unless (idB_B1_1=1659) restart B1_B1B_IDL 
3278  
3279 
let 
3280  
3281 
(idB_B1, a, b) 
3282 
= (idB_B1_1, a_1, b_1); 
3283 

3284  
3285 
tel 
3286  
3287  
3288  
3289 
state POINT__TO__B1_B1A_1: 
3290  
3291 
var idB_B1_2:int; 
3292 
a_2:int; 
3293 
b_2:int; 
3294 
let 
3295  
3296 
 transition trace : 
3297 
POINT__To__B1_B1a_1 
3298 
(idB_B1_2, a_2, b_2) 
3299 
= B1_B1a_en(idB_B1_1, a_1, b_1, false); 
3300 

3301  
3302 
(idB_B1, a, b) 
3303 
= (idB_B1_2, a_2, b_2); 
3304  
3305  
3306 
tel 
3307  
3308 
until true restart POINTB_B1 
3309  
3310  
3311  
3312 
state B1_B1A__TO__B1_B1B_1: 
3313  
3314 
var idB_B1_2, idB_B1_3:int; 
3315 
a_2:int; 
3316 
b_2:int; 
3317 
let 
3318  
3319 
 transition trace : 
3320 
B1_B1a__To__B1_B1b_1 
3321 
(idB_B1_2) 
3322 
= B1_B1a_ex(idB_B1_1, false); 
3323 

3324  
3325 
(idB_B1_3, a_2, b_2) 
3326 
= B1_B1b_en(idB_B1_2, a_1, b_1, false); 
3327 

3328  
3329 
(idB_B1, a, b) 
3330 
= (idB_B1_3, a_2, b_2); 
3331  
3332  
3333 
tel 
3334  
3335 
until true restart POINTB_B1 
3336  
3337  
3338  
3339 
state B1_B1B__TO__B1_B1A_1: 
3340  
3341 
var idB_B1_2, idB_B1_3:int; 
3342 
a_2:int; 
3343 
b_2:int; 
3344 
let 
3345  
3346 
 transition trace : 
3347 
B1_B1b__To__B1_B1a_1 
3348 
(idB_B1_2) 
3349 
= B1_B1b_ex(idB_B1_1, false); 
3350 

3351  
3352 
(idB_B1_3, a_2, b_2) 
3353 
= B1_B1a_en(idB_B1_2, a_1, b_1, false); 
3354 

3355  
3356 
(idB_B1, a, b) 
3357 
= (idB_B1_3, a_2, b_2); 
3358  
3359  
3360 
tel 
3361  
3362 
until true restart POINTB_B1 
3363  
3364  
3365  
3366 
state B1_B1A_IDL: 
3367  
3368 
let 
3369  
3370 

3371  
3372 
(idB_B1, a, b) 
3373 
= (idB_B1_1, a_1, b_1); 
3374 

3375  
3376 
tel 
3377  
3378 
until true restart POINTB_B1 
3379  
3380  
3381  
3382 
state B1_B1B_IDL: 
3383  
3384 
let 
3385  
3386 

3387  
3388 
(idB_B1, a, b) 
3389 
= (idB_B1_1, a_1, b_1); 
3390 

3391  
3392 
tel 
3393  
3394 
until true restart POINTB_B1 
3395  
3396  
3397  
3398 
tel 
3399  
3400  
3401 
***************************************************State :Parallel4_B Automaton*************************************************** 
3402  
3403 
node Parallel4_B_node(idParallel4_B_1:int; 
3404 
a_1:int; 
3405 
b_1:int; 
3406 
idB_B1_1:int; 
3407 
T:bool; 
3408 
idB_B2_1:int; 
3409 
R:bool; 
3410 
S:bool) 
3411  
3412 
returns (idParallel4_B:int; 
3413 
a:int; 
3414 
b:int; 
3415 
idB_B1:int; 
3416 
idB_B2:int); 
3417  
3418  
3419 
let 
3420  
3421 
automaton parallel4_b 
3422  
3423 
state POINTParallel4_B: 
3424 
unless (idParallel4_B_1=0) restart POINT__TO__B_B1_1 
3425  
3426  
3427  
3428 
unless (idParallel4_B_1=1654) and T restart B_B2__TO__B_B1_1 
3429  
3430  
3431  
3432 
unless (idParallel4_B_1=1657) and T restart B_B1__TO__B_B2_1 
3433  
3434  
3435  
3436 
unless (idParallel4_B_1=1654) restart B_B2_IDL 
3437  
3438 
unless (idParallel4_B_1=1657) restart B_B1_IDL 
3439  
3440 
let 
3441  
3442 
(idParallel4_B, a, b, idB_B1, idB_B2) 
3443 
= (idParallel4_B_1, a_1, b_1, idB_B1_1, idB_B2_1); 
3444 

3445  
3446 
tel 
3447  
3448  
3449  
3450 
state POINT__TO__B_B1_1: 
3451  
3452 
var idParallel4_B_2:int; 
3453 
a_2:int; 
3454 
b_2:int; 
3455 
idB_B1_2:int; 
3456 
let 
3457  
3458 
 transition trace : 
3459 
POINT__To__B_B1_1 
3460 
(idB_B1_2, idParallel4_B_2, a_2, b_2) 
3461 
= B_B1_en(idB_B1_1, idParallel4_B_1, a_1, b_1, false); 
3462 

3463  
3464 
(idParallel4_B, a, b, idB_B1) 
3465 
= (idParallel4_B_2, a_2, b_2, idB_B1_2); 
3466  
3467 
add unused variables 
3468 
(idB_B2) 
3469 
= (idB_B2_1); 
3470 

3471  
3472 
tel 
3473  
3474 
until true restart POINTParallel4_B 
3475  
3476  
3477  
3478 
state B_B2__TO__B_B1_1: 
3479  
3480 
var idParallel4_B_2, idParallel4_B_3:int; 
3481 
a_2:int; 
3482 
b_2:int; 
3483 
idB_B1_2:int; 
3484 
idB_B2_2:int; 
3485 
let 
3486  
3487 
 transition trace : 
3488 
B_B2__To__B_B1_1 
3489 
(idB_B2_2, idParallel4_B_2) 
3490 
= B_B2_ex(idB_B2_1, idParallel4_B_1, false); 
3491 

3492  
3493 
(idB_B1_2, idParallel4_B_3, a_2, b_2) 
3494 
= B_B1_en(idB_B1_1, idParallel4_B_2, a_1, b_1, false); 
3495 

3496  
3497 
(idParallel4_B, a, b, idB_B1, idB_B2) 
3498 
= (idParallel4_B_3, a_2, b_2, idB_B1_2, idB_B2_2); 
3499  
3500  
3501 
tel 
3502  
3503 
until true restart POINTParallel4_B 
3504  
3505  
3506  
3507 
state B_B1__TO__B_B2_1: 
3508  
3509 
var idParallel4_B_2, idParallel4_B_3:int; 
3510 
a_2:int; 
3511 
b_2:int; 
3512 
idB_B1_2:int; 
3513 
idB_B2_2:int; 
3514 
let 
3515  
3516 
 transition trace : 
3517 
B_B1__To__B_B2_1 
3518 
(idB_B1_2, idParallel4_B_2) 
3519 
= B_B1_ex(idB_B1_1, idParallel4_B_1, false); 
3520 

3521  
3522 
(idB_B2_2, idParallel4_B_3, a_2, b_2) 
3523 
= B_B2_en(idB_B2_1, idParallel4_B_2, a_1, b_1, false); 
3524 

3525  
3526 
(idParallel4_B, a, b, idB_B1, idB_B2) 
3527 
= (idParallel4_B_3, a_2, b_2, idB_B1_2, idB_B2_2); 
3528  
3529  
3530 
tel 
3531  
3532 
until true restart POINTParallel4_B 
3533  
3534  
3535  
3536 
state B_B2_IDL: 
3537  
3538 
var a_2:int; 
3539 
b_2:int; 
3540 
idB_B2_2:int; 
3541 
let 
3542  
3543 

3544 
(idB_B2_2, a_2, b_2) 
3545 
= B_B2_node(idB_B2_1, a_1, b_1, S, R); 
3546  
3547 

3548  
3549  
3550 
(idParallel4_B, a, b, idB_B1, idB_B2) 
3551 
= (idParallel4_B_1, a_2, b_2, idB_B1_1, idB_B2_2); 
3552 

3553  
3554 
tel 
3555  
3556 
until true restart POINTParallel4_B 
3557  
3558  
3559  
3560 
state B_B1_IDL: 
3561  
3562 
var a_2:int; 
3563 
b_2:int; 
3564 
idB_B1_2:int; 
3565 
let 
3566  
3567 

3568 
(idB_B1_2, a_2, b_2) 
3569 
= B_B1_node(idB_B1_1, a_1, b_1, S, R); 
3570  
3571 

3572  
3573  
3574 
(idParallel4_B, a, b, idB_B1, idB_B2) 
3575 
= (idParallel4_B_1, a_2, b_2, idB_B1_2, idB_B2_1); 
3576 

3577  
3578 
tel 
3579  
3580 
until true restart POINTParallel4_B 
3581  
3582  
3583  
3584 
tel 
3585  
3586  
3587 
***************************************************State :D_D2 Automaton*************************************************** 
3588  
3589 
node D_D2_node(idD_D2_1:int; 
3590 
c_1:int; 
3591 
dd_1:int; 
3592 
S:bool; 
3593 
R:bool) 
3594  
3595 
returns (idD_D2:int; 
3596 
c:int; 
3597 
dd:int); 
3598  
3599  
3600 
let 
3601  
3602 
automaton d_d2 
3603  
3604 
state POINTD_D2: 
3605 
unless (idD_D2_1=0) restart POINT__TO__D2_D2A_1 
3606  
3607  
3608  
3609 
unless (idD_D2_1=1669) and S restart D2_D2A__TO__D2_D2B_1 
3610  
3611  
3612  
3613 
unless (idD_D2_1=1670) and R restart D2_D2B__TO__D2_D2A_1 
3614  
3615  
3616  
3617 
unless (idD_D2_1=1669) restart D2_D2A_IDL 
3618  
3619 
unless (idD_D2_1=1670) restart D2_D2B_IDL 
3620  
3621 
let 
3622  
3623 
(idD_D2, c, dd) 
3624 
= (idD_D2_1, c_1, dd_1); 
3625 

3626  
3627 
tel 
3628  
3629  
3630  
3631 
state POINT__TO__D2_D2A_1: 
3632  
3633 
var idD_D2_2:int; 
3634 
c_2:int; 
3635 
dd_2:int; 
3636 
let 
3637  
3638 
 transition trace : 
3639 
POINT__To__D2_D2a_1 
3640 
(idD_D2_2, c_2, dd_2) 
3641 
= D2_D2a_en(idD_D2_1, c_1, dd_1, false); 
3642 

3643  
3644 
(idD_D2, c, dd) 
3645 
= (idD_D2_2, c_2, dd_2); 
3646  
3647  
3648 
tel 
3649  
3650 
until true restart POINTD_D2 
3651  
3652  
3653  
3654 
state D2_D2A__TO__D2_D2B_1: 
3655  
3656 
var idD_D2_2, idD_D2_3:int; 
3657 
c_2:int; 
3658 
dd_2:int; 
3659 
let 
3660  
3661 
 transition trace : 
3662 
D2_D2a__To__D2_D2b_1 
3663 
(idD_D2_2) 
3664 
= D2_D2a_ex(idD_D2_1, false); 
3665 

3666  
3667 
(idD_D2_3, c_2, dd_2) 
3668 
= D2_D2b_en(idD_D2_2, c_1, dd_1, false); 
3669 

3670  
3671 
(idD_D2, c, dd) 
3672 
= (idD_D2_3, c_2, dd_2); 
3673  
3674  
3675 
tel 
3676  
3677 
until true restart POINTD_D2 
3678  
3679  
3680  
3681 
state D2_D2B__TO__D2_D2A_1: 
3682  
3683 
var idD_D2_2, idD_D2_3:int; 
3684 
c_2:int; 
3685 
dd_2:int; 
3686 
let 
3687  
3688 
 transition trace : 
3689 
D2_D2b__To__D2_D2a_1 
3690 
(idD_D2_2) 
3691 
= D2_D2b_ex(idD_D2_1, false); 
3692 

3693  
3694 
(idD_D2_3, c_2, dd_2) 
3695 
= D2_D2a_en(idD_D2_2, c_1, dd_1, false); 
3696 

3697  
3698 
(idD_D2, c, dd) 
3699 
= (idD_D2_3, c_2, dd_2); 
3700  
3701  
3702 
tel 
3703  
3704 
until true restart POINTD_D2 
3705  
3706  
3707  
3708 
state D2_D2A_IDL: 
3709  
3710 
let 
3711  
3712 

3713  
3714 
(idD_D2, c, dd) 
3715 
= (idD_D2_1, c_1, dd_1); 
3716 

3717  
3718 
tel 
3719  
3720 
until true restart POINTD_D2 
3721  
3722  
3723  
3724 
state D2_D2B_IDL: 
3725  
3726 
let 
3727  
3728 

3729  
3730 
(idD_D2, c, dd) 
3731 
= (idD_D2_1, c_1, dd_1); 
3732 

3733  
3734 
tel 
3735  
3736 
until true restart POINTD_D2 
3737  
3738  
3739  
3740 
tel 
3741  
3742  
3743 
***************************************************State :D_D1 Automaton*************************************************** 
3744  
3745 
node D_D1_node(idD_D1_1:int; 
3746 
c_1:int; 
3747 
dd_1:int; 
3748 
S:bool; 
3749 
R:bool) 
3750  
3751 
returns (idD_D1:int; 
3752 
c:int; 
3753 
dd:int); 
3754  
3755  
3756 
let 
3757  
3758 
automaton d_d1 
3759  
3760 
state POINTD_D1: 
3761 
unless (idD_D1_1=0) restart POINT__TO__D1_D1A_1 
3762  
3763  
3764  
3765 
unless (idD_D1_1=1672) and S restart D1_D1A__TO__D1_D1B_1 
3766  
3767  
3768  
3769 
unless (idD_D1_1=1673) and R restart D1_D1B__TO__D1_D1A_1 
3770  
3771  
3772  
3773 
unless (idD_D1_1=1672) restart D1_D1A_IDL 
3774  
3775 
unless (idD_D1_1=1673) restart D1_D1B_IDL 
3776  
3777 
let 
3778  
3779 
(idD_D1, c, dd) 
3780 
= (idD_D1_1, c_1, dd_1); 
3781 

3782  
3783 
tel 
3784  
3785  
3786  
3787 
state POINT__TO__D1_D1A_1: 
3788  
3789 
var idD_D1_2:int; 
3790 
c_2:int; 
3791 
dd_2:int; 
3792 
let 
3793  
3794 
 transition trace : 
3795 
POINT__To__D1_D1a_1 
3796 
(idD_D1_2, c_2, dd_2) 
3797 
= D1_D1a_en(idD_D1_1, c_1, dd_1, false); 
3798 

3799  
3800 
(idD_D1, c, dd) 
3801 
= (idD_D1_2, c_2, dd_2); 
3802  
3803  
3804 
tel 
3805  
3806 
until true restart POINTD_D1 
3807  
3808  
3809  
3810 
state D1_D1A__TO__D1_D1B_1: 
3811  
3812 
var idD_D1_2, idD_D1_3:int; 
3813 
c_2:int; 
3814 
dd_2:int; 
3815 
let 
3816  
3817 
 transition trace : 
3818 
D1_D1a__To__D1_D1b_1 
3819 
(idD_D1_2) 
3820 
= D1_D1a_ex(idD_D1_1, false); 
3821 

3822  
3823 
(idD_D1_3, c_2, dd_2) 
3824 
= D1_D1b_en(idD_D1_2, c_1, dd_1, false); 
3825 

3826  
3827 
(idD_D1, c, dd) 
3828 
= (idD_D1_3, c_2, dd_2); 
3829  
3830  
3831 
tel 
3832  
3833 
until true restart POINTD_D1 
3834  
3835  
3836  
3837 
state D1_D1B__TO__D1_D1A_1: 
3838  
3839 
var idD_D1_2, idD_D1_3:int; 
3840 
c_2:int; 
3841 
dd_2:int; 
3842 
let 
3843  
3844 
 transition trace : 
3845 
D1_D1b__To__D1_D1a_1 
3846 
(idD_D1_2) 
3847 
= D1_D1b_ex(idD_D1_1, false); 
3848 

3849  
3850 
(idD_D1_3, c_2, dd_2) 
3851 
= D1_D1a_en(idD_D1_2, c_1, dd_1, false); 
3852 

3853  
3854 
(idD_D1, c, dd) 
3855 
= (idD_D1_3, c_2, dd_2); 
3856  
3857  
3858 
tel 
3859  
3860 
until true restart POINTD_D1 
3861  
3862  
3863  
3864 
state D1_D1A_IDL: 
3865  
3866 
let 
3867  
3868 

3869  
3870 
(idD_D1, c, dd) 
3871 
= (idD_D1_1, c_1, dd_1); 
3872 

3873  
3874 
tel 
3875  
3876 
until true restart POINTD_D1 
3877  
3878  
3879  
3880 
state D1_D1B_IDL: 
3881  
3882 
let 
3883  
3884 

3885  
3886 
(idD_D1, c, dd) 
3887 
= (idD_D1_1, c_1, dd_1); 
3888 

3889  
3890 
tel 
3891  
3892 
until true restart POINTD_D1 
3893  
3894  
3895  
3896 
tel 
3897  
3898  
3899 
***************************************************State :CD_D Automaton*************************************************** 
3900  
3901 
node CD_D_node(idCD_D_1:int; 
3902 
c_1:int; 
3903 
dd_1:int; 
3904 
idD_D1_1:int; 
3905 
T:bool; 
3906 
idD_D2_1:int; 
3907 
R:bool; 
3908 
S:bool) 
3909  
3910 
returns (idCD_D:int; 
3911 
c:int; 
3912 
dd:int; 
3913 
idD_D1:int; 
3914 
idD_D2:int); 
3915  
3916  
3917 
let 
3918  
3919 
automaton cd_d 
3920  
3921 
state POINTCD_D: 
3922 
unless (idCD_D_1=0) restart POINT__TO__D_D1_1 
3923  
3924  
3925  
3926 
unless (idCD_D_1=1668) and T restart D_D2__TO__D_D1_1 
3927  
3928  
3929  
3930 
unless (idCD_D_1=1671) and T restart D_D1__TO__D_D2_1 
3931  
3932  
3933  
3934 
unless (idCD_D_1=1668) restart D_D2_IDL 
3935  
3936 
unless (idCD_D_1=1671) restart D_D1_IDL 
3937  
3938 
let 
3939  
3940 
(idCD_D, c, dd, idD_D1, idD_D2) 
3941 
= (idCD_D_1, c_1, dd_1, idD_D1_1, idD_D2_1); 
3942 

3943  
3944 
tel 
3945  
3946  
3947  
3948 
state POINT__TO__D_D1_1: 
3949  
3950 
var idCD_D_2:int; 
3951 
c_2:int; 
3952 
dd_2:int; 
3953 
idD_D1_2:int; 
3954 
let 
3955  
3956 
 transition trace : 
3957 
POINT__To__D_D1_1 
3958 
(idD_D1_2, idCD_D_2, c_2, dd_2) 
3959 
= D_D1_en(idD_D1_1, idCD_D_1, c_1, dd_1, false); 
3960 

3961  
3962 
(idCD_D, c, dd, idD_D1) 
3963 
= (idCD_D_2, c_2, dd_2, idD_D1_2); 
3964  
3965 
add unused variables 
3966 
(idD_D2) 
3967 
= (idD_D2_1); 
3968 

3969  
3970 
tel 
3971  
3972 
until true restart POINTCD_D 
3973  
3974  
3975  
3976 
state D_D2__TO__D_D1_1: 
3977  
3978 
var idCD_D_2, idCD_D_3:int; 
3979 
c_2:int; 
3980 
dd_2:int; 
3981 
idD_D1_2:int; 
3982 
idD_D2_2:int; 
3983 
let 
3984  
3985 
 transition trace : 
3986 
D_D2__To__D_D1_1 
3987 
(idD_D2_2, idCD_D_2) 
3988 
= D_D2_ex(idD_D2_1, idCD_D_1, false); 
3989 

3990  
3991 
(idD_D1_2, idCD_D_3, c_2, dd_2) 
3992 
= D_D1_en(idD_D1_1, idCD_D_2, c_1, dd_1, false); 
3993 

3994  
3995 
(idCD_D, c, dd, idD_D1, idD_D2) 
3996 
= (idCD_D_3, c_2, dd_2, idD_D1_2, idD_D2_2); 
3997  
3998  
3999 
tel 
4000  
4001 
until true restart POINTCD_D 
4002  
4003  
4004  
4005 
state D_D1__TO__D_D2_1: 
4006  
4007 
var idCD_D_2, idCD_D_3:int; 
4008 
c_2:int; 
4009 
dd_2:int; 
4010 
idD_D1_2:int; 
4011 
idD_D2_2:int; 
4012 
let 
4013  
4014 
 transition trace : 
4015 
D_D1__To__D_D2_1 
4016 
(idD_D1_2, idCD_D_2) 
4017 
= D_D1_ex(idD_D1_1, idCD_D_1, false); 
4018 

4019  
4020 
(idD_D2_2, idCD_D_3, c_2, dd_2) 
4021 
= D_D2_en(idD_D2_1, idCD_D_2, c_1, dd_1, false); 
4022 

4023  
4024 
(idCD_D, c, dd, idD_D1, idD_D2) 
4025 
= (idCD_D_3, c_2, dd_2, idD_D1_2, idD_D2_2); 
4026  
4027  
4028 
tel 
4029  
4030 
until true restart POINTCD_D 
4031  
4032  
4033  
4034 
state D_D2_IDL: 
4035  
4036 
var c_2:int; 
4037 
dd_2:int; 
4038 
idD_D2_2:int; 
4039 
let 
4040  
4041 

4042 
(idD_D2_2, c_2, dd_2) 
4043 
= D_D2_node(idD_D2_1, c_1, dd_1, S, R); 
4044  
4045 

4046  
4047  
4048 
(idCD_D, c, dd, idD_D1, idD_D2) 
4049 
= (idCD_D_1, c_2, dd_2, idD_D1_1, idD_D2_2); 
4050 

4051  
4052 
tel 
4053  
4054 
until true restart POINTCD_D 
4055  
4056  
4057  
4058 
state D_D1_IDL: 
4059  
4060 
var c_2:int; 
4061 
dd_2:int; 
4062 
idD_D1_2:int; 
4063 
let 
4064  
4065 

4066 
(idD_D1_2, c_2, dd_2) 
4067 
= D_D1_node(idD_D1_1, c_1, dd_1, S, R); 
4068  
4069 

4070  
4071  
4072 
(idCD_D, c, dd, idD_D1, idD_D2) 
4073 
= (idCD_D_1, c_2, dd_2, idD_D1_2, idD_D2_1); 
4074 

4075  
4076 
tel 
4077  
4078 
until true restart POINTCD_D 
4079  
4080  
4081  
4082 
tel 
4083  
4084  
4085 
***************************************************State :C_C2 Automaton*************************************************** 
4086  
4087 
node C_C2_node(idC_C2_1:int; 
4088 
b_1:int; 
4089 
c_1:int; 
4090 
S:bool; 
4091 
R:bool) 
4092  
4093 
returns (idC_C2:int; 
4094 
b:int; 
4095 
c:int); 
4096  
4097  
4098 
let 
4099  
4100 
automaton c_c2 
4101  
4102 
state POINTC_C2: 
4103 
unless (idC_C2_1=0) restart POINT__TO__C2_C2A_1 
4104  
4105  
4106  
4107 
unless (idC_C2_1=1662) and S restart C2_C2A__TO__C2_C2B_1 
4108  
4109  
4110  
4111 
unless (idC_C2_1=1663) and R restart C2_C2B__TO__C2_C2A_1 
4112  
4113  
4114  
4115 
unless (idC_C2_1=1662) restart C2_C2A_IDL 
4116  
4117 
unless (idC_C2_1=1663) restart C2_C2B_IDL 
4118  
4119 
let 
4120  
4121 
(idC_C2, b, c) 
4122 
= (idC_C2_1, b_1, c_1); 
4123 

4124  
4125 
tel 
4126  
4127  
4128  
4129 
state POINT__TO__C2_C2A_1: 
4130  
4131 
var idC_C2_2:int; 
4132 
b_2:int; 
4133 
c_2:int; 
4134 
let 
4135  
4136 
 transition trace : 
4137 
POINT__To__C2_C2a_1 
4138 
(idC_C2_2, b_2, c_2) 
4139 
= C2_C2a_en(idC_C2_1, b_1, c_1, false); 
4140 

4141  
4142 
(idC_C2, b, c) 
4143 
= (idC_C2_2, b_2, c_2); 
4144  
4145  
4146 
tel 
4147  
4148 
until true restart POINTC_C2 
4149  
4150  
4151  
4152 
state C2_C2A__TO__C2_C2B_1: 
4153  
4154 
var idC_C2_2, idC_C2_3:int; 
4155 
b_2:int; 
4156 
c_2:int; 
4157 
let 
4158  
4159 
 transition trace : 
4160 
C2_C2a__To__C2_C2b_1 
4161 
(idC_C2_2) 
4162 
= C2_C2a_ex(idC_C2_1, false); 
4163 

4164  
4165 
(idC_C2_3, b_2, c_2) 
4166 
= C2_C2b_en(idC_C2_2, b_1, c_1, false); 
4167 

4168  
4169 
(idC_C2, b, c) 
4170 
= (idC_C2_3, b_2, c_2); 
4171  
4172  
4173 
tel 
4174  
4175 
until true restart POINTC_C2 
4176  
4177  
4178  
4179 
state C2_C2B__TO__C2_C2A_1: 
4180  
4181 
var idC_C2_2, idC_C2_3:int; 
4182 
b_2:int; 
4183 
c_2:int; 
4184 
let 
4185  
4186 
 transition trace : 
4187 
C2_C2b__To__C2_C2a_1 
4188 
(idC_C2_2) 
4189 
= C2_C2b_ex(idC_C2_1, false); 
4190 

4191  
4192 
(idC_C2_3, b_2, c_2) 
4193 
= C2_C2a_en(idC_C2_2, b_1, c_1, false); 
4194 

4195  
4196 
(idC_C2, b, c) 
4197 
= (idC_C2_3, b_2, c_2); 
4198  
4199  
4200 
tel 
4201  
4202 
until true restart POINTC_C2 
4203  
4204  
4205  
4206 
state C2_C2A_IDL: 
4207  
4208 
let 
4209  
4210 

4211  
4212 
(idC_C2, b, c) 
4213 
= (idC_C2_1, b_1, c_1); 
4214 

4215  
4216 
tel 
4217  
4218 
until true restart POINTC_C2 
4219  
4220  
4221  
4222 
state C2_C2B_IDL: 
4223  
4224 
let 
4225  
4226 

4227  
4228 
(idC_C2, b, c) 
4229 
= (idC_C2_1, b_1, c_1); 
4230 

4231  
4232 
tel 
4233  
4234 
until true restart POINTC_C2 
4235  
4236  
4237  
4238 
tel 
4239  
4240  
4241 
***************************************************State :C_C1 Automaton*************************************************** 
4242  
4243 
node C_C1_node(idC_C1_1:int; 
4244 
b_1:int; 
4245 
c_1:int; 
4246 
S:bool; 
4247 
R:bool) 
4248  
4249 
returns (idC_C1:int; 
4250 
b:int; 
4251 
c:int); 
4252  
4253  
4254 
let 
4255  
4256 
automaton c_c1 
4257  
4258 
state POINTC_C1: 
4259 
unless (idC_C1_1=0) restart POINT__TO__C1_C1A_1 
4260  
4261  
4262  
4263 
unless (idC_C1_1=1665) and S restart C1_C1A__TO__C1_C1B_1 
4264  
4265  
4266  
4267 
unless (idC_C1_1=1666) and R restart C1_C1B__TO__C1_C1A_1 
4268  
4269  
4270  
4271 
unless (idC_C1_1=1665) restart C1_C1A_IDL 
4272  
4273 
unless (idC_C1_1=1666) restart C1_C1B_IDL 
4274  
4275 
let 
4276  
4277 
(idC_C1, b, c) 
4278 
= (idC_C1_1, b_1, c_1); 
4279 

4280  
4281 
tel 
4282  
4283  
4284  
4285 
state POINT__TO__C1_C1A_1: 
4286  
4287 
var idC_C1_2:int; 
4288 
b_2:int; 
4289 
c_2:int; 
4290 
let 
4291  
4292 
 transition trace : 
4293 
POINT__To__C1_C1a_1 
4294 
(idC_C1_2, b_2, c_2) 
4295 
= C1_C1a_en(idC_C1_1, b_1, c_1, false); 
4296 

4297  
4298 
(idC_C1, b, c) 
4299 
= (idC_C1_2, b_2, c_2); 
4300  
4301  
4302 
tel 
4303  
4304 
until true restart POINTC_C1 
4305  
4306  
4307  
4308 
state C1_C1A__TO__C1_C1B_1: 
4309  
4310 
var idC_C1_2, idC_C1_3:int; 
4311 
b_2:int; 
4312 
c_2:int; 
4313 
let 
4314  
4315 
 transition trace : 
4316 
C1_C1a__To__C1_C1b_1 
4317 
(idC_C1_2) 
4318 
= C1_C1a_ex(idC_C1_1, false); 
4319 

4320  
4321 
(idC_C1_3, b_2, c_2) 
4322 
= C1_C1b_en(idC_C1_2, b_1, c_1, false); 
4323 

4324  
4325 
(idC_C1, b, c) 
4326 
= (idC_C1_3, b_2, c_2); 
4327  
4328  
4329 
tel 
4330  
4331 
until true restart POINTC_C1 
4332  
4333  
4334  
4335 
state C1_C1B__TO__C1_C1A_1: 
4336  
4337 
var idC_C1_2, idC_C1_3:int; 
4338 
b_2:int; 
4339 
c_2:int; 
4340 
let 
4341  
4342 
 transition trace : 
4343 
C1_C1b__To__C1_C1a_1 
4344 
(idC_C1_2) 
4345 
= C1_C1b_ex(idC_C1_1, false); 
4346 

4347  
4348 
(idC_C1_3, b_2, c_2) 
4349 
= C1_C1a_en(idC_C1_2, b_1, c_1, false); 
4350 

4351  
4352 
(idC_C1, b, c) 
4353 
= (idC_C1_3, b_2, c_2); 
4354  
4355  
4356 
tel 
4357  
4358 
until true restart POINTC_C1 
4359  
4360  
4361  
4362 
state C1_C1A_IDL: 
4363  
4364 
let 
4365  
4366 

4367  
4368 
(idC_C1, b, c) 
4369 
= (idC_C1_1, b_1, c_1); 
4370 

4371  
4372 
tel 
4373  
4374 
until true restart POINTC_C1 
4375  
4376  
4377  
4378 
state C1_C1B_IDL: 
4379  
4380 
let 
4381  
4382 

4383  
4384 
(idC_C1, b, c) 
4385 
= (idC_C1_1, b_1, c_1); 
4386 

4387  
4388 
tel 
4389  
4390 
until true restart POINTC_C1 
4391  
4392  
4393  
4394 
tel 
4395  
4396  
4397 
***************************************************State :CD_C Automaton*************************************************** 
4398  
4399 
node CD_C_node(idCD_C_1:int; 
4400 
b_1:int; 
4401 
c_1:int; 
4402 
idC_C1_1:int; 
4403 
T:bool; 
4404 
idC_C2_1:int; 
4405 
R:bool; 
4406 
S:bool) 
4407  
4408 
returns (idCD_C:int; 
4409 
b:int; 
4410 
c:int; 
4411 
idC_C1:int; 
4412 
idC_C2:int); 
4413  
4414  
4415 
let 
4416  
4417 
automaton cd_c 
4418  
4419 
state POINTCD_C: 
4420 
unless (idCD_C_1=0) restart POINT__TO__C_C1_1 
4421  
4422  
4423  
4424 
unless (idCD_C_1=1661) and T restart C_C2__TO__C_C1_1 
4425  
4426  
4427  
4428 
unless (idCD_C_1=1664) and T restart C_C1__TO__C_C2_1 
4429  
4430  
4431  
4432 
unless (idCD_C_1=1661) restart C_C2_IDL 
4433  
4434 
unless (idCD_C_1=1664) restart C_C1_IDL 
4435  
4436 
let 
4437  
4438 
(idCD_C, b, c, idC_C1, idC_C2) 
4439 
= (idCD_C_1, b_1, c_1, idC_C1_1, idC_C2_1); 
4440 

4441  
4442 
tel 
4443  
4444  
4445  
4446 
state POINT__TO__C_C1_1: 
4447  
4448 
var idCD_C_2:int; 
4449 
b_2:int; 
4450 
c_2:int; 
4451 
idC_C1_2:int; 
4452 
let 
4453  
4454 
 transition trace : 
4455 
POINT__To__C_C1_1 
4456 
(idC_C1_2, idCD_C_2, b_2, c_2) 
4457 
= C_C1_en(idC_C1_1, idCD_C_1, b_1, c_1, false); 
4458 

4459  
4460 
(idCD_C, b, c, idC_C1) 
4461 
= (idCD_C_2, b_2, c_2, idC_C1_2); 
4462  
4463 
add unused variables 
4464 
(idC_C2) 
4465 
= (idC_C2_1); 
4466 

4467  
4468 
tel 
4469  
4470 
until true restart POINTCD_C 
4471  
4472  
4473  
4474 
state C_C2__TO__C_C1_1: 
4475  
4476 
var idCD_C_2, idCD_C_3:int; 
4477 
b_2:int; 
4478 
c_2:int; 
4479 
idC_C1_2:int; 
4480 
idC_C2_2:int; 
4481 
let 
4482  
4483 
 transition trace : 
4484 
C_C2__To__C_C1_1 
4485 
(idC_C2_2, idCD_C_2) 
4486 
= C_C2_ex(idC_C2_1, idCD_C_1, false); 
4487 

4488  
4489 
(idC_C1_2, idCD_C_3, b_2, c_2) 
4490 
= C_C1_en(idC_C1_1, idCD_C_2, b_1, c_1, false); 
4491 

4492  
4493 
(idCD_C, b, c, idC_C1, idC_C2) 
4494 
= (idCD_C_3, b_2, c_2, idC_C1_2, idC_C2_2); 
4495  
4496  
4497 
tel 
4498  
4499 
until true restart POINTCD_C 
4500  
4501  
4502  
4503 
state C_C1__TO__C_C2_1: 
4504  
4505 
var idCD_C_2, idCD_C_3:int; 
4506 
b_2:int; 
4507 
c_2:int; 
4508 
idC_C1_2:int; 
4509 
idC_C2_2:int; 
4510 
let 
4511  
4512 
 transition trace : 
4513 
C_C1__To__C_C2_1 
4514 
(idC_C1_2, idCD_C_2) 
4515 
= C_C1_ex(idC_C1_1, idCD_C_1, false); 
4516 

4517  
4518 
(idC_C2_2, idCD_C_3, b_2, c_2) 
4519 
= C_C2_en(idC_C2_1, idCD_C_2, b_1, c_1, false); 
4520 

4521  
4522 
(idCD_C, b, c, idC_C1, idC_C2) 
4523 
= (idCD_C_3, b_2, c_2, idC_C1_2, idC_C2_2); 
4524  
4525  
4526 
tel 
4527  
4528 
until true restart POINTCD_C 
4529  
4530  
4531  
4532 
state C_C2_IDL: 
4533  
4534 
var b_2:int; 
4535 
c_2:int; 
4536 
idC_C2_2:int; 
4537 
let 
4538  
4539 

4540 
(idC_C2_2, b_2, c_2) 
4541 
= C_C2_node(idC_C2_1, b_1, c_1, S, R); 
4542  
4543 

4544  
4545  
4546 
(idCD_C, b, c, idC_C1, idC_C2) 
4547 
= (idCD_C_1, b_2, c_2, idC_C1_1, idC_C2_2); 
4548 

4549  
4550 
tel 
4551  
4552 
until true restart POINTCD_C 
4553  
4554  
4555  
4556 
state C_C1_IDL: 
4557  
4558 
var b_2:int; 
4559 
c_2:int; 
4560 
idC_C1_2:int; 
4561 
let 
4562  
4563 

4564 
(idC_C1_2, b_2, c_2) 
4565 
= C_C1_node(idC_C1_1, b_1, c_1, S, R); 
4566  
4567 

4568  
4569  
4570 
(idCD_C, b, c, idC_C1, idC_C2) 
4571 
= (idCD_C_1, b_2, c_2, idC_C1_2, idC_C2_1); 
4572 

4573  
4574 
tel 
4575  
4576 
until true restart POINTCD_C 
4577  
4578  
4579  
4580 
tel 
4581  
4582  
4583 
***************************************************State :Parallel4_CD Automaton*************************************************** 
4584  
4585 
node Parallel4_CD_node(idParallel4_CD_1:int; 
4586 
b_1:int; 
4587 
c_1:int; 
4588 
idCD_C_1:int; 
4589 
idC_C1_1:int; 
4590 
idC_C2_1:int; 
4591 
dd_1:int; 
4592 
idCD_D_1:int; 
4593 
idD_D1_1:int; 
4594 
idD_D2_1:int; 
4595 
R:bool; 
4596 
S:bool; 
4597 
T:bool) 
4598  
4599 
returns (idParallel4_CD:int; 
4600 
b:int; 
4601 
c:int; 
4602 
idCD_C:int; 
4603 
idC_C1:int; 
4604 
idC_C2:int; 
4605 
dd:int; 
4606 
idCD_D:int; 
4607 
idD_D1:int; 
4608 
idD_D2:int); 
4609  
4610  
4611 
let 
4612  
4613 
automaton parallel4_cd 
4614  
4615 
state POINTParallel4_CD: 
4616 
unless (idParallel4_CD_1=0) restart PARALLEL4_CD_PARALLEL_ENTRY 
4617 
unless true restart PARALLEL4_CD_PARALLEL_IDL 
4618  
4619 
let 
4620  
4621 
(idParallel4_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4622 
= (idParallel4_CD_1, b_1, c_1, idCD_C_1, idC_C1_1, idC_C2_1, dd_1, idCD_D_1, idD_D1_1, idD_D2_1); 
4623 

4624  
4625 
tel 
4626  
4627  
4628  
4629 
state PARALLEL4_CD_PARALLEL_ENTRY: 
4630  
4631 
var idParallel4_CD_2, idParallel4_CD_3:int; 
4632 
b_2:int; 
4633 
c_2, c_3:int; 
4634 
idCD_C_2:int; 
4635 
idC_C1_2:int; 
4636 
idC_C2_2:int; 
4637 
dd_2:int; 
4638 
idCD_D_2:int; 
4639 
idD_D1_2:int; 
4640 
idD_D2_2:int; 
4641 
let 
4642  
4643 

4644 
(idCD_C_2, idParallel4_CD_2, b_2, c_2, idC_C1_2, idC_C2_2) 
4645 
= CD_C_en(idCD_C_1, idParallel4_CD_1, b_1, c_1, idC_C1_1, idC_C2_1, false); 
4646  
4647 
(idCD_D_2, idParallel4_CD_3, c_3, dd_2, idD_D1_2, idD_D2_2) 
4648 
= CD_D_en(idCD_D_1, idParallel4_CD_2, c_2, dd_1, idD_D1_1, idD_D2_1, false); 
4649  
4650  
4651 
(idParallel4_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4652 
= (idParallel4_CD_3, b_2, c_3, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2); 
4653 

4654  
4655 
tel 
4656  
4657 
until true restart POINTParallel4_CD 
4658  
4659  
4660  
4661 
state PARALLEL4_CD_PARALLEL_IDL: 
4662  
4663 
var b_2:int; 
4664 
c_2, c_3:int; 
4665 
idCD_C_2:int; 
4666 
idC_C1_2:int; 
4667 
idC_C2_2:int; 
4668 
dd_2:int; 
4669 
idCD_D_2:int; 
4670 
idD_D1_2:int; 
4671 
idD_D2_2:int; 
4672 
let 
4673  
4674 

4675  
4676 
(idCD_C_2, b_2, c_2, idC_C1_2, idC_C2_2) 
4677 
= if not (idCD_C_1= 0 ) then CD_C_node(idCD_C_1, b_1, c_1, idC_C1_1, T, idC_C2_1, R, S) 
4678  
4679 
else (idCD_C_1, b_1, c_1, idC_C1_1, idC_C2_1); 
4680  
4681 

4682  
4683 

4684  
4685 
(idCD_D_2, c_3, dd_2, idD_D1_2, idD_D2_2) 
4686 
= if not (idCD_D_1= 0 ) then CD_D_node(idCD_D_1, c_2, dd_1, idD_D1_1, T, idD_D2_1, R, S) 
4687  
4688 
else (idCD_D_1, c_2, dd_1, idD_D1_1, idD_D2_1); 
4689  
4690 

4691  
4692 

4693  
4694 
(idParallel4_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4695 
= (idParallel4_CD_1, b_2, c_3, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2); 
4696 

4697  
4698 
tel 
4699  
4700 
until true restart POINTParallel4_CD 
4701  
4702  
4703  
4704 
tel 
4705  
4706  
4707 
***************************************************State :A_A2 Automaton*************************************************** 
4708  
4709 
node A_A2_node(idA_A2_1:int; 
4710 
a_1:int; 
4711 
x:int; 
4712 
S:bool; 
4713 
idCD_C_1:int; 
4714 
idCD_D_1:int; 
4715 
idC_C1_1:int; 
4716 
idC_C2_1:int; 
4717 
idD_D1_1:int; 
4718 
idD_D2_1:int; 
4719 
idParallel4_CD_1:int; 
4720 
idParallel4_Parallel4_1:int; 
4721 
idB_B1_1:int; 
4722 
idB_B2_1:int; 
4723 
idParallel4_B_1:int; 
4724 
idA_A1_1:int; 
4725 
idParallel4_A_1:int; 
4726 
b_1:int; 
4727 
c_1:int; 
4728 
dd_1:int; 
4729 
R:bool) 
4730  
4731 
returns (idA_A2:int; 
4732 
a:int; 
4733 
idCD_C:int; 
4734 
idCD_D:int; 
4735 
idC_C1:int; 
4736 
idC_C2:int; 
4737 
idD_D1:int; 
4738 
idD_D2:int; 
4739 
idParallel4_CD:int; 
4740 
idParallel4_Parallel4:int; 
4741 
idB_B1:int; 
4742 
idB_B2:int; 
4743 
idParallel4_B:int; 
4744 
idA_A1:int; 
4745 
idParallel4_A:int; 
4746 
b:int; 
4747 
c:int; 
4748 
dd:int); 
4749  
4750  
4751 
let 
4752  
4753 
automaton a_a2 
4754  
4755 
state POINTA_A2: 
4756 
unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1 
4757  
4758  
4759  
4760 
unless (idA_A2_1=1651) and S restart A2_A2A__TO__A2_A2B_1 
4761  
4762  
4763  
4764 
unless (idA_A2_1=1652) and S restart A2_A2B__TO__C2_C2A_1 
4765  
4766  
4767  
4768 
unless (idA_A2_1=1652) and R restart A2_A2B__TO__A2_A2A_2 
4769  
4770  
4771  
4772 
unless (idA_A2_1=1651) restart A2_A2A_IDL 
4773  
4774 
unless (idA_A2_1=1652) restart A2_A2B_IDL 
4775  
4776 
let 
4777  
4778 
(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4779 
= (idA_A2_1, a_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1); 
4780 

4781  
4782 
tel 
4783  
4784  
4785  
4786 
state POINT__TO__A2_A2A_1: 
4787  
4788 
var idA_A2_2:int; 
4789 
a_2:int; 
4790 
let 
4791  
4792 
 transition trace : 
4793 
POINT__To__A2_A2a_1 
4794 
(idA_A2_2, a_2) 
4795 
= A2_A2a_en(idA_A2_1, x, a_1, false); 
4796 

4797  
4798 
(idA_A2, a) 
4799 
= (idA_A2_2, a_2); 
4800  
4801 
add unused variables 
4802 
(b, c, dd, idA_A1, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_A, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
4803 
= (b_1, c_1, dd_1, idA_A1_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_A_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
4804 

4805  
4806 
tel 
4807  
4808 
until true restart POINTA_A2 
4809  
4810  
4811  
4812 
state A2_A2A__TO__A2_A2B_1: 
4813  
4814 
var idA_A2_2, idA_A2_3:int; 
4815 
a_2:int; 
4816 
let 
4817  
4818 
 transition trace : 
4819 
A2_A2a__To__A2_A2b_1 
4820 
(idA_A2_2) 
4821 
= A2_A2a_ex(idA_A2_1, false); 
4822 

4823  
4824 
(idA_A2_3, a_2) 
4825 
= A2_A2b_en(idA_A2_2, x, a_1, false); 
4826 

4827  
4828 
(idA_A2, a) 
4829 
= (idA_A2_3, a_2); 
4830  
4831 
add unused variables 
4832 
(b, c, dd, idA_A1, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_A, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
4833 
= (b_1, c_1, dd_1, idA_A1_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_A_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
4834 

4835  
4836 
tel 
4837  
4838 
until true restart POINTA_A2 
4839  
4840  
4841  
4842 
state A2_A2B__TO__C2_C2A_1: 
4843  
4844 
var idA_A2_2, idA_A2_3:int; 
4845 
a_2, a_3:int; 
4846 
idCD_C_2, idCD_C_3, idCD_C_4, idCD_C_5:int; 
4847 
idCD_D_2, idCD_D_3:int; 
4848 
idC_C1_2, idC_C1_3:int; 
4849 
idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5:int; 
4850 
idD_D1_2, idD_D1_3:int; 
4851 
idD_D2_2, idD_D2_3:int; 
4852 
idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4, idParallel4_CD_5:int; 
4853 
idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4, idParallel4_Parallel4_5, idParallel4_Parallel4_6, idParallel4_Parallel4_7:int; 
4854 
idB_B1_2, idB_B1_3:int; 
4855 
idB_B2_2, idB_B2_3:int; 
4856 
idParallel4_B_2, idParallel4_B_3:int; 
4857 
idA_A1_2, idA_A1_3:int; 
4858 
idParallel4_A_2, idParallel4_A_3:int; 
4859 
b_2, b_3:int; 
4860 
c_2:int; 
4861 
dd_2:int; 
4862 
let 
4863  
4864 
 transition trace : 
4865 
A2_A2b__To__C2_C2a_1 
4866 
(idD_D2_2, idCD_D_2, idD_D1_2, idParallel4_CD_2, idCD_C_2, idC_C1_2, idC_C2_2, idParallel4_Parallel4_2) 
4867 
= Parallel4_CD_ex(idD_D2_1, idCD_D_1, idD_D1_1, idParallel4_CD_1, idCD_C_1, idC_C1_1, idC_C2_1, idParallel4_Parallel4_1, false); 
4868 

4869  
4870 
(idB_B2_2, idParallel4_B_2, idB_B1_2, idParallel4_Parallel4_3) 
4871 
= Parallel4_B_ex(idB_B2_1, idParallel4_B_1, idB_B1_1, idParallel4_Parallel4_2, false); 
4872 

4873  
4874 
(idA_A2_2, idParallel4_A_2, idA_A1_2, idParallel4_Parallel4_4) 
4875 
= Parallel4_A_ex(idA_A2_1, idParallel4_A_1, idA_A1_1, idParallel4_Parallel4_3, false); 
4876 

4877  
4878 
idC_C2_3 
4879 
= 1662; 
4880 

4881 
idCD_C_3 
4882 
= 1661; 
4883 

4884 
idParallel4_CD_3 
4885 
= 1660; 
4886 

4887 
(idParallel4_A_3, idParallel4_Parallel4_5, a_2, idA_A1_3, idA_A2_3) 
4888 
= Parallel4_A_en(idParallel4_A_2, idParallel4_Parallel4_4, a_1, idA_A1_2, x, idA_A2_2, false); 
4889 

4890  
4891 
(idParallel4_B_3, idParallel4_Parallel4_6, a_3, b_2, idB_B1_3, idB_B2_3) 
4892 
= Parallel4_B_en(idParallel4_B_2, idParallel4_Parallel4_5, a_2, b_1, idB_B1_2, idB_B2_2, false); 
4893 

4894  
4895 
idC_C2_4 
4896 
= 1662; 
4897 

4898 
idCD_C_4 
4899 
= 1661; 
4900 

4901 
idParallel4_CD_4 
4902 
= 1660; 
4903 

4904 
(idParallel4_CD_5, idParallel4_Parallel4_7, b_3, c_2, idCD_C_5, idC_C1_3, idC_C2_5, dd_2, idCD_D_3, idD_D1_3, idD_D2_3) 
4905 
= Parallel4_CD_en(idParallel4_CD_4, idParallel4_Parallel4_6, b_2, c_1, idCD_C_4, idC_C1_2, idC_C2_4, dd_1, idCD_D_2, idD_D1_2, idD_D2_2, false); 
4906 

4907  
4908 
(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4909 
= (idA_A2_3, a_3, idCD_C_5, idCD_D_3, idC_C1_3, idC_C2_5, idD_D1_3, idD_D2_3, idParallel4_CD_5, idParallel4_Parallel4_7, idB_B1_3, idB_B2_3, idParallel4_B_3, idA_A1_3, idParallel4_A_3, b_3, c_2, dd_2); 
4910  
4911  
4912 
tel 
4913  
4914 
until true restart POINTA_A2 
4915  
4916  
4917  
4918 
state A2_A2B__TO__A2_A2A_2: 
4919  
4920 
var idA_A2_2, idA_A2_3:int; 
4921 
a_2:int; 
4922 
let 
4923  
4924 
 transition trace : 
4925 
A2_A2b__To__A2_A2a_2 
4926 
(idA_A2_2) 
4927 
= A2_A2b_ex(idA_A2_1, false); 
4928 

4929  
4930 
(idA_A2_3, a_2) 
4931 
= A2_A2a_en(idA_A2_2, x, a_1, false); 
4932 

4933  
4934 
(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4935 
= (idA_A2_3, a_2, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1); 
4936  
4937  
4938 
tel 
4939  
4940 
until true restart POINTA_A2 
4941  
4942  
4943  
4944 
state A2_A2A_IDL: 
4945  
4946 
let 
4947  
4948 

4949  
4950 
(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4951 
= (idA_A2_1, a_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1); 
4952 

4953  
4954 
tel 
4955  
4956 
until true restart POINTA_A2 
4957  
4958  
4959  
4960 
state A2_A2B_IDL: 
4961  
4962 
let 
4963  
4964 

4965  
4966 
(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4967 
= (idA_A2_1, a_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1); 
4968 

4969  
4970 
tel 
4971  
4972 
until true restart POINTA_A2 
4973  
4974  
4975  
4976 
tel 
4977  
4978  
4979 
***************************************************State :A_A1 Automaton*************************************************** 
4980  
4981 
node A_A1_node(idA_A1_1:int; 
4982 
a_1:int; 
4983 
x:int; 
4984 
S:bool; 
4985 
R:bool) 
4986  
4987 
returns (idA_A1:int; 
4988 
a:int); 
4989  
4990  
4991 
let 
4992  
4993 
automaton a_a1 
4994  
4995 
state POINTA_A1: 
4996 
unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1 
4997  
4998  
4999  
5000 
unless (idA_A1_1=1648) and S restart A1_A1A__TO__A1_A1B_1 
5001  
5002  
5003  
5004 
unless (idA_A1_1=1649) and R restart A1_A1B__TO__A1_A1A_1 
5005  
5006  
5007  
5008 
unless (idA_A1_1=1648) restart A1_A1A_IDL 
5009  
5010 
unless (idA_A1_1=1649) restart A1_A1B_IDL 
5011  
5012 
let 
5013  
5014 
(idA_A1, a) 
5015 
= (idA_A1_1, a_1); 
5016 

5017  
5018 
tel 
5019  
5020  
5021  
5022 
state POINT__TO__A1_A1A_1: 
5023  
5024 
var idA_A1_2:int; 
5025 
a_2:int; 
5026 
let 
5027  
5028 
 transition trace : 
5029 
POINT__To__A1_A1a_1 
5030 
(idA_A1_2, a_2) 
5031 
= A1_A1a_en(idA_A1_1, x, a_1, false); 
5032 

5033  
5034 
(idA_A1, a) 
5035 
= (idA_A1_2, a_2); 
5036  
5037  
5038 
tel 
5039  
5040 
until true restart POINTA_A1 
5041  
5042  
5043  
5044 
state A1_A1A__TO__A1_A1B_1: 
5045  
5046 
var idA_A1_2, idA_A1_3:int; 
5047 
a_2:int; 
5048 
let 
5049  
5050 
 transition trace : 
5051 
A1_A1a__To__A1_A1b_1 
5052 
(idA_A1_2) 
5053 
= A1_A1a_ex(idA_A1_1, false); 
5054 

5055  
5056 
(idA_A1_3, a_2) 
5057 
= A1_A1b_en(idA_A1_2, x, a_1, false); 
5058 

5059  
5060 
(idA_A1, a) 
5061 
= (idA_A1_3, a_2); 
5062  
5063  
5064 
tel 
5065  
5066 
until true restart POINTA_A1 
5067  
5068  
5069  
5070 
state A1_A1B__TO__A1_A1A_1: 
5071  
5072 
var idA_A1_2, idA_A1_3:int; 
5073 
a_2:int; 
5074 
let 
5075  
5076 
 transition trace : 
5077 
A1_A1b__To__A1_A1a_1 
5078 
(idA_A1_2) 
5079 
= A1_A1b_ex(idA_A1_1, false); 
5080 

5081  
5082 
(idA_A1_3, a_2) 
5083 
= A1_A1a_en(idA_A1_2, x, a_1, false); 
5084 

5085  
5086 
(idA_A1, a) 
5087 
= (idA_A1_3, a_2); 
5088  
5089  
5090 
tel 
5091  
5092 
until true restart POINTA_A1 
5093  
5094  
5095  
5096 
state A1_A1A_IDL: 
5097  
5098 
let 
5099  
5100 

5101  
5102 
(idA_A1, a) 
5103 
= (idA_A1_1, a_1); 
5104 

5105  
5106 
tel 
5107  
5108 
until true restart POINTA_A1 
5109  
5110  
5111  
5112 
state A1_A1B_IDL: 
5113  
5114 
let 
5115  
5116 

5117  
5118 
(idA_A1, a) 
5119 
= (idA_A1_1, a_1); 
5120 

5121  
5122 
tel 
5123  
5124 
until true restart POINTA_A1 
5125  
5126  
5127  
5128 
tel 
5129  
5130  
5131 
***************************************************State :Parallel4_A Automaton*************************************************** 
5132  
5133 
node Parallel4_A_node(idParallel4_A_1:int; 
5134 
a_1:int; 
5135 
idA_A1_1:int; 
5136 
x:int; 
5137 
T:bool; 
5138 
idA_A2_1:int; 
5139 
R:bool; 
5140 
S:bool; 
5141 
b_1:int; 
5142 
c_1:int; 
5143 
dd_1:int; 
5144 
idB_B1_1:int; 
5145 
idB_B2_1:int; 
5146 
idCD_C_1:int; 
5147 
idCD_D_1:int; 
5148 
idC_C1_1:int; 
5149 
idC_C2_1:int; 
5150 
idD_D1_1:int; 
5151 
idD_D2_1:int; 
5152 
idParallel4_B_1:int; 
5153 
idParallel4_CD_1:int; 
5154 
idParallel4_Parallel4_1:int) 
5155  
5156 
returns (idParallel4_A:int; 
5157 
a:int; 
5158 
idA_A1:int; 
5159 
idA_A2:int; 
5160 
b:int; 
5161 
c:int; 
5162 
dd:int; 
5163 
idB_B1:int; 
5164 
idB_B2:int; 
5165 
idCD_C:int; 
5166 
idCD_D:int; 
5167 
idC_C1:int; 
5168 
idC_C2:int; 
5169 
idD_D1:int; 
5170 
idD_D2:int; 
5171 
idParallel4_B:int; 
5172 
idParallel4_CD:int; 
5173 
idParallel4_Parallel4:int); 
5174  
5175  
5176 
let 
5177  
5178 
automaton parallel4_a 
5179  
5180 
state POINTParallel4_A: 
5181 
unless (idParallel4_A_1=0) restart POINT__TO__A_A1_1 
5182  
5183  
5184  
5185 
unless (idParallel4_A_1=1650) and T restart A_A2__TO__A_A1_1 
5186  
5187  
5188  
5189 
unless (idParallel4_A_1=1647) and T restart A_A1__TO__A_A2_1 
5190  
5191  
5192  
5193 
unless (idParallel4_A_1=1650) restart A_A2_IDL 
5194  
5195 
unless (idParallel4_A_1=1647) restart A_A1_IDL 
5196  
5197 
let 
5198  
5199 
(idParallel4_A, a, idA_A1, idA_A2, b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5200 
= (idParallel4_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
5201 

5202  
5203 
tel 
5204  
5205  
5206  
5207 
state POINT__TO__A_A1_1: 
5208  
5209 
var idParallel4_A_2:int; 
5210 
a_2:int; 
5211 
idA_A1_2:int; 
5212 
let 
5213  
5214 
 transition trace : 
5215 
POINT__To__A_A1_1 
5216 
(idA_A1_2, idParallel4_A_2, a_2) 
5217 
= A_A1_en(idA_A1_1, idParallel4_A_1, a_1, x, false); 
5218 

5219  
5220 
(idParallel4_A, a, idA_A1) 
5221 
= (idParallel4_A_2, a_2, idA_A1_2); 
5222  
5223 
add unused variables 
5224 
(b, c, dd, idA_A2, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5225 
= (b_1, c_1, dd_1, idA_A2_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
5226 

5227  
5228 
tel 
5229  
5230 
until true restart POINTParallel4_A 
5231  
5232  
5233  
5234 
state A_A2__TO__A_A1_1: 
5235  
5236 
var idParallel4_A_2, idParallel4_A_3:int; 
5237 
a_2:int; 
5238 
idA_A1_2:int; 
5239 
idA_A2_2:int; 
5240 
let 
5241  
5242 
 transition trace : 
5243 
A_A2__To__A_A1_1 
5244 
(idA_A2_2, idParallel4_A_2) 
5245 
= A_A2_ex(idA_A2_1, idParallel4_A_1, false); 
5246 

5247  
5248 
(idA_A1_2, idParallel4_A_3, a_2) 
5249 
= A_A1_en(idA_A1_1, idParallel4_A_2, a_1, x, false); 
5250 

5251  
5252 
(idParallel4_A, a, idA_A1, idA_A2) 
5253 
= (idParallel4_A_3, a_2, idA_A1_2, idA_A2_2); 
5254  
5255 
add unused variables 
5256 
(b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5257 
= (b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
5258 

5259  
5260 
tel 
5261  
5262 
until true restart POINTParallel4_A 
5263  
5264  
5265  
5266 
state A_A1__TO__A_A2_1: 
5267  
5268 
var idParallel4_A_2, idParallel4_A_3:int; 
5269 
a_2:int; 
5270 
idA_A1_2:int; 
5271 
idA_A2_2:int; 
5272 
let 
5273  
5274 
 transition trace : 
5275 
A_A1__To__A_A2_1 
5276 
(idA_A1_2, idParallel4_A_2) 
5277 
= A_A1_ex(idA_A1_1, idParallel4_A_1, false); 
5278 

5279  
5280 
(idA_A2_2, idParallel4_A_3, a_2) 
5281 
= A_A2_en(idA_A2_1, idParallel4_A_2, a_1, x, false); 
5282 

5283  
5284 
(idParallel4_A, a, idA_A1, idA_A2) 
5285 
= (idParallel4_A_3, a_2, idA_A1_2, idA_A2_2); 
5286  
5287 
add unused variables 
5288 
(b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5289 
= (b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
5290 

5291  
5292 
tel 
5293  
5294 
until true restart POINTParallel4_A 
5295  
5296  
5297  
5298 
state A_A2_IDL: 
5299  
5300 
var idParallel4_A_2:int; 
5301 
a_2:int; 
5302 
idA_A1_2:int; 
5303 
idA_A2_2:int; 
5304 
b_2:int; 
5305 
c_2:int; 
5306 
dd_2:int; 
5307 
idB_B1_2:int; 
5308 
idB_B2_2:int; 
5309 
idCD_C_2:int; 
5310 
idCD_D_2:int; 
5311 
idC_C1_2:int; 
5312 
idC_C2_2:int; 
5313 
idD_D1_2:int; 
5314 
idD_D2_2:int; 
5315 
idParallel4_B_2:int; 
5316 
idParallel4_CD_2:int; 
5317 
idParallel4_Parallel4_2:int; 
5318 
let 
5319  
5320 

5321 
(idA_A2_2, a_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2, idParallel4_Parallel4_2, idB_B1_2, idB_B2_2, idParallel4_B_2, idA_A1_2, idParallel4_A_2, b_2, c_2, dd_2) 
5322 
= A_A2_node(idA_A2_1, a_1, x, S, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1, R); 
5323  
5324 

5325  
5326  
5327 
(idParallel4_A, a, idA_A1, idA_A2, b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5328 
= (idParallel4_A_2, a_2, idA_A1_2, idA_A2_2, b_2, c_2, dd_2, idB_B1_2, idB_B2_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_B_2, idParallel4_CD_2, idParallel4_Parallel4_2); 
5329 

5330  
5331 
tel 
5332  
5333 
until true restart POINTParallel4_A 
5334  
5335  
5336  
5337 
state A_A1_IDL: 
5338  
5339 
var a_2:int; 
5340 
idA_A1_2:int; 
5341 
let 
5342  
5343 

5344 
(idA_A1_2, a_2) 
5345 
= A_A1_node(idA_A1_1, a_1, x, S, R); 
5346  
5347 

5348  
5349  
5350 
(idParallel4_A, a, idA_A1, idA_A2, b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5351 
= (idParallel4_A_1, a_2, idA_A1_2, idA_A2_1, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
5352 

5353  
5354 
tel 
5355  
5356 
until true restart POINTParallel4_A 
5357  
5358  
5359  
5360 
tel 
5361  
5362  
5363 
***************************************************State :Parallel4_Parallel4 Automaton*************************************************** 
5364  
5365 
node Parallel4_Parallel4_node(idParallel4_Parallel4_1:int; 
5366 
a_1:int; 
5367 
idA_A1_1:int; 
5368 
idA_A2_1:int; 
5369 
idParallel4_A_1:int; 
5370 
x:int; 
5371 
b_1:int; 
5372 
idB_B1_1:int; 
5373 
idB_B2_1:int; 
5374 
idParallel4_B_1:int; 
5375 
c_1:int; 
5376 
dd_1:int; 
5377 
idCD_C_1:int; 
5378 
idCD_D_1:int; 
5379 
idC_C1_1:int; 
5380 
idC_C2_1:int; 
5381 
idD_D1_1:int; 
5382 
idD_D2_1:int; 
5383 
idParallel4_CD_1:int; 
5384 
R:bool; 
5385 
S:bool; 
5386 
T:bool) 
5387  
5388 
returns (idParallel4_Parallel4:int; 
5389 
a:int; 
5390 
idA_A1:int; 
5391 
idA_A2:int; 
5392 
idParallel4_A:int; 
5393 
b:int; 
5394 
idB_B1:int; 
5395 
idB_B2:int; 
5396 
idParallel4_B:int; 
5397 
c:int; 
5398 
dd:int; 
5399 
idCD_C:int; 
5400 
idCD_D:int; 
5401 
idC_C1:int; 
5402 
idC_C2:int; 
5403 
idD_D1:int; 
5404 
idD_D2:int; 
5405 
idParallel4_CD:int); 
5406  
5407  
5408 
let 
5409  
5410 
automaton parallel4_parallel4 
5411  
5412 
state POINTParallel4_Parallel4: 
5413 
unless (idParallel4_Parallel4_1=0) restart PARALLEL4_PARALLEL4_PARALLEL_ENTRY 
5414 
unless true restart PARALLEL4_PARALLEL4_PARALLEL_IDL 
5415  
5416 
let 
5417  
5418 
(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD) 
5419 
= (idParallel4_Parallel4_1, a_1, idA_A1_1, idA_A2_1, idParallel4_A_1, b_1, idB_B1_1, idB_B2_1, idParallel4_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1); 
5420 

5421  
5422 
tel 
5423  
5424  
5425  
5426 
state PARALLEL4_PARALLEL4_PARALLEL_ENTRY: 
5427  
5428 
var idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4:int; 
5429 
a_2, a_3:int; 
5430 
idA_A1_2:int; 
5431 
idA_A2_2:int; 
5432 
idParallel4_A_2:int; 
5433 
b_2, b_3:int; 
5434 
idB_B1_2:int; 
5435 
idB_B2_2:int; 
5436 
idParallel4_B_2:int; 
5437 
c_2:int; 
5438 
dd_2:int; 
5439 
idCD_C_2:int; 
5440 
idCD_D_2:int; 
5441 
idC_C1_2:int; 
5442 
idC_C2_2:int; 
5443 
idD_D1_2:int; 
5444 
idD_D2_2:int; 
5445 
idParallel4_CD_2:int; 
5446 
let 
5447  
5448 

5449 
(idParallel4_A_2, idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2) 
5450 
= Parallel4_A_en(idParallel4_A_1, idParallel4_Parallel4_1, a_1, idA_A1_1, x, idA_A2_1, false); 
5451  
5452 
(idParallel4_B_2, idParallel4_Parallel4_3, a_3, b_2, idB_B1_2, idB_B2_2) 
5453 
= Parallel4_B_en(idParallel4_B_1, idParallel4_Parallel4_2, a_2, b_1, idB_B1_1, idB_B2_1, false); 
5454  
5455 
(idParallel4_CD_2, idParallel4_Parallel4_4, b_3, c_2, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2) 
5456 
= Parallel4_CD_en(idParallel4_CD_1, idParallel4_Parallel4_3, b_2, c_1, idCD_C_1, idC_C1_1, idC_C2_1, dd_1, idCD_D_1, idD_D1_1, idD_D2_1, false); 
5457  
5458  
5459 
(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD) 
5460 
= (idParallel4_Parallel4_4, a_3, idA_A1_2, idA_A2_2, idParallel4_A_2, b_3, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2); 
5461 

5462  
5463 
tel 
5464  
5465 
until true restart POINTParallel4_Parallel4 
5466  
5467  
5468  
5469 
state PARALLEL4_PARALLEL4_PARALLEL_IDL: 
5470  
5471 
var idParallel4_Parallel4_2:int; 
5472 
a_2, a_3:int; 
5473 
idA_A1_2:int; 
5474 
idA_A2_2:int; 
5475 
idParallel4_A_2:int; 
5476 
b_2, b_3, b_4:int; 
5477 
idB_B1_2, idB_B1_3:int; 
5478 
idB_B2_2, idB_B2_3:int; 
5479 
idParallel4_B_2, idParallel4_B_3:int; 
5480 
c_2, c_3:int; 
5481 
dd_2, dd_3:int; 
5482 
idCD_C_2, idCD_C_3:int; 
5483 
idCD_D_2, idCD_D_3:int; 
5484 
idC_C1_2, idC_C1_3:int; 
5485 
idC_C2_2, idC_C2_3:int; 
5486 
idD_D1_2, idD_D1_3:int; 
5487 
idD_D2_2, idD_D2_3:int; 
5488 
idParallel4_CD_2, idParallel4_CD_3:int; 
5489 
let 
5490  
5491 

5492  
5493 
(idParallel4_A_2, a_2, idA_A1_2, idA_A2_2, b_2, c_2, dd_2, idB_B1_2, idB_B2_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_B_2, idParallel4_CD_2, idParallel4_Parallel4_2) 
5494 
= if not (idParallel4_A_1= 0 ) then Parallel4_A_node(idParallel4_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R, S, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1) 
5495  
5496 
else (idParallel4_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1); 
5497  
5498 

5499  
5500 

5501  
5502 
(idParallel4_B_3, a_3, b_3, idB_B1_3, idB_B2_3) 
5503 
= if not (idParallel4_B_2= 0 ) then Parallel4_B_node(idParallel4_B_2, a_2, b_2, idB_B1_2, T, idB_B2_2, R, S) 
5504  
5505 
else (idParallel4_B_2, a_2, b_2, idB_B1_2, idB_B2_2); 
5506  
5507 

5508  
5509 

5510  
5511 
(idParallel4_CD_3, b_4, c_3, idCD_C_3, idC_C1_3, idC_C2_3, dd_3, idCD_D_3, idD_D1_3, idD_D2_3) 
5512 
= if not (idParallel4_CD_2= 0 ) then Parallel4_CD_node(idParallel4_CD_2, b_3, c_2, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2, R, S, T) 
5513  
5514 
else (idParallel4_CD_2, b_3, c_2, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2); 
5515  
5516 

5517  
5518 

5519  
5520 
(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD) 
5521 
= (idParallel4_Parallel4_2, a_3, idA_A1_2, idA_A2_2, idParallel4_A_2, b_4, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3); 
5522 

5523  
5524 
tel 
5525  
5526 
until true restart POINTParallel4_Parallel4 
5527  
5528  
5529  
5530 
tel 
5531  
5532  
5533 
***************************************************State :Parallel4_Parallel4 Automaton*************************************************** 
5534  
5535 
node Parallel4_Parallel4(x:int; 
5536 
R:bool; 
5537 
S:bool; 
5538 
T:bool) 
5539  
5540 
returns (a:int; 
5541 
b:int; 
5542 
dd:int; 
5543 
c:int); 
5544  
5545  
5546 
var a_1: int; 
5547  
5548 
b_1: int; 
5549  
5550 
dd_1: int; 
5551  
5552 
c_1: int; 
5553  
5554 
idParallel4_Parallel4, idParallel4_Parallel4_1: int; 
5555  
5556 
idB_B2, idB_B2_1: int; 
5557  
5558 
idB_B1, idB_B1_1: int; 
5559  
5560 
idParallel4_B, idParallel4_B_1: int; 
5561  
5562 
idD_D2, idD_D2_1: int; 
5563  
5564 
idD_D1, idD_D1_1: int; 
5565  
5566 
idCD_D, idCD_D_1: int; 
5567  
5568 
idC_C2, idC_C2_1: int; 
5569  
5570 
idC_C1, idC_C1_1: int; 
5571  
5572 
idCD_C, idCD_C_1: int; 
5573  
5574 
idParallel4_CD, idParallel4_CD_1: int; 
5575  
5576 
idA_A2, idA_A2_1: int; 
5577  
5578 
idA_A1, idA_A1_1: int; 
5579  
5580 
idParallel4_A, idParallel4_A_1: int; 
5581  
5582 
idParallel4_Parallel4_2, idParallel4_Parallel4_3:int; 
5583 
a_2, a_3:int; 
5584 
idA_A1_2, idA_A1_3:int; 
5585 
idA_A2_2, idA_A2_3:int; 
5586 
idParallel4_A_2, idParallel4_A_3:int; 
5587 
b_2, b_3:int; 
5588 
idB_B1_2, idB_B1_3:int; 
5589 
idB_B2_2, idB_B2_3:int; 
5590 
idParallel4_B_2, idParallel4_B_3:int; 
5591 
c_2, c_3:int; 
5592 
dd_2, dd_3:int; 
5593 
idCD_C_2, idCD_C_3:int; 
5594 
idCD_D_2, idCD_D_3:int; 
5595 
idC_C1_2, idC_C1_3:int; 
5596 
idC_C2_2, idC_C2_3:int; 
5597 
idD_D1_2, idD_D1_3:int; 
5598 
idD_D2_2, idD_D2_3:int; 
5599 
idParallel4_CD_2, idParallel4_CD_3:int; 
5600 
let 
5601  
5602 
a_1 = 0 > pre a; 
5603  
5604 
b_1 = 0 > pre b; 
5605  
5606 
dd_1 = 0 > pre dd; 
5607  
5608 
c_1 = 0 > pre c; 
5609  
5610 
idParallel4_Parallel4_1 = 0 > pre idParallel4_Parallel4; 
5611  
5612 
idB_B2_1 = 0 > pre idB_B2; 
5613  
5614 
idB_B1_1 = 0 > pre idB_B1; 
5615  
5616 
idParallel4_B_1 = 0 > pre idParallel4_B; 
5617  
5618 
idD_D2_1 = 0 > pre idD_D2; 
5619  
5620 
idD_D1_1 = 0 > pre idD_D1; 
5621  
5622 
idCD_D_1 = 0 > pre idCD_D; 
5623  
5624 
idC_C2_1 = 0 > pre idC_C2; 
5625  
5626 
idC_C1_1 = 0 > pre idC_C1; 
5627  
5628 
idCD_C_1 = 0 > pre idCD_C; 
5629  
5630 
idParallel4_CD_1 = 0 > pre idParallel4_CD; 
5631  
5632 
idA_A2_1 = 0 > pre idA_A2; 
5633  
5634 
idA_A1_1 = 0 > pre idA_A1; 
5635  
5636 
idParallel4_A_1 = 0 > pre idParallel4_A; 
5637  
5638 

5639  
5640  
5641  
5642 
(idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2, idParallel4_A_2, b_2, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2) 
5643 
= 
5644  
5645 
if R then Parallel4_Parallel4_node(idParallel4_Parallel4_1, a_1, idA_A1_1, idA_A2_1, idParallel4_A_1, x, b_1, idB_B1_1, idB_B2_1, idParallel4_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, R, false, false) 
5646  
5647 
else (idParallel4_Parallel4_1, a_1, idA_A1_1, idA_A2_1, idParallel4_A_1, b_1, idB_B1_1, idB_B2_1, idParallel4_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1); 
5648  
5649 

5650  
5651  
5652  
5653 
(idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_3, idParallel4_A_3, b_3, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3) 
5654 
= 
5655  
5656 
if S then Parallel4_Parallel4_node(idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2, idParallel4_A_2, x, b_2, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2, false, S, false) 
5657  
5658 
else (idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2, idParallel4_A_2, b_2, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2); 
5659  
5660 

5661  
5662  
5663  
5664 
(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD) 
5665 
= 
5666  
5667 
if T then Parallel4_Parallel4_node(idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_3, idParallel4_A_3, x, b_3, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3, false, false, T) 
5668  
5669 
else (idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_3, idParallel4_A_3, b_3, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3); 
5670  
5671 

5672  
5673  
5674 
unused outputs 
5675 

5676  
5677 
tel 
5678  
5679  
5680  
5681 
node Parallel4 (x_1_1 : int; R_1_1 : real; S_1_1 : real; T_1_1 : real) 
5682 
returns (a_1_1 : int; 
5683 
b_2_1 : int; 
5684 
dd_3_1 : int; 
5685 
c_4_1 : int); 
5686 
var 
5687 
Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real; 
5688 
Parallel4_1_1 : int; Parallel4_2_1 : int; Parallel4_3_1 : int; Parallel4_4_1 : int; 
5689 
i_virtual_local : real; 
5690 
Parallel4Mux_1_1_event: bool; 
5691 
Parallel4Mux_1_2_event: bool; 
5692 
Parallel4Mux_1_3_event: bool; 
5693 
let 
5694 
Mux_1_1 = R_1_1 ; 
5695 
Mux_1_2 = S_1_1 ; 
5696 
Mux_1_3 = T_1_1 ; 
5697 
Parallel4Mux_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)); 
5698 
Parallel4Mux_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)); 
5699 
Parallel4Mux_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)); 
5700 
(Parallel4_1_1, Parallel4_2_1, Parallel4_3_1, Parallel4_4_1) = Parallel4_Parallel4(x_1_1, Parallel4Mux_1_1_event, Parallel4Mux_1_2_event, Parallel4Mux_1_3_event); 
5701 
a_1_1 = Parallel4_1_1; 
5702 
b_2_1 = Parallel4_2_1; 
5703 
dd_3_1 = Parallel4_3_1; 
5704 
c_4_1 = Parallel4_4_1; 
5705 
i_virtual_local= 0.0 > 1.0; 
5706 
tel 
5707 