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

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

26  
27 
(a) 
28 
= (a_2); 
29 

30  
31 
tel 
32  
33  
34  
35  
36  
37  
38 
node POINT__To__TOP_A_2_Condition_Action(a_1:int) 
39  
40 
returns (a:int); 
41  
42  
43 
var a_2:int; 
44  
45  
46 
let 
47  
48  
49  
50 
a_2 
51 
= a_1 +1; 
52 

53  
54 
(a) 
55 
= (a_2); 
56 

57  
58 
tel 
59  
60  
61  
62  
63  
64 
node POINT__To__TOP_A_2_Transition_Action(b_1:int) 
65  
66 
returns (b:int); 
67  
68  
69 
var b_2:int; 
70  
71  
72 
let 
73  
74  
75  
76 
b_2 
77 
= b_1 +1; 
78 

79  
80 
(b) 
81 
= (b_2); 
82 

83  
84 
tel 
85  
86  
87  
88  
89  
90  
91 
node TOP_A__To__Junctions4_Junctions4Junction1265_1_Condition_Action(a_1:int) 
92  
93 
returns (a:int); 
94  
95  
96 
var a_2:int; 
97  
98  
99 
let 
100  
101  
102  
103 
a_2 
104 
= a_1 +1000; 
105 

106  
107 
(a) 
108 
= (a_2); 
109 

110  
111 
tel 
112  
113  
114  
115  
116  
117  
118 
node Junctions4_Junctions4Junction1265__To__TOP_B_1_Condition_Action(a_1:int) 
119  
120 
returns (a:int); 
121  
122  
123 
var a_2:int; 
124  
125  
126 
let 
127  
128  
129  
130 
a_2 
131 
= a_1 +100000; 
132 

133  
134 
(a) 
135 
= (a_2); 
136 

137  
138 
tel 
139  
140  
141  
142  
143  
144 
node Junctions4_Junctions4Junction1265__To__TOP_B_1_Transition_Action(b_1:int) 
145  
146 
returns (b:int); 
147  
148  
149 
var b_2:int; 
150  
151  
152 
let 
153  
154  
155  
156 
b_2 
157 
= b_1 +100000; 
158 

159  
160 
(b) 
161 
= (b_2); 
162 

163  
164 
tel 
165  
166  
167  
168  
169  
170  
171 
node Junctions4_Junctions4Junction1265__To__TOP_B_2_Condition_Action(a_1:int) 
172  
173 
returns (a:int); 
174  
175  
176 
var a_2:int; 
177  
178  
179 
let 
180  
181  
182  
183 
a_2 
184 
= a_1 +10000; 
185 

186  
187 
(a) 
188 
= (a_2); 
189 

190  
191 
tel 
192  
193  
194  
195  
196  
197 
node Junctions4_Junctions4Junction1265__To__TOP_B_2_Transition_Action(b_1:int) 
198  
199 
returns (b:int); 
200  
201  
202 
var b_2:int; 
203  
204  
205 
let 
206  
207  
208  
209 
b_2 
210 
= b_1 +10000; 
211 

212  
213 
(b) 
214 
= (b_2); 
215 

216  
217 
tel 
218  
219  
220  
221  
222  
223  
224 
node POINT__To__TOP_A_1_Condition_Action(a_1:int) 
225  
226 
returns (a:int); 
227  
228  
229 
var a_2:int; 
230  
231  
232 
let 
233  
234  
235  
236 
a_2 
237 
= a_1 +10; 
238 

239  
240 
(a) 
241 
= (a_2); 
242 

243  
244 
tel 
245  
246  
247  
248  
249  
250 
node POINT__To__TOP_A_1_Transition_Action(b_1:int) 
251  
252 
returns (b:int); 
253  
254  
255 
var b_2:int; 
256  
257  
258 
let 
259  
260  
261  
262 
b_2 
263 
= b_1 +10; 
264 

265  
266 
(b) 
267 
= (b_2); 
268 

269  
270 
tel 
271  
272  
273  
274  
275  
276  
277 
 Entry action for state :TOP_A 
278 
node TOP_A_en(idJunctions4_TOP_1:int; 
279 
c_1:int; 
280 
isInner:bool) 
281  
282 
returns (idJunctions4_TOP:int; 
283 
c:int); 
284  
285  
286 
var idJunctions4_TOP_2:int; 
287 
c_2:int; 
288  
289  
290 
let 
291  
292  
293  
294 
 set state as active 
