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

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9  
10 
node TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action(y_1:int) 
11  
12 
returns (y:int); 
13  
14  
15 
var y_2:int; 
16  
17  
18 
let 
19  
20  
21  
22 
y_2 
23 
= y_1 +100; 
24 

25  
26 
(y) 
27 
= (y_2); 
28 

29  
30 
tel 
31  
32  
33  
34  
35  
36  
37 
node POINT__To__TOP_B_2_Condition_Action(y_1:int) 
38  
39 
returns (y:int); 
40  
41  
42 
var y_2:int; 
43  
44  
45 
let 
46  
47  
48  
49 
y_2 
50 
= y_1 +10; 
51 

52  
53 
(y) 
54 
= (y_2); 
55 

56  
57 
tel 
58  
59  
60  
61  
62  
63  
64  
65 
node Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action(y_1:int) 
66  
67 
returns (y:int); 
68  
69  
70 
var y_2:int; 
71  
72  
73 
let 
74  
75  
76  
77 
y_2 
78 
= y_1 +10000; 
79 

80  
81 
(y) 
82 
= (y_2); 
83 

84  
85 
tel 
86  
87  
88  
89  
90  
91  
92  
93 
node TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action(y_1:int) 
94  
95 
returns (y:int); 
96  
97  
98 
var y_2:int; 
99  
100  
101 
let 
102  
103  
104  
105 
y_2 
106 
= y_1 +1000; 
107 

108  
109 
(y) 
110 
= (y_2); 
111 

112  
113 
tel 
114  
115  
116  
117  
118  
119  
120 
node POINT__To__TOP_A_1_Condition_Action(y_1:int) 
121  
122 
returns (y:int); 
123  
124  
125 
var y_2:int; 
126  
127  
128 
let 
129  
130  
131  
132 
y_2 
133 
= y_1 +1; 
134 

135  
136 
(y) 
137 
= (y_2); 
138 

139  
140 
tel 
141  
142  
143  
144  
145  
146  
147 
node Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action(y_1:int) 
148  
149 
returns (y:int); 
150  
151  
152 
var y_2:int; 
153  
154  
155 
let 
156  
157  
158  
159 
y_2 
160 
= y_1 +100000; 
161 

162  
163 
(y) 
164 
= (y_2); 
165 

166  
167 
tel 
168  
169  
170  
171  
172  
173  
174 
 Entry action for state :TOP_D 
175 
node TOP_D_en(idJunctions6_TOP_1:int; 
176 
isInner:bool) 
177  
178 
returns (idJunctions6_TOP:int); 
179  
180  
181 
var idJunctions6_TOP_2:int; 
182  
183  
184 
let 
185  
186  
187  
188 
 set state as active 
189 
idJunctions6_TOP_2 
190 
= 1300; 
191 

192  
193 
(idJunctions6_TOP) 
194 
= (idJunctions6_TOP_2); 
195 

196  
197 
tel 
198  
199  
200  
201  
202  
203 
 Exit action for state :TOP_D 
204 
node TOP_D_ex(idJunctions6_TOP_1:int; 
205 
isInner:bool) 
206  
207 
returns (idJunctions6_TOP:int); 
208  
209  
210 
var idJunctions6_TOP_2:int; 
211  
212  
213 
let 
214  
215  
216  
217 
 set state as inactive 
218 
idJunctions6_TOP_2 
219 
= if (not isInner) then 0 else idJunctions6_TOP_1; 
220  
221  
222 
(idJunctions6_TOP) 
223 
= (idJunctions6_TOP_1); 
224 

225  
226 
tel 
227  
228  
229  
230  
231  
232  
233 
 Entry action for state :TOP_B 
234 
node TOP_B_en(idJunctions6_TOP_1:int; 
235 
isInner:bool) 
236  
237 
returns (idJunctions6_TOP:int); 
238  
239  
240 
var idJunctions6_TOP_2:int; 
241  
242  
243 
let 
244  
245  
246  
247 
 set state as active 
248 
idJunctions6_TOP_2 
249 
= 1298; 
250 

251  
252 
(idJunctions6_TOP) 
253 
= (idJunctions6_TOP_2); 
254 

255  
256 
tel 
257  
258  
259  
260  
261  
262 
 Exit action for state :TOP_B 
