Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_EventsOrderV2 / EventsOrderV2.lus @ eb639349

History | View | Annotate | Download (17.1 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
-- Entry action for state :A2_A2a
19
node A2_A2a_en(idA_A2_1:int;
20
	a_1:int;
21
	isInner:bool)
22

    
23
returns (idA_A2:int;
24
	a:int);
25

    
26

    
27
var 	idA_A2_2:int;
28
	a_2:int;
29

    
30

    
31
let
32

    
33

    
34

    
35
	-- set state as active 
36
	idA_A2_2 
37
	= 721;
38
	
39

    
40
	a_2 
41
	= if (not isInner) then  a_1 +3
42
	 else a_1;
43
	
44

    
45
	(idA_A2, a) 
46
	= (idA_A2_2, a_2);
47
	
48

    
49
tel
50

    
51

    
52

    
53

    
54

    
55
-- Exit action for state :A2_A2a
56
node A2_A2a_ex(idA_A2_1:int;
57
	isInner:bool)
58

    
59
returns (idA_A2:int);
60

    
61

    
62
var 	idA_A2_2:int;
63

    
64

    
65
let
66

    
67

    
68

    
69
	-- set state as inactive 
70
	idA_A2_2
71
	 = if (not isInner) then 0 else idA_A2_1;
72

    
73

    
74
	(idA_A2) 
75
	= (idA_A2_1);
76
	
77

    
78
tel
79

    
80

    
81

    
82

    
83

    
84

    
85
-- Entry action for state :A2_A2b
86
node A2_A2b_en(idA_A2_1:int;
87
	a_1:int;
88
	isInner:bool)
89

    
90
returns (idA_A2:int;
91
	a:int);
92

    
93

    
94
var 	idA_A2_2:int;
95
	a_2:int;
96

    
97

    
98
let
99

    
100

    
101

    
102
	-- set state as active 
103
	idA_A2_2 
104
	= 722;
105
	
106

    
107
	a_2 
108
	= if (not isInner) then  a_1 +4
109
	 else a_1;
110
	
111

    
112
	(idA_A2, a) 
113
	= (idA_A2_2, a_2);
114
	
115

    
116
tel
117

    
118

    
119

    
120

    
121

    
122
-- Exit action for state :A2_A2b
123
node A2_A2b_ex(idA_A2_1:int;
124
	isInner:bool)
125

    
126
returns (idA_A2:int);
127

    
128

    
129
var 	idA_A2_2:int;
130

    
131

    
132
let
133

    
134

    
135

    
136
	-- set state as inactive 
137
	idA_A2_2
138
	 = if (not isInner) then 0 else idA_A2_1;
139

    
140

    
141
	(idA_A2) 
142
	= (idA_A2_1);
143
	
144

    
145
tel
146

    
147

    
148

    
149

    
150

    
151

    
152
-- Entry action for state :A_A2
153
node A_A2_en(idA_A2_1:int;
154
	idEvents1_A_1:int;
155
	a_1:int;
156
	isInner:bool)
157

    
158
returns (idA_A2:int;
159
	idEvents1_A:int;
160
	a:int);
161

    
162

    
163
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int;
164
	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int;
165
	a_2, a_3, a_4, a_5, a_6:int;
166

    
167

    
168
let
169

    
170

    
171

    
172
	-- set state as active 
173
	idEvents1_A_2 
174
	= 720;
175
	
176

    
177
	
178
-- transition trace :
179
	--POINT__To__A2_A2a_1
180
		(idA_A2_2, a_2) 
181
	= A2_A2a_en(idA_A2_1, a_1, false);
182
		
183

    
184
	(idA_A2_3, idEvents1_A_3, a_3) 
185
	= 
186

    
187
	if ( idA_A2_1 = 0) then
188

    
189
	 (idA_A2_2, idEvents1_A_2, a_2)
190

    
191
	 else(idA_A2_1, idEvents1_A_2, a_1);
192

    
193
	
194

    
195
	(idA_A2_4, a_4) 
196
	= 
197
	if ( idA_A2_1 = 721) then
198
	A2_A2a_en(idA_A2_1, a_1, false)
199
	 else (idA_A2_1, a_1);
200

    
201
	
202

    
203
	(idA_A2_5, a_5) 
204
	= 
205
	if ( idA_A2_1 = 722) then
206
	A2_A2b_en(idA_A2_1, a_1, false)
207
	 else (idA_A2_1, a_1);
208

    
209
	
210

    
211
	(idA_A2_6, idEvents1_A_4, a_6) 
212
	= 
213
		 if ( idA_A2_1 = 0) then 
214
		(idA_A2_3, idEvents1_A_3, a_3)
215
		 else
216
		 if ( idA_A2_1 = 721) then 
217
		(idA_A2_4, idEvents1_A_3, a_4)
218
		 else
219
		 if ( idA_A2_1 = 722) then 
220
		(idA_A2_5, idEvents1_A_3, a_5)
221
		 else (idA_A2_1, idEvents1_A_2, a_1);
222

    
223

    
224
	(idA_A2, idEvents1_A, a) 
225
	= (idA_A2_6, idEvents1_A_4, a_6);
226
	
227

    
228
tel
229

    
230

    
231

    
232

    
233

    
234
-- Exit action for state :A_A2
235
node A_A2_ex(idA_A2_1:int;
236
	idEvents1_A_1:int;
237
	isInner:bool)
238

    
239
returns (idA_A2:int;
240
	idEvents1_A:int);
241

    
242

    
243
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int;
244
	idEvents1_A_2:int;
245

    
246

    
247
let
248

    
249

    
250

    
251
	
252
	(idA_A2_2) 
253
	= 
254
	if ( idA_A2_1 = 721) then
255
	A2_A2a_ex(idA_A2_1, false)
256
	 else (idA_A2_1);
257

    
258
	
259

    
260
	(idA_A2_3) 
261
	= 
262
	if ( idA_A2_1 = 722) then
263
	A2_A2b_ex(idA_A2_1, false)
264
	 else (idA_A2_1);
265

    
266
	
267

    
268
	(idA_A2_4) 
269
	= 
270
		 if ( idA_A2_1 = 721) then 
271
		(idA_A2_2)
272
		 else
273
		 if ( idA_A2_1 = 722) then 
274
		(idA_A2_3)
275
		 else (idA_A2_1);
276

    
277

    
278
	-- set state as inactive 
279
	idEvents1_A_2
280
	 = if (not isInner) then 0 else idEvents1_A_1;
281

    
282
	idA_A2_5 
283
	= 0;
284
	
285

    
286
	(idA_A2, idEvents1_A) 
287
	= (idA_A2_5, idEvents1_A_1);
288
	
289

    
290
tel
291

    
292

    
293

    
294

    
295

    
296

    
297
-- Entry action for state :A1_A1b
298
node A1_A1b_en(idA_A1_1:int;
299
	a_1:int;
300
	isInner:bool)
301

    
302
returns (idA_A1:int;
303
	a:int);
304

    
305

    
306
var 	idA_A1_2:int;
307
	a_2:int;
308

    
309

    
310
let
311

    
312

    
313

    
314
	-- set state as active 
315
	idA_A1_2 
316
	= 725;
317
	
318

    
319
	a_2 
320
	= if (not isInner) then  a_1 +2
321
	 else a_1;
322
	
323

    
324
	(idA_A1, a) 
325
	= (idA_A1_2, a_2);
326
	
327

    
328
tel
329

    
330

    
331

    
332

    
333

    
334
-- Exit action for state :A1_A1b
335
node A1_A1b_ex(idA_A1_1:int;
336
	isInner:bool)
337

    
338
returns (idA_A1:int);
339

    
340

    
341
var 	idA_A1_2:int;
342

    
343

    
344
let
345

    
346

    
347

    
348
	-- set state as inactive 
349
	idA_A1_2
350
	 = if (not isInner) then 0 else idA_A1_1;
351

    
352

    
353
	(idA_A1) 
354
	= (idA_A1_1);
355
	
356

    
357
tel
358

    
359

    
360

    
361

    
362

    
363

    
364
-- Entry action for state :A1_A1a
365
node A1_A1a_en(idA_A1_1:int;
366
	a_1:int;
367
	isInner:bool)
368

    
369
returns (idA_A1:int;
370
	a:int);
371

    
372

    
373
var 	idA_A1_2:int;
374
	a_2:int;
375

    
376

    
377
let
378

    
379

    
380

    
381
	-- set state as active 
382
	idA_A1_2 
383
	= 724;
384
	
385

    
386
	a_2 
387
	= if (not isInner) then  a_1 +1
388
	 else a_1;
389
	
390

    
391
	(idA_A1, a) 
392
	= (idA_A1_2, a_2);
393
	
394

    
395
tel
396

    
397

    
398

    
399

    
400

    
401
-- Exit action for state :A1_A1a
402
node A1_A1a_ex(idA_A1_1:int;
403
	isInner:bool)
404

    
405
returns (idA_A1:int);
406

    
407

    
408
var 	idA_A1_2:int;
409

    
410

    
411
let
412

    
413

    
414

    
415
	-- set state as inactive 
416
	idA_A1_2
417
	 = if (not isInner) then 0 else idA_A1_1;
418

    
419

    
420
	(idA_A1) 
421
	= (idA_A1_1);
422
	
423

    
424
tel
425

    
426

    
427

    
428

    
429

    
430

    
431
-- Entry action for state :A_A1
432
node A_A1_en(idA_A1_1:int;
433
	idEvents1_A_1:int;
434
	a_1:int;
435
	isInner:bool)
436

    
437
returns (idA_A1:int;
438
	idEvents1_A:int;
439
	a:int);
440

    
441

    
442
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int;
443
	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int;
444
	a_2, a_3, a_4, a_5, a_6:int;
445

    
446

    
447
let
448

    
449

    
450

    
451
	-- set state as active 
452
	idEvents1_A_2 
453
	= 723;
454
	
455

    
456
	
457
-- transition trace :
458
	--POINT__To__A1_A1a_1
459
		(idA_A1_2, a_2) 
460
	= A1_A1a_en(idA_A1_1, a_1, false);
461
		
462

    
463
	(idA_A1_3, idEvents1_A_3, a_3) 
464
	= 
465

    
466
	if ( idA_A1_1 = 0) then
467

    
468
	 (idA_A1_2, idEvents1_A_2, a_2)
469

    
470
	 else(idA_A1_1, idEvents1_A_2, a_1);
471

    
472
	
473

    
474
	(idA_A1_4, a_4) 
475
	= 
476
	if ( idA_A1_1 = 724) then
477
	A1_A1a_en(idA_A1_1, a_1, false)
478
	 else (idA_A1_1, a_1);
479

    
480
	
481

    
482
	(idA_A1_5, a_5) 
483
	= 
484
	if ( idA_A1_1 = 725) then
485
	A1_A1b_en(idA_A1_1, a_1, false)
486
	 else (idA_A1_1, a_1);
487

    
488
	
489

    
490
	(idA_A1_6, idEvents1_A_4, a_6) 
491
	= 
492
		 if ( idA_A1_1 = 0) then 
493
		(idA_A1_3, idEvents1_A_3, a_3)
494
		 else
495
		 if ( idA_A1_1 = 724) then 
496
		(idA_A1_4, idEvents1_A_3, a_4)
497
		 else
498
		 if ( idA_A1_1 = 725) then 
499
		(idA_A1_5, idEvents1_A_3, a_5)
500
		 else (idA_A1_1, idEvents1_A_2, a_1);
501

    
502

    
503
	(idA_A1, idEvents1_A, a) 
504
	= (idA_A1_6, idEvents1_A_4, a_6);
505
	
506

    
507
tel
508

    
509

    
510

    
511

    
512

    
513
-- Exit action for state :A_A1
514
node A_A1_ex(idA_A1_1:int;
515
	idEvents1_A_1:int;
516
	isInner:bool)
517

    
518
returns (idA_A1:int;
519
	idEvents1_A:int);
520

    
521

    
522
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
523
	idEvents1_A_2:int;
524

    
525

    
526
let
527

    
528

    
529

    
530
	
531
	(idA_A1_2) 
532
	= 
533
	if ( idA_A1_1 = 724) then
534
	A1_A1a_ex(idA_A1_1, false)
535
	 else (idA_A1_1);
536

    
537
	
538

    
539
	(idA_A1_3) 
540
	= 
541
	if ( idA_A1_1 = 725) then
542
	A1_A1b_ex(idA_A1_1, false)
543
	 else (idA_A1_1);
544

    
545
	
546

    
547
	(idA_A1_4) 
548
	= 
549
		 if ( idA_A1_1 = 724) then 
550
		(idA_A1_2)
551
		 else
552
		 if ( idA_A1_1 = 725) then 
553
		(idA_A1_3)
554
		 else (idA_A1_1);
555

    
556

    
557
	-- set state as inactive 
558
	idEvents1_A_2
559
	 = if (not isInner) then 0 else idEvents1_A_1;
560

    
561
	idA_A1_5 
562
	= 0;
563
	
564

    
565
	(idA_A1, idEvents1_A) 
566
	= (idA_A1_5, idEvents1_A_1);
567
	
568

    
569
tel
570

    
571

    
572

    
573

    
574

    
575

    
576
-- Entry action for state :Events1_A
577
node Events1_A_en(idEvents1_A_1:int;
578
	idEvents1_Events1_1:int;
579
	a_1:int;
580
	idA_A1_1:int;
581
	idA_A2_1:int;
582
	isInner:bool)
583

    
584
returns (idEvents1_A:int;
585
	idEvents1_Events1:int;
586
	a:int;
587
	idA_A1:int;
588
	idA_A2:int);
589

    
590

    
591
var 	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5, idEvents1_A_6:int;
592
	idEvents1_Events1_2, idEvents1_Events1_3, idEvents1_Events1_4:int;
593
	a_2, a_3, a_4, a_5, a_6:int;
594
	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
595
	idA_A2_2, idA_A2_3:int;
596

    
597

    
598
let
599

    
600

    
601

    
602
	-- set state as active 
603
	idEvents1_Events1_2 
604
	= 719;
605
	
606

    
607
	
608
-- transition trace :
609
	--POINT__To__A_A1_1
610
		(idA_A1_2, idEvents1_A_2, a_2) 
611
	= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false);