295 
idJunctions4_TOP_2 
296 
= 1262; 
297 

298  
299 
c_2 
300 
= if (not isInner) then c_1 +1 
301 
else c_1; 
302 

303  
304 
(idJunctions4_TOP, c) 
305 
= (idJunctions4_TOP_2, c_2); 
306 

307  
308 
tel 
309  
310  
311  
312  
313  
314 
 Exit action for state :TOP_A 
315 
node TOP_A_ex(c_1:int; 
316 
idJunctions4_TOP_1:int; 
317 
isInner:bool) 
318  
319 
returns (c:int; 
320 
idJunctions4_TOP:int); 
321  
322  
323 
var c_2:int; 
324 
idJunctions4_TOP_2:int; 
325  
326  
327 
let 
328  
329  
330  
331 
c_2 
332 
= if (not isInner) then c_1 +10 
333 
else c_1; 
334 

335  
336 
 set state as inactive 
337 
idJunctions4_TOP_2 
338 
= if (not isInner) then 0 else idJunctions4_TOP_1; 
339  
340  
341 
(c, idJunctions4_TOP) 
342 
= (c_2, idJunctions4_TOP_1); 
343 

344  
345 
tel 
346  
347  
348  
349  
350  
351  
352 
 Entry action for state :TOP_B 
353 
node TOP_B_en(idJunctions4_TOP_1:int; 
354 
c_1:int; 
355 
isInner:bool) 
356  
357 
returns (idJunctions4_TOP:int; 
358 
c:int); 
359  
360  
361 
var idJunctions4_TOP_2:int; 
362 
c_2:int; 
363  
364  
365 
let 
366  
367  
368  
369 
 set state as active 
370 
idJunctions4_TOP_2 
371 
= 1263; 
372 

373  
374 
c_2 
375 
= if (not isInner) then c_1 +100 
376 
else c_1; 
377 

378  
379 
(idJunctions4_TOP, c) 
380 
= (idJunctions4_TOP_2, c_2); 
381 

382  
383 
tel 
384  
385  
386  
387  
388  
389 
During action for state :TOP_B 
390 
node TOP_B_du(c_1:int) 
391  
392 
returns (c:int); 
393  
394  
395 
var c_2:int; 
396  
397  
398 
let 
399  
400  
401  
402 
c_2 
403 
= c_1 +1000; 
404 

405  
406 
(c) 
407 
= (c_2); 
408 

409  
410 
tel 
411  
412  
413  
414  
415  
416 
 Exit action for state :TOP_B 
417 
node TOP_B_ex(idJunctions4_TOP_1:int; 
418 
isInner:bool) 
419  
420 
returns (idJunctions4_TOP:int); 
421  
422  
423 
var idJunctions4_TOP_2:int; 
424  
425  
426 
let 
427  
428  
429  
430 
 set state as inactive 
431 
idJunctions4_TOP_2 
432 
= if (not isInner) then 0 else idJunctions4_TOP_1; 
433  
434  
435 
(idJunctions4_TOP) 
436 
= (idJunctions4_TOP_1); 
437 

438  
439 
tel 
440  
441  
442  
443  
444  
445  
446 
 Entry action for state :Junctions4_TOP 
447 
node Junctions4_TOP_en(idJunctions4_TOP_1:int; 
448 
idJunctions4_Junctions4_1:int; 
449 
x:int; 
450 
a_1:int; 
451 
b_1:int; 
452 
c_1:int; 
453 
isInner:bool) 
454  
455 
returns (idJunctions4_TOP:int; 
456 
idJunctions4_Junctions4:int; 
457 
a:int; 
458 
b:int; 
459 
c:int); 
460  
461  
462 
var idJunctions4_TOP_2, idJunctions4_TOP_3, idJunctions4_TOP_4, idJunctions4_TOP_5, idJunctions4_TOP_6, idJunctions4_TOP_7:int; 
463 
idJunctions4_Junctions4_2, idJunctions4_Junctions4_3, idJunctions4_Junctions4_4:int; 
464 
a_2, a_3, a_4, a_5:int; 
465 
b_2, b_3, b_4, b_5:int; 
466 
c_2, c_3, c_4, c_5, c_6, c_7:int; 
467  
468  
469 
let 
470  
471  
472  
473 
 set state as active 
474 
idJunctions4_Junctions4_2 
475 
= 1264; 
476 

477  
478 

