Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Events1 / Events1.lus @ eb639349

History | View | Annotate | Download (42.6 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9

    
10

    
11

    
12
node B_B1__To__B_B2_1_Transition_Action(c_1:int)
13

    
14
returns (c:int);
15

    
16

    
17
var 	c_2:int;
18

    
19

    
20
let
21

    
22

    
23

    
24
	c_2 
25
	=  c_1  + 1;
26
	
27

    
28
	(c) 
29
	= (c_2);
30
	
31

    
32
tel
33

    
34

    
35

    
36

    
37

    
38

    
39
node B_B2__To__B_B1_1_Transition_Action(c_1:int)
40

    
41
returns (c:int);
42

    
43

    
44
var 	c_2:int;
45

    
46

    
47
let
48

    
49

    
50

    
51
	c_2 
52
	=  c_1  + 1;
53
	
54

    
55
	(c) 
56
	= (c_2);
57
	
58

    
59
tel
60

    
61

    
62

    
63

    
64

    
65

    
66

    
67

    
68

    
69

    
70

    
71

    
72

    
73
-- Entry action for state :B2_B2a
74
node B2_B2a_en(idB_B2_1:int;
75
	x:int;
76
	b_1:int;
77
	isInner:bool)
78

    
79
returns (idB_B2:int;
80
	b:int);
81

    
82

    
83
var 	idB_B2_2:int;
84
	b_2:int;
85

    
86

    
87
let
88

    
89

    
90

    
91
	-- set state as active 
92
	idB_B2_2 
93
	= 574;
94
	
95

    
96
	b_2 
97
	= if (not isInner) then x+7
98
	 else b_1;
99
	
100

    
101
	(idB_B2, b) 
102
	= (idB_B2_2, b_2);
103
	
104

    
105
tel
106

    
107

    
108

    
109

    
110

    
111
-- Exit action for state :B2_B2a
112
node B2_B2a_ex(idB_B2_1:int;
113
	isInner:bool)
114

    
115
returns (idB_B2:int);
116

    
117

    
118
var 	idB_B2_2:int;
119

    
120

    
121
let
122

    
123

    
124

    
125
	-- set state as inactive 
126
	idB_B2_2
127
	 = if (not isInner) then 0 else idB_B2_1;
128

    
129

    
130
	(idB_B2) 
131
	= (idB_B2_1);
132
	
133

    
134
tel
135

    
136

    
137

    
138

    
139

    
140

    
141
-- Entry action for state :B2_B2b
142
node B2_B2b_en(idB_B2_1:int;
143
	x:int;
144
	b_1:int;
145
	isInner:bool)
146

    
147
returns (idB_B2:int;
148
	b:int);
149

    
150

    
151
var 	idB_B2_2:int;
152
	b_2:int;
153

    
154

    
155
let
156

    
157

    
158

    
159
	-- set state as active 
160
	idB_B2_2 
161
	= 575;
162
	
163

    
164
	b_2 
165
	= if (not isInner) then x+8
166
	 else b_1;
167
	
168

    
169
	(idB_B2, b) 
170
	= (idB_B2_2, b_2);
171
	
172

    
173
tel
174

    
175

    
176

    
177

    
178

    
179
-- Exit action for state :B2_B2b
180
node B2_B2b_ex(idB_B2_1:int;
181
	isInner:bool)
182

    
183
returns (idB_B2:int);
184

    
185

    
186
var 	idB_B2_2:int;
187

    
188

    
189
let
190

    
191

    
192

    
193
	-- set state as inactive 
194
	idB_B2_2
195
	 = if (not isInner) then 0 else idB_B2_1;
196

    
197

    
198
	(idB_B2) 
199
	= (idB_B2_1);
200
	
201

    
202
tel
203

    
204

    
205

    
206

    
207

    
208

    
209
-- Entry action for state :B_B2
210
node B_B2_en(idB_B2_1:int;
211
	idEvents1_B_1:int;
212
	b_1:int;
213
	x:int;
214
	isInner:bool)
215

    
216
returns (idB_B2:int;
217
	idEvents1_B:int;
218
	b:int);
219

    
220

    
221
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5, idB_B2_6:int;
222
	idEvents1_B_2, idEvents1_B_3, idEvents1_B_4:int;
223
	b_2, b_3, b_4, b_5, b_6:int;
224

    
225

    
226
let
227

    
228

    
229

    
230
	-- set state as active 
231
	idEvents1_B_2 
232
	= 573;
233
	
234

    
235
	
236
-- transition trace :
237
	--POINT__To__B2_B2a_1
238
		(idB_B2_2, b_2) 
239
	= B2_B2a_en(idB_B2_1, x, b_1, false);
240
		
241

    
242
	(idB_B2_3, idEvents1_B_3, b_3) 
243
	= 
244

    
245
	if ( idB_B2_1 = 0) then
246

    
247
	 (idB_B2_2, idEvents1_B_2, b_2)
248

    
249
	 else(idB_B2_1, idEvents1_B_2, b_1);
250

    
251
	
252

    
253
	(idB_B2_4, b_4) 
254
	= 
255
	if ( idB_B2_1 = 574) then
256
	B2_B2a_en(idB_B2_1, x, b_1, false)
257
	 else (idB_B2_1, b_1);
258

    
259
	
260

    
261
	(idB_B2_5, b_5) 
262
	= 
263
	if ( idB_B2_1 = 575) then
264
	B2_B2b_en(idB_B2_1, x, b_1, false)
265
	 else (idB_B2_1, b_1);
266

    
267
	
268

    
269
	(idB_B2_6, idEvents1_B_4, b_6) 
270
	= 
271
		 if ( idB_B2_1 = 0) then 
272
		(idB_B2_3, idEvents1_B_3, b_3)
273
		 else
274
		 if ( idB_B2_1 = 574) then 
275
		(idB_B2_4, idEvents1_B_3, b_4)
276
		 else
277
		 if ( idB_B2_1 = 575) then 
278
		(idB_B2_5, idEvents1_B_3, b_5)
279
		 else (idB_B2_1, idEvents1_B_2, b_1);
280

    
281

    
282
	(idB_B2, idEvents1_B, b) 
283
	= (idB_B2_6, idEvents1_B_4, b_6);
284
	
285

    
286
tel
287

    
288

    
289

    
290

    
291

    
292
-- Exit action for state :B_B2
293
node B_B2_ex(idB_B2_1:int;
294
	idEvents1_B_1:int;
295
	isInner:bool)
296

    
297
returns (idB_B2:int;
298
	idEvents1_B:int);
299

    
300

    
301
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5:int;
302
	idEvents1_B_2:int;
303

    
304

    
305
let
306

    
307

    
308

    
309
	
310
	(idB_B2_2) 
311
	= 
312
	if ( idB_B2_1 = 574) then
313
	B2_B2a_ex(idB_B2_1, false)
314
	 else (idB_B2_1);
315

    
316
	
317

    
318
	(idB_B2_3) 
319
	= 
320
	if ( idB_B2_1 = 575) then
321
	B2_B2b_ex(idB_B2_1, false)
322
	 else (idB_B2_1);
323

    
324
	
325

    
326
	(idB_B2_4) 
327
	= 
328
		 if ( idB_B2_1 = 574) then 
329
		(idB_B2_2)
330
		 else
331
		 if ( idB_B2_1 = 575) then 
332
		(idB_B2_3)
333
		 else (idB_B2_1);
334

    
335

    
336
	-- set state as inactive 
337
	idEvents1_B_2
338
	 = if (not isInner) then 0 else idEvents1_B_1;
339

    
340
	idB_B2_5 
341
	= 0;
342
	
343

    
344
	(idB_B2, idEvents1_B) 
345
	= (idB_B2_5, idEvents1_B_1);
346
	
347

    
348
tel
349

    
350

    
351

    
352

    
353

    
354

    
355
-- Entry action for state :B1_B1a
356
node B1_B1a_en(idB_B1_1:int;
357
	x:int;
358
	b_1:int;
359
	isInner:bool)
360

    
361
returns (idB_B1:int;
362
	b:int);
363

    
364

    
365
var 	idB_B1_2:int;
366
	b_2:int;
367

    
368

    
369
let
370

    
371

    
372

    
373
	-- set state as active 
374
	idB_B1_2 
375
	= 577;
376
	
377

    
378
	b_2 
379
	= if (not isInner) then x+5
380
	 else b_1;
381
	
382

    
383
	(idB_B1, b) 
384
	= (idB_B1_2, b_2);
385
	
386

    
387
tel
388

    
389

    
390

    
391

    
392

    
393
-- Exit action for state :B1_B1a
394
node B1_B1a_ex(idB_B1_1:int;
395
	isInner:bool)
396

    
397
returns (idB_B1:int);
398

    
399

    
400
var 	idB_B1_2:int;
401

    
402

    
403
let
404

    
405

    
406

    
407
	-- set state as inactive 
408
	idB_B1_2
409
	 = if (not isInner) then 0 else idB_B1_1;
410

    
411

    
412
	(idB_B1) 
413
	= (idB_B1_1);
414
	
415

    
416
tel
417

    
418

    
419

    
420

    
421

    
422

    
423
-- Entry action for state :B1_B1b
424
node B1_B1b_en(idB_B1_1:int;
425
	x:int;
426
	b_1:int;
427
	isInner:bool)
428

    
429
returns (idB_B1:int;
430
	b:int);
431

    
432

    
433
var 	idB_B1_2:int;
434
	b_2:int;
435

    
436

    
437
let
438

    
439

    
440

    
441
	-- set state as active 
442
	idB_B1_2 
443
	= 578;
444
	
445

    
446
	b_2 
447
	= if (not isInner) then x+6
448
	 else b_1;
449
	
450

    
451
	(idB_B1, b) 
452
	= (idB_B1_2, b_2);
453
	
454

    
455
tel
456

    
457

    
458

    
459

    
460

    
461
-- Exit action for state :B1_B1b
462
node B1_B1b_ex(idB_B1_1:int;
463
	isInner:bool)
464

    
465
returns (idB_B1:int);
466

    
467

    
468
var 	idB_B1_2:int;
469

    
470

    
471
let
472

    
473

    
474

    
475
	-- set state as inactive 
476
	idB_B1_2
477
	 = if (not isInner) then 0 else idB_B1_1;
478

    
479

    
480
	(idB_B1) 
481
	= (idB_B1_1);
482
	
483

    
484
tel
485

    
486

    
487

    
488

    
489

    
490

    
491
-- Entry action for state :B_B1
492
node B_B1_en(idB_B1_1:int;
493
	idEvents1_B_1:int;
494
	b_1:int;
495
	x:int;
496
	isInner:bool)
497

    
498
returns (idB_B1:int;
499
	idEvents1_B:int;
500
	b:int);
501

    
502

    
503
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5, idB_B1_6:int;
504
	idEvents1_B_2, idEvents1_B_3, idEvents1_B_4:int;
505
	b_2, b_3, b_4, b_5, b_6:int;
506

    
507

    
508
let
509

    
510

    
511

    
512
	-- set state as active 
513
	idEvents1_B_2 
514
	= 576;
515
	
516

    
517
	
518
-- transition trace :
519
	--POINT__To__B1_B1a_1
520
		(idB_B1_2, b_2) 
521
	= B1_B1a_en(idB_B1_1, x, b_1, false);
522
		
523

    
524
	(idB_B1_3, idEvents1_B_3, b_3) 
525
	= 
526

    
527
	if ( idB_B1_1 = 0) then
528

    
529
	 (idB_B1_2, idEvents1_B_2, b_2)
530

    
531
	 else(idB_B1_1, idEvents1_B_2, b_1);
532

    
533
	
534

    
535
	(idB_B1_4, b_4) 
536
	= 
537
	if ( idB_B1_1 = 577) then
538
	B1_B1a_en(idB_B1_1, x, b_1, false)
539
	 else (idB_B1_1, b_1);
540

    
541
	
542

    
543
	(idB_B1_5, b_5) 
544
	= 
545
	if ( idB_B1_1 = 578) then
546
	B1_B1b_en(idB_B1_1, x, b_1, false)
547
	 else (idB_B1_1, b_1);
548

    
549
	
550

    
551
	(idB_B1_6, idEvents1_B_4, b_6) 
552
	= 
553
		 if ( idB_B1_1 = 0) then 
554
		(idB_B1_3, idEvents1_B_3, b_3)
555
		 else
556
		 if ( idB_B1_1 = 577) then 
557
		(idB_B1_4, idEvents1_B_3, b_4)
558
		 else
559
		 if ( idB_B1_1 = 578) then 
560
		(idB_B1_5, idEvents1_B_3, b_5)
561
		 else (idB_B1_1, idEvents1_B_2, b_1);
562

    
563

    
564
	(idB_B1, idEvents1_B, b) 
565
	= (idB_B1_6, idEvents1_B_4, b_6);
566
	
567

    
568
tel
569

    
570

    
571

    
572

    
573

    
574
-- Exit action for state :B_B1
575
node B_B1_ex(idB_B1_1:int;
576
	idEvents1_B_1:int;
577
	isInner:bool)
578

    
579
returns (idB_B1:int;
580
	idEvents1_B:int);
581

    
582

    
583
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
584
	idEvents1_B_2:int;
585

    
586

    
587
let
588

    
589

    
590

    
591
	
592
	(idB_B1_2) 
593
	= 
594
	if ( idB_B1_1 = 577) then
595
	B1_B1a_ex(idB_B1_1, false)
596
	 else (idB_B1_1);
597

    
598
	
599

    
600
	(idB_B1_3) 
601
	= 
602
	if ( idB_B1_1 = 578) then
603
	B1_B1b_ex(idB_B1_1, false)
604
	 else (idB_B1_1);
605

    
606
	
607

    
608
	(idB_B1_4) 
609
	= 
610
		 if ( idB_B1_1 = 577) then 
611
		(idB_B1_2)
612
		 else
613
		 if ( idB_B1_1 = 578) then 
614
		(idB_B1_3)
615
		 else (idB_B1_1);
616

    
617

    
618
	-- set state as inactive 
619
	idEvents1_B_2
620
	 = if (not isInner) then 0 else idEvents1_B_1;
621

    
622
	idB_B1_5 
623
	= 0;
624
	
625

    
626
	(idB_B1, idEvents1_B) 
627
	= (idB_B1_5, idEvents1_B_1);
628
	
629

    
630
tel
631

    
632

    
633

    
634

    
635

    
636

    
637
-- Entry action for state :Events1_B
638
node Events1_B_en(idEvents1_B_1:int;
639
	idEvents1_Events1_1:int;
640
	b_1:int;
641
	idB_B1_1:int;
642
	x:int;
643
	idB_B2_1:int;
644
	isInner:bool)
645

    
646
returns (idEvents1_B:int;
647
	idEvents1_Events1:int;
648
	b:int;
649
	idB_B1:int;
650
	idB_B2:int);
651

    
652

    
653
var 	idEvents1_B_2, idEvents1_B_3, idEvents1_B_4, idEvents1_B_5, idEvents1_B_6:int;
654
	idEvents1_Events1_2, idEvents1_Events1_3, idEvents1_Events1_4:int;
655
	b_2, b_3, b_4, b_5, b_6:int;
656
	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
657
	idB_B2_2, idB_B2_3:int;
658

    
659

    
660
let
661

    
662

    
663

    
664
	-- set state as active 
665
	idEvents1_Events1_2 
666
	= 572;
667
	
668

    
669
	
670
-- transition trace :
671
	--POINT__To__B_B1_1
672
		(idB_B1_2, idEvents1_B_2, b_2) 
673
	= B_B1_en(idB_B1_1, idEvents1_B_1, b_1, x, false);
674
		
675

    
676
	(idEvents1_B_3, idEvents1_Events1_3, b_3, idB_B1_3) 
677
	= 
678

    
679
	if ( idEvents1_B_1 = 0) then
680

    
681
	 (idEvents1_B_2, idEvents1_Events1_2, b_2, idB_B1_2)
682

    
683
	 else(idEvents1_B_1, idEvents1_Events1_2, b_1, idB_B1_1);
684

    
685
	
686

    
687
	(idB_B2_2, idEvents1_B_4, b_4) 
688
	= 
689
	if ( idEvents1_B_1 = 573) then
690
	B_B2_en(idB_B2_1, idEvents1_B_1, b_1, x, false)
691
	 else (idB_B2_1, idEvents1_B_1, b_1);
692

    
693
	
694

    
695
	(idB_B1_4, idEvents1_B_5, b_5) 
696
	= 
697
	if ( idEvents1_B_1 = 576) then
698
	B_B1_en(idB_B1_1, idEvents1_B_1, b_1, x, false)
699
	 else (idB_B1_1, idEvents1_B_1, b_1);
700

    
701
	
702

    
703
	(idEvents1_B_6, idEvents1_Events1_4, b_6, idB_B1_5, idB_B2_3) 
704
	= 
705
		 if ( idEvents1_B_1 = 0) then 
706
		(idEvents1_B_3, idEvents1_Events1_3, b_3, idB_B1_3, idB_B2_1)
707
		 else
708
		 if ( idEvents1_B_1 = 573) then 
709
		(idEvents1_B_4, idEvents1_Events1_3, b_4, idB_B1_1, idB_B2_2)
710
		 else
711
		 if ( idEvents1_B_1 = 576) then 
712
		(idEvents1_B_5, idEvents1_Events1_3, b_5, idB_B1_4, idB_B2_1)
713
		 else (idEvents1_B_1, idEvents1_Events1_2, b_1, idB_B1_1, idB_B2_1);
714

    
715

    
716
	(idEvents1_B, idEvents1_Events1, b, idB_B1, idB_B2) 
717
	= (idEvents1_B_6, idEvents1_Events1_4, b_6, idB_B1_5, idB_B2_3);
718
	
719

    
720
tel
721

    
722

    
723

    
724

    
725

    
726
-- Exit action for state :Events1_B
727
node Events1_B_ex(idB_B2_1:int;
728
	idEvents1_B_1:int;
729
	idB_B1_1:int;
730
	idEvents1_Events1_1:int;
731
	isInner:bool)
732

    
733
returns (idB_B2:int;
734
	idEvents1_B:int;
735
	idB_B1:int;
736
	idEvents1_Events1:int);
737

    
738

    
739
var 	idB_B2_2, idB_B2_3:int;
740
	idEvents1_B_2, idEvents1_B_3, idEvents1_B_4, idEvents1_B_5:int;
741
	idB_B1_2, idB_B1_3:int;
742
	idEvents1_Events1_2:int;
743

    
744

    
745
let
746

    
747

    
748

    
749
	
750
	(idB_B2_2, idEvents1_B_2) 
751
	= 
752
	if ( idEvents1_B_1 = 573) then
753
	B_B2_ex(idB_B2_1, idEvents1_B_1, false)
754
	 else (idB_B2_1, idEvents1_B_1);
755

    
756
	
757

    
758
	(idB_B1_2, idEvents1_B_3) 
759
	= 
760
	if ( idEvents1_B_1 = 576) then
761
	B_B1_ex(idB_B1_1, idEvents1_B_1, false)
762
	 else (idB_B1_1, idEvents1_B_1);
763

    
764
	
765

    
766
	(idB_B2_3, idEvents1_B_4, idB_B1_3) 
767
	= 
768
		 if ( idEvents1_B_1 = 573) then 
769
		(idB_B2_2, idEvents1_B_2, idB_B1_1)
770
		 else
771
		 if ( idEvents1_B_1 = 576) then 
772
		(idB_B2_1, idEvents1_B_3, idB_B1_2)
773
		 else (idB_B2_1, idEvents1_B_1, idB_B1_1);
774

    
775

    
776
	-- set state as inactive 
777
	idEvents1_Events1_2
778
	 = if (not isInner) then 0 else idEvents1_Events1_1;
779

    
780
	idEvents1_B_5 
781
	= 0;
782
	
783

    
784
	(idB_B2, idEvents1_B, idB_B1, idEvents1_Events1) 
785
	= (idB_B2_3, idEvents1_B_5, idB_B1_3, idEvents1_Events1_1);
786
	
787

    
788
tel
789

    
790

    
791

    
792

    
793

    
794

    
795
-- Entry action for state :A2_A2a
796
node A2_A2a_en(idA_A2_1:int;
797
	x:int;
798
	a_1:int;
799
	isInner:bool)
800

    
801
returns (idA_A2:int;
802
	a:int);
803

    
804

    
805
var 	idA_A2_2:int;
806
	a_2:int;
807

    
808

    
809
let
810

    
811

    
812

    
813
	-- set state as active 
814
	idA_A2_2 
815
	= 567;
816
	
817

    
818
	a_2 
819
	= if (not isInner) then x+3
820
	 else a_1;
821
	
822

    
823
	(idA_A2, a) 
824
	= (idA_A2_2, a_2);
825
	
826

    
827
tel
828

    
829

    
830

    
831

    
832

    
833
-- Exit action for state :A2_A2a
834
node A2_A2a_ex(idA_A2_1:int;
835
	isInner:bool)
836

    
837
returns (idA_A2:int);
838

    
839

    
840
var 	idA_A2_2:int;
841

    
842

    
843
let
844

    
845

    
846

    
847
	-- set state as inactive 
848
	idA_A2_2
849
	 = if (not isInner) then 0 else idA_A2_1;
850

    
851

    
852
	(idA_A2) 
853
	= (idA_A2_1);
854
	
855

    
856
tel
857

    
858

    
859

    
860

    
861

    
862

    
863
-- Entry action for state :A2_A2b
864
node A2_A2b_en(idA_A2_1:int;
865
	x:int;
866
	a_1:int;
867
	isInner:bool)
868

    
869
returns (idA_A2:int;
870
	a:int);
871

    
872

    
873
var 	idA_A2_2:int;
874
	a_2:int;
875

    
876

    
877
let
878

    
879

    
880

    
881
	-- set state as active 
882
	idA_A2_2 
883
	= 568;
884
	
885

    
886
	a_2 
887
	= if (not isInner) then x+4
888
	 else a_1;
889
	
890

    
891
	(idA_A2, a) 
892
	= (idA_A2_2, a_2);
893
	
894

    
895
tel
896

    
897

    
898

    
899

    
900

    
901
-- Exit action for state :A2_A2b
902
node A2_A2b_ex(idA_A2_1:int;
903
	isInner:bool)
904

    
905
returns (idA_A2:int);
906

    
907

    
908
var 	idA_A2_2:int;
909

    
910

    
911
let
912

    
913

    
914

    
915
	-- set state as inactive 
916
	idA_A2_2
917
	 = if (not isInner) then 0 else idA_A2_1;
918

    
919

    
920
	(idA_A2) 
921
	= (idA_A2_1);
922
	
923

    
924
tel
925

    
926

    
927

    
928

    
929

    
930

    
931
-- Entry action for state :A_A2
932
node A_A2_en(idA_A2_1:int;
933
	idEvents1_A_1:int;
934
	a_1:int;
935
	x:int;
936
	isInner:bool)
937

    
938
returns (idA_A2:int;
939
	idEvents1_A:int;
940
	a:int);
941

    
942

    
943
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int;
944
	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int;
945
	a_2, a_3, a_4, a_5, a_6:int;
946

    
947

    
948
let
949

    
950

    
951

    
952
	-- set state as active 
953
	idEvents1_A_2 
954
	= 566;
955
	
956

    
957
	
958
-- transition trace :
959
	--POINT__To__A2_A2a_1
960
		(idA_A2_2, a_2) 
961
	= A2_A2a_en(idA_A2_1, x, a_1, false);
962
		
963

    
964
	(idA_A2_3, idEvents1_A_3, a_3) 
965
	= 
966

    
967
	if ( idA_A2_1 = 0) then
968

    
969
	 (idA_A2_2, idEvents1_A_2, a_2)
970

    
971
	 else(idA_A2_1, idEvents1_A_2, a_1);
972

    
973
	
974

    
975
	(idA_A2_4, a_4) 
976
	= 
977
	if ( idA_A2_1 = 567) then
978
	A2_A2a_en(idA_A2_1, x, a_1, false)
979
	 else (idA_A2_1, a_1);
980

    
981
	
982

    
983
	(idA_A2_5, a_5) 
984
	= 
985
	if ( idA_A2_1 = 568) then
986
	A2_A2b_en(idA_A2_1, x, a_1, false)
987
	 else (idA_A2_1, a_1);
988

    
989
	
990

    
991
	(idA_A2_6, idEvents1_A_4, a_6) 
992
	= 
993
		 if ( idA_A2_1 = 0) then 
994
		(idA_A2_3, idEvents1_A_3, a_3)
995
		 else
996
		 if ( idA_A2_1 = 567) then 
997
		(idA_A2_4, idEvents1_A_3, a_4)
998
		 else
999
		 if ( idA_A2_1 = 568) then 
1000
		(idA_A2_5, idEvents1_A_3, a_5)
1001
		 else (idA_A2_1, idEvents1_A_2, a_1);
1002

    
1003

    
1004
	(idA_A2, idEvents1_A, a) 
1005
	= (idA_A2_6, idEvents1_A_4, a_6);
1006
	
1007

    
1008
tel
1009

    
1010

    
1011

    
1012

    
1013

    
1014
-- Exit action for state :A_A2
1015
node A_A2_ex(idA_A2_1:int;
1016
	idEvents1_A_1:int;
1017
	isInner:bool)
1018

    
1019
returns (idA_A2:int;
1020
	idEvents1_A:int);
1021

    
1022

    
1023
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int;
1024
	idEvents1_A_2:int;
1025

    
1026

    
1027
let
1028

    
1029

    
1030

    
1031
	
1032
	(idA_A2_2) 
1033
	= 
1034
	if ( idA_A2_1 = 567) then
1035
	A2_A2a_ex(idA_A2_1, false)
1036
	 else (idA_A2_1);
1037

    
1038
	
1039

    
1040
	(idA_A2_3) 
1041
	= 
1042
	if ( idA_A2_1 = 568) then
1043
	A2_A2b_ex(idA_A2_1, false)
1044
	 else (idA_A2_1);
1045

    
1046
	
1047

    
1048
	(idA_A2_4) 
1049
	= 
1050
		 if ( idA_A2_1 = 567) then 
1051
		(idA_A2_2)
1052
		 else
1053
		 if ( idA_A2_1 = 568) then 
1054
		(idA_A2_3)
1055
		 else (idA_A2_1);
1056

    
1057

    
1058
	-- set state as inactive 
1059
	idEvents1_A_2
1060
	 = if (not isInner) then 0 else idEvents1_A_1;
1061

    
1062
	idA_A2_5 
1063
	= 0;
1064
	
1065

    
1066
	(idA_A2, idEvents1_A) 
1067
	= (idA_A2_5, idEvents1_A_1);
1068
	
1069

    
1070
tel
1071

    
1072

    
1073

    
1074

    
1075

    
1076

    
1077
-- Entry action for state :A1_A1a
1078
node A1_A1a_en(idA_A1_1:int;
1079
	x:int;
1080
	a_1:int;
1081
	isInner:bool)
1082

    
1083
returns (idA_A1:int;
1084
	a:int);
1085

    
1086

    
1087
var 	idA_A1_2:int;
1088
	a_2:int;
1089

    
1090

    
1091
let
1092

    
1093

    
1094

    
1095
	-- set state as active 
1096
	idA_A1_2 
1097
	= 570;
1098
	
1099

    
1100
	a_2 
1101
	= if (not isInner) then x+1
1102
	 else a_1;
1103
	
1104

    
1105
	(idA_A1, a) 
1106
	= (idA_A1_2, a_2);
1107
	
1108

    
1109
tel
1110

    
1111

    
1112

    
1113

    
1114

    
1115
-- Exit action for state :A1_A1a
1116
node A1_A1a_ex(idA_A1_1:int;
1117
	isInner:bool)
1118

    
1119
returns (idA_A1:int);
1120

    
1121

    
1122
var 	idA_A1_2:int;
1123

    
1124

    
1125
let
1126

    
1127

    
1128

    
1129
	-- set state as inactive 
1130
	idA_A1_2
1131
	 = if (not isInner) then 0 else idA_A1_1;
1132

    
1133

    
1134
	(idA_A1) 
1135
	= (idA_A1_1);
1136
	
1137

    
1138
tel
1139

    
1140

    
1141

    
1142

    
1143

    
1144

    
1145
-- Entry action for state :A1_A1b
1146
node A1_A1b_en(idA_A1_1:int;
1147
	x:int;
1148
	a_1:int;
1149
	isInner:bool)
1150

    
1151
returns (idA_A1:int;
1152
	a:int);
1153

    
1154

    
1155
var 	idA_A1_2:int;
1156
	a_2:int;
1157

    
1158

    
1159
let
1160

    
1161

    
1162

    
1163
	-- set state as active 
1164
	idA_A1_2 
1165
	= 571;
1166
	
1167

    
1168
	a_2 
1169
	= if (not isInner) then x+2
1170
	 else a_1;
1171
	
1172

    
1173
	(idA_A1, a) 
1174
	= (idA_A1_2, a_2);
1175
	
1176

    
1177
tel
1178

    
1179

    
1180

    
1181

    
1182

    
1183
-- Exit action for state :A1_A1b
1184
node A1_A1b_ex(idA_A1_1:int;
1185
	isInner:bool)
1186

    
1187
returns (idA_A1:int);
1188

    
1189

    
1190
var 	idA_A1_2:int;
1191

    
1192

    
1193
let
1194

    
1195

    
1196

    
1197
	-- set state as inactive 
1198
	idA_A1_2
1199
	 = if (not isInner) then 0 else idA_A1_1;
1200

    
1201

    
1202
	(idA_A1) 
1203
	= (idA_A1_1);
1204
	
1205

    
1206
tel
1207

    
1208

    
1209

    
1210

    
1211

    
1212

    
1213
-- Entry action for state :A_A1
1214
node A_A1_en(idA_A1_1:int;
1215
	idEvents1_A_1:int;
1216
	a_1:int;
1217
	x:int;
1218
	isInner:bool)
1219

    
1220
returns (idA_A1:int;
1221
	idEvents1_A:int;
1222
	a:int);
1223

    
1224

    
1225
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int;
1226
	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int;
1227
	a_2, a_3, a_4, a_5, a_6:int;
1228

    
1229

    
1230
let
1231

    
1232

    
1233

    
1234
	-- set state as active 
1235
	idEvents1_A_2 
1236
	= 569;
1237
	
1238

    
1239
	
1240
-- transition trace :
1241
	--POINT__To__A1_A1a_1
1242
		(idA_A1_2, a_2) 
1243
	= A1_A1a_en(idA_A1_1, x, a_1, false);
1244
		
1245

    
1246
	(idA_A1_3, idEvents1_A_3, a_3) 
1247
	= 
1248

    
1249
	if ( idA_A1_1 = 0) then
1250

    
1251
	 (idA_A1_2, idEvents1_A_2, a_2)
1252

    
1253
	 else(idA_A1_1, idEvents1_A_2, a_1);
1254

    
1255
	
1256

    
1257
	(idA_A1_4, a_4) 
1258
	= 
1259
	if ( idA_A1_1 = 570) then
1260
	A1_A1a_en(idA_A1_1, x, a_1, false)
1261
	 else (idA_A1_1, a_1);
1262

    
1263
	
1264

    
1265
	(idA_A1_5, a_5) 
1266
	= 
1267
	if ( idA_A1_1 = 571) then
1268
	A1_A1b_en(idA_A1_1, x, a_1, false)
1269
	 else (idA_A1_1, a_1);
1270

    
1271
	
1272

    
1273
	(idA_A1_6, idEvents1_A_4, a_6) 
1274
	= 
1275
		 if ( idA_A1_1 = 0) then 
1276
		(idA_A1_3, idEvents1_A_3, a_3)
1277
		 else
1278
		 if ( idA_A1_1 = 570) then 
1279
		(idA_A1_4, idEvents1_A_3, a_4)
1280
		 else
1281
		 if ( idA_A1_1 = 571) then 
1282
		(idA_A1_5, idEvents1_A_3, a_5)
1283
		 else (idA_A1_1, idEvents1_A_2, a_1);
1284

    
1285

    
1286
	(idA_A1, idEvents1_A, a) 
1287
	= (idA_A1_6, idEvents1_A_4, a_6);
1288
	
1289

    
1290
tel
1291

    
1292

    
1293

    
1294

    
1295

    
1296
-- Exit action for state :A_A1
1297
node A_A1_ex(idA_A1_1:int;
1298
	idEvents1_A_1:int;
1299
	isInner:bool)
1300

    
1301
returns (idA_A1:int;
1302
	idEvents1_A:int);
1303

    
1304

    
1305
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
1306
	idEvents1_A_2:int;
1307

    
1308

    
1309
let
1310

    
1311

    
1312

    
1313
	
1314
	(idA_A1_2) 
1315
	= 
1316
	if ( idA_A1_1 = 570) then
1317
	A1_A1a_ex(idA_A1_1, false)
1318
	 else (idA_A1_1);
1319

    
1320
	
1321

    
1322
	(idA_A1_3) 
1323
	= 
1324
	if ( idA_A1_1 = 571) then
1325
	A1_A1b_ex(idA_A1_1, false)
1326
	 else (idA_A1_1);
1327

    
1328
	
1329

    
1330
	(idA_A1_4) 
1331
	= 
1332
		 if ( idA_A1_1 = 570) then 
1333
		(idA_A1_2)
1334
		 else
1335
		 if ( idA_A1_1 = 571) then 
1336
		(idA_A1_3)
1337
		 else (idA_A1_1);
1338

    
1339

    
1340
	-- set state as inactive 
1341
	idEvents1_A_2
1342
	 = if (not isInner) then 0 else idEvents1_A_1;
1343

    
1344
	idA_A1_5 
1345
	= 0;
1346
	
1347

    
1348
	(idA_A1, idEvents1_A) 
1349
	= (idA_A1_5, idEvents1_A_1);
1350
	
1351

    
1352
tel
1353

    
1354

    
1355

    
1356

    
1357

    
1358

    
1359
-- Entry action for state :Events1_A
1360
node Events1_A_en(idEvents1_A_1:int;
1361
	idEvents1_Events1_1:int;
1362
	a_1:int;
1363
	idA_A1_1:int;
1364
	x:int;
1365
	idA_A2_1:int;
1366
	isInner:bool)
1367

    
1368
returns (idEvents1_A:int;
1369
	idEvents1_Events1:int;
1370
	a:int;
1371
	idA_A1:int;
1372
	idA_A2:int);
1373

    
1374

    
1375
var 	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5, idEvents1_A_6:int;
1376
	idEvents1_Events1_2, idEvents1_Events1_3, idEvents1_Events1_4:int;
1377
	a_2, a_3, a_4, a_5, a_6:int;
1378
	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
1379
	idA_A2_2, idA_A2_3:int;
1380

    
1381

    
1382
let
1383

    
1384

    
1385

    
1386
	-- set state as active 
1387
	idEvents1_Events1_2 
1388
	= 565;
1389
	
1390

    
1391
	
1392
-- transition trace :
1393
	--POINT__To__A_A1_1
1394
		(idA_A1_2, idEvents1_A_2, a_2) 
1395
	= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, x, false);