612
		
613

    
614
	(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3) 
615
	= 
616

    
617
	if ( idEvents1_A_1 = 0) then
618

    
619
	 (idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2)
620

    
621
	 else(idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1);
622

    
623
	
624

    
625
	(idA_A2_2, idEvents1_A_4, a_4) 
626
	= 
627
	if ( idEvents1_A_1 = 720) then
628
	A_A2_en(idA_A2_1, idEvents1_A_1, a_1, false)
629
	 else (idA_A2_1, idEvents1_A_1, a_1);
630

    
631
	
632

    
633
	(idA_A1_4, idEvents1_A_5, a_5) 
634
	= 
635
	if ( idEvents1_A_1 = 723) then
636
	A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false)
637
	 else (idA_A1_1, idEvents1_A_1, a_1);
638

    
639
	
640

    
641
	(idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3) 
642
	= 
643
		 if ( idEvents1_A_1 = 0) then 
644
		(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_1)
645
		 else
646
		 if ( idEvents1_A_1 = 720) then 
647
		(idEvents1_A_4, idEvents1_Events1_3, a_4, idA_A1_1, idA_A2_2)
648
		 else
649
		 if ( idEvents1_A_1 = 723) then 
650
		(idEvents1_A_5, idEvents1_Events1_3, a_5, idA_A1_4, idA_A2_1)