479 
 transition trace : 
480 
POINT__To__TOP_A_1 
481 
 condition Action : a+=10 
482 

483 
(a_2) 
484 
= 
485 
if (( x!=0 )) then 
486 
POINT__To__TOP_A_1_Condition_Action(a_1) 
487 
else (a_1); 
488 

489  
490 
(b_2) 
491 
= 
492 
if (( x!=0 )) then 
493 
POINT__To__TOP_A_1_Transition_Action(b_1) 
494 
else (b_1); 
495 

496  
497 
(idJunctions4_TOP_2, c_2) 
498 
= 
499 
if (( x!=0 )) then 
500 
TOP_A_en(idJunctions4_TOP_1, c_1, false) 
501 
else (idJunctions4_TOP_1, c_1); 
502 

503  
504 
 transition trace : 
505 
POINT__To__TOP_A_2 
506 
 condition Action : a+=1 
507 

508 
(a_3) 
509 
= 
510 
if (( x=0 )) then 
511 
POINT__To__TOP_A_2_Condition_Action(a_1) 
512 
else (a_1); 
513 

514  
515 
(b_3) 
516 
= 
517 
if (( x=0 )) then 
518 
POINT__To__TOP_A_2_Transition_Action(b_1) 
519 
else (b_1); 
520 

521  
522 
(idJunctions4_TOP_3, c_3) 
523 
= 
524 
if (( x=0 )) then 
525 
TOP_A_en(idJunctions4_TOP_1, c_1, false) 
526 
else (idJunctions4_TOP_1, c_1); 
527 

528  
529 
(idJunctions4_TOP_4, idJunctions4_Junctions4_3, a_4, b_4, c_4) 
530 
= 
531  
532 
if ( idJunctions4_TOP_1 = 0) then 
533  
534 

535 
if (( x!=0 )) then 
536 
(idJunctions4_TOP_2, idJunctions4_Junctions4_2, a_2, b_2, c_2) 
537 
else 
538 
if (( x=0 )) then 
539 
(idJunctions4_TOP_3, idJunctions4_Junctions4_2, a_3, b_3, c_3) 
540 
else (idJunctions4_TOP_1, idJunctions4_Junctions4_2, a_1, b_1, c_1) 
541  
542 
else(idJunctions4_TOP_1, idJunctions4_Junctions4_2, a_1, b_1, c_1); 
543  
544 

545  
546 
(idJunctions4_TOP_5, c_5) 
547 
= 
548 
if ( idJunctions4_TOP_1 = 1262) then 
549 
TOP_A_en(idJunctions4_TOP_1, c_1, false) 
550 
else (idJunctions4_TOP_1, c_1); 
551  
552 

553  
554 
(idJunctions4_TOP_6, c_6) 
555 
= 
556 
if ( idJunctions4_TOP_1 = 1263) then 
557 
TOP_B_en(idJunctions4_TOP_1, c_1, false) 
558 
else (idJunctions4_TOP_1, c_1); 
559  
560 

561  
562 
(idJunctions4_TOP_7, idJunctions4_Junctions4_4, a_5, b_5, c_7) 
563 
= 
564 
if ( idJunctions4_TOP_1 = 0) then 
565 
(idJunctions4_TOP_4, idJunctions4_Junctions4_3, a_4, b_4, c_4) 
566 
else 
567 
if ( idJunctions4_TOP_1 = 1262) then 
568 
(idJunctions4_TOP_5, idJunctions4_Junctions4_3, a_1, b_1, c_5) 
569 
else 
570 
if ( idJunctions4_TOP_1 = 1263) then 
571 
(idJunctions4_TOP_6, idJunctions4_Junctions4_3, a_1, b_1, c_6) 
572 
else (idJunctions4_TOP_1, idJunctions4_Junctions4_2, a_1, b_1, c_1); 
573  
574  
575 
(idJunctions4_TOP, idJunctions4_Junctions4, a, b, c) 
576 
= (idJunctions4_TOP_7, idJunctions4_Junctions4_4, a_5, b_5, c_7); 
577 

578  
579 
tel 
580  
581  
582  
583  
584  
585 
 Exit action for state :Junctions4_TOP 