263 
node TOP_B_ex(idJunctions6_TOP_1:int; 
264 
isInner:bool) 
265  
266 
returns (idJunctions6_TOP:int); 
267  
268  
269 
var idJunctions6_TOP_2:int; 
270  
271  
272 
let 
273  
274  
275  
276 
 set state as inactive 
277 
idJunctions6_TOP_2 
278 
= if (not isInner) then 0 else idJunctions6_TOP_1; 
279  
280  
281 
(idJunctions6_TOP) 
282 
= (idJunctions6_TOP_1); 
283 

284  
285 
tel 
286  
287  
288  
289  
290  
291  
292 
 Entry action for state :TOP_A 
293 
node TOP_A_en(idJunctions6_TOP_1:int; 
294 
isInner:bool) 
295  
296 
returns (idJunctions6_TOP:int); 
297  
298  
299 
var idJunctions6_TOP_2:int; 
300  
301  
302 
let 
303  
304  
305  
306 
 set state as active 
307 
idJunctions6_TOP_2 
308 
= 1297; 
309 

310  
311 
(idJunctions6_TOP) 
312 
= (idJunctions6_TOP_2); 
313 

314  
315 
tel 
316  
317  
318  
319  
320  
321 
 Exit action for state :TOP_A 
322 
node TOP_A_ex(idJunctions6_TOP_1:int; 
323 
isInner:bool) 
324  
325 
returns (idJunctions6_TOP:int); 
326  
327  
328 
var idJunctions6_TOP_2:int; 
329  
330  
331 
let 
332  
333  
334  
335 
 set state as inactive 
336 
idJunctions6_TOP_2 
337 
= if (not isInner) then 0 else idJunctions6_TOP_1; 
338  
339  
340 
(idJunctions6_TOP) 
341 
= (idJunctions6_TOP_1); 
342 

343  
344 
tel 
345  
346  
347  
348  
349  
350  
351 
 Entry action for state :TOP_C 
352 
node TOP_C_en(idJunctions6_TOP_1:int; 
353 
isInner:bool) 
354  
355 
returns (idJunctions6_TOP:int); 
356  
357  
358 
var idJunctions6_TOP_2:int; 
359  
360  
361 
let 
362  
363  
364  
365 
 set state as active 
366 
idJunctions6_TOP_2 
367 
= 1299; 
368 

369  
370 
(idJunctions6_TOP) 
371 
= (idJunctions6_TOP_2); 
372 

373  
374 
tel 
375  
376  
377  
378  
379  
380 
 Exit action for state :TOP_C 
381 
node TOP_C_ex(idJunctions6_TOP_1:int; 
382 
isInner:bool) 
383  
384 
returns (idJunctions6_TOP:int); 
385  
386  
387 
var idJunctions6_TOP_2:int; 
388  
389  
390 
let 
391  
392  
393  
394 
 set state as inactive 
395 
idJunctions6_TOP_2 
396 
= if (not isInner) then 0 else idJunctions6_TOP_1; 
397  
398  
399 
(idJunctions6_TOP) 
400 
= (idJunctions6_TOP_1); 
401 

402  
403 
tel 
404  
405  
406  
407  
408  
409  
410 
 Entry action for state :Junctions6_TOP 
411 
node Junctions6_TOP_en(idJunctions6_TOP_1:int; 
412 
idJunctions6_Junctions6_1:int; 
413 
x:int; 
414 
y_1:int; 
415 
isInner:bool) 
416  
417 
returns (idJunctions6_TOP:int; 
418 
idJunctions6_Junctions6:int; 
419 
y:int); 
420  
421  
422 
var idJunctions6_TOP_2, idJunctions6_TOP_3, idJunctions6_TOP_4, idJunctions6_TOP_5, idJunctions6_TOP_6, idJunctions6_TOP_7, idJunctions6_TOP_8, idJunctions6_TOP_9:int; 
423 
idJunctions6_Junctions6_2, idJunctions6_Junctions6_3, idJunctions6_Junctions6_4:int; 
424 
y_2, y_3, y_4, y_5:int; 
425  
426  
427 
let 
428  
429  
430  
431 
 set state as active 