651
		 else (idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1, idA_A2_1);
652

    
653

    
654
	(idEvents1_A, idEvents1_Events1, a, idA_A1, idA_A2) 
655
	= (idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3);
656
	
657

    
658
tel
659

    
660

    
661

    
662

    
663

    
664
-- Exit action for state :Events1_A
665
node Events1_A_ex(idA_A2_1:int;
666
	idEvents1_A_1:int;
667
	idA_A1_1:int;
668
	idEvents1_Events1_1:int;
669
	isInner:bool)
670

    
671
returns (idA_A2:int;
672
	idEvents1_A:int;
673
	idA_A1:int;
674
	idEvents1_Events1:int);
675

    
676

    
677
var 	idA_A2_2, idA_A2_3:int;
678
	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5:int;
679
	idA_A1_2, idA_A1_3:int;
680
	idEvents1_Events1_2:int;
681

    
682

    
683
let
684

    
685

    
686

    
687
	
688
	(idA_A2_2, idEvents1_A_2) 
689
	= 
690
	if ( idEvents1_A_1 = 720) then
691
	A_A2_ex(idA_A2_1, idEvents1_A_1, false)
692
	 else (idA_A2_1, idEvents1_A_1);
693

    
694
	
695

    
696
	(idA_A1_2, idEvents1_A_3) 