1396
		
1397

    
1398
	(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3) 
1399
	= 
1400

    
1401
	if ( idEvents1_A_1 = 0) then
1402

    
1403
	 (idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2)
1404

    
1405
	 else(idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1);
1406

    
1407
	
1408

    
1409
	(idA_A2_2, idEvents1_A_4, a_4) 
1410
	= 
1411
	if ( idEvents1_A_1 = 566) then
1412
	A_A2_en(idA_A2_1, idEvents1_A_1, a_1, x, false)
1413
	 else (idA_A2_1, idEvents1_A_1, a_1);
1414

    
1415
	
1416

    
1417
	(idA_A1_4, idEvents1_A_5, a_5) 
1418
	= 
1419
	if ( idEvents1_A_1 = 569) then
1420
	A_A1_en(idA_A1_1, idEvents1_A_1, a_1, x, false)
1421
	 else (idA_A1_1, idEvents1_A_1, a_1);
1422

    
1423
	
1424

    
1425
	(idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3) 
1426
	= 
1427
		 if ( idEvents1_A_1 = 0) then 
1428
		(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_1)
1429
		 else
1430
		 if ( idEvents1_A_1 = 566) then 
1431
		(idEvents1_A_4, idEvents1_Events1_3, a_4, idA_A1_1, idA_A2_2)
