Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / 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