697
	= 
698
	if ( idEvents1_A_1 = 723) then
699
	A_A1_ex(idA_A1_1, idEvents1_A_1, false)
700
	 else (idA_A1_1, idEvents1_A_1);
701

    
702
	
703

    
704
	(idA_A2_3, idEvents1_A_4, idA_A1_3) 
705
	= 
706
		 if ( idEvents1_A_1 = 720) then 
707
		(idA_A2_2, idEvents1_A_2, idA_A1_1)
708
		 else
709
		 if ( idEvents1_A_1 = 723) then 
710
		(idA_A2_1, idEvents1_A_3, idA_A1_2)
711
		 else (idA_A2_1, idEvents1_A_1, idA_A1_1);
712

    
713

    
714
	-- set state as inactive 
715
	idEvents1_Events1_2
716
	 = if (not isInner) then 0 else idEvents1_Events1_1;
717

    
718
	idEvents1_A_5 
719
	= 0;
720
	
721

    
722
	(idA_A2, idEvents1_A, idA_A1, idEvents1_Events1) 
723
	= (idA_A2_3, idEvents1_A_5, idA_A1_3, idEvents1_Events1_1);
724
	
725

    
726
tel
727

    
728

    
729
--***************************************************State :A_A2 Automaton***************************************************
730

    
731
node A_A2_node(idA_A2_1:int;
732
	a_1:int;
733
	S:bool;
734
	R:bool)