1432
		 else
1433
		 if ( idEvents1_A_1 = 569) then 
1434
		(idEvents1_A_5, idEvents1_Events1_3, a_5, idA_A1_4, idA_A2_1)
1435
		 else (idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1, idA_A2_1);
1436

    
1437

    
1438
	(idEvents1_A, idEvents1_Events1, a, idA_A1, idA_A2) 
1439
	= (idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3);
1440
	
1441

    
1442
tel
1443

    
1444

    
1445

    
1446

    
1447

    
1448
-- Exit action for state :Events1_A
1449
node Events1_A_ex(idA_A2_1:int;
1450
	idEvents1_A_1:int;
1451
	idA_A1_1:int;
1452
	idEvents1_Events1_1:int;
1453
	isInner:bool)
1454

    
1455
returns (idA_A2:int;
1456
	idEvents1_A:int;
1457
	idA_A1:int;
1458
	idEvents1_Events1:int);
1459

    
1460

    
1461
var 	idA_A2_2, idA_A2_3:int;
1462
	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5:int;
1463
	idA_A1_2, idA_A1_3:int;
1464
	idEvents1_Events1_2:int;
1465

    
1466

    
1467
let
1468

    
1469

    
1470

    
1471
	
1472
	(idA_A2_2, idEvents1_A_2) 