432 
idJunctions6_Junctions6_2 
433 
= 1301; 
434 

435  
436 

437 
 transition trace : 
438 
POINT__To__TOP_A_1 
439 
 condition Action : y+=1 
440 

441 
(y_2) 
442 
= 
443 
if (( x<4 )) then 
444 
POINT__To__TOP_A_1_Condition_Action(y_1) 
445 
else (y_1); 
446 

447  
448 
(idJunctions6_TOP_2) 
449 
= 
450 
if (( x<4 )) then 
451 
TOP_A_en(idJunctions6_TOP_1, false) 
452 
else (idJunctions6_TOP_1); 
453 

454  
455 
 transition trace : 
456 
POINT__To__TOP_B_2 
457 
 condition Action : y+=10 
458 

459 
(y_3) 
460 
= 
461 
if (( x>=4 )) then 
462 
POINT__To__TOP_B_2_Condition_Action(y_1) 
463 
else (y_1); 
464 

465  
466 
(idJunctions6_TOP_3) 
467 
= 
468 
if (( x>=4 )) then 
469 
TOP_B_en(idJunctions6_TOP_1, false) 
470 
else (idJunctions6_TOP_1); 
471 

472  
473 
(idJunctions6_TOP_4, idJunctions6_Junctions6_3, y_4) 
474 
= 
475  
476 
if ( idJunctions6_TOP_1 = 0) then 
477  
478 

479 
if (( x<4 )) then 
480 
(idJunctions6_TOP_2, idJunctions6_Junctions6_2, y_2) 
481 
else 
482 
if (( x>=4 )) then 
483 
(idJunctions6_TOP_3, idJunctions6_Junctions6_2, y_3) 
484 
else (idJunctions6_TOP_1, idJunctions6_Junctions6_2, y_1) 
485  
486 
else(idJunctions6_TOP_1, idJunctions6_Junctions6_2, y_1); 
487  
488 

489  
490 
(idJunctions6_TOP_5) 
491 
= 
492 
if ( idJunctions6_TOP_1 = 1297) then 
493 
TOP_A_en(idJunctions6_TOP_1, false) 
494 
else (idJunctions6_TOP_1); 
495  
496 

497  
498 
(idJunctions6_TOP_6) 
499 
= 
500 
if ( idJunctions6_TOP_1 = 1298) then 
501 
TOP_B_en(idJunctions6_TOP_1, false) 
502 
else (idJunctions6_TOP_1); 
503  
504 

505  
506 
(idJunctions6_TOP_7) 
507 
= 
508 
if ( idJunctions6_TOP_1 = 1299) then 
509 
TOP_C_en(idJunctions6_TOP_1, false) 
510 
else (idJunctions6_TOP_1); 
511  
512 

513  
514 
(idJunctions6_TOP_8) 
515 
= 
516 
if ( idJunctions6_TOP_1 = 1300) then 
517 
TOP_D_en(idJunctions6_TOP_1, false) 
518 
else (idJunctions6_TOP_1); 
519  
520 

521  
522 
(idJunctions6_TOP_9, idJunctions6_Junctions6_4, y_5) 
523 
= 
524 
if ( idJunctions6_TOP_1 = 0) then 
525 
(idJunctions6_TOP_4, idJunctions6_Junctions6_3, y_4) 
526 
else 
527 
if ( idJunctions6_TOP_1 = 1297) then 
528 
(idJunctions6_TOP_5, idJunctions6_Junctions6_3, y_1) 
529 
else 
530 
if ( idJunctions6_TOP_1 = 1298) then 
531 
(idJunctions6_TOP_6, idJunctions6_Junctions6_3, y_1) 
532 
else 
533 
if ( idJunctions6_TOP_1 = 1299) then 
534 
(idJunctions6_TOP_7, idJunctions6_Junctions6_3, y_1) 
535 
else 
536 
if ( idJunctions6_TOP_1 = 1300) then 
537 
(idJunctions6_TOP_8, idJunctions6_Junctions6_3, y_1) 
538 
else (idJunctions6_TOP_1, idJunctions6_Junctions6_2, y_1); 
539  
540  
541 
(idJunctions6_TOP, idJunctions6_Junctions6, y) 
542 
= (idJunctions6_TOP_9, idJunctions6_Junctions6_4, y_5); 
543 