586 
node Junctions4_TOP_ex(c_1:int; 
587 
idJunctions4_TOP_1:int; 
588 
idJunctions4_Junctions4_1:int; 
589 
isInner:bool) 
590  
591 
returns (c:int; 
592 
idJunctions4_TOP:int; 
593 
idJunctions4_Junctions4:int); 
594  
595  
596 
var c_2, c_3:int; 
597 
idJunctions4_TOP_2, idJunctions4_TOP_3, idJunctions4_TOP_4, idJunctions4_TOP_5:int; 
598 
idJunctions4_Junctions4_2:int; 
599  
600  
601 
let 
602  
603  
604  
605 

606 
(c_2, idJunctions4_TOP_2) 
607 
= 
608 
if ( idJunctions4_TOP_1 = 1262) then 
609 
TOP_A_ex(c_1, idJunctions4_TOP_1, false) 
610 
else (c_1, idJunctions4_TOP_1); 
611  
612 

613  
614 
(idJunctions4_TOP_3) 
615 
= 
616 
if ( idJunctions4_TOP_1 = 1263) then 
617 
TOP_B_ex(idJunctions4_TOP_1, false) 
618 
else (idJunctions4_TOP_1); 
619  
620 

621  
622 
(c_3, idJunctions4_TOP_4) 
623 
= 
624 
if ( idJunctions4_TOP_1 = 1262) then 
625 
(c_2, idJunctions4_TOP_2) 
626 
else 
627 
if ( idJunctions4_TOP_1 = 1263) then 
628 
(c_1, idJunctions4_TOP_3) 
629 
else (c_1, idJunctions4_TOP_1); 
630  
631  
632 
 set state as inactive 
633 
idJunctions4_Junctions4_2 
634 
= if (not isInner) then 0 else idJunctions4_Junctions4_1; 
635  
636 
idJunctions4_TOP_5 
637 
= 0; 
638 

639  
640 
(c, idJunctions4_TOP, idJunctions4_Junctions4) 
641 
= (c_3, idJunctions4_TOP_5, idJunctions4_Junctions4_1); 
642 

643  
644 
tel 
645  
646  
647 
***************************************************State :Junctions4_TOP Automaton*************************************************** 
648  
649 
node Junctions4_TOP_node(idJunctions4_TOP_1:int; 
650 
x:int; 
651 
a_1:int; 
652 
b_1:int; 
653 
c_1:int; 
654 
idJunctions4_Junctions4_1:int) 
655  
656 
returns (idJunctions4_TOP:int; 
657 
a:int; 
658 
b:int; 
659 
c:int; 
660 
idJunctions4_Junctions4:int); 
661  
662  
663 
let 
664  
665 
automaton junctions4_top 
666  
667 
state POINTJunctions4_TOP: 
668 
unless (idJunctions4_TOP_1=0) and ( x!=0 ) restart POINT__TO__TOP_A_1 
669  
670  
671  
672 
unless (idJunctions4_TOP_1=0) and ( x=0 ) restart POINT__TO__TOP_A_2 
673  
674  
675  
676 
unless (idJunctions4_TOP_1=1262) and ( x>=4 ) restart TOP_A__TO__JUNCTIONS4_JUNCTIONS4JUNCTION1265_1 
677  
678  
679  
680 
unless (idJunctions4_TOP_1=1262) and ( x<4 ) restart TOP_A__TO__JUNCTIONS4_JUNCTIONS4JUNCTION1265_2 
681  
682  
683  
684 
unless (idJunctions4_TOP_1=1263) restart TOP_B__TO__JUNCTIONS4_TOP_1 
685  
686  
687  
688 
unless (idJunctions4_TOP_1=1262) restart TOP_A_IDL 
689  
690 
unless (idJunctions4_TOP_1=1263) restart TOP_B_IDL 
691  
692 
let 
693  
694 
(idJunctions4_TOP, a, b, c, idJunctions4_Junctions4) 
695 
= (idJunctions4_TOP_1, a_1, b_1, c_1, idJunctions4_Junctions4_1); 
696 

697  
698 
tel 
699  
700  
701  
702 
state POINT__TO__TOP_A_1: 
703  
704 
var idJunctions4_TOP_2:int; 
705 
a_2:int; 
706 
b_2:int; 
707 
c_2:int; 
708 
let 
709  
710 
 transition trace : 
711 
POINT__To__TOP_A_1 
712 
 condition Action : a+=10 
713 

714 
(a_2) 
715 
= POINT__To__TOP_A_1_Condition_Action(a_1); 
716 

717  
718 
(b_2) 
719 
= POINT__To__TOP_A_1_Transition_Action(b_1); 
720 