1473
	= 
1474
	if ( idEvents1_A_1 = 566) then
1475
	A_A2_ex(idA_A2_1, idEvents1_A_1, false)
1476
	 else (idA_A2_1, idEvents1_A_1);
1477

    
1478
	
1479

    
1480
	(idA_A1_2, idEvents1_A_3) 
1481
	= 
1482
	if ( idEvents1_A_1 = 569) then
1483
	A_A1_ex(idA_A1_1, idEvents1_A_1, false)
1484
	 else (idA_A1_1, idEvents1_A_1);
1485

    
1486
	
1487

    
1488
	(idA_A2_3, idEvents1_A_4, idA_A1_3) 
1489
	= 
1490
		 if ( idEvents1_A_1 = 566) then 
1491
		(idA_A2_2, idEvents1_A_2, idA_A1_1)
1492
		 else
1493
		 if ( idEvents1_A_1 = 569) then 
1494
		(idA_A2_1, idEvents1_A_3, idA_A1_2)
1495
		 else (idA_A2_1, idEvents1_A_1, idA_A1_1);
1496

    
1497

    
1498
	-- set state as inactive 
1499
	idEvents1_Events1_2
1500
	 = if (not isInner) then 0 else idEvents1_Events1_1;
1501

    
1502
	idEvents1_A_5 
1503
	= 0;
1504
	
1505

    
1506
	(idA_A2, idEvents1_A, idA_A1, idEvents1_Events1) 
1507
	= (idA_A2_3, idEvents1_A_5, idA_A1_3, idEvents1_Events1_1);
1508
	
1509

    
1510
tel
1511

    
1512

    
1513
--***************************************************State :B_B2 Automaton***************************************************
1514

    
1515
node B_B2_node(idB_B2_1:int;
1516
	b_1:int;
1517
	x:int;
1518
	S1:bool;
1519
	R1:bool)
1520

    
1521
returns (idB_B2:int;
1522
	b:int);
1523

    
1524

    
1525
let
1526

    
1527
	 automaton b_b2
1528

    
1529
	state POINTB_B2:
1530
	unless (idB_B2_1=0) restart POINT__TO__B2_B2A_1
1531

    
1532

    
1533

    
1534
	unless (idB_B2_1=574) and S1 restart B2_B2A__TO__B2_B2B_1
1535

    
1536

    
1537

    
1538
	unless (idB_B2_1=575) and R1 restart B2_B2B__TO__B2_B2A_1
1539

    
1540

    
1541

    
1542
	unless (idB_B2_1=574) restart B2_B2A_IDL
1543

    
1544
	unless (idB_B2_1=575) restart B2_B2B_IDL
1545

    
1546
	let
1547

    
1548
		(idB_B2, b) 
1549
	= (idB_B2_1, b_1);
1550
	
1551

    
1552
	tel
1553

    
1554

    
1555

    
1556
	state POINT__TO__B2_B2A_1:
1557

    
1558
	 var 	idB_B2_2:int;
1559
	b_2:int;
1560
	let
1561

    
1562
		-- transition trace :
1563
	--POINT__To__B2_B2a_1
1564
		(idB_B2_2, b_2) 
1565
	= B2_B2a_en(idB_B2_1, x, b_1, false);
1566
		
1567

    
1568
	(idB_B2, b) 
1569
	=  (idB_B2_2, b_2);
1570

    
1571

    
1572
	tel
1573

    
1574
	until true restart POINTB_B2
1575

    
1576

    
1577

    
1578
	state B2_B2A__TO__B2_B2B_1:
1579

    
1580
	 var 	idB_B2_2, idB_B2_3:int;
1581
	b_2:int;
1582
	let
1583

    
1584
		-- transition trace :
1585
	--B2_B2a__To__B2_B2b_1
1586
		(idB_B2_2) 
1587
	= B2_B2a_ex(idB_B2_1, false);
1588
		
1589

    
1590
		(idB_B2_3, b_2) 
1591
	= B2_B2b_en(idB_B2_2, x, b_1, false);
1592
		
1593

    
1594
	(idB_B2, b) 
1595
	=  (idB_B2_3, b_2);
1596

    
1597

    
1598
	tel
1599

    
1600
	until true restart POINTB_B2
1601

    
1602

    
1603

    
1604
	state B2_B2B__TO__B2_B2A_1:
1605

    
1606
	 var 	idB_B2_2, idB_B2_3:int;
1607
	b_2:int;
1608
	let
1609

    
1610
		-- transition trace :
1611
	--B2_B2b__To__B2_B2a_1
1612
		(idB_B2_2) 
1613
	= B2_B2b_ex(idB_B2_1, false);
1614
		
1615

    
1616
		(idB_B2_3, b_2) 
1617
	= B2_B2a_en(idB_B2_2, x, b_1, false);
1618
		
1619

    
1620
	(idB_B2, b) 
1621
	=  (idB_B2_3, b_2);
1622

    
1623

    
1624
	tel
1625

    
1626
	until true restart POINTB_B2
1627

    
1628

    
1629

    
1630
	state B2_B2A_IDL:
1631

    
1632
	 	let
1633

    
1634
		
1635

    
1636
	(idB_B2, b) 
1637
	= (idB_B2_1, b_1);
1638
	
1639

    
1640
	tel
1641

    
1642
	until true restart POINTB_B2
1643

    
1644

    
1645

    
1646
	state B2_B2B_IDL:
1647

    
1648
	 	let
1649

    
1650
		
1651

    
1652
	(idB_B2, b) 
1653
	= (idB_B2_1, b_1);
1654
	
1655

    
1656
	tel
1657

    
1658
	until true restart POINTB_B2
1659

    
1660

    
1661

    
1662
tel
1663

    
1664

    
1665
--***************************************************State :B_B1 Automaton***************************************************
1666

    
1667
node B_B1_node(idB_B1_1:int;
1668
	b_1:int;
1669
	x:int;
1670
	S1:bool;
1671
	R1:bool)
1672

    
1673
returns (idB_B1:int;
1674
	b:int);
1675

    
1676

    
1677
let
1678

    
1679
	 automaton b_b1
1680

    
1681
	state POINTB_B1:
1682
	unless (idB_B1_1=0) restart POINT__TO__B1_B1A_1
1683

    
1684

    
1685

    
1686
	unless (idB_B1_1=577) and S1 restart B1_B1A__TO__B1_B1B_1
1687

    
1688

    
1689

    
1690
	unless (idB_B1_1=578) and R1 restart B1_B1B__TO__B1_B1A_1
1691

    
1692

    
1693

    
1694
	unless (idB_B1_1=577) restart B1_B1A_IDL
1695

    
1696
	unless (idB_B1_1=578) restart B1_B1B_IDL
1697

    
1698
	let
1699

    
1700
		(idB_B1, b) 
1701
	= (idB_B1_1, b_1);
1702
	
1703

    
1704
	tel
1705

    
1706

    
1707

    
1708
	state POINT__TO__B1_B1A_1:
1709

    
1710
	 var 	idB_B1_2:int;
1711
	b_2:int;
1712
	let
1713

    
1714
		-- transition trace :
1715
	--POINT__To__B1_B1a_1
1716
		(idB_B1_2, b_2) 
1717
	= B1_B1a_en(idB_B1_1, x, b_1, false);
1718
		
1719

    
1720
	(idB_B1, b) 
1721
	=  (idB_B1_2, b_2);
1722

    
1723

    
1724
	tel
1725

    
1726
	until true restart POINTB_B1
1727

    
1728

    
1729

    
1730
	state B1_B1A__TO__B1_B1B_1:
1731

    
1732
	 var 	idB_B1_2, idB_B1_3:int;
1733
	b_2:int;
1734
	let
1735

    
1736
		-- transition trace :
1737
	--B1_B1a__To__B1_B1b_1
1738
		(idB_B1_2) 
1739
	= B1_B1a_ex(idB_B1_1, false);
1740
		
1741

    
1742
		(idB_B1_3, b_2) 
1743
	= B1_B1b_en(idB_B1_2, x, b_1, false);
1744
		
1745

    
1746
	(idB_B1, b) 
1747
	=  (idB_B1_3, b_2);
1748

    
1749

    
1750
	tel
1751

    
1752
	until true restart POINTB_B1
1753

    
1754

    
1755

    
1756
	state B1_B1B__TO__B1_B1A_1:
1757

    
1758
	 var 	idB_B1_2, idB_B1_3:int;
1759
	b_2:int;
1760
	let
1761

    
1762
		-- transition trace :
1763
	--B1_B1b__To__B1_B1a_1
1764
		(idB_B1_2) 
1765
	= B1_B1b_ex(idB_B1_1, false);
1766
		
1767

    
1768
		(idB_B1_3, b_2) 
1769
	= B1_B1a_en(idB_B1_2, x, b_1, false);
1770
		
1771

    
1772
	(idB_B1, b) 
1773
	=  (idB_B1_3, b_2);
1774

    
1775

    
1776
	tel
1777

    
1778
	until true restart POINTB_B1
1779

    
1780

    
1781

    
1782
	state B1_B1A_IDL:
1783

    
1784
	 	let
1785

    
1786
		
1787

    
1788
	(idB_B1, b) 
1789
	= (idB_B1_1, b_1);
1790
	
1791

    
1792
	tel
1793

    
1794
	until true restart POINTB_B1
1795

    
1796

    
1797

    
1798
	state B1_B1B_IDL:
1799

    
1800
	 	let
1801

    
1802
		
1803

    
1804
	(idB_B1, b) 
1805
	= (idB_B1_1, b_1);
1806
	
1807

    
1808
	tel
1809

    
1810
	until true restart POINTB_B1
1811

    
1812

    
1813

    
1814
tel
1815

    
1816

    
1817
--***************************************************State :Events1_B Automaton***************************************************
1818

    
1819
node Events1_B_node(idEvents1_B_1:int;
1820
	b_1:int;
1821
	idB_B1_1:int;
1822
	x:int;
1823
	T1:bool;
1824
	idB_B2_1:int;
1825
	c_1:int;
1826
	R1:bool;
1827
	S1:bool)
1828

    
1829
returns (idEvents1_B:int;
1830
	b:int;
1831
	idB_B1:int;
1832
	idB_B2:int;
1833
	c:int);
1834

    
1835

    
1836
let
1837

    
1838
	 automaton events1_b
1839

    
1840
	state POINTEvents1_B:
1841
	unless (idEvents1_B_1=0) restart POINT__TO__B_B1_1
1842

    
1843

    
1844

    
1845
	unless (idEvents1_B_1=573) and T1 restart B_B2__TO__B_B1_1
1846

    
1847

    
1848

    
1849
	unless (idEvents1_B_1=576) and T1 restart B_B1__TO__B_B2_1
1850

    
1851

    
1852

    
1853
	unless (idEvents1_B_1=573) restart B_B2_IDL
1854

    
1855
	unless (idEvents1_B_1=576) restart B_B1_IDL
1856

    
1857
	let
1858

    
1859
		(idEvents1_B, b, idB_B1, idB_B2, c) 
1860
	= (idEvents1_B_1, b_1, idB_B1_1, idB_B2_1, c_1);
1861
	
1862

    
1863
	tel
1864

    
1865

    
1866

    
1867
	state POINT__TO__B_B1_1:
1868

    
1869
	 var 	idEvents1_B_2:int;
1870
	b_2:int;
1871
	idB_B1_2:int;
1872
	let
1873

    
1874
		-- transition trace :
1875
	--POINT__To__B_B1_1
1876
		(idB_B1_2, idEvents1_B_2, b_2) 
1877
	= B_B1_en(idB_B1_1, idEvents1_B_1, b_1, x, false);
1878
		
1879

    
1880
	(idEvents1_B, b, idB_B1) 
1881
	=  (idEvents1_B_2, b_2, idB_B1_2);
1882

    
1883
	--add unused variables
1884
	(c, idB_B2) 
1885
	= (c_1, idB_B2_1);
1886
	
1887

    
1888
	tel
1889

    
1890
	until true restart POINTEvents1_B
1891

    
1892

    
1893

    
1894
	state B_B2__TO__B_B1_1:
1895

    
1896
	 var 	idEvents1_B_2, idEvents1_B_3:int;
1897
	b_2:int;
1898
	idB_B1_2:int;
1899
	idB_B2_2:int;
1900
	c_2:int;
1901
	let
1902

    
1903
		-- transition trace :
1904
	--B_B2__To__B_B1_1
1905
		(idB_B2_2, idEvents1_B_2) 
1906
	= B_B2_ex(idB_B2_1, idEvents1_B_1, false);
1907
		
1908

    
1909
		(c_2) 
1910
	= B_B2__To__B_B1_1_Transition_Action(c_1);
1911
		
1912

    
1913
		(idB_B1_2, idEvents1_B_3, b_2) 
1914
	= B_B1_en(idB_B1_1, idEvents1_B_2, b_1, x, false);
1915
		
1916

    
1917
	(idEvents1_B, b, idB_B1, idB_B2, c) 
1918
	=  (idEvents1_B_3, b_2, idB_B1_2, idB_B2_2, c_2);
1919

    
1920

    
1921
	tel
1922

    
1923
	until true restart POINTEvents1_B
1924

    
1925

    
1926

    
1927
	state B_B1__TO__B_B2_1:
1928

    
1929
	 var 	idEvents1_B_2, idEvents1_B_3:int;
1930
	b_2:int;
1931
	idB_B1_2:int;
1932
	idB_B2_2:int;
1933
	c_2:int;
1934
	let
1935

    
1936
		-- transition trace :
1937
	--B_B1__To__B_B2_1
1938
		(idB_B1_2, idEvents1_B_2) 
1939
	= B_B1_ex(idB_B1_1, idEvents1_B_1, false);
1940
		
1941

    
1942
		(c_2) 
1943
	= B_B1__To__B_B2_1_Transition_Action(c_1);
1944
		
1945

    
1946
		(idB_B2_2, idEvents1_B_3, b_2) 
1947
	= B_B2_en(idB_B2_1, idEvents1_B_2, b_1, x, false);
1948
		
1949

    
1950
	(idEvents1_B, b, idB_B1, idB_B2, c) 
1951
	=  (idEvents1_B_3, b_2, idB_B1_2, idB_B2_2, c_2);
1952

    
1953

    
1954
	tel
1955

    
1956
	until true restart POINTEvents1_B
1957

    
1958

    
1959

    
1960
	state B_B2_IDL:
1961

    
1962
	 var 	b_2:int;
1963
	idB_B2_2:int;
1964
	let
1965

    
1966
		
1967
	(idB_B2_2, b_2) 
1968
	= B_B2_node(idB_B2_1, b_1, x, S1, R1);
1969

    
1970
		
1971

    
1972

    
1973
	(idEvents1_B, b, idB_B1, idB_B2, c) 
1974
	= (idEvents1_B_1, b_2, idB_B1_1, idB_B2_2, c_1);
1975
	
1976

    
1977
	tel
1978

    
1979
	until true restart POINTEvents1_B
1980

    
1981

    
1982

    
1983
	state B_B1_IDL:
1984

    
1985
	 var 	b_2:int;
1986
	idB_B1_2:int;
1987
	let
1988

    
1989
		
1990
	(idB_B1_2, b_2) 
1991
	= B_B1_node(idB_B1_1, b_1, x, S1, R1);
1992

    
1993
		
1994

    
1995

    
1996
	(idEvents1_B, b, idB_B1, idB_B2, c) 
1997
	= (idEvents1_B_1, b_2, idB_B1_2, idB_B2_1, c_1);
1998
	
1999

    
2000
	tel
2001

    
2002
	until true restart POINTEvents1_B
2003

    
2004

    
2005

    
2006
tel
2007

    
2008

    
2009

    
2010

    
2011

    
2012

    
2013
node A2_A2a__To__A2_A2b_1_Transition_Action(idEvents1_B_1:int;
2014
	b_1:int;
2015
	idB_B1_1:int;
2016
	x:int;
2017
	T1:bool;
2018
	idB_B2_1:int;
2019
	c_1:int;
2020
	R1:bool;
2021
	S1:bool)