544  
545 
tel 
546  
547  
548  
549  
550  
551 
 Exit action for state :Junctions6_TOP 
552 
node Junctions6_TOP_ex(idJunctions6_TOP_1:int; 
553 
idJunctions6_Junctions6_1:int; 
554 
isInner:bool) 
555  
556 
returns (idJunctions6_TOP:int; 
557 
idJunctions6_Junctions6:int); 
558  
559  
560 
var idJunctions6_TOP_2, idJunctions6_TOP_3, idJunctions6_TOP_4, idJunctions6_TOP_5, idJunctions6_TOP_6, idJunctions6_TOP_7:int; 
561 
idJunctions6_Junctions6_2:int; 
562  
563  
564 
let 
565  
566  
567  
568 

569 
(idJunctions6_TOP_2) 
570 
= 
571 
if ( idJunctions6_TOP_1 = 1297) then 
572 
TOP_A_ex(idJunctions6_TOP_1, false) 
573 
else (idJunctions6_TOP_1); 
574  
575 

576  
577 
(idJunctions6_TOP_3) 
578 
= 
579 
if ( idJunctions6_TOP_1 = 1298) then 
580 
TOP_B_ex(idJunctions6_TOP_1, false) 
581 
else (idJunctions6_TOP_1); 
582  
583 

584  
585 
(idJunctions6_TOP_4) 
586 
= 
587 
if ( idJunctions6_TOP_1 = 1299) then 
588 
TOP_C_ex(idJunctions6_TOP_1, false) 
589 
else (idJunctions6_TOP_1); 
590  
591 

592  
593 
(idJunctions6_TOP_5) 
594 
= 
595 
if ( idJunctions6_TOP_1 = 1300) then 
596 
TOP_D_ex(idJunctions6_TOP_1, false) 
597 
else (idJunctions6_TOP_1); 
598  
599 

600  
601 
(idJunctions6_TOP_6) 
602 
= 
603 
if ( idJunctions6_TOP_1 = 1297) then 
604 
(idJunctions6_TOP_2) 
605 
else 
606 
if ( idJunctions6_TOP_1 = 1298) then 
607 
(idJunctions6_TOP_3) 
608 
else 
609 
if ( idJunctions6_TOP_1 = 1299) then 
610 
(idJunctions6_TOP_4) 
611 
else 
612 
if ( idJunctions6_TOP_1 = 1300) then 
613 
(idJunctions6_TOP_5) 
614 
else (idJunctions6_TOP_1); 
615  
616  
617 
 set state as inactive 
618 
idJunctions6_Junctions6_2 
619 
= if (not isInner) then 0 else idJunctions6_Junctions6_1; 
620  
621 
idJunctions6_TOP_7 
622 
= 0; 
623 

624  
625 
(idJunctions6_TOP, idJunctions6_Junctions6) 
626 
= (idJunctions6_TOP_7, idJunctions6_Junctions6_1); 
627 

628  
629 
tel 
630  
631  
632 
***************************************************State :Junctions6_TOP Automaton*************************************************** 
633  
634 
node Junctions6_TOP_node(idJunctions6_TOP_1:int; 
635 
x:int; 
636 
y_1:int; 
637 
idJunctions6_Junctions6_1:int) 
638  
639 
returns (idJunctions6_TOP:int; 
640 
y:int; 
641 
idJunctions6_Junctions6:int); 
642  
643  
644 
let 
645  
646 
automaton junctions6_top 
647  
648 
state POINTJunctions6_TOP: 
649 
unless (idJunctions6_TOP_1=0) and ( x<4 ) restart POINT__TO__TOP_A_1 
650  
651  
652  
653 
unless (idJunctions6_TOP_1=0) and ( x>=4 ) restart POINT__TO__TOP_B_2 
654  
655  
656  
657 
unless (idJunctions6_TOP_1=1297) and ( x<=2 ) restart TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1 
658  
659  
660  
661 
unless (idJunctions6_TOP_1=1298) and ( x>=6 ) restart TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1 
662  
663  
664  
665 
unless (idJunctions6_TOP_1=1299) restart TOP_C__TO__JUNCTIONS6_TOP_1 
666  
667  
668  
669 
unless (idJunctions6_TOP_1=1300) restart TOP_D__TO__TOP_C_1 
670  
671  
672  
673 
unless (idJunctions6_TOP_1=1297) restart TOP_A_IDL 
674  
675 
unless (idJunctions6_TOP_1=1298) restart TOP_B_IDL 
676  
677 
unless (idJunctions6_TOP_1=1299) restart TOP_C_IDL 
678  
679 
unless (idJunctions6_TOP_1=1300) restart TOP_D_IDL 
680  
681 
let 
682  
683 
(idJunctions6_TOP, y, idJunctions6_Junctions6) 
684 
= (idJunctions6_TOP_1, y_1, idJunctions6_Junctions6_1); 
685 