735

    
736
returns (idA_A2:int;
737
	a:int);
738

    
739

    
740
let
741

    
742
	 automaton a_a2
743

    
744
	state POINTA_A2:
745
	unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1
746

    
747

    
748

    
749
	unless (idA_A2_1=721) and ( S ) restart A2_A2A__TO__A2_A2B_1
750

    
751

    
752

    
753
	unless (idA_A2_1=722) and ( R ) restart A2_A2B__TO__A2_A2A_1
754

    
755

    
756

    
757
	unless (idA_A2_1=721) restart A2_A2A_IDL
758

    
759
	unless (idA_A2_1=722) restart A2_A2B_IDL
760

    
761
	let
762

    
763
		(idA_A2, a) 
764
	= (idA_A2_1, a_1);
765
	
766

    
767
	tel
768

    
769

    
770

    
771
	state POINT__TO__A2_A2A_1:
772

    
773
	 var 	idA_A2_2:int;
774
	a_2:int;
775
	let
776

    
777
		-- transition trace :
778
	--POINT__To__A2_A2a_1
779
		(idA_A2_2, a_2) 
780
	= A2_A2a_en(idA_A2_1, a_1, false);
781
		
782

    
783
	(idA_A2, a) 
784
	=  (idA_A2_2, a_2);
785

    
786

    
787
	tel
788

    
789
	until true restart POINTA_A2
790

    
791

    
792

    
793
	state A2_A2A__TO__A2_A2B_1:
794

    
795
	 var 	idA_A2_2, idA_A2_3:int;
796
	a_2:int;
797
	let
798

    
799
		-- transition trace :
800
	--A2_A2a__To__A2_A2b_1
801
		(idA_A2_2) 
802
	= A2_A2a_ex(idA_A2_1, false);
803
		
804

    
805
		(idA_A2_3, a_2) 
806
	= A2_A2b_en(idA_A2_2, a_1, false);
807
		
808

    
809
	(idA_A2, a) 
810
	=  (idA_A2_3, a_2);
811

    
812

    
813
	tel
814

    
815
	until true restart POINTA_A2
816

    
817

    
818

    
819
	state A2_A2B__TO__A2_A2A_1:
820

    
821
	 var 	idA_A2_2, idA_A2_3:int;
822
	a_2:int;
823
	let
824

    
825
		-- transition trace :
826
	--A2_A2b__To__A2_A2a_1
827
		(idA_A2_2) 
828
	= A2_A2b_ex(idA_A2_1, false);
829
		
830

    
831
		(idA_A2_3, a_2) 
832
	= A2_A2a_en(idA_A2_2, a_1, false);
833
		
834

    
835
	(idA_A2, a) 
836
	=  (idA_A2_3, a_2);
837

    
838

    
839
	tel
840

    
841
	until true restart POINTA_A2
842

    
843

    
844

    
845
	state A2_A2A_IDL:
846

    
847
	 	let
848

    
849
		
850

    
851
	(idA_A2, a) 
852
	= (idA_A2_1, a_1);
853
	
854

    
855
	tel
856

    
857
	until true restart POINTA_A2
858

    
859

    
860

    
861
	state A2_A2B_IDL:
862

    
863
	 	let
864

    
865
		
866

    
867
	(idA_A2, a) 
868
	= (idA_A2_1, a_1);
869
	
870

    
871
	tel
872

    
873
	until true restart POINTA_A2
874

    
875

    
876

    
877
tel
878

    
879

    
880
--***************************************************State :A_A1 Automaton***************************************************
881

    
882
node A_A1_node(idA_A1_1:int;
883
	a_1:int;
884
	S:bool;
885
	R:bool)
886

    
887
returns (idA_A1:int;
888
	a:int);