721  
722 
(idJunctions4_TOP_2, c_2) 
723 
= TOP_A_en(idJunctions4_TOP_1, c_1, false); 
724 

725  
726 
(idJunctions4_TOP, a, b, c) 
727 
= (idJunctions4_TOP_2, a_2, b_2, c_2); 
728  
729 
add unused variables 
730 
(idJunctions4_Junctions4) 
731 
= (idJunctions4_Junctions4_1); 
732 

733  
734 
tel 
735  
736 
until true restart POINTJunctions4_TOP 
737  
738  
739  
740 
state POINT__TO__TOP_A_2: 
741  
742 
var idJunctions4_TOP_2:int; 
743 
a_2:int; 
744 
b_2:int; 
745 
c_2:int; 
746 
let 
747  
748 
 transition trace : 
749 
POINT__To__TOP_A_2 
750 
 condition Action : a+=1 
751 

752 
(a_2) 
753 
= POINT__To__TOP_A_2_Condition_Action(a_1); 
754 

755  
756 
(b_2) 
757 
= POINT__To__TOP_A_2_Transition_Action(b_1); 
758 

759  
760 
(idJunctions4_TOP_2, c_2) 
761 
= TOP_A_en(idJunctions4_TOP_1, c_1, false); 
762 

763  
764 
(idJunctions4_TOP, a, b, c) 
765 
= (idJunctions4_TOP_2, a_2, b_2, c_2); 
766  
767 
add unused variables 
768 
(idJunctions4_Junctions4) 
769 
= (idJunctions4_Junctions4_1); 
770 

771  
772 
tel 
773  
774 
until true restart POINTJunctions4_TOP 
775  
776  
777  
778 
state TOP_A__TO__JUNCTIONS4_JUNCTIONS4JUNCTION1265_1: 
779  
780 
var idJunctions4_TOP_2, idJunctions4_TOP_3, idJunctions4_TOP_4, idJunctions4_TOP_5:int; 
781 
a_2, a_3, a_4, a_5:int; 
782 
b_2, b_3:int; 
783 
c_2, c_3, c_4, c_5:int; 
784 
let 
785  
786 

787  
788 
 transition trace : 
789 
TOP_A__To__Junction1265_1, Junction1265__To__TOP_B_1 
790 
 condition Action : a+=1000 
791 

792 
(a_2) 
793 
= TOP_A__To__Junctions4_Junctions4Junction1265_1_Condition_Action(a_1); 
794 

795  
796 
 condition Action : a+=100000 
797 

798 
(a_3) 
799 
= 
800 
if (( x mod 3!=0 )) then 
801 
Junctions4_Junctions4Junction1265__To__TOP_B_1_Condition_Action(a_2) 
802 
else (a_2); 
803 

804  
805 
(c_2, idJunctions4_TOP_2) 
806 
= 
807 
if (( x mod 3!=0 )) then 
808 
TOP_A_ex(c_1, idJunctions4_TOP_1, false) 
809 
else (c_1, idJunctions4_TOP_1); 
810 

811  
812 
(b_2) 
813 
= 
814 
if (( x mod 3!=0 )) then 
815 
Junctions4_Junctions4Junction1265__To__TOP_B_1_Transition_Action(b_1) 
816 
else (b_1); 
817 

818  
819 
(idJunctions4_TOP_3, c_3) 
820 
= 
821 
if (( x mod 3!=0 )) then 
822 
TOP_B_en(idJunctions4_TOP_2, c_2, false) 
823 
else (idJunctions4_TOP_2, c_2); 
824 

825  
826  
827 
 transition trace : 
828 
TOP_A__To__Junction1265_1, Junction1265__To__TOP_B_2 
829 
 condition Action : a+=1000 
830 

831 
(a_4) 
832 
= TOP_A__To__Junctions4_Junctions4Junction1265_1_Condition_Action(a_1); 
833 

834  
835 
 condition Action : a+=10000 
836 

837 
(a_5) 
838 
= 
839 
if (( x mod 3=0 )) then 
840 
Junctions4_Junctions4Junction1265__To__TOP_B_2_Condition_Action(a_4) 
841 
else (a_4); 
842 

843  
844 
(c_4, idJunctions4_TOP_4) 
845 
= 
846 
if (( x mod 3=0 )) then 
847 
TOP_A_ex(c_1, idJunctions4_TOP_1, false) 
848 
else (c_1, idJunctions4_TOP_1); 
849 