686  
687 
tel 
688  
689  
690  
691 
state POINT__TO__TOP_A_1: 
692  
693 
var idJunctions6_TOP_2:int; 
694 
y_2:int; 
695 
let 
696  
697 
 transition trace : 
698 
POINT__To__TOP_A_1 
699 
 condition Action : y+=1 
700 

701 
(y_2) 
702 
= POINT__To__TOP_A_1_Condition_Action(y_1); 
703 

704  
705 
(idJunctions6_TOP_2) 
706 
= TOP_A_en(idJunctions6_TOP_1, false); 
707 

708  
709 
(idJunctions6_TOP, y) 
710 
= (idJunctions6_TOP_2, y_2); 
711  
712 
add unused variables 
713 
(idJunctions6_Junctions6) 
714 
= (idJunctions6_Junctions6_1); 
715 

716  
717 
tel 
718  
719 
until true restart POINTJunctions6_TOP 
720  
721  
722  
723 
state POINT__TO__TOP_B_2: 
724  
725 
var idJunctions6_TOP_2:int; 
726 
y_2:int; 
727 
let 
728  
729 
 transition trace : 
730 
POINT__To__TOP_B_2 
731 
 condition Action : y+=10 
732 

733 
(y_2) 
734 
= POINT__To__TOP_B_2_Condition_Action(y_1); 
735 

736  
737 
(idJunctions6_TOP_2) 
738 
= TOP_B_en(idJunctions6_TOP_1, false); 
739 

740  
741 
(idJunctions6_TOP, y) 
742 
= (idJunctions6_TOP_2, y_2); 
743  
744 
add unused variables 
745 
(idJunctions6_Junctions6) 
746 
= (idJunctions6_Junctions6_1); 
747 

748  
749 
tel 
750  
751 
until true restart POINTJunctions6_TOP 
752  
753  
754  
755 
state TOP_A__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1: 
756  
757 
var idJunctions6_TOP_2, idJunctions6_TOP_3, idJunctions6_TOP_4, idJunctions6_TOP_5:int; 
758 
y_2, y_3, y_4, y_5:int; 
759 
let 
760  
761 

762  
763 
 transition trace : 
764 
TOP_A__To__Junction1302_1, Junction1302__To__TOP_D_1 
765 
 condition Action : y+=100 
766 

767 
(y_2) 
768 
= TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action(y_1); 
769 

770  
771 
 condition Action : y+=100000 
772 

773 
(y_3) 
774 
= 
775 
if (( x mod 3=0 )) then 
776 
Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action(y_2) 
777 
else (y_2); 
778 

779  
780 
(idJunctions6_TOP_2) 
781 
= 
782 
if (( x mod 3=0 )) then 
783 
TOP_A_ex(idJunctions6_TOP_1, false) 
784 
else (idJunctions6_TOP_1); 
785 

786  
787 
(idJunctions6_TOP_3) 
788 
= 
789 
if (( x mod 3=0 )) then 
790 
TOP_D_en(idJunctions6_TOP_2, false) 
791 
else (idJunctions6_TOP_2); 
792 

793  
794  
795 
 transition trace : 
796 
TOP_A__To__Junction1302_1, Junction1302__To__TOP_C_2 
797 
 condition Action : y+=100 
798 

799 
(y_4) 
800 
= TOP_A__To__Junctions6_Junctions6Junction1302_1_Condition_Action(y_1); 
801 

802  
803 
 condition Action : y+=10000 
804 