889

    
890

    
891
let
892

    
893
	 automaton a_a1
894

    
895
	state POINTA_A1:
896
	unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1
897

    
898

    
899

    
900
	unless (idA_A1_1=724) and ( S ) restart A1_A1A__TO__A1_A1B_1
901

    
902

    
903

    
904
	unless (idA_A1_1=725) and ( R ) restart A1_A1B__TO__A1_A1A_1
905

    
906

    
907

    
908
	unless (idA_A1_1=724) restart A1_A1A_IDL
909

    
910
	unless (idA_A1_1=725) restart A1_A1B_IDL
911

    
912
	let
913

    
914
		(idA_A1, a) 
915
	= (idA_A1_1, a_1);
916
	
917

    
918
	tel
919

    
920

    
921

    
922
	state POINT__TO__A1_A1A_1:
923

    
924
	 var 	idA_A1_2:int;
925
	a_2:int;
926
	let
927

    
928
		-- transition trace :
929
	--POINT__To__A1_A1a_1
930
		(idA_A1_2, a_2) 
931
	= A1_A1a_en(idA_A1_1, a_1, false);
932
		
933

    
934
	(idA_A1, a) 
935
	=  (idA_A1_2, a_2);
936

    
937

    
938
	tel
939

    
940
	until true restart POINTA_A1
941

    
942

    
943

    
944
	state A1_A1A__TO__A1_A1B_1:
945

    
946
	 var 	idA_A1_2, idA_A1_3:int;
947
	a_2:int;
948
	let
949

    
950
		-- transition trace :
951
	--A1_A1a__To__A1_A1b_1
952
		(idA_A1_2) 
953
	= A1_A1a_ex(idA_A1_1, false);
954
		
955

    
956
		(idA_A1_3, a_2) 
957
	= A1_A1b_en(idA_A1_2, a_1, false);
958
		
959

    
960
	(idA_A1, a) 
961
	=  (idA_A1_3, a_2);
962

    
963

    
964
	tel
965

    
966
	until true restart POINTA_A1
967

    
968

    
969

    
970
	state A1_A1B__TO__A1_A1A_1:
971

    
972
	 var 	idA_A1_2, idA_A1_3:int;
973
	a_2:int;
974
	let
975

    
976
		-- transition trace :
977
	--A1_A1b__To__A1_A1a_1
978
		(idA_A1_2) 
979
	= A1_A1b_ex(idA_A1_1, false);
980
		
981

    
982
		(idA_A1_3, a_2) 
983
	= A1_A1a_en(idA_A1_2, a_1, false);
984
		
985

    
986
	(idA_A1, a) 
987
	=  (idA_A1_3, a_2);
988

    
989

    
990
	tel
991

    
992
	until true restart POINTA_A1
993

    
994

    
995

    
996
	state A1_A1A_IDL:
997

    
998
	 	let
999

    
1000
		
1001

    
1002
	(idA_A1, a) 
1003
	= (idA_A1_1, a_1);
1004
	
1005

    
1006
	tel
1007

    
1008
	until true restart POINTA_A1
1009

    
1010

    
1011

    
1012
	state A1_A1B_IDL:
1013

    
1014
	 	let
1015

    
1016
		
1017

    
1018
	(idA_A1, a) 
1019
	= (idA_A1_1, a_1);
1020
	
1021

    
1022
	tel
1023

    
1024
	until true restart POINTA_A1
1025

    
1026

    
1027

    
1028
tel
1029

    
1030

    
1031
--***************************************************State :Events1_A Automaton***************************************************
1032

    
1033
node Events1_A_node(idEvents1_A_1:int;
1034
	a_1:int;
1035
	idA_A1_1:int;
1036
	T:bool;
1037
	idA_A2_1:int;
1038
	R:bool;
1039
	S:bool)
1040

    
1041
returns (idEvents1_A:int;
1042
	a:int;
1043
	idA_A1:int;
1044
	idA_A2:int);
1045

    
1046

    
1047
let
1048

    
1049
	 automaton events1_a
1050

    
1051
	state POINTEvents1_A:
1052
	unless (idEvents1_A_1=0) restart POINT__TO__A_A1_1
1053

    
1054

    
1055

    
1056
	unless (idEvents1_A_1=720) and ( T ) restart A_A2__TO__A_A1_1
1057

    
1058

    
1059

    
1060
	unless (idEvents1_A_1=723) and ( T ) restart A_A1__TO__A_A2_1