850  
851 
(b_3) 
852 
= 
853 
if (( x mod 3=0 )) then 
854 
Junctions4_Junctions4Junction1265__To__TOP_B_2_Transition_Action(b_1) 
855 
else (b_1); 
856 

857  
858 
(idJunctions4_TOP_5, c_5) 
859 
= 
860 
if (( x mod 3=0 )) then 
861 
TOP_B_en(idJunctions4_TOP_4, c_4, false) 
862 
else (idJunctions4_TOP_4, c_4); 
863 

864  
865 
(idJunctions4_TOP, a, b, c) 
866 
= 
867 
if (( x mod 3!=0 )) then 
868 
(idJunctions4_TOP_3, a_3, b_2, c_3) 
869 
else 
870 
if (( x mod 3=0 )) then 
871 
(idJunctions4_TOP_5, a_5, b_3, c_5) 
872 
else (idJunctions4_TOP_1, a_4, b_1, c_1); 
873  
874 
add unused variables 
875 
(idJunctions4_Junctions4) 
876 
= (idJunctions4_Junctions4_1); 
877 

878  
879 
tel 
880  
881 
until true restart POINTJunctions4_TOP 
882  
883  
884  
885 
state TOP_A__TO__JUNCTIONS4_JUNCTIONS4JUNCTION1265_2: 
886  
887 
var idJunctions4_TOP_2, idJunctions4_TOP_3, idJunctions4_TOP_4, idJunctions4_TOP_5:int; 
888 
a_2, a_3, a_4, a_5:int; 
889 
b_2, b_3:int; 
890 
c_2, c_3, c_4, c_5:int; 
891 
let 
892  
893 

894  
895 
 transition trace : 
896 
TOP_A__To__Junction1265_2, Junction1265__To__TOP_B_1 
897 
 condition Action : a+=100 
898 

899 
(a_2) 
900 
= TOP_A__To__Junctions4_Junctions4Junction1265_2_Condition_Action(a_1); 
901 

902  
903 
 condition Action : a+=100000 
904 

905 
(a_3) 
906 
= 
907 
if (( x mod 3!=0 )) then 
908 
Junctions4_Junctions4Junction1265__To__TOP_B_1_Condition_Action(a_2) 
909 
else (a_2); 
910 

911  
912 
(c_2, idJunctions4_TOP_2) 
913 
= 
914 
if (( x mod 3!=0 )) then 
915 
TOP_A_ex(c_1, idJunctions4_TOP_1, false) 
916 
else (c_1, idJunctions4_TOP_1); 
917 

918  
919 
(b_2) 
920 
= 
921 
if (( x mod 3!=0 )) then 
922 
Junctions4_Junctions4Junction1265__To__TOP_B_1_Transition_Action(b_1) 
923 
else (b_1); 
924 

925  
926 
(idJunctions4_TOP_3, c_3) 
927 
= 
928 
if (( x mod 3!=0 )) then 
929 
TOP_B_en(idJunctions4_TOP_2, c_2, false) 
930 
else (idJunctions4_TOP_2, c_2); 
931 

932  
933  
934 
 transition trace : 
935 
TOP_A__To__Junction1265_2, Junction1265__To__TOP_B_2 
936 
 condition Action : a+=100 
937 

938 
(a_4) 
939 
= TOP_A__To__Junctions4_Junctions4Junction1265_2_Condition_Action(a_1); 
940 

941  
942 
 condition Action : a+=10000 
943 

944 
(a_5) 
945 
= 
946 
if (( x mod 3=0 )) then 
947 
Junctions4_Junctions4Junction1265__To__TOP_B_2_Condition_Action(a_4) 
948 
else (a_4); 
949 

950  
951 
(c_4, idJunctions4_TOP_4) 
952 
= 
953 
if (( x mod 3=0 )) then 
954 
TOP_A_ex(c_1, idJunctions4_TOP_1, false) 
955 
else (c_1, idJunctions4_TOP_1); 
956 

957  
958 
(b_3) 
959 
= 
960 
if (( x mod 3=0 )) then 
961 
Junctions4_Junctions4Junction1265__To__TOP_B_2_Transition_Action(b_1) 
962 
else (b_1); 
963 

964  
965 
(idJunctions4_TOP_5, c_5) 
966 
= 
967 
if (( x mod 3=0 )) then 
968 
TOP_B_en(idJunctions4_TOP_4, c_4, false) 
969 
else (idJunctions4_TOP_4, c_4); 
970 