805 
(y_5) 
806 
= 
807 
if (( x mod 3=1 )) then 
808 
Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action(y_4) 
809 
else (y_4); 
810 

811  
812 
(idJunctions6_TOP_4) 
813 
= 
814 
if (( x mod 3=1 )) then 
815 
TOP_A_ex(idJunctions6_TOP_1, false) 
816 
else (idJunctions6_TOP_1); 
817 

818  
819 
(idJunctions6_TOP_5) 
820 
= 
821 
if (( x mod 3=1 )) then 
822 
TOP_C_en(idJunctions6_TOP_4, false) 
823 
else (idJunctions6_TOP_4); 
824 

825  
826 
(idJunctions6_TOP, y) 
827 
= 
828 
if (( x mod 3=0 )) then 
829 
(idJunctions6_TOP_3, y_3) 
830 
else 
831 
if (( x mod 3=1 )) then 
832 
(idJunctions6_TOP_5, y_5) 
833 
else (idJunctions6_TOP_1, y_4); 
834  
835 
add unused variables 
836 
(idJunctions6_Junctions6) 
837 
= (idJunctions6_Junctions6_1); 
838 

839  
840 
tel 
841  
842 
until true restart POINTJunctions6_TOP 
843  
844  
845  
846 
state TOP_B__TO__JUNCTIONS6_JUNCTIONS6JUNCTION1302_1: 
847  
848 
var idJunctions6_TOP_2, idJunctions6_TOP_3, idJunctions6_TOP_4, idJunctions6_TOP_5:int; 
849 
y_2, y_3, y_4, y_5:int; 
850 
let 
851  
852 

853  
854 
 transition trace : 
855 
TOP_B__To__Junction1302_1, Junction1302__To__TOP_D_1 
856 
 condition Action : y+=1000 
857 

858 
(y_2) 
859 
= TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action(y_1); 
860 

861  
862 
 condition Action : y+=100000 
863 

864 
(y_3) 
865 
= 
866 
if (( x mod 3=0 )) then 
867 
Junctions6_Junctions6Junction1302__To__TOP_D_1_Condition_Action(y_2) 
868 
else (y_2); 
869 

870  
871 
(idJunctions6_TOP_2) 
872 
= 
873 
if (( x mod 3=0 )) then 
874 
TOP_B_ex(idJunctions6_TOP_1, false) 
875 
else (idJunctions6_TOP_1); 
876 

877  
878 
(idJunctions6_TOP_3) 
879 
= 
880 
if (( x mod 3=0 )) then 
881 
TOP_D_en(idJunctions6_TOP_2, false) 
882 
else (idJunctions6_TOP_2); 
883 

884  
885  
886 
 transition trace : 
887 
TOP_B__To__Junction1302_1, Junction1302__To__TOP_C_2 
888 
 condition Action : y+=1000 
889 

890 
(y_4) 
891 
= TOP_B__To__Junctions6_Junctions6Junction1302_1_Condition_Action(y_1); 
892 

893  
894 
 condition Action : y+=10000 
895 

896 
(y_5) 
897 
= 
898 
if (( x mod 3=1 )) then 
899 
Junctions6_Junctions6Junction1302__To__TOP_C_2_Condition_Action(y_4) 
900 
else (y_4); 
901 

902  
903 
(idJunctions6_TOP_4) 
904 
= 
905 
if (( x mod 3=1 )) then 
906 
TOP_B_ex(idJunctions6_TOP_1, false) 
907 
else (idJunctions6_TOP_1); 
908 

909  
910 
(idJunctions6_TOP_5) 
911 
= 
912 
if (( x mod 3=1 )) then 
913 
TOP_C_en(idJunctions6_TOP_4, false) 
914 
else (idJunctions6_TOP_4); 
915 

916  
917 
(idJunctions6_TOP, y) 
918 
= 
919 
if (( x mod 3=0 )) then 
920 
(idJunctions6_TOP_3, y_3) 
921 
else 
922 
if (( x mod 3=1 )) then 
923 
(idJunctions6_TOP_5, y_5) 
924 
else (idJunctions6_TOP_1, y_4); 
925  
926 
add unused variables 
927 
(idJunctions6_Junctions6) 
928 
= (idJunctions6_Junctions6_1); 
929 