2022

    
2023
returns (idEvents1_B:int;
2024
	b:int;
2025
	idB_B1:int;
2026
	idB_B2:int;
2027
	c:int);
2028

    
2029

    
2030
var 	idEvents1_B_2:int;
2031
	b_2:int;
2032
	idB_B1_2:int;
2033
	idB_B2_2:int;
2034
	c_2:int;
2035

    
2036

    
2037
let
2038

    
2039

    
2040

    
2041
	(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2042
	= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, true);
2043
	
2044

    
2045
	(idEvents1_B, b, idB_B1, idB_B2, c) 
2046
	= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2);
2047
	
2048

    
2049
tel
2050

    
2051

    
2052

    
2053

    
2054

    
2055

    
2056
node A2_A2b__To__A2_A2a_1_Transition_Action(idEvents1_B_1:int;
2057
	b_1:int;
2058
	idB_B1_1:int;
2059
	x:int;
2060
	T1:bool;
2061
	idB_B2_1:int;
2062
	c_1:int;
2063
	R1:bool;
2064
	S1:bool)
2065

    
2066
returns (idEvents1_B:int;
2067
	b:int;
2068
	idB_B1:int;
2069
	idB_B2:int;
2070
	c:int);
2071

    
2072

    
2073
var 	idEvents1_B_2:int;
2074
	b_2:int;
2075
	idB_B1_2:int;
2076
	idB_B2_2:int;
2077
	c_2:int;
2078

    
2079

    
2080
let
2081

    
2082

    
2083

    
2084
	(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2085
	= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, true, S1);
2086
	
2087

    
2088
	(idEvents1_B, b, idB_B1, idB_B2, c) 
2089
	= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2);
2090
	
2091

    
2092
tel
2093

    
2094

    
2095
--***************************************************State :A_A2 Automaton***************************************************
2096

    
2097
node A_A2_node(idA_A2_1:int;
2098
	a_1:int;
2099
	x:int;
2100
	S:bool;
2101
	R1:bool;
2102
	S1:bool;
2103
	T1:bool;
2104
	b_1:int;
2105
	c_1:int;
2106
	idB_B1_1:int;
2107
	idB_B2_1:int;
2108
	idEvents1_B_1:int;
2109
	R:bool)
2110

    
2111
returns (idA_A2:int;
2112
	a:int;
2113
	b:int;
2114
	c:int;
2115
	idB_B1:int;
2116
	idB_B2:int;
2117
	idEvents1_B:int);
2118

    
2119

    
2120
let
2121

    
2122
	 automaton a_a2
2123

    
2124
	state POINTA_A2:
2125
	unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1
2126

    
2127

    
2128

    
2129
	unless (idA_A2_1=567) and S restart A2_A2A__TO__A2_A2B_1
2130

    
2131

    
2132

    
2133
	unless (idA_A2_1=568) and R restart A2_A2B__TO__A2_A2A_1
2134

    
2135

    
2136

    
2137
	unless (idA_A2_1=567) restart A2_A2A_IDL
2138

    
2139
	unless (idA_A2_1=568) restart A2_A2B_IDL
2140

    
2141
	let