971  
972 
(idJunctions4_TOP, a, b, c) 
973 
= 
974 
if (( x mod 3!=0 )) then 
975 
(idJunctions4_TOP_3, a_3, b_2, c_3) 
976 
else 
977 
if (( x mod 3=0 )) then 
978 
(idJunctions4_TOP_5, a_5, b_3, c_5) 
979 
else (idJunctions4_TOP_1, a_4, b_1, c_1); 
980  
981 
add unused variables 
982 
(idJunctions4_Junctions4) 
983 
= (idJunctions4_Junctions4_1); 
984 

985  
986 
tel 
987  
988 
until true restart POINTJunctions4_TOP 
989  
990  
991  
992 
state TOP_B__TO__JUNCTIONS4_TOP_1: 
993  
994 
var idJunctions4_TOP_2, idJunctions4_TOP_3, idJunctions4_TOP_4:int; 
995 
a_2:int; 
996 
b_2:int; 
997 
c_2:int; 
998 
idJunctions4_Junctions4_2:int; 
999 
let 
1000  
1001 
 transition trace : 
1002 
TOP_B__To__Junctions4_TOP_1 
1003 
(idJunctions4_TOP_2) 
1004 
= TOP_B_ex(idJunctions4_TOP_1, false); 
1005 

1006  
1007 
idJunctions4_TOP_3 
1008 
= 0; 
1009 

1010 
(idJunctions4_TOP_4, idJunctions4_Junctions4_2, a_2, b_2, c_2) 
1011 
= Junctions4_TOP_en(idJunctions4_TOP_3, idJunctions4_Junctions4_1, x, a_1, b_1, c_1, true); 
1012 

1013  
1014 
(idJunctions4_TOP, a, b, c, idJunctions4_Junctions4) 
1015 
= (idJunctions4_TOP_4, a_2, b_2, c_2, idJunctions4_Junctions4_2); 
1016  
1017  
1018 
tel 
1019  
1020 
until true restart POINTJunctions4_TOP 
1021  
1022  
1023  
1024 
state TOP_A_IDL: 
1025  
1026 
let 
1027  
1028 

1029  
1030 
(idJunctions4_TOP, a, b, c, idJunctions4_Junctions4) 
1031 
= (idJunctions4_TOP_1, a_1, b_1, c_1, idJunctions4_Junctions4_1); 
1032 

1033  
1034 
tel 
1035  
1036 
until true restart POINTJunctions4_TOP 
1037  
1038  
1039  
1040 
state TOP_B_IDL: 
1041  
1042 
var c_2:int; 
1043 
let 
1044  
1045 

1046 
(c_2) 
1047 
= TOP_B_du(c_1); 
1048  
1049 

1050  
1051  
1052 
(idJunctions4_TOP, a, b, c, idJunctions4_Junctions4) 
1053 
= (idJunctions4_TOP_1, a_1, b_1, c_2, idJunctions4_Junctions4_1); 
1054 

1055  
1056 
tel 
1057  
1058 
until true restart POINTJunctions4_TOP 
1059  
1060  
1061  
1062 
tel 
1063  
1064  
1065 
***************************************************State :Junctions4_Junctions4 Automaton*************************************************** 
1066  
1067 
node Junctions4_Junctions4_node(idJunctions4_Junctions4_1:int; 
1068 
a_1:int; 
1069 
b_1:int; 
1070 
c_1:int; 
1071 
idJunctions4_TOP_1:int; 
1072 
x:int) 
1073  
1074 
returns (idJunctions4_Junctions4:int; 
1075 
a:int; 
1076 
b:int; 
1077 
c:int; 
1078 
idJunctions4_TOP:int); 
1079  
1080  
1081 
let 
1082  
1083 
automaton junctions4_junctions4 
1084  
1085 
state POINTJunctions4_Junctions4: 
1086 
unless (idJunctions4_Junctions4_1=0) restart POINT__TO__JUNCTIONS4_TOP_1 
1087  
1088  
1089  
1090 
unless (idJunctions4_Junctions4_1=1264) restart JUNCTIONS4_TOP_IDL 
1091  
1092 
let 
1093  
1094 
(idJunctions4_Junctions4, a, b, c, idJunctions4_TOP) 
1095 
= (idJunctions4_Junctions4_1, a_1, b_1, c_1, idJunctions4_TOP_1); 
1096 