930  
931 
tel 
932  
933 
until true restart POINTJunctions6_TOP 
934  
935  
936  
937 
state TOP_C__TO__JUNCTIONS6_TOP_1: 
938  
939 
var idJunctions6_TOP_2, idJunctions6_TOP_3, idJunctions6_TOP_4:int; 
940 
y_2:int; 
941 
idJunctions6_Junctions6_2:int; 
942 
let 
943  
944 
 transition trace : 
945 
TOP_C__To__Junctions6_TOP_1 
946 
(idJunctions6_TOP_2) 
947 
= TOP_C_ex(idJunctions6_TOP_1, false); 
948 

949  
950 
idJunctions6_TOP_3 
951 
= 0; 
952 

953 
(idJunctions6_TOP_4, idJunctions6_Junctions6_2, y_2) 
954 
= Junctions6_TOP_en(idJunctions6_TOP_3, idJunctions6_Junctions6_1, x, y_1, true); 
955 

956  
957 
(idJunctions6_TOP, y, idJunctions6_Junctions6) 
958 
= (idJunctions6_TOP_4, y_2, idJunctions6_Junctions6_2); 
959  
960  
961 
tel 
962  
963 
until true restart POINTJunctions6_TOP 
964  
965  
966  
967 
state TOP_D__TO__TOP_C_1: 
968  
969 
var idJunctions6_TOP_2, idJunctions6_TOP_3:int; 
970 
let 
971  
972 
 transition trace : 
973 
TOP_D__To__TOP_C_1 
974 
(idJunctions6_TOP_2) 
975 
= TOP_D_ex(idJunctions6_TOP_1, false); 
976 

977  
978 
(idJunctions6_TOP_3) 
979 
= TOP_C_en(idJunctions6_TOP_2, false); 
980 

981  
982 
(idJunctions6_TOP, y, idJunctions6_Junctions6) 
983 
= (idJunctions6_TOP_3, y_1, idJunctions6_Junctions6_1); 
984  
985  
986 
tel 
987  
988 
until true restart POINTJunctions6_TOP 
989  
990  
991  
992 
state TOP_A_IDL: 
993  
994 
let 
995  
996 

997  
998 
(idJunctions6_TOP, y, idJunctions6_Junctions6) 
999 
= (idJunctions6_TOP_1, y_1, idJunctions6_Junctions6_1); 
1000 

1001  
1002 
tel 
1003  
1004 
until true restart POINTJunctions6_TOP 
1005  
1006  
1007  
1008 
state TOP_B_IDL: 
1009  
1010 
let 
1011  
1012 

1013  
1014 
(idJunctions6_TOP, y, idJunctions6_Junctions6) 
1015 
= (idJunctions6_TOP_1, y_1, idJunctions6_Junctions6_1); 
1016 

1017  
1018 
tel 
1019  
1020 
until true restart POINTJunctions6_TOP 
1021  
1022  
1023  
1024 
state TOP_C_IDL: 
1025  
1026 
let 
1027  
1028 

1029  
1030 
(idJunctions6_TOP, y, idJunctions6_Junctions6) 
1031 
= (idJunctions6_TOP_1, y_1, idJunctions6_Junctions6_1); 
1032 

1033  
1034 
tel 
1035  
1036 
until true restart POINTJunctions6_TOP 
1037  
1038  
1039  
1040 
state TOP_D_IDL: 
1041  
1042 
let 
1043  
1044 

1045  
1046 
(idJunctions6_TOP, y, idJunctions6_Junctions6) 
1047 
= (idJunctions6_TOP_1, y_1, idJunctions6_Junctions6_1); 
1048 