2142

    
2143
		(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2144
	= (idA_A2_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2145
	
2146

    
2147
	tel
2148

    
2149

    
2150

    
2151
	state POINT__TO__A2_A2A_1:
2152

    
2153
	 var 	idA_A2_2:int;
2154
	a_2:int;
2155
	let
2156

    
2157
		-- transition trace :
2158
	--POINT__To__A2_A2a_1
2159
		(idA_A2_2, a_2) 
2160
	= A2_A2a_en(idA_A2_1, x, a_1, false);
2161
		
2162

    
2163
	(idA_A2, a) 
2164
	=  (idA_A2_2, a_2);
2165

    
2166
	--add unused variables
2167
	(b, c, idB_B1, idB_B2, idEvents1_B) 
2168
	= (b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2169
	
2170

    
2171
	tel
2172

    
2173
	until true restart POINTA_A2
2174

    
2175

    
2176

    
2177
	state A2_A2A__TO__A2_A2B_1:
2178

    
2179
	 var 	idA_A2_2, idA_A2_3:int;
2180
	a_2:int;
2181
	b_2:int;
2182
	c_2:int;
2183
	idB_B1_2:int;
2184
	idB_B2_2:int;
2185
	idEvents1_B_2:int;
2186
	let
2187

    
2188
		-- transition trace :
2189
	--A2_A2a__To__A2_A2b_1
2190
		(idA_A2_2) 
2191
	= A2_A2a_ex(idA_A2_1, false);
2192
		
2193

    
2194
		(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2195
	= A2_A2a__To__A2_A2b_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1);
2196
		
2197

    
2198
		(idA_A2_3, a_2) 
2199
	= A2_A2b_en(idA_A2_2, x, a_1, false);
2200
		
2201

    
2202
	(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2203
	=  (idA_A2_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2204

    
2205

    
2206
	tel
2207

    
2208
	until true restart POINTA_A2
2209

    
2210

    
2211

    
2212
	state A2_A2B__TO__A2_A2A_1:
2213

    
2214
	 var 	idA_A2_2, idA_A2_3:int;
2215
	a_2:int;
2216
	b_2:int;
2217
	c_2:int;
2218
	idB_B1_2:int;
2219
	idB_B2_2:int;
2220
	idEvents1_B_2:int;
2221
	let
2222

    
2223
		-- transition trace :
2224
	--A2_A2b__To__A2_A2a_1
2225
		(idA_A2_2) 
2226
	= A2_A2b_ex(idA_A2_1, false);
2227
		
2228

    
2229
		(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2230
	= A2_A2b__To__A2_A2a_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1);
2231
		
2232

    
2233
		(idA_A2_3, a_2) 
2234
	= A2_A2a_en(idA_A2_2, x, a_1, false);
2235
		
2236

    
2237
	(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2238
	=  (idA_A2_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2239

    
2240

    
2241
	tel
2242

    
2243
	until true restart POINTA_A2
2244

    
2245

    
2246

    
2247
	state A2_A2A_IDL:
2248

    
2249
	 	let
2250

    
2251
		
2252

    
2253
	(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2254
	= (idA_A2_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2255
	
2256

    
2257
	tel
2258

    
2259
	until true restart POINTA_A2
2260

    
2261

    
2262

    
2263
	state A2_A2B_IDL:
2264

    
2265
	 	let
2266

    
2267
		
2268

    
2269
	(idA_A2, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2270
	= (idA_A2_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2271
	
2272

    
2273
	tel
2274

    
2275
	until true restart POINTA_A2
2276

    
2277

    
2278

    
2279
tel
2280

    
2281

    
2282

    
2283

    
2284

    
2285

    
2286
node A1_A1a__To__A1_A1b_1_Transition_Action(idEvents1_B_1:int;
2287
	b_1:int;
2288
	idB_B1_1:int;
2289
	x:int;
2290
	T1:bool;
2291
	idB_B2_1:int;
2292
	c_1:int;
2293
	R1:bool;
2294
	S1:bool)
2295

    
2296
returns (idEvents1_B:int;
2297
	b:int;
2298
	idB_B1:int;
2299
	idB_B2:int;
2300
	c:int);
2301

    
2302

    
2303
var 	idEvents1_B_2:int;
2304
	b_2:int;
2305
	idB_B1_2:int;
2306
	idB_B2_2:int;
2307
	c_2:int;
2308

    
2309

    
2310
let
2311

    
2312

    
2313

    
2314
	(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2315
	= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, true);
2316
	
2317

    
2318
	(idEvents1_B, b, idB_B1, idB_B2, c) 
2319
	= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2);
2320
	
2321

    
2322
tel
2323

    
2324

    
2325

    
2326

    
2327

    
2328

    
2329
node A1_A1b__To__A1_A1a_1_Transition_Action(idEvents1_B_1:int;
2330
	b_1:int;
2331
	idB_B1_1:int;
2332
	x:int;
2333
	T1:bool;
2334
	idB_B2_1:int;
2335
	c_1:int;
2336
	R1:bool;
2337
	S1:bool)
2338

    
2339
returns (idEvents1_B:int;
2340
	b:int;
2341
	idB_B1:int;
2342
	idB_B2:int;
2343
	c:int);
2344

    
2345

    
2346
var 	idEvents1_B_2:int;
2347
	b_2:int;
2348
	idB_B1_2:int;
2349
	idB_B2_2:int;
2350
	c_2:int;
2351

    
2352

    
2353
let
2354

    
2355

    
2356

    
2357
	(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2358
	= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, true, S1);
2359
	
2360

    
2361
	(idEvents1_B, b, idB_B1, idB_B2, c) 
2362
	= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2);
2363
	
2364

    
2365
tel
2366

    
2367

    
2368
--***************************************************State :A_A1 Automaton***************************************************
2369

    
2370
node A_A1_node(idA_A1_1:int;
2371
	a_1:int;
2372
	x:int;
2373
	S:bool;
2374
	R1:bool;
2375
	S1:bool;
2376
	T1:bool;
2377
	b_1:int;
2378
	c_1:int;
2379
	idB_B1_1:int;
2380
	idB_B2_1:int;
2381
	idEvents1_B_1:int;
2382
	R:bool)
2383

    
2384
returns (idA_A1:int;
2385
	a:int;
2386
	b:int;
2387
	c:int;
2388
	idB_B1:int;
2389
	idB_B2:int;
2390
	idEvents1_B:int);
2391

    
2392

    
2393
let
2394

    
2395
	 automaton a_a1
2396

    
2397
	state POINTA_A1:
2398
	unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1
2399

    
2400

    
2401

    
2402
	unless (idA_A1_1=570) and S restart A1_A1A__TO__A1_A1B_1
2403

    
2404

    
2405

    
2406
	unless (idA_A1_1=571) and R restart A1_A1B__TO__A1_A1A_1
2407

    
2408

    
2409

    
2410
	unless (idA_A1_1=570) restart A1_A1A_IDL
2411

    
2412
	unless (idA_A1_1=571) restart A1_A1B_IDL
2413

    
2414
	let
2415

    
2416
		(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2417
	= (idA_A1_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2418
	
2419

    
2420
	tel
2421

    
2422

    
2423

    
2424
	state POINT__TO__A1_A1A_1:
2425

    
2426
	 var 	idA_A1_2:int;
2427
	a_2:int;
2428
	let
2429

    
2430
		-- transition trace :
2431
	--POINT__To__A1_A1a_1
2432
		(idA_A1_2, a_2) 
2433
	= A1_A1a_en(idA_A1_1, x, a_1, false);
2434
		
2435

    
2436
	(idA_A1, a) 
2437
	=  (idA_A1_2, a_2);
2438

    
2439
	--add unused variables
2440
	(b, c, idB_B1, idB_B2, idEvents1_B) 
2441
	= (b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2442
	
2443

    
2444
	tel
2445

    
2446
	until true restart POINTA_A1
2447

    
2448

    
2449

    
2450
	state A1_A1A__TO__A1_A1B_1:
2451

    
2452
	 var 	idA_A1_2, idA_A1_3:int;
2453
	a_2:int;
2454
	b_2:int;
2455
	c_2:int;
2456
	idB_B1_2:int;
2457
	idB_B2_2:int;
2458
	idEvents1_B_2:int;
2459
	let
2460

    
2461
		-- transition trace :
2462
	--A1_A1a__To__A1_A1b_1
2463
		(idA_A1_2) 
2464
	= A1_A1a_ex(idA_A1_1, false);
2465
		
2466

    
2467
		(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2468
	= A1_A1a__To__A1_A1b_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1);
2469
		
2470

    
2471
		(idA_A1_3, a_2) 
2472
	= A1_A1b_en(idA_A1_2, x, a_1, false);
2473
		
2474

    
2475
	(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2476
	=  (idA_A1_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2477

    
2478

    
2479
	tel
2480

    
2481
	until true restart POINTA_A1
2482

    
2483

    
2484

    
2485
	state A1_A1B__TO__A1_A1A_1:
2486

    
2487
	 var 	idA_A1_2, idA_A1_3:int;
2488
	a_2:int;
2489
	b_2:int;
2490
	c_2:int;
2491
	idB_B1_2:int;
2492
	idB_B2_2:int;
2493
	idEvents1_B_2:int;
2494
	let
2495

    
2496
		-- transition trace :
2497
	--A1_A1b__To__A1_A1a_1
2498
		(idA_A1_2) 
2499
	= A1_A1b_ex(idA_A1_1, false);
2500
		
2501

    
2502
		(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2503
	= A1_A1b__To__A1_A1a_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1);
2504
		
2505

    
2506
		(idA_A1_3, a_2) 
2507
	= A1_A1a_en(idA_A1_2, x, a_1, false);
2508
		
2509

    
2510
	(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2511
	=  (idA_A1_3, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2512

    
2513

    
2514
	tel
2515

    
2516
	until true restart POINTA_A1
2517

    
2518

    
2519

    
2520
	state A1_A1A_IDL:
2521

    
2522
	 	let
2523

    
2524
		
2525

    
2526
	(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2527
	= (idA_A1_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2528
	
2529

    
2530
	tel
2531

    
2532
	until true restart POINTA_A1
2533

    
2534

    
2535

    
2536
	state A1_A1B_IDL:
2537

    
2538
	 	let
2539

    
2540
		
2541

    
2542
	(idA_A1, a, b, c, idB_B1, idB_B2, idEvents1_B) 
2543
	= (idA_A1_1, a_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2544
	
2545

    
2546
	tel
2547

    
2548
	until true restart POINTA_A1
2549

    
2550

    
2551

    
2552
tel
2553

    
2554

    
2555

    
2556

    
2557

    
2558

    
2559
node A_A2__To__A_A1_1_Transition_Action(idEvents1_B_1:int;
2560
	b_1:int;
2561
	idB_B1_1:int;
2562
	x:int;
2563
	T1:bool;
2564
	idB_B2_1:int;
2565
	c_1:int;
2566
	R1:bool;
2567
	S1:bool)
2568

    
2569
returns (idEvents1_B:int;
2570
	b:int;
2571
	idB_B1:int;
2572
	idB_B2:int;
2573
	c:int);
2574

    
2575

    
2576
var 	idEvents1_B_2:int;
2577
	b_2:int;
2578
	idB_B1_2:int;
2579
	idB_B2_2:int;
2580
	c_2:int;
2581

    
2582

    
2583
let
2584

    
2585

    
2586

    
2587
	(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2588
	= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, true, idB_B2_1, c_1, R1, S1);
2589
	
2590

    
2591
	(idEvents1_B, b, idB_B1, idB_B2, c) 
2592
	= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2);
2593
	
2594

    
2595
tel
2596

    
2597

    
2598

    
2599

    
2600

    
2601

    
2602
node A_A1__To__A_A2_1_Transition_Action(idEvents1_B_1:int;
2603
	b_1:int;
2604
	idB_B1_1:int;
2605
	x:int;
2606
	T1:bool;
2607
	idB_B2_1:int;
2608
	c_1:int;
2609
	R1:bool;
2610
	S1:bool)
2611

    
2612
returns (idEvents1_B:int;
2613
	b:int;
2614
	idB_B1:int;
2615
	idB_B2:int;
2616
	c:int);
2617

    
2618

    
2619
var 	idEvents1_B_2:int;
2620
	b_2:int;
2621
	idB_B1_2:int;
2622
	idB_B2_2:int;
2623
	c_2:int;
2624

    
2625

    
2626
let
2627

    
2628

    
2629

    
2630
	(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2631
	= Events1_B_node(idEvents1_B_1, b_1, idB_B1_1, x, true, idB_B2_1, c_1, R1, S1);
2632
	
2633

    
2634
	(idEvents1_B, b, idB_B1, idB_B2, c) 
2635
	= (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2);
2636
	
2637

    
2638
tel
2639

    
2640

    
2641
--***************************************************State :Events1_A Automaton***************************************************
2642

    
2643
node Events1_A_node(idEvents1_A_1:int;
2644
	a_1:int;
2645
	idA_A1_1:int;
2646
	x:int;
2647
	T:bool;
2648
	idA_A2_1:int;
2649
	R1:bool;
2650
	S1:bool;
2651
	T1:bool;
2652
	b_1:int;
2653
	c_1:int;
2654
	idB_B1_1:int;
2655
	idB_B2_1:int;
2656
	idEvents1_B_1:int;
2657
	R:bool;
2658
	S:bool)
2659

    
2660
returns (idEvents1_A:int;
2661
	a:int;
2662
	idA_A1:int;
2663
	idA_A2:int;
2664
	b:int;
2665
	c:int;
2666
	idB_B1:int;
2667
	idB_B2:int;
2668
	idEvents1_B:int);
2669

    
2670

    
2671
let
2672

    
2673
	 automaton events1_a
2674

    
2675
	state POINTEvents1_A:
2676
	unless (idEvents1_A_1=0) restart POINT__TO__A_A1_1
2677

    
2678

    
2679

    
2680
	unless (idEvents1_A_1=566) and T restart A_A2__TO__A_A1_1
2681

    
2682

    
2683

    
2684
	unless (idEvents1_A_1=569) and T restart A_A1__TO__A_A2_1
2685

    
2686

    
2687

    
2688
	unless (idEvents1_A_1=566) restart A_A2_IDL
2689

    
2690
	unless (idEvents1_A_1=569) restart A_A1_IDL
2691

    
2692
	let
2693

    
2694
		(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2695
	= (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2696
	
2697

    
2698
	tel
2699

    
2700

    
2701

    
2702
	state POINT__TO__A_A1_1:
2703

    
2704
	 var 	idEvents1_A_2:int;
2705
	a_2:int;
2706
	idA_A1_2:int;
2707
	let
2708

    
2709
		-- transition trace :
2710
	--POINT__To__A_A1_1
2711
		(idA_A1_2, idEvents1_A_2, a_2) 
2712
	= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, x, false);
2713
		
2714

    
2715
	(idEvents1_A, a, idA_A1) 
2716
	=  (idEvents1_A_2, a_2, idA_A1_2);
2717

    
2718
	--add unused variables
2719
	(b, c, idA_A2, idB_B1, idB_B2, idEvents1_B) 
2720
	= (b_1, c_1, idA_A2_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2721
	
2722

    
2723
	tel
2724

    
2725
	until true restart POINTEvents1_A
2726

    
2727

    
2728

    
2729
	state A_A2__TO__A_A1_1:
2730

    
2731
	 var 	idEvents1_A_2, idEvents1_A_3:int;
2732
	a_2:int;
2733
	idA_A1_2:int;
2734
	idA_A2_2:int;
2735
	b_2:int;
2736
	c_2:int;
2737
	idB_B1_2:int;
2738
	idB_B2_2:int;
2739
	idEvents1_B_2:int;
2740
	let
2741

    
2742
		-- transition trace :
2743
	--A_A2__To__A_A1_1
2744
		(idA_A2_2, idEvents1_A_2) 
2745
	= A_A2_ex(idA_A2_1, idEvents1_A_1, false);
2746
		
2747

    
2748
		(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2749
	= A_A2__To__A_A1_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1);
2750
		
2751

    
2752
		(idA_A1_2, idEvents1_A_3, a_2) 
2753
	= A_A1_en(idA_A1_1, idEvents1_A_2, a_1, x, false);
2754
		
2755

    
2756
	(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2757
	=  (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2758

    
2759

    
2760
	tel
2761

    
2762
	until true restart POINTEvents1_A
2763

    
2764

    
2765

    
2766
	state A_A1__TO__A_A2_1:
2767

    
2768
	 var 	idEvents1_A_2, idEvents1_A_3:int;
2769
	a_2:int;
2770
	idA_A1_2:int;
2771
	idA_A2_2:int;
2772
	b_2:int;
2773
	c_2:int;
2774
	idB_B1_2:int;
2775
	idB_B2_2:int;
2776
	idEvents1_B_2:int;
2777
	let
2778

    
2779
		-- transition trace :
2780
	--A_A1__To__A_A2_1
2781
		(idA_A1_2, idEvents1_A_2) 
2782
	= A_A1_ex(idA_A1_1, idEvents1_A_1, false);
2783
		
2784

    
2785
		(idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2) 
2786
	= A_A1__To__A_A2_1_Transition_Action(idEvents1_B_1, b_1, idB_B1_1, x, T1, idB_B2_1, c_1, R1, S1);
2787
		
2788

    
2789
		(idA_A2_2, idEvents1_A_3, a_2) 
2790
	= A_A2_en(idA_A2_1, idEvents1_A_2, a_1, x, false);
2791
		
2792

    
2793
	(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2794
	=  (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2795

    
2796

    
2797
	tel
2798

    
2799
	until true restart POINTEvents1_A
2800

    
2801

    
2802

    
2803
	state A_A2_IDL:
2804

    
2805
	 var 	a_2:int;
2806
	idA_A2_2:int;
2807
	b_2:int;
2808
	c_2:int;
2809
	idB_B1_2:int;
2810
	idB_B2_2:int;
2811
	idEvents1_B_2:int;
2812
	let
2813

    
2814
		
2815
	(idA_A2_2, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2) 
2816
	= A_A2_node(idA_A2_1, a_1, x, S, R1, S1, T1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R);
2817

    
2818
		
2819

    
2820

    
2821
	(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2822
	= (idEvents1_A_1, a_2, idA_A1_1, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2823
	
2824

    
2825
	tel
2826

    
2827
	until true restart POINTEvents1_A
2828

    
2829

    
2830

    
2831
	state A_A1_IDL:
2832

    
2833
	 var 	a_2:int;
2834
	idA_A1_2:int;
2835
	b_2:int;
2836
	c_2:int;
2837
	idB_B1_2:int;
2838
	idB_B2_2:int;
2839
	idEvents1_B_2:int;
2840
	let
2841

    
2842
		
2843
	(idA_A1_2, a_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2) 
2844
	= A_A1_node(idA_A1_1, a_1, x, S, R1, S1, T1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R);
2845

    
2846
		
2847

    
2848

    
2849
	(idEvents1_A, a, idA_A1, idA_A2, b, c, idB_B1, idB_B2, idEvents1_B) 
2850
	= (idEvents1_A_1, a_2, idA_A1_2, idA_A2_1, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2851
	
2852

    
2853
	tel
2854

    
2855
	until true restart POINTEvents1_A
2856

    
2857

    
2858

    
2859
tel
2860

    
2861

    
2862
--***************************************************State :Events1_Events1 Automaton***************************************************
2863

    
2864
node Events1_Events1_node(idEvents1_Events1_1:int;
2865
	a_1:int;
2866
	idA_A1_1:int;
2867
	idA_A2_1:int;
2868
	idEvents1_A_1:int;
2869
	x:int;
2870
	b_1:int;
2871
	idB_B1_1:int;
2872
	idB_B2_1:int;
2873
	idEvents1_B_1:int;
2874
	R:bool;
2875
	R1:bool;
2876
	S:bool;
2877
	S1:bool;
2878
	T:bool;
2879
	T1:bool;
2880
	c_1:int)
2881

    
2882
returns (idEvents1_Events1:int;
2883
	a:int;
2884
	idA_A1:int;
2885
	idA_A2:int;
2886
	idEvents1_A:int;
2887
	b:int;
2888
	idB_B1:int;
2889
	idB_B2:int;
2890
	idEvents1_B:int;
2891
	c:int);
2892

    
2893

    
2894
let
2895

    
2896
	 automaton events1_events1
2897

    
2898
	state POINTEvents1_Events1:
2899
	unless (idEvents1_Events1_1=0) restart EVENTS1_EVENTS1_PARALLEL_ENTRY
2900
	unless true  restart EVENTS1_EVENTS1_PARALLEL_IDL
2901

    
2902
	let
2903

    
2904
		(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B, c) 
2905
	= (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, b_1, idB_B1_1, idB_B2_1, idEvents1_B_1, c_1);
2906
	
2907

    
2908
	tel
2909

    
2910

    
2911

    
2912
	state EVENTS1_EVENTS1_PARALLEL_ENTRY:
2913

    
2914
	 var 	idEvents1_Events1_2, idEvents1_Events1_3:int;
2915
	a_2:int;
2916
	idA_A1_2:int;
2917
	idA_A2_2:int;
2918
	idEvents1_A_2:int;
2919
	b_2:int;
2920
	idB_B1_2:int;
2921
	idB_B2_2:int;
2922
	idEvents1_B_2:int;
2923
	let
2924

    
2925
		
2926
	(idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2) 
2927
	= Events1_A_en(idEvents1_A_1, idEvents1_Events1_1, a_1, idA_A1_1, x, idA_A2_1, false);
2928

    
2929
	(idEvents1_B_2, idEvents1_Events1_3, b_2, idB_B1_2, idB_B2_2) 
2930
	= Events1_B_en(idEvents1_B_1, idEvents1_Events1_2, b_1, idB_B1_1, x, idB_B2_1, false);
2931

    
2932

    
2933
	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B) 
2934
	= (idEvents1_Events1_3, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2);
2935
	
2936
	--add unused variables
2937
	(c) 
2938
	= (c_1);
2939
	
2940

    
2941
	tel
2942

    
2943
	until true restart POINTEvents1_Events1
2944

    
2945

    
2946

    
2947
	state EVENTS1_EVENTS1_PARALLEL_IDL:
2948

    
2949
	 var 	a_2:int;
2950
	idA_A1_2:int;
2951
	idA_A2_2:int;
2952
	idEvents1_A_2:int;
2953
	b_2, b_3:int;
2954
	idB_B1_2, idB_B1_3:int;
2955
	idB_B2_2, idB_B2_3:int;
2956
	idEvents1_B_2, idEvents1_B_3:int;
2957
	c_2, c_3:int;
2958
	let
2959

    
2960
		
2961

    
2962
		(idEvents1_A_2, a_2, idA_A1_2, idA_A2_2, b_2, c_2, idB_B1_2, idB_B2_2, idEvents1_B_2)
2963
	= if not (idEvents1_A_1= 0 ) then Events1_A_node(idEvents1_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R1, S1, T1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R, S)
2964

    
2965
		 else (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, idB_B1_1, idB_B2_1, idEvents1_B_1);
2966

    
2967
		
2968

    
2969
		
2970

    
2971
		(idEvents1_B_3, b_3, idB_B1_3, idB_B2_3, c_3)
2972
	= if not (idEvents1_B_2= 0 ) then Events1_B_node(idEvents1_B_2, b_2, idB_B1_2, x, T1, idB_B2_2, c_2, R1, S1)
2973

    
2974
		 else (idEvents1_B_2, b_2, idB_B1_2, idB_B2_2, c_2);
2975

    
2976
		
2977

    
2978
		
2979

    
2980
	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B, c) 
2981
	= (idEvents1_Events1_1, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, c_3);
2982
	
2983

    
2984
	tel
2985

    
2986
	until true restart POINTEvents1_Events1
2987

    
2988

    
2989

    
2990
tel
2991

    
2992

    
2993
--***************************************************State :Events1_Events1 Automaton***************************************************
2994

    
2995
node Events1_Events1(x:int;
2996
	R:bool;
2997
	S:bool;
2998
	T:bool)
2999

    
3000
returns (a:int;
3001
	b:int;
3002
	c:int);
3003

    
3004

    
3005
var a_1: int;
3006

    
3007
	b_1: int;
3008

    
3009
	c_1: int;
3010

    
3011
	R1, R1_1: bool;
3012

    
3013
	S1, S1_1: bool;
3014

    
3015
	T1, T1_1: bool;
3016

    
3017
	idEvents1_Events1, idEvents1_Events1_1: int;
3018

    
3019
	idB_B2, idB_B2_1: int;
3020

    
3021
	idB_B1, idB_B1_1: int;
3022

    
3023
	idEvents1_B, idEvents1_B_1: int;
3024

    
3025
	idA_A2, idA_A2_1: int;
3026

    
3027
	idA_A1, idA_A1_1: int;
3028

    
3029
	idEvents1_A, idEvents1_A_1: int;
3030

    
3031
		idEvents1_Events1_2, idEvents1_Events1_3:int;
3032
	a_2, a_3:int;
3033
	idA_A1_2, idA_A1_3:int;
3034
	idA_A2_2, idA_A2_3:int;
3035
	idEvents1_A_2, idEvents1_A_3:int;
3036
	b_2, b_3:int;
3037
	idB_B1_2, idB_B1_3:int;
3038
	idB_B2_2, idB_B2_3:int;
3039
	idEvents1_B_2, idEvents1_B_3:int;
3040
	c_2, c_3:int;
3041
let
3042

    
3043
	a_1 = 0 -> pre a;
3044

    
3045
	b_1 = 0 -> pre b;
3046

    
3047
	c_1 = 0 -> pre c;
3048

    
3049
	R1_1 = false -> pre R1;
3050

    
3051
	S1_1 = false -> pre S1;
3052

    
3053
	T1_1 = false -> pre T1;
3054

    
3055
	idEvents1_Events1_1 = 0 -> pre idEvents1_Events1;
3056

    
3057
	idB_B2_1 = 0 -> pre idB_B2;
3058

    
3059
	idB_B1_1 = 0 -> pre idB_B1;
3060

    
3061
	idEvents1_B_1 = 0 -> pre idEvents1_B;
3062

    
3063
	idA_A2_1 = 0 -> pre idA_A2;
3064

    
3065
	idA_A1_1 = 0 -> pre idA_A1;
3066

    
3067
	idEvents1_A_1 = 0 -> pre idEvents1_A;
3068

    
3069
	
3070

    
3071

    
3072

    
3073
	(idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2, c_2)
3074
	 = 
3075

    
3076
	 if R then Events1_Events1_node(idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, x, b_1, idB_B1_1, idB_B2_1, idEvents1_B_1, R, R1, false, S1, false, T1, c_1)
3077

    
3078
	 else (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, b_1, idB_B1_1, idB_B2_1, idEvents1_B_1, c_1);
3079

    
3080
	
3081

    
3082

    
3083

    
3084
	(idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, c_3)
3085
	 = 
3086

    
3087
	 if S then Events1_Events1_node(idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, x, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2, false, R1, S, S1, false, T1, c_2)
3088

    
3089
	 else (idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, b_2, idB_B1_2, idB_B2_2, idEvents1_B_2, c_2);
3090

    
3091
	
3092

    
3093

    
3094

    
3095
	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A, b, idB_B1, idB_B2, idEvents1_B, c)
3096
	 = 
3097

    
3098
	 if T then Events1_Events1_node(idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3, x, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, false, R1, false, S1, T, T1, c_3)
3099

    
3100
	 else (idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3, b_3, idB_B1_3, idB_B2_3, idEvents1_B_3, c_3);
3101

    
3102
	
3103

    
3104

    
3105
--unused outputs
3106
	R1 = false;
3107

    
3108
	S1 = false;
3109

    
3110
	T1 = false;
3111

    
3112
	
3113

    
3114
tel
3115

    
3116

    
3117

    
3118
node Events1 (x_1_1 : int; R_1_1 : real; S_1_1 : real; T_1_1 : real)
3119
returns (a_1_1 : int;
3120
	b_2_1 : int;
3121
	c_3_1 : int); 
3122
var
3123
	Events1_1_1 : int; Events1_2_1 : int; Events1_3_1 : int;
3124
	Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real;
3125
	i_virtual_local : real;
3126
	Events1Mux_1_1_event: bool;
3127
	Events1Mux_1_2_event: bool;
3128
	Events1Mux_1_3_event: bool;
3129
let 
3130
	Events1Mux_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));
3131
	Events1Mux_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));
3132
	Events1Mux_1_3_event = false -> ((pre(Mux_1_3) > 0.0 and Mux_1_3 <= 0.0) or (pre(Mux_1_3) <= 0.0 and Mux_1_3 > 0.0));
3133
	(Events1_1_1, Events1_2_1, Events1_3_1) =  Events1_Events1(x_1_1, Events1Mux_1_1_event, Events1Mux_1_2_event, Events1Mux_1_3_event);
3134
	Mux_1_1 = R_1_1 ;
3135
	Mux_1_2 = S_1_1 ;
3136
	Mux_1_3 = T_1_1 ;
3137
	a_1_1 = Events1_1_1;
3138
	b_2_1 = Events1_2_1;
3139
	c_3_1 = Events1_3_1;
3140
	i_virtual_local= 0.0 -> 1.0;
3141
tel
3142