Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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