1049  
1050 
tel 
1051  
1052 
until true restart POINTJunctions6_TOP 
1053  
1054  
1055  
1056 
tel 
1057  
1058  
1059 
***************************************************State :Junctions6_Junctions6 Automaton*************************************************** 
1060  
1061 
node Junctions6_Junctions6_node(idJunctions6_Junctions6_1:int; 
1062 
idJunctions6_TOP_1:int; 
1063 
x:int; 
1064 
y_1:int) 
1065  
1066 
returns (idJunctions6_Junctions6:int; 
1067 
idJunctions6_TOP:int; 
1068 
y:int); 
1069  
1070  
1071 
let 
1072  
1073 
automaton junctions6_junctions6 
1074  
1075 
state POINTJunctions6_Junctions6: 
1076 
unless (idJunctions6_Junctions6_1=0) restart POINT__TO__JUNCTIONS6_TOP_1 
1077  
1078  
1079  
1080 
unless (idJunctions6_Junctions6_1=1301) restart JUNCTIONS6_TOP_IDL 
1081  
1082 
let 
1083  
1084 
(idJunctions6_Junctions6, idJunctions6_TOP, y) 
1085 
= (idJunctions6_Junctions6_1, idJunctions6_TOP_1, y_1); 
1086 

1087  
1088 
tel 
1089  
1090  
1091  
1092 
state POINT__TO__JUNCTIONS6_TOP_1: 
1093  
1094 
var idJunctions6_Junctions6_2:int; 
1095 
idJunctions6_TOP_2:int; 
1096 
y_2:int; 
1097 
let 
1098  
1099 
 transition trace : 
1100 
POINT__To__Junctions6_TOP_1 
1101 
(idJunctions6_TOP_2, idJunctions6_Junctions6_2, y_2) 
1102 
= Junctions6_TOP_en(idJunctions6_TOP_1, idJunctions6_Junctions6_1, x, y_1, false); 
1103 

1104  
1105 
(idJunctions6_Junctions6, idJunctions6_TOP, y) 
1106 
= (idJunctions6_Junctions6_2, idJunctions6_TOP_2, y_2); 
1107  
1108  
1109 
tel 
1110  
1111 
until true restart POINTJunctions6_Junctions6 
1112  
1113  
1114  
1115 
state JUNCTIONS6_TOP_IDL: 
1116  
1117 
var idJunctions6_Junctions6_2:int; 
1118 
idJunctions6_TOP_2:int; 
1119 
y_2:int; 
1120 
let 
1121  
1122 

1123 
(idJunctions6_TOP_2, y_2, idJunctions6_Junctions6_2) 
1124 
= Junctions6_TOP_node(idJunctions6_TOP_1, x, y_1, idJunctions6_Junctions6_1); 
1125  
1126 

1127  
1128  
1129 
(idJunctions6_Junctions6, idJunctions6_TOP, y) 
1130 
= (idJunctions6_Junctions6_2, idJunctions6_TOP_2, y_2); 
1131 

1132  
1133 
tel 
1134  
1135 
until true restart POINTJunctions6_Junctions6 
1136  
1137  
1138  
1139 
tel 
1140  
1141  
1142 
***************************************************State :Junctions6_Junctions6 Automaton*************************************************** 
1143  
1144 
node Junctions6_Junctions6(x:int) 
1145  
1146 
returns (y:int); 
1147  
1148  
1149 
var y_1: int; 
1150  
1151 
idJunctions6_Junctions6, idJunctions6_Junctions6_1: int; 
1152  
1153 
idJunctions6_TOP, idJunctions6_TOP_1: int; 
1154  
1155 
let 
1156  
1157 
y_1 = 111111 > pre y; 
1158  
1159 
idJunctions6_Junctions6_1 = 0 > pre idJunctions6_Junctions6; 
1160  
1161 
idJunctions6_TOP_1 = 0 > pre idJunctions6_TOP; 
1162  
1163 

1164  
1165  
1166  
1167 
(idJunctions6_Junctions6, idJunctions6_TOP, y) 
1168 
= Junctions6_Junctions6_node(idJunctions6_Junctions6_1, idJunctions6_TOP_1, x, y_1); 
1169  
1170  
1171 
unused outputs 
1172 

1173  
1174 
tel 
1175  
1176  
1177  
1178 
node Junctions6 (x_1_1 : int) 
1179 
returns (y_1_1 : int); 
1180 
var 
1181 
Junctions6_1_1 : int; 
1182 
i_virtual_local : real; 
1183 
let 
1184 
Junctions6_1_1 = Junctions6_Junctions6(x_1_1); 
1185 
y_1_1 = Junctions6_1_1; 
1186 
i_virtual_local= 0.0 > 1.0; 
1187 
tel 
1188 