1097  
1098 
tel 
1099  
1100  
1101  
1102 
state POINT__TO__JUNCTIONS4_TOP_1: 
1103  
1104 
var idJunctions4_Junctions4_2:int; 
1105 
a_2:int; 
1106 
b_2:int; 
1107 
c_2:int; 
1108 
idJunctions4_TOP_2:int; 
1109 
let 
1110  
1111 
 transition trace : 
1112 
POINT__To__Junctions4_TOP_1 
1113 
(idJunctions4_TOP_2, idJunctions4_Junctions4_2, a_2, b_2, c_2) 
1114 
= Junctions4_TOP_en(idJunctions4_TOP_1, idJunctions4_Junctions4_1, x, a_1, b_1, c_1, false); 
1115 

1116  
1117 
(idJunctions4_Junctions4, a, b, c, idJunctions4_TOP) 
1118 
= (idJunctions4_Junctions4_2, a_2, b_2, c_2, idJunctions4_TOP_2); 
1119  
1120  
1121 
tel 
1122  
1123 
until true restart POINTJunctions4_Junctions4 
1124  
1125  
1126  
1127 
state JUNCTIONS4_TOP_IDL: 
1128  
1129 
var idJunctions4_Junctions4_2:int; 
1130 
a_2:int; 
1131 
b_2:int; 
1132 
c_2:int; 
1133 
idJunctions4_TOP_2:int; 
1134 
let 
1135  
1136 

1137 
(idJunctions4_TOP_2, a_2, b_2, c_2, idJunctions4_Junctions4_2) 
1138 
= Junctions4_TOP_node(idJunctions4_TOP_1, x, a_1, b_1, c_1, idJunctions4_Junctions4_1); 
1139  
1140 

1141  
1142  
1143 
(idJunctions4_Junctions4, a, b, c, idJunctions4_TOP) 
1144 
= (idJunctions4_Junctions4_2, a_2, b_2, c_2, idJunctions4_TOP_2); 
1145 

1146  
1147 
tel 
1148  
1149 
until true restart POINTJunctions4_Junctions4 
1150  
1151  
1152  
1153 
tel 
1154  
1155  
1156 
***************************************************State :Junctions4_Junctions4 Automaton*************************************************** 
1157  
1158 
node Junctions4Modified_Junctions4(x:int) 
1159  
1160 
returns (a:int; 
1161 
b:int; 
1162 
c:int); 
1163  
1164  
1165 
var a_1: int; 
1166  
1167 
b_1: int; 
1168  
1169 
c_1: int; 
1170  
1171 
idJunctions4_Junctions4, idJunctions4_Junctions4_1: int; 
1172  
1173 
idJunctions4_TOP, idJunctions4_TOP_1: int; 
1174  
1175 
let 
1176  
1177 
a_1 = 111111 > pre a; 
1178  
1179 
b_1 = 111111 > pre b; 
1180  
1181 
c_1 = 111111 > pre c; 
1182  
1183 
idJunctions4_Junctions4_1 = 0 > pre idJunctions4_Junctions4; 
1184  
1185 
idJunctions4_TOP_1 = 0 > pre idJunctions4_TOP; 
1186  
1187 

1188  
1189  
1190  
1191 
(idJunctions4_Junctions4, a, b, c, idJunctions4_TOP) 
1192 
= Junctions4_Junctions4_node(idJunctions4_Junctions4_1, a_1, b_1, c_1, idJunctions4_TOP_1, x); 
1193  
1194  
1195 
unused outputs 
1196 

1197  
1198 
tel 
1199  
1200  
1201  
1202 
node Junctions4Modified (x_1_1 : int) 
1203 
returns (a_1_1 : int; 
1204 
b_2_1 : int; 
1205 
c_3_1 : int); 
1206 
var 
1207 
Junctions4_1_1 : int; Junctions4_2_1 : int; Junctions4_3_1 : int; 
1208 
i_virtual_local : real; 
1209 
let 
1210 
(Junctions4_1_1, Junctions4_2_1, Junctions4_3_1) = Junctions4Modified_Junctions4(x_1_1); 
1211 
a_1_1 = Junctions4_1_1; 
1212 
b_2_1 = Junctions4_2_1; 
1213 
c_3_1 = Junctions4_3_1; 
1214 
i_virtual_local= 0.0 > 1.0; 
1215 
tel 
1216 