1061

    
1062

    
1063

    
1064
	unless (idEvents1_A_1=720) restart A_A2_IDL
1065

    
1066
	unless (idEvents1_A_1=723) restart A_A1_IDL
1067

    
1068
	let
1069

    
1070
		(idEvents1_A, a, idA_A1, idA_A2) 
1071
	= (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1);
1072
	
1073

    
1074
	tel
1075

    
1076

    
1077

    
1078
	state POINT__TO__A_A1_1:
1079

    
1080
	 var 	idEvents1_A_2:int;
1081
	a_2:int;
1082
	idA_A1_2:int;
1083
	let
1084

    
1085
		-- transition trace :
1086
	--POINT__To__A_A1_1
1087
		(idA_A1_2, idEvents1_A_2, a_2) 
1088
	= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false);
1089
		
1090

    
1091
	(idEvents1_A, a, idA_A1) 
1092
	=  (idEvents1_A_2, a_2, idA_A1_2);
1093

    
1094
	--add unused variables
1095
	(idA_A2) 
1096
	= (idA_A2_1);
1097
	
1098

    
1099
	tel
1100

    
1101
	until true restart POINTEvents1_A
1102

    
1103

    
1104

    
1105
	state A_A2__TO__A_A1_1:
1106

    
1107
	 var 	idEvents1_A_2, idEvents1_A_3:int;
1108
	a_2:int;
1109
	idA_A1_2:int;
1110
	idA_A2_2:int;
1111
	let
1112

    
1113
		-- transition trace :
1114
	--A_A2__To__A_A1_1
1115
		(idA_A2_2, idEvents1_A_2) 
1116
	= A_A2_ex(idA_A2_1, idEvents1_A_1, false);
1117
		
1118

    
1119
		(idA_A1_2, idEvents1_A_3, a_2) 
1120
	= A_A1_en(idA_A1_1, idEvents1_A_2, a_1, false);
1121
		
1122

    
1123
	(idEvents1_A, a, idA_A1, idA_A2) 
1124
	=  (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2);
1125

    
1126

    
1127
	tel
1128

    
1129
	until true restart POINTEvents1_A
1130

    
1131

    
1132

    
1133
	state A_A1__TO__A_A2_1:
1134

    
1135
	 var 	idEvents1_A_2, idEvents1_A_3:int;
1136
	a_2:int;
1137
	idA_A1_2:int;
1138
	idA_A2_2:int;
1139
	let
1140

    
1141
		-- transition trace :
1142
	--A_A1__To__A_A2_1
1143
		(idA_A1_2, idEvents1_A_2) 
1144
	= A_A1_ex(idA_A1_1, idEvents1_A_1, false);
1145
		
1146

    
1147
		(idA_A2_2, idEvents1_A_3, a_2) 
1148
	= A_A2_en(idA_A2_1, idEvents1_A_2, a_1, false);
1149
		
1150

    
1151
	(idEvents1_A, a, idA_A1, idA_A2) 
1152
	=  (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2);
1153

    
1154

    
1155
	tel
1156

    
1157
	until true restart POINTEvents1_A
1158

    
1159

    
1160

    
1161
	state A_A2_IDL:
1162

    
1163
	 var 	a_2:int;
1164
	idA_A2_2:int;
1165
	let
1166

    
1167
		
1168
	(idA_A2_2, a_2) 
1169
	= A_A2_node(idA_A2_1, a_1, S, R);
1170

    
1171
		
1172

    
1173

    
1174
	(idEvents1_A, a, idA_A1, idA_A2) 
1175
	= (idEvents1_A_1, a_2, idA_A1_1, idA_A2_2);
1176
	
1177

    
1178
	tel
1179

    
1180
	until true restart POINTEvents1_A
1181

    
1182

    
1183

    
1184
	state A_A1_IDL:
1185

    
1186
	 var 	a_2:int;
1187
	idA_A1_2:int;
1188
	let
1189

    
1190
		
1191
	(idA_A1_2, a_2) 
1192
	= A_A1_node(idA_A1_1, a_1, S, R);
1193

    
1194
		
1195

    
1196

    
1197
	(idEvents1_A, a, idA_A1, idA_A2) 
1198
	= (idEvents1_A_1, a_2, idA_A1_2, idA_A2_1);
1199
	
1200

    
1201
	tel
1202

    
1203
	until true restart POINTEvents1_A
