Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Super12Modif / Super12Modif.lus @ eb639349

History | View | Annotate | Download (24.2 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9

    
10

    
11

    
12

    
13

    
14

    
15

    
16

    
17

    
18

    
19
-- Entry action for state :B_B0
20
node B_B0_en(idSuper12_B_1:int;
21
	isInner:bool)
22

    
23
returns (idSuper12_B:int);
24

    
25

    
26
var 	idSuper12_B_2:int;
27

    
28

    
29
let
30

    
31

    
32

    
33
	-- set state as active 
34
	idSuper12_B_2 
35
	= 1919;
36
	
37

    
38
	(idSuper12_B) 
39
	= (idSuper12_B_2);
40
	
41

    
42
tel
43

    
44

    
45

    
46

    
47

    
48
-- Exit action for state :B_B0
49
node B_B0_ex(idSuper12_B_1:int;
50
	isInner:bool)
51

    
52
returns (idSuper12_B:int);
53

    
54

    
55
var 	idSuper12_B_2:int;
56

    
57

    
58
let
59

    
60

    
61

    
62
	-- set state as inactive 
63
	idSuper12_B_2
64
	 = if (not isInner) then 0 else idSuper12_B_1;
65

    
66

    
67
	(idSuper12_B) 
68
	= (idSuper12_B_1);
69
	
70

    
71
tel
72

    
73

    
74

    
75

    
76

    
77

    
78
-- Entry action for state :B_B1
79
node B_B1_en(idSuper12_B_1:int;
80
	enB1_1:int;
81
	isInner:bool)
82

    
83
returns (idSuper12_B:int;
84
	enB1:int);
85

    
86

    
87
var 	idSuper12_B_2:int;
88
	enB1_2:int;
89

    
90

    
91
let
92

    
93

    
94

    
95
	-- set state as active 
96
	idSuper12_B_2 
97
	= 1918;
98
	
99

    
100
	enB1_2 
101
	= if (not isInner) then  enB1_1  + 1
102
	 else enB1_1;
103
	
104

    
105
	(idSuper12_B, enB1) 
106
	= (idSuper12_B_2, enB1_2);
107
	
108

    
109
tel
110

    
111

    
112

    
113

    
114

    
115
--During action for state :B_B1
116
node B_B1_du(durB1_1:int)
117

    
118
returns (durB1:int);
119

    
120

    
121
var 	durB1_2:int;
122

    
123

    
124
let
125

    
126

    
127

    
128
	durB1_2 
129
	=  durB1_1  + 1;
130
	
131

    
132
	(durB1) 
133
	= (durB1_2);
134
	
135

    
136
tel
137

    
138

    
139

    
140

    
141

    
142
-- Exit action for state :B_B1
143
node B_B1_ex(exB1_1:int;
144
	idSuper12_B_1:int;
145
	isInner:bool)
146

    
147
returns (exB1:int;
148
	idSuper12_B:int);
149

    
150

    
151
var 	exB1_2:int;
152
	idSuper12_B_2:int;
153

    
154

    
155
let
156

    
157

    
158

    
159
	exB1_2 
160
	= if (not isInner) then  exB1_1  + 1
161
	 else exB1_1;
162
	
163

    
164
	-- set state as inactive 
165
	idSuper12_B_2
166
	 = if (not isInner) then 0 else idSuper12_B_1;
167

    
168

    
169
	(exB1, idSuper12_B) 
170
	= (exB1_2, idSuper12_B_1);
171
	
172

    
173
tel
174

    
175

    
176

    
177

    
178

    
179

    
180
-- Entry action for state :Super12_B
181
node Super12_B_en(idSuper12_B_1:int;
182
	idSuper12_Super12_1:int;
183
	enB_1:int;
184
	enB1_1:int;
185
	isInner:bool)
186

    
187
returns (idSuper12_B:int;
188
	idSuper12_Super12:int;
189
	enB:int;
190
	enB1:int);
191

    
192

    
193
var 	idSuper12_B_2, idSuper12_B_3, idSuper12_B_4, idSuper12_B_5, idSuper12_B_6:int;
194
	idSuper12_Super12_2, idSuper12_Super12_3, idSuper12_Super12_4:int;
195
	enB_2, enB_3, enB_4:int;
196
	enB1_2, enB1_3:int;
197

    
198

    
199
let
200

    
201

    
202

    
203
	-- set state as active 
204
	idSuper12_Super12_2 
205
	= 1917;
206
	
207

    
208
	enB_2 
209
	= if (not isInner) then  enB_1  + 1
210
	 else enB_1;
211
	
212

    
213
	
214
-- transition trace :
215
	--POINT__To__B_B0_1
216
		(idSuper12_B_2) 
217
	= B_B0_en(idSuper12_B_1, false);
218
		
219

    
220
	(idSuper12_B_3, idSuper12_Super12_3, enB_3) 
221
	= 
222

    
223
	if ( idSuper12_B_1 = 0) then
224

    
225
	 (idSuper12_B_2, idSuper12_Super12_2, enB_2)
226

    
227
	 else(idSuper12_B_1, idSuper12_Super12_2, enB_2);
228

    
229
	
230

    
231
	(idSuper12_B_4) 
232
	= 
233
	if ( idSuper12_B_1 = 1919) then
234
	B_B0_en(idSuper12_B_1, false)
235
	 else (idSuper12_B_1);
236

    
237
	
238

    
239
	(idSuper12_B_5, enB1_2) 
240
	= 
241
	if ( idSuper12_B_1 = 1918) then
242
	B_B1_en(idSuper12_B_1, enB1_1, false)
243
	 else (idSuper12_B_1, enB1_1);
244

    
245
	
246

    
247
	(idSuper12_B_6, idSuper12_Super12_4, enB_4, enB1_3) 
248
	= 
249
		 if ( idSuper12_B_1 = 0) then 
250
		(idSuper12_B_3, idSuper12_Super12_3, enB_3, enB1_1)
251
		 else
252
		 if ( idSuper12_B_1 = 1919) then 
253
		(idSuper12_B_4, idSuper12_Super12_3, enB_3, enB1_1)
254
		 else
255
		 if ( idSuper12_B_1 = 1918) then 
256
		(idSuper12_B_5, idSuper12_Super12_3, enB_3, enB1_2)
257
		 else (idSuper12_B_1, idSuper12_Super12_2, enB_2, enB1_1);
258

    
259

    
260
	(idSuper12_B, idSuper12_Super12, enB, enB1) 
261
	= (idSuper12_B_6, idSuper12_Super12_4, enB_4, enB1_3);
262
	
263

    
264
tel
265

    
266

    
267

    
268

    
269

    
270
--During action for state :Super12_B
271
node Super12_B_du(durB_1:int)
272

    
273
returns (durB:int);
274

    
275

    
276
var 	durB_2:int;
277

    
278

    
279
let
280

    
281

    
282

    
283
	durB_2 
284
	=  durB_1  + 1;
285
	
286

    
287
	(durB) 
288
	= (durB_2);
289
	
290

    
291
tel
292

    
293

    
294

    
295

    
296

    
297
-- Exit action for state :Super12_B
298
node Super12_B_ex(idSuper12_B_1:int;
299
	exB1_1:int;
300
	exB_1:int;
301
	idSuper12_Super12_1:int;
302
	isInner:bool)
303

    
304
returns (idSuper12_B:int;
305
	exB1:int;
306
	exB:int;
307
	idSuper12_Super12:int);
308

    
309

    
310
var 	idSuper12_B_2, idSuper12_B_3, idSuper12_B_4, idSuper12_B_5:int;
311
	exB1_2, exB1_3:int;
312
	exB_2:int;
313
	idSuper12_Super12_2:int;
314

    
315

    
316
let
317

    
318

    
319

    
320
	
321
	(idSuper12_B_2) 
322
	= 
323
	if ( idSuper12_B_1 = 1919) then
324
	B_B0_ex(idSuper12_B_1, false)
325
	 else (idSuper12_B_1);
326

    
327
	
328

    
329
	(exB1_2, idSuper12_B_3) 
330
	= 
331
	if ( idSuper12_B_1 = 1918) then
332
	B_B1_ex(exB1_1, idSuper12_B_1, false)
333
	 else (exB1_1, idSuper12_B_1);
334

    
335
	
336

    
337
	(idSuper12_B_4, exB1_3) 
338
	= 
339
		 if ( idSuper12_B_1 = 1919) then 
340
		(idSuper12_B_2, exB1_1)
341
		 else
342
		 if ( idSuper12_B_1 = 1918) then 
343
		(idSuper12_B_3, exB1_2)
344
		 else (idSuper12_B_1, exB1_1);
345

    
346

    
347
	exB_2 
348
	= if (not isInner) then  exB_1  + 1
349
	 else exB_1;
350
	
351

    
352
	-- set state as inactive 
353
	idSuper12_Super12_2
354
	 = if (not isInner) then 0 else idSuper12_Super12_1;
355

    
356
	idSuper12_B_5 
357
	= 0;
358
	
359

    
360
	(idSuper12_B, exB1, exB, idSuper12_Super12) 
361
	= (idSuper12_B_5, exB1_3, exB_2, idSuper12_Super12_1);
362
	
363

    
364
tel
365

    
366

    
367

    
368

    
369

    
370

    
371
-- Entry action for state :A_A1
372
node A_A1_en(idSuper12_A_1:int;
373
	isInner:bool)
374

    
375
returns (idSuper12_A:int);
376

    
377

    
378
var 	idSuper12_A_2:int;
379

    
380

    
381
let
382

    
383

    
384

    
385
	-- set state as active 
386
	idSuper12_A_2 
387
	= 1920;
388
	
389

    
390
	(idSuper12_A) 
391
	= (idSuper12_A_2);
392
	
393

    
394
tel
395

    
396

    
397

    
398

    
399

    
400
-- Exit action for state :A_A1
401
node A_A1_ex(idSuper12_A_1:int;
402
	isInner:bool)
403

    
404
returns (idSuper12_A:int);
405

    
406

    
407
var 	idSuper12_A_2:int;
408

    
409

    
410
let
411

    
412

    
413

    
414
	-- set state as inactive 
415
	idSuper12_A_2
416
	 = if (not isInner) then 0 else idSuper12_A_1;
417

    
418

    
419
	(idSuper12_A) 
420
	= (idSuper12_A_1);
421
	
422

    
423
tel
424

    
425

    
426

    
427

    
428

    
429

    
430
-- Entry action for state :A_A0
431
node A_A0_en(idSuper12_A_1:int;
432
	enA0_1:int;
433
	isInner:bool)
434

    
435
returns (idSuper12_A:int;
436
	enA0:int);
437

    
438

    
439
var 	idSuper12_A_2:int;
440
	enA0_2:int;
441

    
442

    
443
let
444

    
445

    
446

    
447
	-- set state as active 
448
	idSuper12_A_2 
449
	= 1915;
450
	
451

    
452
	enA0_2 
453
	= if (not isInner) then  enA0_1  + 1
454
	 else enA0_1;
455
	
456

    
457
	(idSuper12_A, enA0) 
458
	= (idSuper12_A_2, enA0_2);
459
	
460

    
461
tel
462

    
463

    
464

    
465

    
466

    
467
--During action for state :A_A0
468
node A_A0_du(durA0_1:int)
469

    
470
returns (durA0:int);
471

    
472

    
473
var 	durA0_2:int;
474

    
475

    
476
let
477

    
478

    
479

    
480
	durA0_2 
481
	=  durA0_1  + 1;
482
	
483

    
484
	(durA0) 
485
	= (durA0_2);
486
	
487

    
488
tel
489

    
490

    
491

    
492

    
493

    
494
-- Exit action for state :A_A0
495
node A_A0_ex(exA0_1:int;
496
	idSuper12_A_1:int;
497
	isInner:bool)
498

    
499
returns (exA0:int;
500
	idSuper12_A:int);
501

    
502

    
503
var 	exA0_2:int;
504
	idSuper12_A_2:int;
505

    
506

    
507
let
508

    
509

    
510

    
511
	exA0_2 
512
	= if (not isInner) then  exA0_1  + 1
513
	 else exA0_1;
514
	
515

    
516
	-- set state as inactive 
517
	idSuper12_A_2
518
	 = if (not isInner) then 0 else idSuper12_A_1;
519

    
520

    
521
	(exA0, idSuper12_A) 
522
	= (exA0_2, idSuper12_A_1);
523
	
524

    
525
tel
526

    
527

    
528

    
529

    
530

    
531

    
532
-- Entry action for state :Super12_A
533
node Super12_A_en(idSuper12_A_1:int;
534
	idSuper12_Super12_1:int;
535
	enA_1:int;
536
	enA0_1:int;
537
	isInner:bool)
538

    
539
returns (idSuper12_A:int;
540
	idSuper12_Super12:int;
541
	enA:int;
542
	enA0:int);
543

    
544

    
545
var 	idSuper12_A_2, idSuper12_A_3, idSuper12_A_4, idSuper12_A_5, idSuper12_A_6:int;
546
	idSuper12_Super12_2, idSuper12_Super12_3, idSuper12_Super12_4:int;
547
	enA_2, enA_3, enA_4:int;
548
	enA0_2, enA0_3, enA0_4, enA0_5:int;
549

    
550

    
551
let
552

    
553

    
554

    
555
	-- set state as active 
556
	idSuper12_Super12_2 
557
	= 1916;
558
	
559

    
560
	enA_2 
561
	= if (not isInner) then  enA_1  + 1
562
	 else enA_1;
563
	
564

    
565
	
566
-- transition trace :
567
	--POINT__To__A_A0_1
568
		(idSuper12_A_2, enA0_2) 
569
	= A_A0_en(idSuper12_A_1, enA0_1, false);
570
		
571

    
572
	(idSuper12_A_3, idSuper12_Super12_3, enA_3, enA0_3) 
573
	= 
574

    
575
	if ( idSuper12_A_1 = 0) then
576

    
577
	 (idSuper12_A_2, idSuper12_Super12_2, enA_2, enA0_2)
578

    
579
	 else(idSuper12_A_1, idSuper12_Super12_2, enA_2, enA0_1);
580

    
581
	
582

    
583
	(idSuper12_A_4) 
584
	= 
585
	if ( idSuper12_A_1 = 1920) then
586
	A_A1_en(idSuper12_A_1, false)
587
	 else (idSuper12_A_1);
588

    
589
	
590

    
591
	(idSuper12_A_5, enA0_4) 
592
	= 
593
	if ( idSuper12_A_1 = 1915) then
594
	A_A0_en(idSuper12_A_1, enA0_1, false)
595
	 else (idSuper12_A_1, enA0_1);
596

    
597
	
598

    
599
	(idSuper12_A_6, idSuper12_Super12_4, enA_4, enA0_5) 
600
	= 
601
		 if ( idSuper12_A_1 = 0) then 
602
		(idSuper12_A_3, idSuper12_Super12_3, enA_3, enA0_3)
603
		 else
604
		 if ( idSuper12_A_1 = 1920) then 
605
		(idSuper12_A_4, idSuper12_Super12_3, enA_3, enA0_1)
606
		 else
607
		 if ( idSuper12_A_1 = 1915) then 
608
		(idSuper12_A_5, idSuper12_Super12_3, enA_3, enA0_4)
609
		 else (idSuper12_A_1, idSuper12_Super12_2, enA_2, enA0_1);
610

    
611

    
612
	(idSuper12_A, idSuper12_Super12, enA, enA0) 
613
	= (idSuper12_A_6, idSuper12_Super12_4, enA_4, enA0_5);
614
	
615

    
616
tel
617

    
618

    
619

    
620

    
621

    
622
-- Exit action for state :Super12_A
623
node Super12_A_ex(idSuper12_A_1:int;
624
	exA0_1:int;
625
	exA_1:int;
626
	idSuper12_Super12_1:int;
627
	isInner:bool)
628

    
629
returns (idSuper12_A:int;
630
	exA0:int;
631
	exA:int;
632
	idSuper12_Super12:int);
633

    
634

    
635
var 	idSuper12_A_2, idSuper12_A_3, idSuper12_A_4, idSuper12_A_5:int;
636
	exA0_2, exA0_3:int;
637
	exA_2:int;
638
	idSuper12_Super12_2:int;
639

    
640

    
641
let
642

    
643

    
644

    
645
	
646
	(idSuper12_A_2) 
647
	= 
648
	if ( idSuper12_A_1 = 1920) then
649
	A_A1_ex(idSuper12_A_1, false)
650
	 else (idSuper12_A_1);
651

    
652
	
653

    
654
	(exA0_2, idSuper12_A_3) 
655
	= 
656
	if ( idSuper12_A_1 = 1915) then
657
	A_A0_ex(exA0_1, idSuper12_A_1, false)
658
	 else (exA0_1, idSuper12_A_1);
659

    
660
	
661

    
662
	(idSuper12_A_4, exA0_3) 
663
	= 
664
		 if ( idSuper12_A_1 = 1920) then 
665
		(idSuper12_A_2, exA0_1)
666
		 else
667
		 if ( idSuper12_A_1 = 1915) then 
668
		(idSuper12_A_3, exA0_2)
669
		 else (idSuper12_A_1, exA0_1);
670

    
671

    
672
	exA_2 
673
	= if (not isInner) then  exA_1  + 1
674
	 else exA_1;
675
	
676

    
677
	-- set state as inactive 
678
	idSuper12_Super12_2
679
	 = if (not isInner) then 0 else idSuper12_Super12_1;
680

    
681
	idSuper12_A_5 
682
	= 0;
683
	
684

    
685
	(idSuper12_A, exA0, exA, idSuper12_Super12) 
686
	= (idSuper12_A_5, exA0_3, exA_2, idSuper12_Super12_1);
687
	
688

    
689
tel
690

    
691

    
692

    
693

    
694

    
695
--During action for state :Super12_A
696
node Super12_A_du(durA_1:int)
697

    
698
returns (durA:int);
699

    
700

    
701
var 	durA_2:int;
702

    
703

    
704
let
705

    
706

    
707

    
708
	durA_2 
709
	=  durA_1  + 1;
710
	
711

    
712
	(durA) 
713
	= (durA_2);
714
	
715

    
716
tel
717

    
718

    
719
--***************************************************State :Super12_B Automaton***************************************************
720

    
721
node Super12_B_node(idSuper12_B_1:int;
722
	E:bool;
723
	enB1_1:int;
724
	F:bool;
725
	exB_1:int;
726
	exB1_1:int;
727
	idSuper12_Super12_1:int;
728
	idSuper12_A_1:int;
729
	enA_1:int;
730
	enA0_1:int;
731
	durB1_1:int)
732

    
733
returns (idSuper12_B:int;
734
	enB1:int;
735
	exB:int;
736
	exB1:int;
737
	idSuper12_Super12:int;
738
	idSuper12_A:int;
739
	enA:int;
740
	enA0:int;
741
	durB1:int);
742

    
743

    
744
let
745

    
746
	 automaton super12_b
747

    
748
	state POINTSuper12_B:
749
	unless (idSuper12_B_1=0) restart POINT__TO__B_B0_1
750

    
751

    
752

    
753
	unless (idSuper12_B_1=1919) and E restart B_B0__TO__B_B1_1
754

    
755

    
756

    
757
	unless (idSuper12_B_1=1918) and F restart B_B1__TO__A_A0_1
758

    
759

    
760

    
761
	unless (idSuper12_B_1=1918) and E restart B_B1__TO__B_B0_2
762

    
763

    
764

    
765
	unless (idSuper12_B_1=1919) restart B_B0_IDL
766

    
767
	unless (idSuper12_B_1=1918) restart B_B1_IDL
768

    
769
	let
770

    
771
		(idSuper12_B, enB1, exB, exB1, idSuper12_Super12, idSuper12_A, enA, enA0, durB1) 
772
	= (idSuper12_B_1, enB1_1, exB_1, exB1_1, idSuper12_Super12_1, idSuper12_A_1, enA_1, enA0_1, durB1_1);
773
	
774

    
775
	tel
776

    
777

    
778

    
779
	state POINT__TO__B_B0_1:
780

    
781
	 var 	idSuper12_B_2:int;
782
	let
783

    
784
		-- transition trace :
785
	--POINT__To__B_B0_1
786
		(idSuper12_B_2) 
787
	= B_B0_en(idSuper12_B_1, false);
788
		
789

    
790
	(idSuper12_B) 
791
	=  (idSuper12_B_2);
792

    
793
	--add unused variables
794
	(durB1, enA, enA0, enB1, exB, exB1, idSuper12_A, idSuper12_Super12) 
795
	= (durB1_1, enA_1, enA0_1, enB1_1, exB_1, exB1_1, idSuper12_A_1, idSuper12_Super12_1);
796
	
797

    
798
	tel
799

    
800
	until true restart POINTSuper12_B
801

    
802

    
803

    
804
	state B_B0__TO__B_B1_1:
805

    
806
	 var 	idSuper12_B_2, idSuper12_B_3:int;
807
	enB1_2:int;
808
	let
809

    
810
		-- transition trace :
811
	--B_B0__To__B_B1_1
812
		(idSuper12_B_2) 
813
	= B_B0_ex(idSuper12_B_1, false);
814
		
815

    
816
		(idSuper12_B_3, enB1_2) 
817
	= B_B1_en(idSuper12_B_2, enB1_1, false);
818
		
819

    
820
	(idSuper12_B, enB1) 
821
	=  (idSuper12_B_3, enB1_2);
822

    
823
	--add unused variables
824
	(durB1, enA, enA0, exB, exB1, idSuper12_A, idSuper12_Super12) 
825
	= (durB1_1, enA_1, enA0_1, exB_1, exB1_1, idSuper12_A_1, idSuper12_Super12_1);
826
	
827

    
828
	tel
829

    
830
	until true restart POINTSuper12_B
831

    
832

    
833

    
834
	state B_B1__TO__A_A0_1:
835

    
836
	 var 	idSuper12_B_2:int;
837
	exB_2:int;
838
	exB1_2:int;
839
	idSuper12_Super12_2, idSuper12_Super12_3:int;
840
	idSuper12_A_2, idSuper12_A_3:int;
841
	enA_2:int;
842
	enA0_2:int;
843
	let
844

    
845
		-- transition trace :
846
	--B_B1__To__A_A0_1
847
		(idSuper12_B_2, exB1_2, exB_2, idSuper12_Super12_2) 
848
	= Super12_B_ex(idSuper12_B_1, exB1_1, exB_1, idSuper12_Super12_1, false);
849
		
850

    
851
		idSuper12_A_2 
852
	= 1915;
853
	
854
		(idSuper12_A_3, idSuper12_Super12_3, enA_2, enA0_2) 
855
	= Super12_A_en(idSuper12_A_2, idSuper12_Super12_2, enA_1, enA0_1, false);
856
		
857

    
858
	(idSuper12_B, enB1, exB, exB1, idSuper12_Super12, idSuper12_A, enA, enA0) 
859
	=  (idSuper12_B_2, enB1_1, exB_2, exB1_2, idSuper12_Super12_3, idSuper12_A_3, enA_2, enA0_2);
860

    
861
	--add unused variables
862
	(durB1) 
863
	= (durB1_1);
864
	
865

    
866
	tel
867

    
868
	until true restart POINTSuper12_B
869

    
870

    
871

    
872
	state B_B1__TO__B_B0_2:
873

    
874
	 var 	idSuper12_B_2, idSuper12_B_3:int;
875
	exB1_2:int;
876
	let
877

    
878
		-- transition trace :
879
	--B_B1__To__B_B0_2
880
		(exB1_2, idSuper12_B_2) 
881
	= B_B1_ex(exB1_1, idSuper12_B_1, false);
882
		
883

    
884
		(idSuper12_B_3) 
885
	= B_B0_en(idSuper12_B_2, false);
886
		
887

    
888
	(idSuper12_B, enB1, exB, exB1, idSuper12_Super12, idSuper12_A, enA, enA0) 
889
	=  (idSuper12_B_3, enB1_1, exB_1, exB1_2, idSuper12_Super12_1, idSuper12_A_1, enA_1, enA0_1);
890

    
891
	--add unused variables
892
	(durB1) 
893
	= (durB1_1);
894
	
895

    
896
	tel
897

    
898
	until true restart POINTSuper12_B
899

    
900

    
901

    
902
	state B_B0_IDL:
903

    
904
	 	let
905

    
906
		
907

    
908
	(idSuper12_B, enB1, exB, exB1, idSuper12_Super12, idSuper12_A, enA, enA0) 
909
	= (idSuper12_B_1, enB1_1, exB_1, exB1_1, idSuper12_Super12_1, idSuper12_A_1, enA_1, enA0_1);
910
	
911
	--add unused variables
912
	(durB1) 
913
	= (durB1_1);
914
	
915

    
916
	tel
917

    
918
	until true restart POINTSuper12_B
919

    
920

    
921

    
922
	state B_B1_IDL:
923

    
924
	 var 	durB1_2:int;
925
	let
926

    
927
		
928
	(durB1_2) 
929
	= B_B1_du(durB1_1);
930

    
931
		
932

    
933

    
934
	(idSuper12_B, enB1, exB, exB1, idSuper12_Super12, idSuper12_A, enA, enA0, durB1) 
935
	= (idSuper12_B_1, enB1_1, exB_1, exB1_1, idSuper12_Super12_1, idSuper12_A_1, enA_1, enA0_1, durB1_2);
936
	
937

    
938
	tel
939

    
940
	until true restart POINTSuper12_B
941

    
942

    
943

    
944
tel
945

    
946

    
947
--***************************************************State :Super12_A Automaton***************************************************
948

    
949
node Super12_A_node(idSuper12_A_1:int;
950
	enA0_1:int;
951
	F:bool;
952
	E:bool;
953
	exA_1:int;
954
	exA0_1:int;
955
	idSuper12_Super12_1:int;
956
	idSuper12_B_1:int;
957
	enB_1:int;
958
	enB1_1:int;
959
	durA0_1:int)
960

    
961
returns (idSuper12_A:int;
962
	enA0:int;
963
	exA:int;
964
	exA0:int;
965
	idSuper12_Super12:int;
966
	idSuper12_B:int;
967
	enB:int;
968
	enB1:int;
969
	durA0:int);
970

    
971

    
972
let
973

    
974
	 automaton super12_a
975

    
976
	state POINTSuper12_A:
977
	unless (idSuper12_A_1=0) restart POINT__TO__A_A0_1
978

    
979

    
980

    
981
	unless (idSuper12_A_1=1920) and F restart A_A1__TO__A_A0_1
982

    
983

    
984

    
985
	unless (idSuper12_A_1=1915) and E restart A_A0__TO__B_B1_1
986

    
987

    
988

    
989
	unless (idSuper12_A_1=1915) and F restart A_A0__TO__A_A1_2
990

    
991

    
992

    
993
	unless (idSuper12_A_1=1920) restart A_A1_IDL
994

    
995
	unless (idSuper12_A_1=1915) restart A_A0_IDL
996

    
997
	let
998

    
999
		(idSuper12_A, enA0, exA, exA0, idSuper12_Super12, idSuper12_B, enB, enB1, durA0) 
1000
	= (idSuper12_A_1, enA0_1, exA_1, exA0_1, idSuper12_Super12_1, idSuper12_B_1, enB_1, enB1_1, durA0_1);
1001
	
1002

    
1003
	tel
1004

    
1005

    
1006

    
1007
	state POINT__TO__A_A0_1:
1008

    
1009
	 var 	idSuper12_A_2:int;
1010
	enA0_2:int;
1011
	let
1012

    
1013
		-- transition trace :
1014
	--POINT__To__A_A0_1
1015
		(idSuper12_A_2, enA0_2) 
1016
	= A_A0_en(idSuper12_A_1, enA0_1, false);
1017
		
1018

    
1019
	(idSuper12_A, enA0) 
1020
	=  (idSuper12_A_2, enA0_2);
1021

    
1022
	--add unused variables
1023
	(durA0, enB, enB1, exA, exA0, idSuper12_B, idSuper12_Super12) 
1024
	= (durA0_1, enB_1, enB1_1, exA_1, exA0_1, idSuper12_B_1, idSuper12_Super12_1);
1025
	
1026

    
1027
	tel
1028

    
1029
	until true restart POINTSuper12_A
1030

    
1031

    
1032

    
1033
	state A_A1__TO__A_A0_1:
1034

    
1035
	 var 	idSuper12_A_2, idSuper12_A_3:int;
1036
	enA0_2:int;
1037
	let
1038

    
1039
		-- transition trace :
1040
	--A_A1__To__A_A0_1
1041
		(idSuper12_A_2) 
1042
	= A_A1_ex(idSuper12_A_1, false);
1043
		
1044

    
1045
		(idSuper12_A_3, enA0_2) 
1046
	= A_A0_en(idSuper12_A_2, enA0_1, false);
1047
		
1048

    
1049
	(idSuper12_A, enA0) 
1050
	=  (idSuper12_A_3, enA0_2);
1051

    
1052
	--add unused variables
1053
	(durA0, enB, enB1, exA, exA0, idSuper12_B, idSuper12_Super12) 
1054
	= (durA0_1, enB_1, enB1_1, exA_1, exA0_1, idSuper12_B_1, idSuper12_Super12_1);
1055
	
1056

    
1057
	tel
1058

    
1059
	until true restart POINTSuper12_A
1060

    
1061

    
1062

    
1063
	state A_A0__TO__B_B1_1:
1064

    
1065
	 var 	idSuper12_A_2:int;
1066
	exA_2:int;
1067
	exA0_2:int;
1068
	idSuper12_Super12_2, idSuper12_Super12_3:int;
1069
	idSuper12_B_2, idSuper12_B_3:int;
1070
	enB_2:int;
1071
	enB1_2:int;
1072
	let
1073

    
1074
		-- transition trace :
1075
	--A_A0__To__B_B1_1
1076
		(idSuper12_A_2, exA0_2, exA_2, idSuper12_Super12_2) 
1077
	= Super12_A_ex(idSuper12_A_1, exA0_1, exA_1, idSuper12_Super12_1, false);
1078
		
1079

    
1080
		idSuper12_B_2 
1081
	= 1918;
1082
	
1083
		(idSuper12_B_3, idSuper12_Super12_3, enB_2, enB1_2) 
1084
	= Super12_B_en(idSuper12_B_2, idSuper12_Super12_2, enB_1, enB1_1, false);
1085
		
1086

    
1087
	(idSuper12_A, enA0, exA, exA0, idSuper12_Super12, idSuper12_B, enB, enB1) 
1088
	=  (idSuper12_A_2, enA0_1, exA_2, exA0_2, idSuper12_Super12_3, idSuper12_B_3, enB_2, enB1_2);
1089

    
1090
	--add unused variables
1091
	(durA0) 
1092
	= (durA0_1);
1093
	
1094

    
1095
	tel
1096

    
1097
	until true restart POINTSuper12_A
1098

    
1099

    
1100

    
1101
	state A_A0__TO__A_A1_2:
1102

    
1103
	 var 	idSuper12_A_2, idSuper12_A_3:int;
1104
	exA0_2:int;
1105
	let
1106

    
1107
		-- transition trace :
1108
	--A_A0__To__A_A1_2
1109
		(exA0_2, idSuper12_A_2) 
1110
	= A_A0_ex(exA0_1, idSuper12_A_1, false);
1111
		
1112

    
1113
		(idSuper12_A_3) 
1114
	= A_A1_en(idSuper12_A_2, false);
1115
		
1116

    
1117
	(idSuper12_A, enA0, exA, exA0, idSuper12_Super12, idSuper12_B, enB, enB1) 
1118
	=  (idSuper12_A_3, enA0_1, exA_1, exA0_2, idSuper12_Super12_1, idSuper12_B_1, enB_1, enB1_1);
1119

    
1120
	--add unused variables
1121
	(durA0) 
1122
	= (durA0_1);
1123
	
1124

    
1125
	tel
1126

    
1127
	until true restart POINTSuper12_A
1128

    
1129

    
1130

    
1131
	state A_A1_IDL:
1132

    
1133
	 	let
1134

    
1135
		
1136

    
1137
	(idSuper12_A, enA0, exA, exA0, idSuper12_Super12, idSuper12_B, enB, enB1) 
1138
	= (idSuper12_A_1, enA0_1, exA_1, exA0_1, idSuper12_Super12_1, idSuper12_B_1, enB_1, enB1_1);
1139
	
1140
	--add unused variables
1141
	(durA0) 
1142
	= (durA0_1);
1143
	
1144

    
1145
	tel
1146

    
1147
	until true restart POINTSuper12_A
1148

    
1149

    
1150

    
1151
	state A_A0_IDL:
1152

    
1153
	 var 	durA0_2:int;
1154
	let
1155

    
1156
		
1157
	(durA0_2) 
1158
	= A_A0_du(durA0_1);
1159

    
1160
		
1161

    
1162

    
1163
	(idSuper12_A, enA0, exA, exA0, idSuper12_Super12, idSuper12_B, enB, enB1, durA0) 
1164
	= (idSuper12_A_1, enA0_1, exA_1, exA0_1, idSuper12_Super12_1, idSuper12_B_1, enB_1, enB1_1, durA0_2);
1165
	
1166

    
1167
	tel
1168

    
1169
	until true restart POINTSuper12_A
1170

    
1171

    
1172

    
1173
tel
1174

    
1175

    
1176
--***************************************************State :Super12_Super12 Automaton***************************************************
1177

    
1178
node Super12_Super12_node(idSuper12_Super12_1:int;
1179
	enA_1:int;
1180
	enA0_1:int;
1181
	idSuper12_A_1:int;
1182
	F:bool;
1183
	exA_1:int;
1184
	exA0_1:int;
1185
	enB_1:int;
1186
	enB1_1:int;
1187
	idSuper12_B_1:int;
1188
	durA_1:int;
1189
	E:bool;
1190
	durA0_1:int;
1191
	durB_1:int;
1192
	durB1_1:int;
1193
	exB_1:int;
1194
	exB1_1:int)
1195

    
1196
returns (idSuper12_Super12:int;
1197
	enA:int;
1198
	enA0:int;
1199
	idSuper12_A:int;
1200
	exA:int;
1201
	exA0:int;
1202
	enB:int;
1203
	enB1:int;
1204
	idSuper12_B:int;
1205
	durA:int;
1206
	durA0:int;
1207
	durB:int;
1208
	durB1:int;
1209
	exB:int;
1210
	exB1:int);
1211

    
1212

    
1213
let
1214

    
1215
	 automaton super12_super12
1216

    
1217
	state POINTSuper12_Super12:
1218
	unless (idSuper12_Super12_1=0) restart POINT__TO__SUPER12_A_1
1219

    
1220

    
1221

    
1222
	unless (idSuper12_Super12_1=1916) and F restart SUPER12_A__TO__SUPER12_B_1
1223

    
1224

    
1225

    
1226
	unless (idSuper12_Super12_1=1916) restart SUPER12_A_IDL
1227

    
1228
	unless (idSuper12_Super12_1=1917) restart SUPER12_B_IDL
1229

    
1230
	let
1231

    
1232
		(idSuper12_Super12, enA, enA0, idSuper12_A, exA, exA0, enB, enB1, idSuper12_B, durA, durA0, durB, durB1, exB, exB1) 
1233
	= (idSuper12_Super12_1, enA_1, enA0_1, idSuper12_A_1, exA_1, exA0_1, enB_1, enB1_1, idSuper12_B_1, durA_1, durA0_1, durB_1, durB1_1, exB_1, exB1_1);
1234
	
1235

    
1236
	tel
1237

    
1238

    
1239

    
1240
	state POINT__TO__SUPER12_A_1:
1241

    
1242
	 var 	idSuper12_Super12_2:int;
1243
	enA_2:int;
1244
	enA0_2:int;
1245
	idSuper12_A_2:int;
1246
	let
1247

    
1248
		-- transition trace :
1249
	--POINT__To__Super12_A_1
1250
		(idSuper12_A_2, idSuper12_Super12_2, enA_2, enA0_2) 
1251
	= Super12_A_en(idSuper12_A_1, idSuper12_Super12_1, enA_1, enA0_1, false);
1252
		
1253

    
1254
	(idSuper12_Super12, enA, enA0, idSuper12_A) 
1255
	=  (idSuper12_Super12_2, enA_2, enA0_2, idSuper12_A_2);
1256

    
1257
	--add unused variables
1258
	(durA, durA0, durB, durB1, enB, enB1, exA, exA0, exB, exB1, idSuper12_B) 
1259
	= (durA_1, durA0_1, durB_1, durB1_1, enB_1, enB1_1, exA_1, exA0_1, exB_1, exB1_1, idSuper12_B_1);
1260
	
1261

    
1262
	tel
1263

    
1264
	until true restart POINTSuper12_Super12
1265

    
1266

    
1267

    
1268
	state SUPER12_A__TO__SUPER12_B_1:
1269

    
1270
	 var 	idSuper12_Super12_2, idSuper12_Super12_3:int;
1271
	idSuper12_A_2:int;
1272
	exA_2:int;
1273
	exA0_2:int;
1274
	enB_2:int;
1275
	enB1_2:int;
1276
	idSuper12_B_2:int;
1277
	let
1278

    
1279
		-- transition trace :
1280
	--Super12_A__To__Super12_B_1
1281
		(idSuper12_A_2, exA0_2, exA_2, idSuper12_Super12_2) 
1282
	= Super12_A_ex(idSuper12_A_1, exA0_1, exA_1, idSuper12_Super12_1, false);
1283
		
1284

    
1285
		(idSuper12_B_2, idSuper12_Super12_3, enB_2, enB1_2) 
1286
	= Super12_B_en(idSuper12_B_1, idSuper12_Super12_2, enB_1, enB1_1, false);
1287
		
1288

    
1289
	(idSuper12_Super12, enA, enA0, idSuper12_A, exA, exA0, enB, enB1, idSuper12_B) 
1290
	=  (idSuper12_Super12_3, enA_1, enA0_1, idSuper12_A_2, exA_2, exA0_2, enB_2, enB1_2, idSuper12_B_2);
1291

    
1292
	--add unused variables
1293
	(durA, durA0, durB, durB1, exB, exB1) 
1294
	= (durA_1, durA0_1, durB_1, durB1_1, exB_1, exB1_1);
1295
	
1296

    
1297
	tel
1298

    
1299
	until true restart POINTSuper12_Super12
1300

    
1301

    
1302

    
1303
	state SUPER12_A_IDL:
1304

    
1305
	 var 	idSuper12_Super12_2:int;
1306
	enA0_2:int;
1307
	idSuper12_A_2:int;
1308
	exA_2:int;
1309
	exA0_2:int;
1310
	enB_2:int;
1311
	enB1_2:int;
1312
	idSuper12_B_2:int;
1313
	durA_2:int;
1314
	durA0_2:int;
1315
	let
1316

    
1317
		
1318
	(durA_2) 
1319
	= Super12_A_du(durA_1);
1320

    
1321
		
1322

    
1323
	(idSuper12_A_2, enA0_2, exA_2, exA0_2, idSuper12_Super12_2, idSuper12_B_2, enB_2, enB1_2, durA0_2) 
1324
	= Super12_A_node(idSuper12_A_1, enA0_1, F, E, exA_1, exA0_1, idSuper12_Super12_1, idSuper12_B_1, enB_1, enB1_1, durA0_1);
1325

    
1326
		
1327

    
1328

    
1329
	(idSuper12_Super12, enA, enA0, idSuper12_A, exA, exA0, enB, enB1, idSuper12_B, durA, durA0) 
1330
	= (idSuper12_Super12_2, enA_1, enA0_2, idSuper12_A_2, exA_2, exA0_2, enB_2, enB1_2, idSuper12_B_2, durA_2, durA0_2);
1331
	
1332
	--add unused variables
1333
	(durB, durB1, exB, exB1) 
1334
	= (durB_1, durB1_1, exB_1, exB1_1);
1335
	
1336

    
1337
	tel
1338

    
1339
	until true restart POINTSuper12_Super12
1340

    
1341

    
1342

    
1343
	state SUPER12_B_IDL:
1344

    
1345
	 var 	idSuper12_Super12_2:int;
1346
	enA_2:int;
1347
	enA0_2:int;
1348
	idSuper12_A_2:int;
1349
	enB1_2:int;
1350
	idSuper12_B_2:int;
1351
	durB_2:int;
1352
	durB1_2:int;
1353
	exB_2:int;
1354
	exB1_2:int;
1355
	let
1356

    
1357
		
1358
	(durB_2) 
1359
	= Super12_B_du(durB_1);
1360

    
1361
		
1362

    
1363
	(idSuper12_B_2, enB1_2, exB_2, exB1_2, idSuper12_Super12_2, idSuper12_A_2, enA_2, enA0_2, durB1_2) 
1364
	= Super12_B_node(idSuper12_B_1, E, enB1_1, F, exB_1, exB1_1, idSuper12_Super12_1, idSuper12_A_1, enA_1, enA0_1, durB1_1);
1365

    
1366
		
1367

    
1368

    
1369
	(idSuper12_Super12, enA, enA0, idSuper12_A, exA, exA0, enB, enB1, idSuper12_B, durA, durA0, durB, durB1, exB, exB1) 
1370
	= (idSuper12_Super12_2, enA_2, enA0_2, idSuper12_A_2, exA_1, exA0_1, enB_1, enB1_2, idSuper12_B_2, durA_1, durA0_1, durB_2, durB1_2, exB_2, exB1_2);
1371
	
1372

    
1373
	tel
1374

    
1375
	until true restart POINTSuper12_Super12
1376

    
1377

    
1378

    
1379
tel
1380

    
1381

    
1382
--***************************************************State :Super12_Super12 Automaton***************************************************
1383

    
1384
node Super12Modif_Super12(E:bool;
1385
	F:bool)
1386

    
1387
returns (durA:int;
1388
	durA0:int;
1389
	durB:int;
1390
	durB1:int;
1391
	enA:int;
1392
	enA0:int;
1393
	enB:int;
1394
	enB1:int;
1395
	exA:int;
1396
	exA0:int;
1397
	exB:int;
1398
	exB1:int);
1399

    
1400

    
1401
var durA_1: int;
1402

    
1403
	durA0_1: int;
1404

    
1405
	durB_1: int;
1406

    
1407
	durB1_1: int;
1408

    
1409
	enA_1: int;
1410

    
1411
	enA0_1: int;
1412

    
1413
	enB_1: int;
1414

    
1415
	enB1_1: int;
1416

    
1417
	exA_1: int;
1418

    
1419
	exA0_1: int;
1420

    
1421
	exB_1: int;
1422

    
1423
	exB1_1: int;
1424

    
1425
	idSuper12_Super12, idSuper12_Super12_1: int;
1426

    
1427
	idSuper12_B, idSuper12_B_1: int;
1428

    
1429
	idSuper12_A, idSuper12_A_1: int;
1430

    
1431
		idSuper12_Super12_2:int;
1432
	enA_2:int;
1433
	enA0_2:int;
1434
	idSuper12_A_2:int;
1435
	exA_2:int;
1436
	exA0_2:int;
1437
	enB_2:int;
1438
	enB1_2:int;
1439
	idSuper12_B_2:int;
1440
	durA_2:int;
1441
	durA0_2:int;
1442
	durB_2:int;
1443
	durB1_2:int;
1444
	exB_2:int;
1445
	exB1_2:int;
1446
let
1447

    
1448
	durA_1 = 0 -> pre durA;
1449

    
1450
	durA0_1 = 0 -> pre durA0;
1451

    
1452
	durB_1 = 0 -> pre durB;
1453

    
1454
	durB1_1 = 0 -> pre durB1;
1455

    
1456
	enA_1 = 0 -> pre enA;
1457

    
1458
	enA0_1 = 0 -> pre enA0;
1459

    
1460
	enB_1 = 0 -> pre enB;
1461

    
1462
	enB1_1 = 0 -> pre enB1;
1463

    
1464
	exA_1 = 0 -> pre exA;
1465

    
1466
	exA0_1 = 0 -> pre exA0;
1467

    
1468
	exB_1 = 0 -> pre exB;
1469

    
1470
	exB1_1 = 0 -> pre exB1;
1471

    
1472
	idSuper12_Super12_1 = 0 -> pre idSuper12_Super12;
1473

    
1474
	idSuper12_B_1 = 0 -> pre idSuper12_B;
1475

    
1476
	idSuper12_A_1 = 0 -> pre idSuper12_A;
1477

    
1478
	
1479

    
1480

    
1481

    
1482
	(idSuper12_Super12_2, enA_2, enA0_2, idSuper12_A_2, exA_2, exA0_2, enB_2, enB1_2, idSuper12_B_2, durA_2, durA0_2, durB_2, durB1_2, exB_2, exB1_2)
1483
	 = 
1484

    
1485
	 if E then Super12_Super12_node(idSuper12_Super12_1, enA_1, enA0_1, idSuper12_A_1, false, exA_1, exA0_1, enB_1, enB1_1, idSuper12_B_1, durA_1, E, durA0_1, durB_1, durB1_1, exB_1, exB1_1)
1486

    
1487
	 else (idSuper12_Super12_1, enA_1, enA0_1, idSuper12_A_1, exA_1, exA0_1, enB_1, enB1_1, idSuper12_B_1, durA_1, durA0_1, durB_1, durB1_1, exB_1, exB1_1);
1488

    
1489
	
1490

    
1491

    
1492

    
1493
	(idSuper12_Super12, enA, enA0, idSuper12_A, exA, exA0, enB, enB1, idSuper12_B, durA, durA0, durB, durB1, exB, exB1)
1494
	 = 
1495

    
1496
	 if F then Super12_Super12_node(idSuper12_Super12_2, enA_2, enA0_2, idSuper12_A_2, F, exA_2, exA0_2, enB_2, enB1_2, idSuper12_B_2, durA_2, false, durA0_2, durB_2, durB1_2, exB_2, exB1_2)
1497

    
1498
	 else (idSuper12_Super12_2, enA_2, enA0_2, idSuper12_A_2, exA_2, exA0_2, enB_2, enB1_2, idSuper12_B_2, durA_2, durA0_2, durB_2, durB1_2, exB_2, exB1_2);
1499

    
1500
	
1501

    
1502

    
1503
--unused outputs
1504
	
1505

    
1506
tel
1507

    
1508

    
1509

    
1510
node Super12Modif (E_1_1 : real; F_1_1 : real)
1511
returns (duA_1_1 : int;
1512
	durA0_2_1 : int;
1513
	durB_3_1 : int;
1514
	durB1_4_1 : int;
1515
	enA_5_1 : int;
1516
	enA0_6_1 : int;
1517
	enB_7_1 : int;
1518
	enB1_8_1 : int;
1519
	exA_9_1 : int;
1520
	exA0_10_1 : int;
1521
	exB_11_1 : int;
1522
	exB1_12_1 : int); 
1523
var
1524
	Mux_1_1 : real; Mux_1_2 : real;
1525
	Super12_1_1 : int; Super12_2_1 : int; Super12_3_1 : int; Super12_4_1 : int; Super12_5_1 : int; Super12_6_1 : int; Super12_7_1 : int; Super12_8_1 : int; Super12_9_1 : int; Super12_10_1 : int; Super12_11_1 : int; Super12_12_1 : int;
1526
	i_virtual_local : real;
1527
	Super12Mux_1_1_event: bool;
1528
	Super12Mux_1_2_event: bool;
1529
let 
1530
	Mux_1_1 = E_1_1 ;
1531
	Mux_1_2 = F_1_1 ;
1532
	Super12Mux_1_1_event = false -> ((pre(Mux_1_1) > 0.0 and Mux_1_1 <= 0.0) or (pre(Mux_1_1) <= 0.0 and Mux_1_1 > 0.0));
1533
	Super12Mux_1_2_event = false -> ((pre(Mux_1_2) > 0.0 and Mux_1_2 <= 0.0) or (pre(Mux_1_2) <= 0.0 and Mux_1_2 > 0.0));
1534
	(Super12_1_1, Super12_2_1, Super12_3_1, Super12_4_1, Super12_5_1, Super12_6_1, Super12_7_1, Super12_8_1, Super12_9_1, Super12_10_1, Super12_11_1, Super12_12_1) =  Super12Modif_Super12(Super12Mux_1_1_event, Super12Mux_1_2_event);
1535
	duA_1_1 = Super12_1_1;
1536
	durA0_2_1 = Super12_2_1;
1537
	durB_3_1 = Super12_3_1;
1538
	durB1_4_1 = Super12_4_1;
1539
	enA_5_1 = Super12_5_1;
1540
	enA0_6_1 = Super12_6_1;
1541
	enB_7_1 = Super12_7_1;
1542
	enB1_8_1 = Super12_8_1;
1543
	exA_9_1 = Super12_9_1;
1544
	exA0_10_1 = Super12_10_1;
1545
	exB_11_1 = Super12_11_1;
1546
	exB1_12_1 = Super12_12_1;
1547
	i_virtual_local= 0.0 -> 1.0;
1548
tel
1549