1204

    
1205

    
1206

    
1207
tel
1208

    
1209

    
1210
--***************************************************State :Events1_Events1 Automaton***************************************************
1211

    
1212
node Events1_Events1_node(idEvents1_Events1_1:int;
1213
	a_1:int;
1214
	idA_A1_1:int;
1215
	idA_A2_1:int;
1216
	idEvents1_A_1:int;
1217
	R:bool;
1218
	S:bool;
1219
	T:bool)
1220

    
1221
returns (idEvents1_Events1:int;
1222
	a:int;
1223
	idA_A1:int;
1224
	idA_A2:int;
1225
	idEvents1_A:int);
1226

    
1227

    
1228
let
1229

    
1230
	 automaton events1_events1
1231

    
1232
	state POINTEvents1_Events1:
1233
	unless (idEvents1_Events1_1=0) restart POINT__TO__EVENTS1_A_1
1234

    
1235

    
1236

    
1237
	unless true  restart EVENTS1_EVENTS1_PARALLEL_IDL
1238

    
1239
	let
1240

    
1241
		(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A) 
1242
	= (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1);
1243
	
1244

    
1245
	tel
1246

    
1247

    
1248

    
1249
	state POINT__TO__EVENTS1_A_1:
1250

    
1251
	 var 	idEvents1_Events1_2:int;
1252
	a_2:int;
1253
	idA_A1_2:int;
1254
	idA_A2_2:int;
1255
	idEvents1_A_2:int;
1256
	let
1257

    
1258
		-- transition trace :
1259
	--POINT__To__Events1_A_1
1260
		(idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2) 
1261
	= Events1_A_en(idEvents1_A_1, idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, false);
1262
		
1263

    
1264
	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A) 
1265
	=  (idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2);
1266

    
1267

    
1268
	tel
1269

    
1270
	until true restart POINTEvents1_Events1
1271

    
1272

    
1273

    
1274
	state EVENTS1_EVENTS1_PARALLEL_IDL:
1275

    
1276
	 var 	a_2:int;
1277
	idA_A1_2:int;
1278
	idA_A2_2:int;
1279
	idEvents1_A_2:int;
1280
	let
1281

    
1282
		
1283

    
1284
		(idEvents1_A_2, a_2, idA_A1_2, idA_A2_2)
1285
	= if not (idEvents1_A_1= 0 ) then Events1_A_node(idEvents1_A_1, a_1, idA_A1_1, T, idA_A2_1, R, S)
1286

    
1287
		 else (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1);
1288

    
1289
		
1290

    
1291
		
1292

    
1293
	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A) 
1294
	= (idEvents1_Events1_1, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2);
1295
	
1296

    
1297
	tel
1298

    
1299
	until true restart POINTEvents1_Events1
1300

    
1301

    
1302

    
1303
tel
1304

    
1305

    
1306
--***************************************************State :Events1_Events1 Automaton***************************************************
1307

    
1308
node EventsOrderV2_Events1(R:bool;
1309
	S:bool;
1310
	T:bool)
1311

    
1312
returns (a:int);
1313

    
1314

    
1315
var a_1: int;
1316

    
1317
	idEvents1_Events1, idEvents1_Events1_1: int;
1318

    
1319
	idA_A2, idA_A2_1: int;
1320

    
1321
	idA_A1, idA_A1_1: int;
1322

    
1323
	idEvents1_A, idEvents1_A_1: int;
1324

    
1325
	let
1326

    
1327
	a_1 = 0 -> pre a;
1328

    
1329
	idEvents1_Events1_1 = 0 -> pre idEvents1_Events1;
1330

    
1331
	idA_A2_1 = 0 -> pre idA_A2;
1332

    
1333
	idA_A1_1 = 0 -> pre idA_A1;
1334

    
1335
	idEvents1_A_1 = 0 -> pre idEvents1_A;
1336

    
1337
	
1338

    
1339

    
1340

    
1341
	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A)
1342
	 = Events1_Events1_node(idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, R, S, T);
1343

    
1344

    
1345
--unused outputs
1346
	
1347

    
1348
tel
1349

    
1350

    
1351

    
1352
node EventsOrderV2 (R_1_1 : bool; S_1_1 : bool; T_1_1 : bool)
1353
returns (a_1_1 : int); 
1354
var
1355
	Events1_1_1 : int;
1356
	i_virtual_local : real;
1357
let 
1358
	Events1_1_1 =  EventsOrderV2_Events1(R_1_1, S_1_1, T_1_1);
1359
	a_1_1 = Events1_1_1;
1360
	i_virtual_local= 0.0 -> 1.0;
1361
tel
1362