Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Parallel3 / Parallel3.lus @ eb639349

History | View | Annotate | Download (69.3 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

    
20

    
21

    
22

    
23

    
24

    
25

    
26

    
27

    
28

    
29

    
30

    
31

    
32

    
33

    
34

    
35

    
36

    
37

    
38

    
39

    
40

    
41

    
42

    
43

    
44

    
45
-- Entry action for state :B2_B2a
46
node B2_B2a_en(idB_B2_1:int;
47
	x:int;
48
	b_1:int;
49
	isInner:bool)
50

    
51
returns (idB_B2:int;
52
	b:int);
53

    
54

    
55
var 	idB_B2_2:int;
56
	b_2:int;
57

    
58

    
59
let
60

    
61

    
62

    
63
	-- set state as active 
64
	idB_B2_2 
65
	= 1501;
66
	
67

    
68
	b_2 
69
	= if (not isInner) then x+7
70
	 else b_1;
71
	
72

    
73
	(idB_B2, b) 
74
	= (idB_B2_2, b_2);
75
	
76

    
77
tel
78

    
79

    
80

    
81

    
82

    
83
-- Exit action for state :B2_B2a
84
node B2_B2a_ex(idB_B2_1:int;
85
	isInner:bool)
86

    
87
returns (idB_B2:int);
88

    
89

    
90
var 	idB_B2_2:int;
91

    
92

    
93
let
94

    
95

    
96

    
97
	-- set state as inactive 
98
	idB_B2_2
99
	 = if (not isInner) then 0 else idB_B2_1;
100

    
101

    
102
	(idB_B2) 
103
	= (idB_B2_1);
104
	
105

    
106
tel
107

    
108

    
109

    
110

    
111

    
112

    
113
-- Entry action for state :B2_B2b
114
node B2_B2b_en(idB_B2_1:int;
115
	x:int;
116
	b_1:int;
117
	isInner:bool)
118

    
119
returns (idB_B2:int;
120
	b:int);
121

    
122

    
123
var 	idB_B2_2:int;
124
	b_2:int;
125

    
126

    
127
let
128

    
129

    
130

    
131
	-- set state as active 
132
	idB_B2_2 
133
	= 1502;
134
	
135

    
136
	b_2 
137
	= if (not isInner) then x+8
138
	 else b_1;
139
	
140

    
141
	(idB_B2, b) 
142
	= (idB_B2_2, b_2);
143
	
144

    
145
tel
146

    
147

    
148

    
149

    
150

    
151
-- Exit action for state :B2_B2b
152
node B2_B2b_ex(idB_B2_1:int;
153
	isInner:bool)
154

    
155
returns (idB_B2:int);
156

    
157

    
158
var 	idB_B2_2:int;
159

    
160

    
161
let
162

    
163

    
164

    
165
	-- set state as inactive 
166
	idB_B2_2
167
	 = if (not isInner) then 0 else idB_B2_1;
168

    
169

    
170
	(idB_B2) 
171
	= (idB_B2_1);
172
	
173

    
174
tel
175

    
176

    
177

    
178

    
179

    
180

    
181
-- Entry action for state :B_B2
182
node B_B2_en(idB_B2_1:int;
183
	idParallel3_B_1:int;
184
	b_1:int;
185
	x:int;
186
	isInner:bool)
187

    
188
returns (idB_B2:int;
189
	idParallel3_B:int;
190
	b:int);
191

    
192

    
193
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5, idB_B2_6:int;
194
	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4:int;
195
	b_2, b_3, b_4, b_5, b_6:int;
196

    
197

    
198
let
199

    
200

    
201

    
202
	-- set state as active 
203
	idParallel3_B_2 
204
	= 1500;
205
	
206

    
207
	
208
-- transition trace :
209
	--POINT__To__B2_B2a_1
210
		(idB_B2_2, b_2) 
211
	= B2_B2a_en(idB_B2_1, x, b_1, false);
212
		
213

    
214
	(idB_B2_3, idParallel3_B_3, b_3) 
215
	= 
216

    
217
	if ( idB_B2_1 = 0) then
218

    
219
	 (idB_B2_2, idParallel3_B_2, b_2)
220

    
221
	 else(idB_B2_1, idParallel3_B_2, b_1);
222

    
223
	
224

    
225
	(idB_B2_4, b_4) 
226
	= 
227
	if ( idB_B2_1 = 1501) then
228
	B2_B2a_en(idB_B2_1, x, b_1, false)
229
	 else (idB_B2_1, b_1);
230

    
231
	
232

    
233
	(idB_B2_5, b_5) 
234
	= 
235
	if ( idB_B2_1 = 1502) then
236
	B2_B2b_en(idB_B2_1, x, b_1, false)
237
	 else (idB_B2_1, b_1);
238

    
239
	
240

    
241
	(idB_B2_6, idParallel3_B_4, b_6) 
242
	= 
243
		 if ( idB_B2_1 = 0) then 
244
		(idB_B2_3, idParallel3_B_3, b_3)
245
		 else
246
		 if ( idB_B2_1 = 1501) then 
247
		(idB_B2_4, idParallel3_B_3, b_4)
248
		 else
249
		 if ( idB_B2_1 = 1502) then 
250
		(idB_B2_5, idParallel3_B_3, b_5)
251
		 else (idB_B2_1, idParallel3_B_2, b_1);
252

    
253

    
254
	(idB_B2, idParallel3_B, b) 
255
	= (idB_B2_6, idParallel3_B_4, b_6);
256
	
257

    
258
tel
259

    
260

    
261

    
262

    
263

    
264
-- Exit action for state :B_B2
265
node B_B2_ex(idB_B2_1:int;
266
	idParallel3_B_1:int;
267
	isInner:bool)
268

    
269
returns (idB_B2:int;
270
	idParallel3_B:int);
271

    
272

    
273
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5:int;
274
	idParallel3_B_2:int;
275

    
276

    
277
let
278

    
279

    
280

    
281
	
282
	(idB_B2_2) 
283
	= 
284
	if ( idB_B2_1 = 1501) then
285
	B2_B2a_ex(idB_B2_1, false)
286
	 else (idB_B2_1);
287

    
288
	
289

    
290
	(idB_B2_3) 
291
	= 
292
	if ( idB_B2_1 = 1502) then
293
	B2_B2b_ex(idB_B2_1, false)
294
	 else (idB_B2_1);
295

    
296
	
297

    
298
	(idB_B2_4) 
299
	= 
300
		 if ( idB_B2_1 = 1501) then 
301
		(idB_B2_2)
302
		 else
303
		 if ( idB_B2_1 = 1502) then 
304
		(idB_B2_3)
305
		 else (idB_B2_1);
306

    
307

    
308
	-- set state as inactive 
309
	idParallel3_B_2
310
	 = if (not isInner) then 0 else idParallel3_B_1;
311

    
312
	idB_B2_5 
313
	= 0;
314
	
315

    
316
	(idB_B2, idParallel3_B) 
317
	= (idB_B2_5, idParallel3_B_1);
318
	
319

    
320
tel
321

    
322

    
323

    
324

    
325

    
326

    
327
-- Entry action for state :B1_B1a
328
node B1_B1a_en(idB_B1_1:int;
329
	x:int;
330
	b_1:int;
331
	isInner:bool)
332

    
333
returns (idB_B1:int;
334
	b:int);
335

    
336

    
337
var 	idB_B1_2:int;
338
	b_2:int;
339

    
340

    
341
let
342

    
343

    
344

    
345
	-- set state as active 
346
	idB_B1_2 
347
	= 1504;
348
	
349

    
350
	b_2 
351
	= if (not isInner) then x+5
352
	 else b_1;
353
	
354

    
355
	(idB_B1, b) 
356
	= (idB_B1_2, b_2);
357
	
358

    
359
tel
360

    
361

    
362

    
363

    
364

    
365
-- Exit action for state :B1_B1a
366
node B1_B1a_ex(idB_B1_1:int;
367
	isInner:bool)
368

    
369
returns (idB_B1:int);
370

    
371

    
372
var 	idB_B1_2:int;
373

    
374

    
375
let
376

    
377

    
378

    
379
	-- set state as inactive 
380
	idB_B1_2
381
	 = if (not isInner) then 0 else idB_B1_1;
382

    
383

    
384
	(idB_B1) 
385
	= (idB_B1_1);
386
	
387

    
388
tel
389

    
390

    
391

    
392

    
393

    
394

    
395
-- Entry action for state :B1_B1b
396
node B1_B1b_en(idB_B1_1:int;
397
	x:int;
398
	b_1:int;
399
	isInner:bool)
400

    
401
returns (idB_B1:int;
402
	b:int);
403

    
404

    
405
var 	idB_B1_2:int;
406
	b_2:int;
407

    
408

    
409
let
410

    
411

    
412

    
413
	-- set state as active 
414
	idB_B1_2 
415
	= 1505;
416
	
417

    
418
	b_2 
419
	= if (not isInner) then x+6
420
	 else b_1;
421
	
422

    
423
	(idB_B1, b) 
424
	= (idB_B1_2, b_2);
425
	
426

    
427
tel
428

    
429

    
430

    
431

    
432

    
433
-- Exit action for state :B1_B1b
434
node B1_B1b_ex(idB_B1_1:int;
435
	isInner:bool)
436

    
437
returns (idB_B1:int);
438

    
439

    
440
var 	idB_B1_2:int;
441

    
442

    
443
let
444

    
445

    
446

    
447
	-- set state as inactive 
448
	idB_B1_2
449
	 = if (not isInner) then 0 else idB_B1_1;
450

    
451

    
452
	(idB_B1) 
453
	= (idB_B1_1);
454
	
455

    
456
tel
457

    
458

    
459

    
460

    
461

    
462

    
463
-- Entry action for state :B_B1
464
node B_B1_en(idB_B1_1:int;
465
	idParallel3_B_1:int;
466
	b_1:int;
467
	x:int;
468
	isInner:bool)
469

    
470
returns (idB_B1:int;
471
	idParallel3_B:int;
472
	b:int);
473

    
474

    
475
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5, idB_B1_6:int;
476
	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4:int;
477
	b_2, b_3, b_4, b_5, b_6:int;
478

    
479

    
480
let
481

    
482

    
483

    
484
	-- set state as active 
485
	idParallel3_B_2 
486
	= 1503;
487
	
488

    
489
	
490
-- transition trace :
491
	--POINT__To__B1_B1a_1
492
		(idB_B1_2, b_2) 
493
	= B1_B1a_en(idB_B1_1, x, b_1, false);
494
		
495

    
496
	(idB_B1_3, idParallel3_B_3, b_3) 
497
	= 
498

    
499
	if ( idB_B1_1 = 0) then
500

    
501
	 (idB_B1_2, idParallel3_B_2, b_2)
502

    
503
	 else(idB_B1_1, idParallel3_B_2, b_1);
504

    
505
	
506

    
507
	(idB_B1_4, b_4) 
508
	= 
509
	if ( idB_B1_1 = 1504) then
510
	B1_B1a_en(idB_B1_1, x, b_1, false)
511
	 else (idB_B1_1, b_1);
512

    
513
	
514

    
515
	(idB_B1_5, b_5) 
516
	= 
517
	if ( idB_B1_1 = 1505) then
518
	B1_B1b_en(idB_B1_1, x, b_1, false)
519
	 else (idB_B1_1, b_1);
520

    
521
	
522

    
523
	(idB_B1_6, idParallel3_B_4, b_6) 
524
	= 
525
		 if ( idB_B1_1 = 0) then 
526
		(idB_B1_3, idParallel3_B_3, b_3)
527
		 else
528
		 if ( idB_B1_1 = 1504) then 
529
		(idB_B1_4, idParallel3_B_3, b_4)
530
		 else
531
		 if ( idB_B1_1 = 1505) then 
532
		(idB_B1_5, idParallel3_B_3, b_5)
533
		 else (idB_B1_1, idParallel3_B_2, b_1);
534

    
535

    
536
	(idB_B1, idParallel3_B, b) 
537
	= (idB_B1_6, idParallel3_B_4, b_6);
538
	
539

    
540
tel
541

    
542

    
543

    
544

    
545

    
546
-- Exit action for state :B_B1
547
node B_B1_ex(idB_B1_1:int;
548
	idParallel3_B_1:int;
549
	isInner:bool)
550

    
551
returns (idB_B1:int;
552
	idParallel3_B:int);
553

    
554

    
555
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
556
	idParallel3_B_2:int;
557

    
558

    
559
let
560

    
561

    
562

    
563
	
564
	(idB_B1_2) 
565
	= 
566
	if ( idB_B1_1 = 1504) then
567
	B1_B1a_ex(idB_B1_1, false)
568
	 else (idB_B1_1);
569

    
570
	
571

    
572
	(idB_B1_3) 
573
	= 
574
	if ( idB_B1_1 = 1505) then
575
	B1_B1b_ex(idB_B1_1, false)
576
	 else (idB_B1_1);
577

    
578
	
579

    
580
	(idB_B1_4) 
581
	= 
582
		 if ( idB_B1_1 = 1504) then 
583
		(idB_B1_2)
584
		 else
585
		 if ( idB_B1_1 = 1505) then 
586
		(idB_B1_3)
587
		 else (idB_B1_1);
588

    
589

    
590
	-- set state as inactive 
591
	idParallel3_B_2
592
	 = if (not isInner) then 0 else idParallel3_B_1;
593

    
594
	idB_B1_5 
595
	= 0;
596
	
597

    
598
	(idB_B1, idParallel3_B) 
599
	= (idB_B1_5, idParallel3_B_1);
600
	
601

    
602
tel
603

    
604

    
605

    
606

    
607

    
608

    
609
-- Entry action for state :Parallel3_B
610
node Parallel3_B_en(idParallel3_B_1:int;
611
	idParallel3_Parallel3_1:int;
612
	b_1:int;
613
	idB_B1_1:int;
614
	x:int;
615
	idB_B2_1:int;
616
	isInner:bool)
617

    
618
returns (idParallel3_B:int;
619
	idParallel3_Parallel3:int;
620
	b:int;
621
	idB_B1:int;
622
	idB_B2:int);
623

    
624

    
625
var 	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4, idParallel3_B_5, idParallel3_B_6:int;
626
	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int;
627
	b_2, b_3, b_4, b_5, b_6:int;
628
	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
629
	idB_B2_2, idB_B2_3:int;
630

    
631

    
632
let
633

    
634

    
635

    
636
	-- set state as active 
637
	idParallel3_Parallel3_2 
638
	= 1499;
639
	
640

    
641
	
642
-- transition trace :
643
	--POINT__To__B_B1_1
644
		(idB_B1_2, idParallel3_B_2, b_2) 
645
	= B_B1_en(idB_B1_1, idParallel3_B_1, b_1, x, false);
646
		
647

    
648
	(idParallel3_B_3, idParallel3_Parallel3_3, b_3, idB_B1_3) 
649
	= 
650

    
651
	if ( idParallel3_B_1 = 0) then
652

    
653
	 (idParallel3_B_2, idParallel3_Parallel3_2, b_2, idB_B1_2)
654

    
655
	 else(idParallel3_B_1, idParallel3_Parallel3_2, b_1, idB_B1_1);
656

    
657
	
658

    
659
	(idB_B2_2, idParallel3_B_4, b_4) 
660
	= 
661
	if ( idParallel3_B_1 = 1500) then
662
	B_B2_en(idB_B2_1, idParallel3_B_1, b_1, x, false)
663
	 else (idB_B2_1, idParallel3_B_1, b_1);
664

    
665
	
666

    
667
	(idB_B1_4, idParallel3_B_5, b_5) 
668
	= 
669
	if ( idParallel3_B_1 = 1503) then
670
	B_B1_en(idB_B1_1, idParallel3_B_1, b_1, x, false)
671
	 else (idB_B1_1, idParallel3_B_1, b_1);
672

    
673
	
674

    
675
	(idParallel3_B_6, idParallel3_Parallel3_4, b_6, idB_B1_5, idB_B2_3) 
676
	= 
677
		 if ( idParallel3_B_1 = 0) then 
678
		(idParallel3_B_3, idParallel3_Parallel3_3, b_3, idB_B1_3, idB_B2_1)
679
		 else
680
		 if ( idParallel3_B_1 = 1500) then 
681
		(idParallel3_B_4, idParallel3_Parallel3_3, b_4, idB_B1_1, idB_B2_2)
682
		 else
683
		 if ( idParallel3_B_1 = 1503) then 
684
		(idParallel3_B_5, idParallel3_Parallel3_3, b_5, idB_B1_4, idB_B2_1)
685
		 else (idParallel3_B_1, idParallel3_Parallel3_2, b_1, idB_B1_1, idB_B2_1);
686

    
687

    
688
	(idParallel3_B, idParallel3_Parallel3, b, idB_B1, idB_B2) 
689
	= (idParallel3_B_6, idParallel3_Parallel3_4, b_6, idB_B1_5, idB_B2_3);
690
	
691

    
692
tel
693

    
694

    
695

    
696

    
697

    
698
-- Exit action for state :Parallel3_B
699
node Parallel3_B_ex(idB_B2_1:int;
700
	idParallel3_B_1:int;
701
	idB_B1_1:int;
702
	idParallel3_Parallel3_1:int;
703
	isInner:bool)
704

    
705
returns (idB_B2:int;
706
	idParallel3_B:int;
707
	idB_B1:int;
708
	idParallel3_Parallel3:int);
709

    
710

    
711
var 	idB_B2_2, idB_B2_3:int;
712
	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4, idParallel3_B_5:int;
713
	idB_B1_2, idB_B1_3:int;
714
	idParallel3_Parallel3_2:int;
715

    
716

    
717
let
718

    
719

    
720

    
721
	
722
	(idB_B2_2, idParallel3_B_2) 
723
	= 
724
	if ( idParallel3_B_1 = 1500) then
725
	B_B2_ex(idB_B2_1, idParallel3_B_1, false)
726
	 else (idB_B2_1, idParallel3_B_1);
727

    
728
	
729

    
730
	(idB_B1_2, idParallel3_B_3) 
731
	= 
732
	if ( idParallel3_B_1 = 1503) then
733
	B_B1_ex(idB_B1_1, idParallel3_B_1, false)
734
	 else (idB_B1_1, idParallel3_B_1);
735

    
736
	
737

    
738
	(idB_B2_3, idParallel3_B_4, idB_B1_3) 
739
	= 
740
		 if ( idParallel3_B_1 = 1500) then 
741
		(idB_B2_2, idParallel3_B_2, idB_B1_1)
742
		 else
743
		 if ( idParallel3_B_1 = 1503) then 
744
		(idB_B2_1, idParallel3_B_3, idB_B1_2)
745
		 else (idB_B2_1, idParallel3_B_1, idB_B1_1);
746

    
747

    
748
	-- set state as inactive 
749
	idParallel3_Parallel3_2
750
	 = if (not isInner) then 0 else idParallel3_Parallel3_1;
751

    
752
	idParallel3_B_5 
753
	= 0;
754
	
755

    
756
	(idB_B2, idParallel3_B, idB_B1, idParallel3_Parallel3) 
757
	= (idB_B2_3, idParallel3_B_5, idB_B1_3, idParallel3_Parallel3_1);
758
	
759

    
760
tel
761

    
762

    
763

    
764

    
765

    
766

    
767
-- Entry action for state :D2_D2a
768
node D2_D2a_en(idD_D2_1:int;
769
	y:int;
770
	dd_1:int;
771
	isInner:bool)
772

    
773
returns (idD_D2:int;
774
	dd:int);
775

    
776

    
777
var 	idD_D2_2:int;
778
	dd_2:int;
779

    
780

    
781
let
782

    
783

    
784

    
785
	-- set state as active 
786
	idD_D2_2 
787
	= 1515;
788
	
789

    
790
	dd_2 
791
	= if (not isInner) then y+7
792
	 else dd_1;
793
	
794

    
795
	(idD_D2, dd) 
796
	= (idD_D2_2, dd_2);
797
	
798

    
799
tel
800

    
801

    
802

    
803

    
804

    
805
-- Exit action for state :D2_D2a
806
node D2_D2a_ex(idD_D2_1:int;
807
	isInner:bool)
808

    
809
returns (idD_D2:int);
810

    
811

    
812
var 	idD_D2_2:int;
813

    
814

    
815
let
816

    
817

    
818

    
819
	-- set state as inactive 
820
	idD_D2_2
821
	 = if (not isInner) then 0 else idD_D2_1;
822

    
823

    
824
	(idD_D2) 
825
	= (idD_D2_1);
826
	
827

    
828
tel
829

    
830

    
831

    
832

    
833

    
834

    
835
-- Entry action for state :D2_D2b
836
node D2_D2b_en(idD_D2_1:int;
837
	y:int;
838
	dd_1:int;
839
	isInner:bool)
840

    
841
returns (idD_D2:int;
842
	dd:int);
843

    
844

    
845
var 	idD_D2_2:int;
846
	dd_2:int;
847

    
848

    
849
let
850

    
851

    
852

    
853
	-- set state as active 
854
	idD_D2_2 
855
	= 1516;
856
	
857

    
858
	dd_2 
859
	= if (not isInner) then y+8
860
	 else dd_1;
861
	
862

    
863
	(idD_D2, dd) 
864
	= (idD_D2_2, dd_2);
865
	
866

    
867
tel
868

    
869

    
870

    
871

    
872

    
873
-- Exit action for state :D2_D2b
874
node D2_D2b_ex(idD_D2_1:int;
875
	isInner:bool)
876

    
877
returns (idD_D2:int);
878

    
879

    
880
var 	idD_D2_2:int;
881

    
882

    
883
let
884

    
885

    
886

    
887
	-- set state as inactive 
888
	idD_D2_2
889
	 = if (not isInner) then 0 else idD_D2_1;
890

    
891

    
892
	(idD_D2) 
893
	= (idD_D2_1);
894
	
895

    
896
tel
897

    
898

    
899

    
900

    
901

    
902

    
903
-- Entry action for state :D_D2
904
node D_D2_en(idD_D2_1:int;
905
	idParallel3_D_1:int;
906
	dd_1:int;
907
	y:int;
908
	isInner:bool)
909

    
910
returns (idD_D2:int;
911
	idParallel3_D:int;
912
	dd:int);
913

    
914

    
915
var 	idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5, idD_D2_6:int;
916
	idParallel3_D_2, idParallel3_D_3, idParallel3_D_4:int;
917
	dd_2, dd_3, dd_4, dd_5, dd_6:int;
918

    
919

    
920
let
921

    
922

    
923

    
924
	-- set state as active 
925
	idParallel3_D_2 
926
	= 1514;
927
	
928

    
929
	
930
-- transition trace :
931
	--POINT__To__D2_D2a_1
932
		(idD_D2_2, dd_2) 
933
	= D2_D2a_en(idD_D2_1, y, dd_1, false);
934
		
935

    
936
	(idD_D2_3, idParallel3_D_3, dd_3) 
937
	= 
938

    
939
	if ( idD_D2_1 = 0) then
940

    
941
	 (idD_D2_2, idParallel3_D_2, dd_2)
942

    
943
	 else(idD_D2_1, idParallel3_D_2, dd_1);
944

    
945
	
946

    
947
	(idD_D2_4, dd_4) 
948
	= 
949
	if ( idD_D2_1 = 1515) then
950
	D2_D2a_en(idD_D2_1, y, dd_1, false)
951
	 else (idD_D2_1, dd_1);
952

    
953
	
954

    
955
	(idD_D2_5, dd_5) 
956
	= 
957
	if ( idD_D2_1 = 1516) then
958
	D2_D2b_en(idD_D2_1, y, dd_1, false)
959
	 else (idD_D2_1, dd_1);
960

    
961
	
962

    
963
	(idD_D2_6, idParallel3_D_4, dd_6) 
964
	= 
965
		 if ( idD_D2_1 = 0) then 
966
		(idD_D2_3, idParallel3_D_3, dd_3)
967
		 else
968
		 if ( idD_D2_1 = 1515) then 
969
		(idD_D2_4, idParallel3_D_3, dd_4)
970
		 else
971
		 if ( idD_D2_1 = 1516) then 
972
		(idD_D2_5, idParallel3_D_3, dd_5)
973
		 else (idD_D2_1, idParallel3_D_2, dd_1);
974

    
975

    
976
	(idD_D2, idParallel3_D, dd) 
977
	= (idD_D2_6, idParallel3_D_4, dd_6);
978
	
979

    
980
tel
981

    
982

    
983

    
984

    
985

    
986
-- Exit action for state :D_D2
987
node D_D2_ex(idD_D2_1:int;
988
	idParallel3_D_1:int;
989
	isInner:bool)
990

    
991
returns (idD_D2:int;
992
	idParallel3_D:int);
993

    
994

    
995
var 	idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5:int;
996
	idParallel3_D_2:int;
997

    
998

    
999
let
1000

    
1001

    
1002

    
1003
	
1004
	(idD_D2_2) 
1005
	= 
1006
	if ( idD_D2_1 = 1515) then
1007
	D2_D2a_ex(idD_D2_1, false)
1008
	 else (idD_D2_1);
1009

    
1010
	
1011

    
1012
	(idD_D2_3) 
1013
	= 
1014
	if ( idD_D2_1 = 1516) then
1015
	D2_D2b_ex(idD_D2_1, false)
1016
	 else (idD_D2_1);
1017

    
1018
	
1019

    
1020
	(idD_D2_4) 
1021
	= 
1022
		 if ( idD_D2_1 = 1515) then 
1023
		(idD_D2_2)
1024
		 else
1025
		 if ( idD_D2_1 = 1516) then 
1026
		(idD_D2_3)
1027
		 else (idD_D2_1);
1028

    
1029

    
1030
	-- set state as inactive 
1031
	idParallel3_D_2
1032
	 = if (not isInner) then 0 else idParallel3_D_1;
1033

    
1034
	idD_D2_5 
1035
	= 0;
1036
	
1037

    
1038
	(idD_D2, idParallel3_D) 
1039
	= (idD_D2_5, idParallel3_D_1);
1040
	
1041

    
1042
tel
1043

    
1044

    
1045

    
1046

    
1047

    
1048

    
1049
-- Entry action for state :D1_D1a
1050
node D1_D1a_en(idD_D1_1:int;
1051
	y:int;
1052
	dd_1:int;
1053
	isInner:bool)
1054

    
1055
returns (idD_D1:int;
1056
	dd:int);
1057

    
1058

    
1059
var 	idD_D1_2:int;
1060
	dd_2:int;
1061

    
1062

    
1063
let
1064

    
1065

    
1066

    
1067
	-- set state as active 
1068
	idD_D1_2 
1069
	= 1518;
1070
	
1071

    
1072
	dd_2 
1073
	= if (not isInner) then y+5
1074
	 else dd_1;
1075
	
1076

    
1077
	(idD_D1, dd) 
1078
	= (idD_D1_2, dd_2);
1079
	
1080

    
1081
tel
1082

    
1083

    
1084

    
1085

    
1086

    
1087
-- Exit action for state :D1_D1a
1088
node D1_D1a_ex(idD_D1_1:int;
1089
	isInner:bool)
1090

    
1091
returns (idD_D1:int);
1092

    
1093

    
1094
var 	idD_D1_2:int;
1095

    
1096

    
1097
let
1098

    
1099

    
1100

    
1101
	-- set state as inactive 
1102
	idD_D1_2
1103
	 = if (not isInner) then 0 else idD_D1_1;
1104

    
1105

    
1106
	(idD_D1) 
1107
	= (idD_D1_1);
1108
	
1109

    
1110
tel
1111

    
1112

    
1113

    
1114

    
1115

    
1116

    
1117
-- Entry action for state :D1_D1b
1118
node D1_D1b_en(idD_D1_1:int;
1119
	y:int;
1120
	dd_1:int;
1121
	isInner:bool)
1122

    
1123
returns (idD_D1:int;
1124
	dd:int);
1125

    
1126

    
1127
var 	idD_D1_2:int;
1128
	dd_2:int;
1129

    
1130

    
1131
let
1132

    
1133

    
1134

    
1135
	-- set state as active 
1136
	idD_D1_2 
1137
	= 1519;
1138
	
1139

    
1140
	dd_2 
1141
	= if (not isInner) then y+6
1142
	 else dd_1;
1143
	
1144

    
1145
	(idD_D1, dd) 
1146
	= (idD_D1_2, dd_2);
1147
	
1148

    
1149
tel
1150

    
1151

    
1152

    
1153

    
1154

    
1155
-- Exit action for state :D1_D1b
1156
node D1_D1b_ex(idD_D1_1:int;
1157
	isInner:bool)
1158

    
1159
returns (idD_D1:int);
1160

    
1161

    
1162
var 	idD_D1_2:int;
1163

    
1164

    
1165
let
1166

    
1167

    
1168

    
1169
	-- set state as inactive 
1170
	idD_D1_2
1171
	 = if (not isInner) then 0 else idD_D1_1;
1172

    
1173

    
1174
	(idD_D1) 
1175
	= (idD_D1_1);
1176
	
1177

    
1178
tel
1179

    
1180

    
1181

    
1182

    
1183

    
1184

    
1185
-- Entry action for state :D_D1
1186
node D_D1_en(idD_D1_1:int;
1187
	idParallel3_D_1:int;
1188
	dd_1:int;
1189
	y:int;
1190
	isInner:bool)
1191

    
1192
returns (idD_D1:int;
1193
	idParallel3_D:int;
1194
	dd:int);
1195

    
1196

    
1197
var 	idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5, idD_D1_6:int;
1198
	idParallel3_D_2, idParallel3_D_3, idParallel3_D_4:int;
1199
	dd_2, dd_3, dd_4, dd_5, dd_6:int;
1200

    
1201

    
1202
let
1203

    
1204

    
1205

    
1206
	-- set state as active 
1207
	idParallel3_D_2 
1208
	= 1517;
1209
	
1210

    
1211
	
1212
-- transition trace :
1213
	--POINT__To__D1_D1a_1
1214
		(idD_D1_2, dd_2) 
1215
	= D1_D1a_en(idD_D1_1, y, dd_1, false);
1216
		
1217

    
1218
	(idD_D1_3, idParallel3_D_3, dd_3) 
1219
	= 
1220

    
1221
	if ( idD_D1_1 = 0) then
1222

    
1223
	 (idD_D1_2, idParallel3_D_2, dd_2)
1224

    
1225
	 else(idD_D1_1, idParallel3_D_2, dd_1);
1226

    
1227
	
1228

    
1229
	(idD_D1_4, dd_4) 
1230
	= 
1231
	if ( idD_D1_1 = 1518) then
1232
	D1_D1a_en(idD_D1_1, y, dd_1, false)
1233
	 else (idD_D1_1, dd_1);
1234

    
1235
	
1236

    
1237
	(idD_D1_5, dd_5) 
1238
	= 
1239
	if ( idD_D1_1 = 1519) then
1240
	D1_D1b_en(idD_D1_1, y, dd_1, false)
1241
	 else (idD_D1_1, dd_1);
1242

    
1243
	
1244

    
1245
	(idD_D1_6, idParallel3_D_4, dd_6) 
1246
	= 
1247
		 if ( idD_D1_1 = 0) then 
1248
		(idD_D1_3, idParallel3_D_3, dd_3)
1249
		 else
1250
		 if ( idD_D1_1 = 1518) then 
1251
		(idD_D1_4, idParallel3_D_3, dd_4)
1252
		 else
1253
		 if ( idD_D1_1 = 1519) then 
1254
		(idD_D1_5, idParallel3_D_3, dd_5)
1255
		 else (idD_D1_1, idParallel3_D_2, dd_1);
1256

    
1257

    
1258
	(idD_D1, idParallel3_D, dd) 
1259
	= (idD_D1_6, idParallel3_D_4, dd_6);
1260
	
1261

    
1262
tel
1263

    
1264

    
1265

    
1266

    
1267

    
1268
-- Exit action for state :D_D1
1269
node D_D1_ex(idD_D1_1:int;
1270
	idParallel3_D_1:int;
1271
	isInner:bool)
1272

    
1273
returns (idD_D1:int;
1274
	idParallel3_D:int);
1275

    
1276

    
1277
var 	idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int;
1278
	idParallel3_D_2:int;
1279

    
1280

    
1281
let
1282

    
1283

    
1284

    
1285
	
1286
	(idD_D1_2) 
1287
	= 
1288
	if ( idD_D1_1 = 1518) then
1289
	D1_D1a_ex(idD_D1_1, false)
1290
	 else (idD_D1_1);
1291

    
1292
	
1293

    
1294
	(idD_D1_3) 
1295
	= 
1296
	if ( idD_D1_1 = 1519) then
1297
	D1_D1b_ex(idD_D1_1, false)
1298
	 else (idD_D1_1);
1299

    
1300
	
1301

    
1302
	(idD_D1_4) 
1303
	= 
1304
		 if ( idD_D1_1 = 1518) then 
1305
		(idD_D1_2)
1306
		 else
1307
		 if ( idD_D1_1 = 1519) then 
1308
		(idD_D1_3)
1309
		 else (idD_D1_1);
1310

    
1311

    
1312
	-- set state as inactive 
1313
	idParallel3_D_2
1314
	 = if (not isInner) then 0 else idParallel3_D_1;
1315

    
1316
	idD_D1_5 
1317
	= 0;
1318
	
1319

    
1320
	(idD_D1, idParallel3_D) 
1321
	= (idD_D1_5, idParallel3_D_1);
1322
	
1323

    
1324
tel
1325

    
1326

    
1327

    
1328

    
1329

    
1330

    
1331
-- Entry action for state :Parallel3_D
1332
node Parallel3_D_en(idParallel3_D_1:int;
1333
	idParallel3_Parallel3_1:int;
1334
	dd_1:int;
1335
	idD_D1_1:int;
1336
	y:int;
1337
	idD_D2_1:int;
1338
	isInner:bool)
1339

    
1340
returns (idParallel3_D:int;
1341
	idParallel3_Parallel3:int;
1342
	dd:int;
1343
	idD_D1:int;
1344
	idD_D2:int);
1345

    
1346

    
1347
var 	idParallel3_D_2, idParallel3_D_3, idParallel3_D_4, idParallel3_D_5, idParallel3_D_6:int;
1348
	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int;
1349
	dd_2, dd_3, dd_4, dd_5, dd_6:int;
1350
	idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int;
1351
	idD_D2_2, idD_D2_3:int;
1352

    
1353

    
1354
let
1355

    
1356

    
1357

    
1358
	-- set state as active 
1359
	idParallel3_Parallel3_2 
1360
	= 1513;
1361
	
1362

    
1363
	
1364
-- transition trace :
1365
	--POINT__To__D_D1_1
1366
		(idD_D1_2, idParallel3_D_2, dd_2) 
1367
	= D_D1_en(idD_D1_1, idParallel3_D_1, dd_1, y, false);
1368
		
1369

    
1370
	(idParallel3_D_3, idParallel3_Parallel3_3, dd_3, idD_D1_3) 
1371
	= 
1372

    
1373
	if ( idParallel3_D_1 = 0) then
1374

    
1375
	 (idParallel3_D_2, idParallel3_Parallel3_2, dd_2, idD_D1_2)
1376

    
1377
	 else(idParallel3_D_1, idParallel3_Parallel3_2, dd_1, idD_D1_1);
1378

    
1379
	
1380

    
1381
	(idD_D2_2, idParallel3_D_4, dd_4) 
1382
	= 
1383
	if ( idParallel3_D_1 = 1514) then
1384
	D_D2_en(idD_D2_1, idParallel3_D_1, dd_1, y, false)
1385
	 else (idD_D2_1, idParallel3_D_1, dd_1);
1386

    
1387
	
1388

    
1389
	(idD_D1_4, idParallel3_D_5, dd_5) 
1390
	= 
1391
	if ( idParallel3_D_1 = 1517) then
1392
	D_D1_en(idD_D1_1, idParallel3_D_1, dd_1, y, false)
1393
	 else (idD_D1_1, idParallel3_D_1, dd_1);
1394

    
1395
	
1396

    
1397
	(idParallel3_D_6, idParallel3_Parallel3_4, dd_6, idD_D1_5, idD_D2_3) 
1398
	= 
1399
		 if ( idParallel3_D_1 = 0) then 
1400
		(idParallel3_D_3, idParallel3_Parallel3_3, dd_3, idD_D1_3, idD_D2_1)
1401
		 else
1402
		 if ( idParallel3_D_1 = 1514) then 
1403
		(idParallel3_D_4, idParallel3_Parallel3_3, dd_4, idD_D1_1, idD_D2_2)
1404
		 else
1405
		 if ( idParallel3_D_1 = 1517) then 
1406
		(idParallel3_D_5, idParallel3_Parallel3_3, dd_5, idD_D1_4, idD_D2_1)
1407
		 else (idParallel3_D_1, idParallel3_Parallel3_2, dd_1, idD_D1_1, idD_D2_1);
1408

    
1409

    
1410
	(idParallel3_D, idParallel3_Parallel3, dd, idD_D1, idD_D2) 
1411
	= (idParallel3_D_6, idParallel3_Parallel3_4, dd_6, idD_D1_5, idD_D2_3);
1412
	
1413

    
1414
tel
1415

    
1416

    
1417

    
1418

    
1419

    
1420
-- Exit action for state :Parallel3_D
1421
node Parallel3_D_ex(idD_D2_1:int;
1422
	idParallel3_D_1:int;
1423
	idD_D1_1:int;
1424
	idParallel3_Parallel3_1:int;
1425
	isInner:bool)
1426

    
1427
returns (idD_D2:int;
1428
	idParallel3_D:int;
1429
	idD_D1:int;
1430
	idParallel3_Parallel3:int);
1431

    
1432

    
1433
var 	idD_D2_2, idD_D2_3:int;
1434
	idParallel3_D_2, idParallel3_D_3, idParallel3_D_4, idParallel3_D_5:int;
1435
	idD_D1_2, idD_D1_3:int;
1436
	idParallel3_Parallel3_2:int;
1437

    
1438

    
1439
let
1440

    
1441

    
1442

    
1443
	
1444
	(idD_D2_2, idParallel3_D_2) 
1445
	= 
1446
	if ( idParallel3_D_1 = 1514) then
1447
	D_D2_ex(idD_D2_1, idParallel3_D_1, false)
1448
	 else (idD_D2_1, idParallel3_D_1);
1449

    
1450
	
1451

    
1452
	(idD_D1_2, idParallel3_D_3) 
1453
	= 
1454
	if ( idParallel3_D_1 = 1517) then
1455
	D_D1_ex(idD_D1_1, idParallel3_D_1, false)
1456
	 else (idD_D1_1, idParallel3_D_1);
1457

    
1458
	
1459

    
1460
	(idD_D2_3, idParallel3_D_4, idD_D1_3) 
1461
	= 
1462
		 if ( idParallel3_D_1 = 1514) then 
1463
		(idD_D2_2, idParallel3_D_2, idD_D1_1)
1464
		 else
1465
		 if ( idParallel3_D_1 = 1517) then 
1466
		(idD_D2_1, idParallel3_D_3, idD_D1_2)
1467
		 else (idD_D2_1, idParallel3_D_1, idD_D1_1);
1468

    
1469

    
1470
	-- set state as inactive 
1471
	idParallel3_Parallel3_2
1472
	 = if (not isInner) then 0 else idParallel3_Parallel3_1;
1473

    
1474
	idParallel3_D_5 
1475
	= 0;
1476
	
1477

    
1478
	(idD_D2, idParallel3_D, idD_D1, idParallel3_Parallel3) 
1479
	= (idD_D2_3, idParallel3_D_5, idD_D1_3, idParallel3_Parallel3_1);
1480
	
1481

    
1482
tel
1483

    
1484

    
1485

    
1486

    
1487

    
1488

    
1489
-- Entry action for state :C2_C2a
1490
node C2_C2a_en(idC_C2_1:int;
1491
	y:int;
1492
	c_1:int;
1493
	isInner:bool)
1494

    
1495
returns (idC_C2:int;
1496
	c:int);
1497

    
1498

    
1499
var 	idC_C2_2:int;
1500
	c_2:int;
1501

    
1502

    
1503
let
1504

    
1505

    
1506

    
1507
	-- set state as active 
1508
	idC_C2_2 
1509
	= 1508;
1510
	
1511

    
1512
	c_2 
1513
	= if (not isInner) then y+3
1514
	 else c_1;
1515
	
1516

    
1517
	(idC_C2, c) 
1518
	= (idC_C2_2, c_2);
1519
	
1520

    
1521
tel
1522

    
1523

    
1524

    
1525

    
1526

    
1527
-- Exit action for state :C2_C2a
1528
node C2_C2a_ex(idC_C2_1:int;
1529
	isInner:bool)
1530

    
1531
returns (idC_C2:int);
1532

    
1533

    
1534
var 	idC_C2_2:int;
1535

    
1536

    
1537
let
1538

    
1539

    
1540

    
1541
	-- set state as inactive 
1542
	idC_C2_2
1543
	 = if (not isInner) then 0 else idC_C2_1;
1544

    
1545

    
1546
	(idC_C2) 
1547
	= (idC_C2_1);
1548
	
1549

    
1550
tel
1551

    
1552

    
1553

    
1554

    
1555

    
1556

    
1557
-- Entry action for state :C2_C2b
1558
node C2_C2b_en(idC_C2_1:int;
1559
	y:int;
1560
	c_1:int;
1561
	isInner:bool)
1562

    
1563
returns (idC_C2:int;
1564
	c:int);
1565

    
1566

    
1567
var 	idC_C2_2:int;
1568
	c_2:int;
1569

    
1570

    
1571
let
1572

    
1573

    
1574

    
1575
	-- set state as active 
1576
	idC_C2_2 
1577
	= 1509;
1578
	
1579

    
1580
	c_2 
1581
	= if (not isInner) then y+4
1582
	 else c_1;
1583
	
1584

    
1585
	(idC_C2, c) 
1586
	= (idC_C2_2, c_2);
1587
	
1588

    
1589
tel
1590

    
1591

    
1592

    
1593

    
1594

    
1595
-- Exit action for state :C2_C2b
1596
node C2_C2b_ex(idC_C2_1:int;
1597
	isInner:bool)
1598

    
1599
returns (idC_C2:int);
1600

    
1601

    
1602
var 	idC_C2_2:int;
1603

    
1604

    
1605
let
1606

    
1607

    
1608

    
1609
	-- set state as inactive 
1610
	idC_C2_2
1611
	 = if (not isInner) then 0 else idC_C2_1;
1612

    
1613

    
1614
	(idC_C2) 
1615
	= (idC_C2_1);
1616
	
1617

    
1618
tel
1619

    
1620

    
1621

    
1622

    
1623

    
1624

    
1625
-- Entry action for state :C_C2
1626
node C_C2_en(idC_C2_1:int;
1627
	idParallel3_C_1:int;
1628
	c_1:int;
1629
	y:int;
1630
	isInner:bool)
1631

    
1632
returns (idC_C2:int;
1633
	idParallel3_C:int;
1634
	c:int);
1635

    
1636

    
1637
var 	idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5, idC_C2_6:int;
1638
	idParallel3_C_2, idParallel3_C_3, idParallel3_C_4:int;
1639
	c_2, c_3, c_4, c_5, c_6:int;
1640

    
1641

    
1642
let
1643

    
1644

    
1645

    
1646
	-- set state as active 
1647
	idParallel3_C_2 
1648
	= 1507;
1649
	
1650

    
1651
	
1652
-- transition trace :
1653
	--POINT__To__C2_C2a_1
1654
		(idC_C2_2, c_2) 
1655
	= C2_C2a_en(idC_C2_1, y, c_1, false);
1656
		
1657

    
1658
	(idC_C2_3, idParallel3_C_3, c_3) 
1659
	= 
1660

    
1661
	if ( idC_C2_1 = 0) then
1662

    
1663
	 (idC_C2_2, idParallel3_C_2, c_2)
1664

    
1665
	 else(idC_C2_1, idParallel3_C_2, c_1);
1666

    
1667
	
1668

    
1669
	(idC_C2_4, c_4) 
1670
	= 
1671
	if ( idC_C2_1 = 1508) then
1672
	C2_C2a_en(idC_C2_1, y, c_1, false)
1673
	 else (idC_C2_1, c_1);
1674

    
1675
	
1676

    
1677
	(idC_C2_5, c_5) 
1678
	= 
1679
	if ( idC_C2_1 = 1509) then
1680
	C2_C2b_en(idC_C2_1, y, c_1, false)
1681
	 else (idC_C2_1, c_1);
1682

    
1683
	
1684

    
1685
	(idC_C2_6, idParallel3_C_4, c_6) 
1686
	= 
1687
		 if ( idC_C2_1 = 0) then 
1688
		(idC_C2_3, idParallel3_C_3, c_3)
1689
		 else
1690
		 if ( idC_C2_1 = 1508) then 
1691
		(idC_C2_4, idParallel3_C_3, c_4)
1692
		 else
1693
		 if ( idC_C2_1 = 1509) then 
1694
		(idC_C2_5, idParallel3_C_3, c_5)
1695
		 else (idC_C2_1, idParallel3_C_2, c_1);
1696

    
1697

    
1698
	(idC_C2, idParallel3_C, c) 
1699
	= (idC_C2_6, idParallel3_C_4, c_6);
1700
	
1701

    
1702
tel
1703

    
1704

    
1705

    
1706

    
1707

    
1708
-- Exit action for state :C_C2
1709
node C_C2_ex(idC_C2_1:int;
1710
	idParallel3_C_1:int;
1711
	isInner:bool)
1712

    
1713
returns (idC_C2:int;
1714
	idParallel3_C:int);
1715

    
1716

    
1717
var 	idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5:int;
1718
	idParallel3_C_2:int;
1719

    
1720

    
1721
let
1722

    
1723

    
1724

    
1725
	
1726
	(idC_C2_2) 
1727
	= 
1728
	if ( idC_C2_1 = 1508) then
1729
	C2_C2a_ex(idC_C2_1, false)
1730
	 else (idC_C2_1);
1731

    
1732
	
1733

    
1734
	(idC_C2_3) 
1735
	= 
1736
	if ( idC_C2_1 = 1509) then
1737
	C2_C2b_ex(idC_C2_1, false)
1738
	 else (idC_C2_1);
1739

    
1740
	
1741

    
1742
	(idC_C2_4) 
1743
	= 
1744
		 if ( idC_C2_1 = 1508) then 
1745
		(idC_C2_2)
1746
		 else
1747
		 if ( idC_C2_1 = 1509) then 
1748
		(idC_C2_3)
1749
		 else (idC_C2_1);
1750

    
1751

    
1752
	-- set state as inactive 
1753
	idParallel3_C_2
1754
	 = if (not isInner) then 0 else idParallel3_C_1;
1755

    
1756
	idC_C2_5 
1757
	= 0;
1758
	
1759

    
1760
	(idC_C2, idParallel3_C) 
1761
	= (idC_C2_5, idParallel3_C_1);
1762
	
1763

    
1764
tel
1765

    
1766

    
1767

    
1768

    
1769

    
1770

    
1771
-- Entry action for state :C1_C1a
1772
node C1_C1a_en(idC_C1_1:int;
1773
	y:int;
1774
	c_1:int;
1775
	isInner:bool)
1776

    
1777
returns (idC_C1:int;
1778
	c:int);
1779

    
1780

    
1781
var 	idC_C1_2:int;
1782
	c_2:int;
1783

    
1784

    
1785
let
1786

    
1787

    
1788

    
1789
	-- set state as active 
1790
	idC_C1_2 
1791
	= 1511;
1792
	
1793

    
1794
	c_2 
1795
	= if (not isInner) then y+1
1796
	 else c_1;
1797
	
1798

    
1799
	(idC_C1, c) 
1800
	= (idC_C1_2, c_2);
1801
	
1802

    
1803
tel
1804

    
1805

    
1806

    
1807

    
1808

    
1809
-- Exit action for state :C1_C1a
1810
node C1_C1a_ex(idC_C1_1:int;
1811
	isInner:bool)
1812

    
1813
returns (idC_C1:int);
1814

    
1815

    
1816
var 	idC_C1_2:int;
1817

    
1818

    
1819
let
1820

    
1821

    
1822

    
1823
	-- set state as inactive 
1824
	idC_C1_2
1825
	 = if (not isInner) then 0 else idC_C1_1;
1826

    
1827

    
1828
	(idC_C1) 
1829
	= (idC_C1_1);
1830
	
1831

    
1832
tel
1833

    
1834

    
1835

    
1836

    
1837

    
1838

    
1839
-- Entry action for state :C1_C1b
1840
node C1_C1b_en(idC_C1_1:int;
1841
	y:int;
1842
	c_1:int;
1843
	isInner:bool)
1844

    
1845
returns (idC_C1:int;
1846
	c:int);
1847

    
1848

    
1849
var 	idC_C1_2:int;
1850
	c_2:int;
1851

    
1852

    
1853
let
1854

    
1855

    
1856

    
1857
	-- set state as active 
1858
	idC_C1_2 
1859
	= 1512;
1860
	
1861

    
1862
	c_2 
1863
	= if (not isInner) then y+2
1864
	 else c_1;
1865
	
1866

    
1867
	(idC_C1, c) 
1868
	= (idC_C1_2, c_2);
1869
	
1870

    
1871
tel
1872

    
1873

    
1874

    
1875

    
1876

    
1877
-- Exit action for state :C1_C1b
1878
node C1_C1b_ex(idC_C1_1:int;
1879
	isInner:bool)
1880

    
1881
returns (idC_C1:int);
1882

    
1883

    
1884
var 	idC_C1_2:int;
1885

    
1886

    
1887
let
1888

    
1889

    
1890

    
1891
	-- set state as inactive 
1892
	idC_C1_2
1893
	 = if (not isInner) then 0 else idC_C1_1;
1894

    
1895

    
1896
	(idC_C1) 
1897
	= (idC_C1_1);
1898
	
1899

    
1900
tel
1901

    
1902

    
1903

    
1904

    
1905

    
1906

    
1907
-- Entry action for state :C_C1
1908
node C_C1_en(idC_C1_1:int;
1909
	idParallel3_C_1:int;
1910
	c_1:int;
1911
	y:int;
1912
	isInner:bool)
1913

    
1914
returns (idC_C1:int;
1915
	idParallel3_C:int;
1916
	c:int);
1917

    
1918

    
1919
var 	idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5, idC_C1_6:int;
1920
	idParallel3_C_2, idParallel3_C_3, idParallel3_C_4:int;
1921
	c_2, c_3, c_4, c_5, c_6:int;
1922

    
1923

    
1924
let
1925

    
1926

    
1927

    
1928
	-- set state as active 
1929
	idParallel3_C_2 
1930
	= 1510;
1931
	
1932

    
1933
	
1934
-- transition trace :
1935
	--POINT__To__C1_C1a_1
1936
		(idC_C1_2, c_2) 
1937
	= C1_C1a_en(idC_C1_1, y, c_1, false);
1938
		
1939

    
1940
	(idC_C1_3, idParallel3_C_3, c_3) 
1941
	= 
1942

    
1943
	if ( idC_C1_1 = 0) then
1944

    
1945
	 (idC_C1_2, idParallel3_C_2, c_2)
1946

    
1947
	 else(idC_C1_1, idParallel3_C_2, c_1);
1948

    
1949
	
1950

    
1951
	(idC_C1_4, c_4) 
1952
	= 
1953
	if ( idC_C1_1 = 1511) then
1954
	C1_C1a_en(idC_C1_1, y, c_1, false)
1955
	 else (idC_C1_1, c_1);
1956

    
1957
	
1958

    
1959
	(idC_C1_5, c_5) 
1960
	= 
1961
	if ( idC_C1_1 = 1512) then
1962
	C1_C1b_en(idC_C1_1, y, c_1, false)
1963
	 else (idC_C1_1, c_1);
1964

    
1965
	
1966

    
1967
	(idC_C1_6, idParallel3_C_4, c_6) 
1968
	= 
1969
		 if ( idC_C1_1 = 0) then 
1970
		(idC_C1_3, idParallel3_C_3, c_3)
1971
		 else
1972
		 if ( idC_C1_1 = 1511) then 
1973
		(idC_C1_4, idParallel3_C_3, c_4)
1974
		 else
1975
		 if ( idC_C1_1 = 1512) then 
1976
		(idC_C1_5, idParallel3_C_3, c_5)
1977
		 else (idC_C1_1, idParallel3_C_2, c_1);
1978

    
1979

    
1980
	(idC_C1, idParallel3_C, c) 
1981
	= (idC_C1_6, idParallel3_C_4, c_6);
1982
	
1983

    
1984
tel
1985

    
1986

    
1987

    
1988

    
1989

    
1990
-- Exit action for state :C_C1
1991
node C_C1_ex(idC_C1_1:int;
1992
	idParallel3_C_1:int;
1993
	isInner:bool)
1994

    
1995
returns (idC_C1:int;
1996
	idParallel3_C:int);
1997

    
1998

    
1999
var 	idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int;
2000
	idParallel3_C_2:int;
2001

    
2002

    
2003
let
2004

    
2005

    
2006

    
2007
	
2008
	(idC_C1_2) 
2009
	= 
2010
	if ( idC_C1_1 = 1511) then
2011
	C1_C1a_ex(idC_C1_1, false)
2012
	 else (idC_C1_1);
2013

    
2014
	
2015

    
2016
	(idC_C1_3) 
2017
	= 
2018
	if ( idC_C1_1 = 1512) then
2019
	C1_C1b_ex(idC_C1_1, false)
2020
	 else (idC_C1_1);
2021

    
2022
	
2023

    
2024
	(idC_C1_4) 
2025
	= 
2026
		 if ( idC_C1_1 = 1511) then 
2027
		(idC_C1_2)
2028
		 else
2029
		 if ( idC_C1_1 = 1512) then 
2030
		(idC_C1_3)
2031
		 else (idC_C1_1);
2032

    
2033

    
2034
	-- set state as inactive 
2035
	idParallel3_C_2
2036
	 = if (not isInner) then 0 else idParallel3_C_1;
2037

    
2038
	idC_C1_5 
2039
	= 0;
2040
	
2041

    
2042
	(idC_C1, idParallel3_C) 
2043
	= (idC_C1_5, idParallel3_C_1);
2044
	
2045

    
2046
tel
2047

    
2048

    
2049

    
2050

    
2051

    
2052

    
2053
-- Entry action for state :Parallel3_C
2054
node Parallel3_C_en(idParallel3_C_1:int;
2055
	idParallel3_Parallel3_1:int;
2056
	c_1:int;
2057
	idC_C1_1:int;
2058
	y:int;
2059
	idC_C2_1:int;
2060
	isInner:bool)
2061

    
2062
returns (idParallel3_C:int;
2063
	idParallel3_Parallel3:int;
2064
	c:int;
2065
	idC_C1:int;
2066
	idC_C2:int);
2067

    
2068

    
2069
var 	idParallel3_C_2, idParallel3_C_3, idParallel3_C_4, idParallel3_C_5, idParallel3_C_6:int;
2070
	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int;
2071
	c_2, c_3, c_4, c_5, c_6:int;
2072
	idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int;
2073
	idC_C2_2, idC_C2_3:int;
2074

    
2075

    
2076
let
2077

    
2078

    
2079

    
2080
	-- set state as active 
2081
	idParallel3_Parallel3_2 
2082
	= 1506;
2083
	
2084

    
2085
	
2086
-- transition trace :
2087
	--POINT__To__C_C1_1
2088
		(idC_C1_2, idParallel3_C_2, c_2) 
2089
	= C_C1_en(idC_C1_1, idParallel3_C_1, c_1, y, false);
2090
		
2091

    
2092
	(idParallel3_C_3, idParallel3_Parallel3_3, c_3, idC_C1_3) 
2093
	= 
2094

    
2095
	if ( idParallel3_C_1 = 0) then
2096

    
2097
	 (idParallel3_C_2, idParallel3_Parallel3_2, c_2, idC_C1_2)
2098

    
2099
	 else(idParallel3_C_1, idParallel3_Parallel3_2, c_1, idC_C1_1);
2100

    
2101
	
2102

    
2103
	(idC_C2_2, idParallel3_C_4, c_4) 
2104
	= 
2105
	if ( idParallel3_C_1 = 1507) then
2106
	C_C2_en(idC_C2_1, idParallel3_C_1, c_1, y, false)
2107
	 else (idC_C2_1, idParallel3_C_1, c_1);
2108

    
2109
	
2110

    
2111
	(idC_C1_4, idParallel3_C_5, c_5) 
2112
	= 
2113
	if ( idParallel3_C_1 = 1510) then
2114
	C_C1_en(idC_C1_1, idParallel3_C_1, c_1, y, false)
2115
	 else (idC_C1_1, idParallel3_C_1, c_1);
2116

    
2117
	
2118

    
2119
	(idParallel3_C_6, idParallel3_Parallel3_4, c_6, idC_C1_5, idC_C2_3) 
2120
	= 
2121
		 if ( idParallel3_C_1 = 0) then 
2122
		(idParallel3_C_3, idParallel3_Parallel3_3, c_3, idC_C1_3, idC_C2_1)
2123
		 else
2124
		 if ( idParallel3_C_1 = 1507) then 
2125
		(idParallel3_C_4, idParallel3_Parallel3_3, c_4, idC_C1_1, idC_C2_2)
2126
		 else
2127
		 if ( idParallel3_C_1 = 1510) then 
2128
		(idParallel3_C_5, idParallel3_Parallel3_3, c_5, idC_C1_4, idC_C2_1)
2129
		 else (idParallel3_C_1, idParallel3_Parallel3_2, c_1, idC_C1_1, idC_C2_1);
2130

    
2131

    
2132
	(idParallel3_C, idParallel3_Parallel3, c, idC_C1, idC_C2) 
2133
	= (idParallel3_C_6, idParallel3_Parallel3_4, c_6, idC_C1_5, idC_C2_3);
2134
	
2135

    
2136
tel
2137

    
2138

    
2139

    
2140

    
2141

    
2142
-- Exit action for state :Parallel3_C
2143
node Parallel3_C_ex(idC_C2_1:int;
2144
	idParallel3_C_1:int;
2145
	idC_C1_1:int;
2146
	idParallel3_Parallel3_1:int;
2147
	isInner:bool)
2148

    
2149
returns (idC_C2:int;
2150
	idParallel3_C:int;
2151
	idC_C1:int;
2152
	idParallel3_Parallel3:int);
2153

    
2154

    
2155
var 	idC_C2_2, idC_C2_3:int;
2156
	idParallel3_C_2, idParallel3_C_3, idParallel3_C_4, idParallel3_C_5:int;
2157
	idC_C1_2, idC_C1_3:int;
2158
	idParallel3_Parallel3_2:int;
2159

    
2160

    
2161
let
2162

    
2163

    
2164

    
2165
	
2166
	(idC_C2_2, idParallel3_C_2) 
2167
	= 
2168
	if ( idParallel3_C_1 = 1507) then
2169
	C_C2_ex(idC_C2_1, idParallel3_C_1, false)
2170
	 else (idC_C2_1, idParallel3_C_1);
2171

    
2172
	
2173

    
2174
	(idC_C1_2, idParallel3_C_3) 
2175
	= 
2176
	if ( idParallel3_C_1 = 1510) then
2177
	C_C1_ex(idC_C1_1, idParallel3_C_1, false)
2178
	 else (idC_C1_1, idParallel3_C_1);
2179

    
2180
	
2181

    
2182
	(idC_C2_3, idParallel3_C_4, idC_C1_3) 
2183
	= 
2184
		 if ( idParallel3_C_1 = 1507) then 
2185
		(idC_C2_2, idParallel3_C_2, idC_C1_1)
2186
		 else
2187
		 if ( idParallel3_C_1 = 1510) then 
2188
		(idC_C2_1, idParallel3_C_3, idC_C1_2)
2189
		 else (idC_C2_1, idParallel3_C_1, idC_C1_1);
2190

    
2191

    
2192
	-- set state as inactive 
2193
	idParallel3_Parallel3_2
2194
	 = if (not isInner) then 0 else idParallel3_Parallel3_1;
2195

    
2196
	idParallel3_C_5 
2197
	= 0;
2198
	
2199

    
2200
	(idC_C2, idParallel3_C, idC_C1, idParallel3_Parallel3) 
2201
	= (idC_C2_3, idParallel3_C_5, idC_C1_3, idParallel3_Parallel3_1);
2202
	
2203

    
2204
tel
2205

    
2206

    
2207

    
2208

    
2209

    
2210

    
2211
-- Entry action for state :A2_A2a
2212
node A2_A2a_en(idA_A2_1:int;
2213
	x:int;
2214
	a_1:int;
2215
	isInner:bool)
2216

    
2217
returns (idA_A2:int;
2218
	a:int);
2219

    
2220

    
2221
var 	idA_A2_2:int;
2222
	a_2:int;
2223

    
2224

    
2225
let
2226

    
2227

    
2228

    
2229
	-- set state as active 
2230
	idA_A2_2 
2231
	= 1497;
2232
	
2233

    
2234
	a_2 
2235
	= if (not isInner) then x+3
2236
	 else a_1;
2237
	
2238

    
2239
	(idA_A2, a) 
2240
	= (idA_A2_2, a_2);
2241
	
2242

    
2243
tel
2244

    
2245

    
2246

    
2247

    
2248

    
2249
-- Exit action for state :A2_A2a
2250
node A2_A2a_ex(idA_A2_1:int;
2251
	isInner:bool)
2252

    
2253
returns (idA_A2:int);
2254

    
2255

    
2256
var 	idA_A2_2:int;
2257

    
2258

    
2259
let
2260

    
2261

    
2262

    
2263
	-- set state as inactive 
2264
	idA_A2_2
2265
	 = if (not isInner) then 0 else idA_A2_1;
2266

    
2267

    
2268
	(idA_A2) 
2269
	= (idA_A2_1);
2270
	
2271

    
2272
tel
2273

    
2274

    
2275

    
2276

    
2277

    
2278

    
2279
-- Entry action for state :A2_A2b
2280
node A2_A2b_en(idA_A2_1:int;
2281
	x:int;
2282
	a_1:int;
2283
	isInner:bool)
2284

    
2285
returns (idA_A2:int;
2286
	a:int);
2287

    
2288

    
2289
var 	idA_A2_2:int;
2290
	a_2:int;
2291

    
2292

    
2293
let
2294

    
2295

    
2296

    
2297
	-- set state as active 
2298
	idA_A2_2 
2299
	= 1498;
2300
	
2301

    
2302
	a_2 
2303
	= if (not isInner) then x+4
2304
	 else a_1;
2305
	
2306

    
2307
	(idA_A2, a) 
2308
	= (idA_A2_2, a_2);
2309
	
2310

    
2311
tel
2312

    
2313

    
2314

    
2315

    
2316

    
2317
-- Exit action for state :A2_A2b
2318
node A2_A2b_ex(idA_A2_1:int;
2319
	isInner:bool)
2320

    
2321
returns (idA_A2:int);
2322

    
2323

    
2324
var 	idA_A2_2:int;
2325

    
2326

    
2327
let
2328

    
2329

    
2330

    
2331
	-- set state as inactive 
2332
	idA_A2_2
2333
	 = if (not isInner) then 0 else idA_A2_1;
2334

    
2335

    
2336
	(idA_A2) 
2337
	= (idA_A2_1);
2338
	
2339

    
2340
tel
2341

    
2342

    
2343

    
2344

    
2345

    
2346

    
2347
-- Entry action for state :A_A2
2348
node A_A2_en(idA_A2_1:int;
2349
	idParallel3_A_1:int;
2350
	a_1:int;
2351
	x:int;
2352
	isInner:bool)
2353

    
2354
returns (idA_A2:int;
2355
	idParallel3_A:int;
2356
	a:int);
2357

    
2358

    
2359
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int;
2360
	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4:int;
2361
	a_2, a_3, a_4, a_5, a_6:int;
2362

    
2363

    
2364
let
2365

    
2366

    
2367

    
2368
	-- set state as active 
2369
	idParallel3_A_2 
2370
	= 1496;
2371
	
2372

    
2373
	
2374
-- transition trace :
2375
	--POINT__To__A2_A2a_1
2376
		(idA_A2_2, a_2) 
2377
	= A2_A2a_en(idA_A2_1, x, a_1, false);
2378
		
2379

    
2380
	(idA_A2_3, idParallel3_A_3, a_3) 
2381
	= 
2382

    
2383
	if ( idA_A2_1 = 0) then
2384

    
2385
	 (idA_A2_2, idParallel3_A_2, a_2)
2386

    
2387
	 else(idA_A2_1, idParallel3_A_2, a_1);
2388

    
2389
	
2390

    
2391
	(idA_A2_4, a_4) 
2392
	= 
2393
	if ( idA_A2_1 = 1497) then
2394
	A2_A2a_en(idA_A2_1, x, a_1, false)
2395
	 else (idA_A2_1, a_1);
2396

    
2397
	
2398

    
2399
	(idA_A2_5, a_5) 
2400
	= 
2401
	if ( idA_A2_1 = 1498) then
2402
	A2_A2b_en(idA_A2_1, x, a_1, false)
2403
	 else (idA_A2_1, a_1);
2404

    
2405
	
2406

    
2407
	(idA_A2_6, idParallel3_A_4, a_6) 
2408
	= 
2409
		 if ( idA_A2_1 = 0) then 
2410
		(idA_A2_3, idParallel3_A_3, a_3)
2411
		 else
2412
		 if ( idA_A2_1 = 1497) then 
2413
		(idA_A2_4, idParallel3_A_3, a_4)
2414
		 else
2415
		 if ( idA_A2_1 = 1498) then 
2416
		(idA_A2_5, idParallel3_A_3, a_5)
2417
		 else (idA_A2_1, idParallel3_A_2, a_1);
2418

    
2419

    
2420
	(idA_A2, idParallel3_A, a) 
2421
	= (idA_A2_6, idParallel3_A_4, a_6);
2422
	
2423

    
2424
tel
2425

    
2426

    
2427

    
2428

    
2429

    
2430
-- Exit action for state :A_A2
2431
node A_A2_ex(idA_A2_1:int;
2432
	idParallel3_A_1:int;
2433
	isInner:bool)
2434

    
2435
returns (idA_A2:int;
2436
	idParallel3_A:int);
2437

    
2438

    
2439
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int;
2440
	idParallel3_A_2:int;
2441

    
2442

    
2443
let
2444

    
2445

    
2446

    
2447
	
2448
	(idA_A2_2) 
2449
	= 
2450
	if ( idA_A2_1 = 1497) then
2451
	A2_A2a_ex(idA_A2_1, false)
2452
	 else (idA_A2_1);
2453

    
2454
	
2455

    
2456
	(idA_A2_3) 
2457
	= 
2458
	if ( idA_A2_1 = 1498) then
2459
	A2_A2b_ex(idA_A2_1, false)
2460
	 else (idA_A2_1);
2461

    
2462
	
2463

    
2464
	(idA_A2_4) 
2465
	= 
2466
		 if ( idA_A2_1 = 1497) then 
2467
		(idA_A2_2)
2468
		 else
2469
		 if ( idA_A2_1 = 1498) then 
2470
		(idA_A2_3)
2471
		 else (idA_A2_1);
2472

    
2473

    
2474
	-- set state as inactive 
2475
	idParallel3_A_2
2476
	 = if (not isInner) then 0 else idParallel3_A_1;
2477

    
2478
	idA_A2_5 
2479
	= 0;
2480
	
2481

    
2482
	(idA_A2, idParallel3_A) 
2483
	= (idA_A2_5, idParallel3_A_1);
2484
	
2485

    
2486
tel
2487

    
2488

    
2489

    
2490

    
2491

    
2492

    
2493
-- Entry action for state :A1_A1a
2494
node A1_A1a_en(idA_A1_1:int;
2495
	x:int;
2496
	a_1:int;
2497
	isInner:bool)
2498

    
2499
returns (idA_A1:int;
2500
	a:int);
2501

    
2502

    
2503
var 	idA_A1_2:int;
2504
	a_2:int;
2505

    
2506

    
2507
let
2508

    
2509

    
2510

    
2511
	-- set state as active 
2512
	idA_A1_2 
2513
	= 1494;
2514
	
2515

    
2516
	a_2 
2517
	= if (not isInner) then x+1
2518
	 else a_1;
2519
	
2520

    
2521
	(idA_A1, a) 
2522
	= (idA_A1_2, a_2);
2523
	
2524

    
2525
tel
2526

    
2527

    
2528

    
2529

    
2530

    
2531
-- Exit action for state :A1_A1a
2532
node A1_A1a_ex(idA_A1_1:int;
2533
	isInner:bool)
2534

    
2535
returns (idA_A1:int);
2536

    
2537

    
2538
var 	idA_A1_2:int;
2539

    
2540

    
2541
let
2542

    
2543

    
2544

    
2545
	-- set state as inactive 
2546
	idA_A1_2
2547
	 = if (not isInner) then 0 else idA_A1_1;
2548

    
2549

    
2550
	(idA_A1) 
2551
	= (idA_A1_1);
2552
	
2553

    
2554
tel
2555

    
2556

    
2557

    
2558

    
2559

    
2560

    
2561
-- Entry action for state :A1_A1b
2562
node A1_A1b_en(idA_A1_1:int;
2563
	x:int;
2564
	a_1:int;
2565
	isInner:bool)
2566

    
2567
returns (idA_A1:int;
2568
	a:int);
2569

    
2570

    
2571
var 	idA_A1_2:int;
2572
	a_2:int;
2573

    
2574

    
2575
let
2576

    
2577

    
2578

    
2579
	-- set state as active 
2580
	idA_A1_2 
2581
	= 1495;
2582
	
2583

    
2584
	a_2 
2585
	= if (not isInner) then x+2
2586
	 else a_1;
2587
	
2588

    
2589
	(idA_A1, a) 
2590
	= (idA_A1_2, a_2);
2591
	
2592

    
2593
tel
2594

    
2595

    
2596

    
2597

    
2598

    
2599
-- Exit action for state :A1_A1b
2600
node A1_A1b_ex(idA_A1_1:int;
2601
	isInner:bool)
2602

    
2603
returns (idA_A1:int);
2604

    
2605

    
2606
var 	idA_A1_2:int;
2607

    
2608

    
2609
let
2610

    
2611

    
2612

    
2613
	-- set state as inactive 
2614
	idA_A1_2
2615
	 = if (not isInner) then 0 else idA_A1_1;
2616

    
2617

    
2618
	(idA_A1) 
2619
	= (idA_A1_1);
2620
	
2621

    
2622
tel
2623

    
2624

    
2625

    
2626

    
2627

    
2628

    
2629
-- Entry action for state :A_A1
2630
node A_A1_en(idA_A1_1:int;
2631
	idParallel3_A_1:int;
2632
	a_1:int;
2633
	x:int;
2634
	isInner:bool)
2635

    
2636
returns (idA_A1:int;
2637
	idParallel3_A:int;
2638
	a:int);
2639

    
2640

    
2641
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int;
2642
	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4:int;
2643
	a_2, a_3, a_4, a_5, a_6:int;
2644

    
2645

    
2646
let
2647

    
2648

    
2649

    
2650
	-- set state as active 
2651
	idParallel3_A_2 
2652
	= 1493;
2653
	
2654

    
2655
	
2656
-- transition trace :
2657
	--POINT__To__A1_A1a_1
2658
		(idA_A1_2, a_2) 
2659
	= A1_A1a_en(idA_A1_1, x, a_1, false);
2660
		
2661

    
2662
	(idA_A1_3, idParallel3_A_3, a_3) 
2663
	= 
2664

    
2665
	if ( idA_A1_1 = 0) then
2666

    
2667
	 (idA_A1_2, idParallel3_A_2, a_2)
2668

    
2669
	 else(idA_A1_1, idParallel3_A_2, a_1);
2670

    
2671
	
2672

    
2673
	(idA_A1_4, a_4) 
2674
	= 
2675
	if ( idA_A1_1 = 1494) then
2676
	A1_A1a_en(idA_A1_1, x, a_1, false)
2677
	 else (idA_A1_1, a_1);
2678

    
2679
	
2680

    
2681
	(idA_A1_5, a_5) 
2682
	= 
2683
	if ( idA_A1_1 = 1495) then
2684
	A1_A1b_en(idA_A1_1, x, a_1, false)
2685
	 else (idA_A1_1, a_1);
2686

    
2687
	
2688

    
2689
	(idA_A1_6, idParallel3_A_4, a_6) 
2690
	= 
2691
		 if ( idA_A1_1 = 0) then 
2692
		(idA_A1_3, idParallel3_A_3, a_3)
2693
		 else
2694
		 if ( idA_A1_1 = 1494) then 
2695
		(idA_A1_4, idParallel3_A_3, a_4)
2696
		 else
2697
		 if ( idA_A1_1 = 1495) then 
2698
		(idA_A1_5, idParallel3_A_3, a_5)
2699
		 else (idA_A1_1, idParallel3_A_2, a_1);
2700

    
2701

    
2702
	(idA_A1, idParallel3_A, a) 
2703
	= (idA_A1_6, idParallel3_A_4, a_6);
2704
	
2705

    
2706
tel
2707

    
2708

    
2709

    
2710

    
2711

    
2712
-- Exit action for state :A_A1
2713
node A_A1_ex(idA_A1_1:int;
2714
	idParallel3_A_1:int;
2715
	isInner:bool)
2716

    
2717
returns (idA_A1:int;
2718
	idParallel3_A:int);
2719

    
2720

    
2721
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2722
	idParallel3_A_2:int;
2723

    
2724

    
2725
let
2726

    
2727

    
2728

    
2729
	
2730
	(idA_A1_2) 
2731
	= 
2732
	if ( idA_A1_1 = 1494) then
2733
	A1_A1a_ex(idA_A1_1, false)
2734
	 else (idA_A1_1);
2735

    
2736
	
2737

    
2738
	(idA_A1_3) 
2739
	= 
2740
	if ( idA_A1_1 = 1495) then
2741
	A1_A1b_ex(idA_A1_1, false)
2742
	 else (idA_A1_1);
2743

    
2744
	
2745

    
2746
	(idA_A1_4) 
2747
	= 
2748
		 if ( idA_A1_1 = 1494) then 
2749
		(idA_A1_2)
2750
		 else
2751
		 if ( idA_A1_1 = 1495) then 
2752
		(idA_A1_3)
2753
		 else (idA_A1_1);
2754

    
2755

    
2756
	-- set state as inactive 
2757
	idParallel3_A_2
2758
	 = if (not isInner) then 0 else idParallel3_A_1;
2759

    
2760
	idA_A1_5 
2761
	= 0;
2762
	
2763

    
2764
	(idA_A1, idParallel3_A) 
2765
	= (idA_A1_5, idParallel3_A_1);
2766
	
2767

    
2768
tel
2769

    
2770

    
2771

    
2772

    
2773

    
2774

    
2775
-- Entry action for state :Parallel3_A
2776
node Parallel3_A_en(idParallel3_A_1:int;
2777
	idParallel3_Parallel3_1:int;
2778
	a_1:int;
2779
	idA_A1_1:int;
2780
	x:int;
2781
	idA_A2_1:int;
2782
	isInner:bool)
2783

    
2784
returns (idParallel3_A:int;
2785
	idParallel3_Parallel3:int;
2786
	a:int;
2787
	idA_A1:int;
2788
	idA_A2:int);
2789

    
2790

    
2791
var 	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4, idParallel3_A_5, idParallel3_A_6:int;
2792
	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int;
2793
	a_2, a_3, a_4, a_5, a_6:int;
2794
	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2795
	idA_A2_2, idA_A2_3:int;
2796

    
2797

    
2798
let
2799

    
2800

    
2801

    
2802
	-- set state as active 
2803
	idParallel3_Parallel3_2 
2804
	= 1492;
2805
	
2806

    
2807
	
2808
-- transition trace :
2809
	--POINT__To__A_A1_1
2810
		(idA_A1_2, idParallel3_A_2, a_2) 
2811
	= A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false);
2812
		
2813

    
2814
	(idParallel3_A_3, idParallel3_Parallel3_3, a_3, idA_A1_3) 
2815
	= 
2816

    
2817
	if ( idParallel3_A_1 = 0) then
2818

    
2819
	 (idParallel3_A_2, idParallel3_Parallel3_2, a_2, idA_A1_2)
2820

    
2821
	 else(idParallel3_A_1, idParallel3_Parallel3_2, a_1, idA_A1_1);
2822

    
2823
	
2824

    
2825
	(idA_A1_4, idParallel3_A_4, a_4) 
2826
	= 
2827
	if ( idParallel3_A_1 = 1493) then
2828
	A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false)
2829
	 else (idA_A1_1, idParallel3_A_1, a_1);
2830

    
2831
	
2832

    
2833
	(idA_A2_2, idParallel3_A_5, a_5) 
2834
	= 
2835
	if ( idParallel3_A_1 = 1496) then
2836
	A_A2_en(idA_A2_1, idParallel3_A_1, a_1, x, false)
2837
	 else (idA_A2_1, idParallel3_A_1, a_1);
2838

    
2839
	
2840

    
2841
	(idParallel3_A_6, idParallel3_Parallel3_4, a_6, idA_A1_5, idA_A2_3) 
2842
	= 
2843
		 if ( idParallel3_A_1 = 0) then 
2844
		(idParallel3_A_3, idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_1)
2845
		 else
2846
		 if ( idParallel3_A_1 = 1493) then 
2847
		(idParallel3_A_4, idParallel3_Parallel3_3, a_4, idA_A1_4, idA_A2_1)
2848
		 else
2849
		 if ( idParallel3_A_1 = 1496) then 
2850
		(idParallel3_A_5, idParallel3_Parallel3_3, a_5, idA_A1_1, idA_A2_2)
2851
		 else (idParallel3_A_1, idParallel3_Parallel3_2, a_1, idA_A1_1, idA_A2_1);
2852

    
2853

    
2854
	(idParallel3_A, idParallel3_Parallel3, a, idA_A1, idA_A2) 
2855
	= (idParallel3_A_6, idParallel3_Parallel3_4, a_6, idA_A1_5, idA_A2_3);
2856
	
2857

    
2858
tel
2859

    
2860

    
2861

    
2862

    
2863

    
2864
-- Exit action for state :Parallel3_A
2865
node Parallel3_A_ex(idA_A1_1:int;
2866
	idParallel3_A_1:int;
2867
	idA_A2_1:int;
2868
	idParallel3_Parallel3_1:int;
2869
	isInner:bool)
2870

    
2871
returns (idA_A1:int;
2872
	idParallel3_A:int;
2873
	idA_A2:int;
2874
	idParallel3_Parallel3:int);
2875

    
2876

    
2877
var 	idA_A1_2, idA_A1_3:int;
2878
	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4, idParallel3_A_5:int;
2879
	idA_A2_2, idA_A2_3:int;
2880
	idParallel3_Parallel3_2:int;
2881

    
2882

    
2883
let
2884

    
2885

    
2886

    
2887
	
2888
	(idA_A1_2, idParallel3_A_2) 
2889
	= 
2890
	if ( idParallel3_A_1 = 1493) then
2891
	A_A1_ex(idA_A1_1, idParallel3_A_1, false)
2892
	 else (idA_A1_1, idParallel3_A_1);
2893

    
2894
	
2895

    
2896
	(idA_A2_2, idParallel3_A_3) 
2897
	= 
2898
	if ( idParallel3_A_1 = 1496) then
2899
	A_A2_ex(idA_A2_1, idParallel3_A_1, false)
2900
	 else (idA_A2_1, idParallel3_A_1);
2901

    
2902
	
2903

    
2904
	(idA_A1_3, idParallel3_A_4, idA_A2_3) 
2905
	= 
2906
		 if ( idParallel3_A_1 = 1493) then 
2907
		(idA_A1_2, idParallel3_A_2, idA_A2_1)
2908
		 else
2909
		 if ( idParallel3_A_1 = 1496) then 
2910
		(idA_A1_1, idParallel3_A_3, idA_A2_2)
2911
		 else (idA_A1_1, idParallel3_A_1, idA_A2_1);
2912

    
2913

    
2914
	-- set state as inactive 
2915
	idParallel3_Parallel3_2
2916
	 = if (not isInner) then 0 else idParallel3_Parallel3_1;
2917

    
2918
	idParallel3_A_5 
2919
	= 0;
2920
	
2921

    
2922
	(idA_A1, idParallel3_A, idA_A2, idParallel3_Parallel3) 
2923
	= (idA_A1_3, idParallel3_A_5, idA_A2_3, idParallel3_Parallel3_1);
2924
	
2925

    
2926
tel
2927

    
2928

    
2929
--***************************************************State :B_B2 Automaton***************************************************
2930

    
2931
node B_B2_node(idB_B2_1:int;
2932
	b_1:int;
2933
	x:int;
2934
	S:bool;
2935
	R:bool)
2936

    
2937
returns (idB_B2:int;
2938
	b:int);
2939

    
2940

    
2941
let
2942

    
2943
	 automaton b_b2
2944

    
2945
	state POINTB_B2:
2946
	unless (idB_B2_1=0) restart POINT__TO__B2_B2A_1
2947

    
2948

    
2949

    
2950
	unless (idB_B2_1=1501) and S restart B2_B2A__TO__B2_B2B_1
2951

    
2952

    
2953

    
2954
	unless (idB_B2_1=1502) and R restart B2_B2B__TO__B2_B2A_1
2955

    
2956

    
2957

    
2958
	unless (idB_B2_1=1501) restart B2_B2A_IDL
2959

    
2960
	unless (idB_B2_1=1502) restart B2_B2B_IDL
2961

    
2962
	let
2963

    
2964
		(idB_B2, b) 
2965
	= (idB_B2_1, b_1);
2966
	
2967

    
2968
	tel
2969

    
2970

    
2971

    
2972
	state POINT__TO__B2_B2A_1:
2973

    
2974
	 var 	idB_B2_2:int;
2975
	b_2:int;
2976
	let
2977

    
2978
		-- transition trace :
2979
	--POINT__To__B2_B2a_1
2980
		(idB_B2_2, b_2) 
2981
	= B2_B2a_en(idB_B2_1, x, b_1, false);
2982
		
2983

    
2984
	(idB_B2, b) 
2985
	=  (idB_B2_2, b_2);
2986

    
2987

    
2988
	tel
2989

    
2990
	until true restart POINTB_B2
2991

    
2992

    
2993

    
2994
	state B2_B2A__TO__B2_B2B_1:
2995

    
2996
	 var 	idB_B2_2, idB_B2_3:int;
2997
	b_2:int;
2998
	let
2999

    
3000
		-- transition trace :
3001
	--B2_B2a__To__B2_B2b_1
3002
		(idB_B2_2) 
3003
	= B2_B2a_ex(idB_B2_1, false);
3004
		
3005

    
3006
		(idB_B2_3, b_2) 
3007
	= B2_B2b_en(idB_B2_2, x, b_1, false);
3008
		
3009

    
3010
	(idB_B2, b) 
3011
	=  (idB_B2_3, b_2);
3012

    
3013

    
3014
	tel
3015

    
3016
	until true restart POINTB_B2
3017

    
3018

    
3019

    
3020
	state B2_B2B__TO__B2_B2A_1:
3021

    
3022
	 var 	idB_B2_2, idB_B2_3:int;
3023
	b_2:int;
3024
	let
3025

    
3026
		-- transition trace :
3027
	--B2_B2b__To__B2_B2a_1
3028
		(idB_B2_2) 
3029
	= B2_B2b_ex(idB_B2_1, false);
3030
		
3031

    
3032
		(idB_B2_3, b_2) 
3033
	= B2_B2a_en(idB_B2_2, x, b_1, false);
3034
		
3035

    
3036
	(idB_B2, b) 
3037
	=  (idB_B2_3, b_2);
3038

    
3039

    
3040
	tel
3041

    
3042
	until true restart POINTB_B2
3043

    
3044

    
3045

    
3046
	state B2_B2A_IDL:
3047

    
3048
	 	let
3049

    
3050
		
3051

    
3052
	(idB_B2, b) 
3053
	= (idB_B2_1, b_1);
3054
	
3055

    
3056
	tel
3057

    
3058
	until true restart POINTB_B2
3059

    
3060

    
3061

    
3062
	state B2_B2B_IDL:
3063

    
3064
	 	let
3065

    
3066
		
3067

    
3068
	(idB_B2, b) 
3069
	= (idB_B2_1, b_1);
3070
	
3071

    
3072
	tel
3073

    
3074
	until true restart POINTB_B2
3075

    
3076

    
3077

    
3078
tel
3079

    
3080

    
3081
--***************************************************State :B_B1 Automaton***************************************************
3082

    
3083
node B_B1_node(idB_B1_1:int;
3084
	b_1:int;
3085
	x:int;
3086
	S:bool;
3087
	R:bool)
3088

    
3089
returns (idB_B1:int;
3090
	b:int);
3091

    
3092

    
3093
let
3094

    
3095
	 automaton b_b1
3096

    
3097
	state POINTB_B1:
3098
	unless (idB_B1_1=0) restart POINT__TO__B1_B1A_1
3099

    
3100

    
3101

    
3102
	unless (idB_B1_1=1504) and S restart B1_B1A__TO__B1_B1B_1
3103

    
3104

    
3105

    
3106
	unless (idB_B1_1=1505) and R restart B1_B1B__TO__B1_B1A_1
3107

    
3108

    
3109

    
3110
	unless (idB_B1_1=1504) restart B1_B1A_IDL
3111

    
3112
	unless (idB_B1_1=1505) restart B1_B1B_IDL
3113

    
3114
	let
3115

    
3116
		(idB_B1, b) 
3117
	= (idB_B1_1, b_1);
3118
	
3119

    
3120
	tel
3121

    
3122

    
3123

    
3124
	state POINT__TO__B1_B1A_1:
3125

    
3126
	 var 	idB_B1_2:int;
3127
	b_2:int;
3128
	let
3129

    
3130
		-- transition trace :
3131
	--POINT__To__B1_B1a_1
3132
		(idB_B1_2, b_2) 
3133
	= B1_B1a_en(idB_B1_1, x, b_1, false);
3134
		
3135

    
3136
	(idB_B1, b) 
3137
	=  (idB_B1_2, b_2);
3138

    
3139

    
3140
	tel
3141

    
3142
	until true restart POINTB_B1
3143

    
3144

    
3145

    
3146
	state B1_B1A__TO__B1_B1B_1:
3147

    
3148
	 var 	idB_B1_2, idB_B1_3:int;
3149
	b_2:int;
3150
	let
3151

    
3152
		-- transition trace :
3153
	--B1_B1a__To__B1_B1b_1
3154
		(idB_B1_2) 
3155
	= B1_B1a_ex(idB_B1_1, false);
3156
		
3157

    
3158
		(idB_B1_3, b_2) 
3159
	= B1_B1b_en(idB_B1_2, x, b_1, false);
3160
		
3161

    
3162
	(idB_B1, b) 
3163
	=  (idB_B1_3, b_2);
3164

    
3165

    
3166
	tel
3167

    
3168
	until true restart POINTB_B1
3169

    
3170

    
3171

    
3172
	state B1_B1B__TO__B1_B1A_1:
3173

    
3174
	 var 	idB_B1_2, idB_B1_3:int;
3175
	b_2:int;
3176
	let
3177

    
3178
		-- transition trace :
3179
	--B1_B1b__To__B1_B1a_1
3180
		(idB_B1_2) 
3181
	= B1_B1b_ex(idB_B1_1, false);
3182
		
3183

    
3184
		(idB_B1_3, b_2) 
3185
	= B1_B1a_en(idB_B1_2, x, b_1, false);
3186
		
3187

    
3188
	(idB_B1, b) 
3189
	=  (idB_B1_3, b_2);
3190

    
3191

    
3192
	tel
3193

    
3194
	until true restart POINTB_B1
3195

    
3196

    
3197

    
3198
	state B1_B1A_IDL:
3199

    
3200
	 	let
3201

    
3202
		
3203

    
3204
	(idB_B1, b) 
3205
	= (idB_B1_1, b_1);
3206
	
3207

    
3208
	tel
3209

    
3210
	until true restart POINTB_B1
3211

    
3212

    
3213

    
3214
	state B1_B1B_IDL:
3215

    
3216
	 	let
3217

    
3218
		
3219

    
3220
	(idB_B1, b) 
3221
	= (idB_B1_1, b_1);
3222
	
3223

    
3224
	tel
3225

    
3226
	until true restart POINTB_B1
3227

    
3228

    
3229

    
3230
tel
3231

    
3232

    
3233
--***************************************************State :Parallel3_B Automaton***************************************************
3234

    
3235
node Parallel3_B_node(idParallel3_B_1:int;
3236
	b_1:int;
3237
	idB_B1_1:int;
3238
	x:int;
3239
	T:bool;
3240
	idB_B2_1:int;
3241
	R:bool;
3242
	S:bool)
3243

    
3244
returns (idParallel3_B:int;
3245
	b:int;
3246
	idB_B1:int;
3247
	idB_B2:int);
3248

    
3249

    
3250
let
3251

    
3252
	 automaton parallel3_b
3253

    
3254
	state POINTParallel3_B:
3255
	unless (idParallel3_B_1=0) restart POINT__TO__B_B1_1
3256

    
3257

    
3258

    
3259
	unless (idParallel3_B_1=1500) and T restart B_B2__TO__B_B1_1
3260

    
3261

    
3262

    
3263
	unless (idParallel3_B_1=1503) and T restart B_B1__TO__B_B2_1
3264

    
3265

    
3266

    
3267
	unless (idParallel3_B_1=1500) restart B_B2_IDL
3268

    
3269
	unless (idParallel3_B_1=1503) restart B_B1_IDL
3270

    
3271
	let
3272

    
3273
		(idParallel3_B, b, idB_B1, idB_B2) 
3274
	= (idParallel3_B_1, b_1, idB_B1_1, idB_B2_1);
3275
	
3276

    
3277
	tel
3278

    
3279

    
3280

    
3281
	state POINT__TO__B_B1_1:
3282

    
3283
	 var 	idParallel3_B_2:int;
3284
	b_2:int;
3285
	idB_B1_2:int;
3286
	let
3287

    
3288
		-- transition trace :
3289
	--POINT__To__B_B1_1
3290
		(idB_B1_2, idParallel3_B_2, b_2) 
3291
	= B_B1_en(idB_B1_1, idParallel3_B_1, b_1, x, false);
3292
		
3293

    
3294
	(idParallel3_B, b, idB_B1) 
3295
	=  (idParallel3_B_2, b_2, idB_B1_2);
3296

    
3297
	--add unused variables
3298
	(idB_B2) 
3299
	= (idB_B2_1);
3300
	
3301

    
3302
	tel
3303

    
3304
	until true restart POINTParallel3_B
3305

    
3306

    
3307

    
3308
	state B_B2__TO__B_B1_1:
3309

    
3310
	 var 	idParallel3_B_2, idParallel3_B_3:int;
3311
	b_2:int;
3312
	idB_B1_2:int;
3313
	idB_B2_2:int;
3314
	let
3315

    
3316
		-- transition trace :
3317
	--B_B2__To__B_B1_1
3318
		(idB_B2_2, idParallel3_B_2) 
3319
	= B_B2_ex(idB_B2_1, idParallel3_B_1, false);
3320
		
3321

    
3322
		(idB_B1_2, idParallel3_B_3, b_2) 
3323
	= B_B1_en(idB_B1_1, idParallel3_B_2, b_1, x, false);
3324
		
3325

    
3326
	(idParallel3_B, b, idB_B1, idB_B2) 
3327
	=  (idParallel3_B_3, b_2, idB_B1_2, idB_B2_2);
3328

    
3329

    
3330
	tel
3331

    
3332
	until true restart POINTParallel3_B
3333

    
3334

    
3335

    
3336
	state B_B1__TO__B_B2_1:
3337

    
3338
	 var 	idParallel3_B_2, idParallel3_B_3:int;
3339
	b_2:int;
3340
	idB_B1_2:int;
3341
	idB_B2_2:int;
3342
	let
3343

    
3344
		-- transition trace :
3345
	--B_B1__To__B_B2_1
3346
		(idB_B1_2, idParallel3_B_2) 
3347
	= B_B1_ex(idB_B1_1, idParallel3_B_1, false);
3348
		
3349

    
3350
		(idB_B2_2, idParallel3_B_3, b_2) 
3351
	= B_B2_en(idB_B2_1, idParallel3_B_2, b_1, x, false);
3352
		
3353

    
3354
	(idParallel3_B, b, idB_B1, idB_B2) 
3355
	=  (idParallel3_B_3, b_2, idB_B1_2, idB_B2_2);
3356

    
3357

    
3358
	tel
3359

    
3360
	until true restart POINTParallel3_B
3361

    
3362

    
3363

    
3364
	state B_B2_IDL:
3365

    
3366
	 var 	b_2:int;
3367
	idB_B2_2:int;
3368
	let
3369

    
3370
		
3371
	(idB_B2_2, b_2) 
3372
	= B_B2_node(idB_B2_1, b_1, x, S, R);
3373

    
3374
		
3375

    
3376

    
3377
	(idParallel3_B, b, idB_B1, idB_B2) 
3378
	= (idParallel3_B_1, b_2, idB_B1_1, idB_B2_2);
3379
	
3380

    
3381
	tel
3382

    
3383
	until true restart POINTParallel3_B
3384

    
3385

    
3386

    
3387
	state B_B1_IDL:
3388

    
3389
	 var 	b_2:int;
3390
	idB_B1_2:int;
3391
	let
3392

    
3393
		
3394
	(idB_B1_2, b_2) 
3395
	= B_B1_node(idB_B1_1, b_1, x, S, R);
3396

    
3397
		
3398

    
3399

    
3400
	(idParallel3_B, b, idB_B1, idB_B2) 
3401
	= (idParallel3_B_1, b_2, idB_B1_2, idB_B2_1);
3402
	
3403

    
3404
	tel
3405

    
3406
	until true restart POINTParallel3_B
3407

    
3408

    
3409

    
3410
tel
3411

    
3412

    
3413
--***************************************************State :D_D2 Automaton***************************************************
3414

    
3415
node D_D2_node(idD_D2_1:int;
3416
	dd_1:int;
3417
	y:int;
3418
	S:bool;
3419
	R:bool)
3420

    
3421
returns (idD_D2:int;
3422
	dd:int);
3423

    
3424

    
3425
let
3426

    
3427
	 automaton d_d2
3428

    
3429
	state POINTD_D2:
3430
	unless (idD_D2_1=0) restart POINT__TO__D2_D2A_1
3431

    
3432

    
3433

    
3434
	unless (idD_D2_1=1515) and S restart D2_D2A__TO__D2_D2B_1
3435

    
3436

    
3437

    
3438
	unless (idD_D2_1=1516) and R restart D2_D2B__TO__D2_D2A_1
3439

    
3440

    
3441

    
3442
	unless (idD_D2_1=1515) restart D2_D2A_IDL
3443

    
3444
	unless (idD_D2_1=1516) restart D2_D2B_IDL
3445

    
3446
	let
3447

    
3448
		(idD_D2, dd) 
3449
	= (idD_D2_1, dd_1);
3450
	
3451

    
3452
	tel
3453

    
3454

    
3455

    
3456
	state POINT__TO__D2_D2A_1:
3457

    
3458
	 var 	idD_D2_2:int;
3459
	dd_2:int;
3460
	let
3461

    
3462
		-- transition trace :
3463
	--POINT__To__D2_D2a_1
3464
		(idD_D2_2, dd_2) 
3465
	= D2_D2a_en(idD_D2_1, y, dd_1, false);
3466
		
3467

    
3468
	(idD_D2, dd) 
3469
	=  (idD_D2_2, dd_2);
3470

    
3471

    
3472
	tel
3473

    
3474
	until true restart POINTD_D2
3475

    
3476

    
3477

    
3478
	state D2_D2A__TO__D2_D2B_1:
3479

    
3480
	 var 	idD_D2_2, idD_D2_3:int;
3481
	dd_2:int;
3482
	let
3483

    
3484
		-- transition trace :
3485
	--D2_D2a__To__D2_D2b_1
3486
		(idD_D2_2) 
3487
	= D2_D2a_ex(idD_D2_1, false);
3488
		
3489

    
3490
		(idD_D2_3, dd_2) 
3491
	= D2_D2b_en(idD_D2_2, y, dd_1, false);
3492
		
3493

    
3494
	(idD_D2, dd) 
3495
	=  (idD_D2_3, dd_2);
3496

    
3497

    
3498
	tel
3499

    
3500
	until true restart POINTD_D2
3501

    
3502

    
3503

    
3504
	state D2_D2B__TO__D2_D2A_1:
3505

    
3506
	 var 	idD_D2_2, idD_D2_3:int;
3507
	dd_2:int;
3508
	let
3509

    
3510
		-- transition trace :
3511
	--D2_D2b__To__D2_D2a_1
3512
		(idD_D2_2) 
3513
	= D2_D2b_ex(idD_D2_1, false);
3514
		
3515

    
3516
		(idD_D2_3, dd_2) 
3517
	= D2_D2a_en(idD_D2_2, y, dd_1, false);
3518
		
3519

    
3520
	(idD_D2, dd) 
3521
	=  (idD_D2_3, dd_2);
3522

    
3523

    
3524
	tel
3525

    
3526
	until true restart POINTD_D2
3527

    
3528

    
3529

    
3530
	state D2_D2A_IDL:
3531

    
3532
	 	let
3533

    
3534
		
3535

    
3536
	(idD_D2, dd) 
3537
	= (idD_D2_1, dd_1);
3538
	
3539

    
3540
	tel
3541

    
3542
	until true restart POINTD_D2
3543

    
3544

    
3545

    
3546
	state D2_D2B_IDL:
3547

    
3548
	 	let
3549

    
3550
		
3551

    
3552
	(idD_D2, dd) 
3553
	= (idD_D2_1, dd_1);
3554
	
3555

    
3556
	tel
3557

    
3558
	until true restart POINTD_D2
3559

    
3560

    
3561

    
3562
tel
3563

    
3564

    
3565
--***************************************************State :D_D1 Automaton***************************************************
3566

    
3567
node D_D1_node(idD_D1_1:int;
3568
	dd_1:int;
3569
	y:int;
3570
	S:bool;
3571
	R:bool)
3572

    
3573
returns (idD_D1:int;
3574
	dd:int);
3575

    
3576

    
3577
let
3578

    
3579
	 automaton d_d1
3580

    
3581
	state POINTD_D1:
3582
	unless (idD_D1_1=0) restart POINT__TO__D1_D1A_1
3583

    
3584

    
3585

    
3586
	unless (idD_D1_1=1518) and S restart D1_D1A__TO__D1_D1B_1
3587

    
3588

    
3589

    
3590
	unless (idD_D1_1=1519) and R restart D1_D1B__TO__D1_D1A_1
3591

    
3592

    
3593

    
3594
	unless (idD_D1_1=1518) restart D1_D1A_IDL
3595

    
3596
	unless (idD_D1_1=1519) restart D1_D1B_IDL
3597

    
3598
	let
3599

    
3600
		(idD_D1, dd) 
3601
	= (idD_D1_1, dd_1);
3602
	
3603

    
3604
	tel
3605

    
3606

    
3607

    
3608
	state POINT__TO__D1_D1A_1:
3609

    
3610
	 var 	idD_D1_2:int;
3611
	dd_2:int;
3612
	let
3613

    
3614
		-- transition trace :
3615
	--POINT__To__D1_D1a_1
3616
		(idD_D1_2, dd_2) 
3617
	= D1_D1a_en(idD_D1_1, y, dd_1, false);
3618
		
3619

    
3620
	(idD_D1, dd) 
3621
	=  (idD_D1_2, dd_2);
3622

    
3623

    
3624
	tel
3625

    
3626
	until true restart POINTD_D1
3627

    
3628

    
3629

    
3630
	state D1_D1A__TO__D1_D1B_1:
3631

    
3632
	 var 	idD_D1_2, idD_D1_3:int;
3633
	dd_2:int;
3634
	let
3635

    
3636
		-- transition trace :
3637
	--D1_D1a__To__D1_D1b_1
3638
		(idD_D1_2) 
3639
	= D1_D1a_ex(idD_D1_1, false);
3640
		
3641

    
3642
		(idD_D1_3, dd_2) 
3643
	= D1_D1b_en(idD_D1_2, y, dd_1, false);
3644
		
3645

    
3646
	(idD_D1, dd) 
3647
	=  (idD_D1_3, dd_2);
3648

    
3649

    
3650
	tel
3651

    
3652
	until true restart POINTD_D1
3653

    
3654

    
3655

    
3656
	state D1_D1B__TO__D1_D1A_1:
3657

    
3658
	 var 	idD_D1_2, idD_D1_3:int;
3659
	dd_2:int;
3660
	let
3661

    
3662
		-- transition trace :
3663
	--D1_D1b__To__D1_D1a_1
3664
		(idD_D1_2) 
3665
	= D1_D1b_ex(idD_D1_1, false);
3666
		
3667

    
3668
		(idD_D1_3, dd_2) 
3669
	= D1_D1a_en(idD_D1_2, y, dd_1, false);
3670
		
3671

    
3672
	(idD_D1, dd) 
3673
	=  (idD_D1_3, dd_2);
3674

    
3675

    
3676
	tel
3677

    
3678
	until true restart POINTD_D1
3679

    
3680

    
3681

    
3682
	state D1_D1A_IDL:
3683

    
3684
	 	let
3685

    
3686
		
3687

    
3688
	(idD_D1, dd) 
3689
	= (idD_D1_1, dd_1);
3690
	
3691

    
3692
	tel
3693

    
3694
	until true restart POINTD_D1
3695

    
3696

    
3697

    
3698
	state D1_D1B_IDL:
3699

    
3700
	 	let
3701

    
3702
		
3703

    
3704
	(idD_D1, dd) 
3705
	= (idD_D1_1, dd_1);
3706
	
3707

    
3708
	tel
3709

    
3710
	until true restart POINTD_D1
3711

    
3712

    
3713

    
3714
tel
3715

    
3716

    
3717
--***************************************************State :Parallel3_D Automaton***************************************************
3718

    
3719
node Parallel3_D_node(idParallel3_D_1:int;
3720
	dd_1:int;
3721
	idD_D1_1:int;
3722
	y:int;
3723
	T:bool;
3724
	idD_D2_1:int;
3725
	R:bool;
3726
	S:bool)
3727

    
3728
returns (idParallel3_D:int;
3729
	dd:int;
3730
	idD_D1:int;
3731
	idD_D2:int);
3732

    
3733

    
3734
let
3735

    
3736
	 automaton parallel3_d
3737

    
3738
	state POINTParallel3_D:
3739
	unless (idParallel3_D_1=0) restart POINT__TO__D_D1_1
3740

    
3741

    
3742

    
3743
	unless (idParallel3_D_1=1514) and T restart D_D2__TO__D_D1_1
3744

    
3745

    
3746

    
3747
	unless (idParallel3_D_1=1517) and T restart D_D1__TO__D_D2_1
3748

    
3749

    
3750

    
3751
	unless (idParallel3_D_1=1514) restart D_D2_IDL
3752

    
3753
	unless (idParallel3_D_1=1517) restart D_D1_IDL
3754

    
3755
	let
3756

    
3757
		(idParallel3_D, dd, idD_D1, idD_D2) 
3758
	= (idParallel3_D_1, dd_1, idD_D1_1, idD_D2_1);
3759
	
3760

    
3761
	tel
3762

    
3763

    
3764

    
3765
	state POINT__TO__D_D1_1:
3766

    
3767
	 var 	idParallel3_D_2:int;
3768
	dd_2:int;
3769
	idD_D1_2:int;
3770
	let
3771

    
3772
		-- transition trace :
3773
	--POINT__To__D_D1_1
3774
		(idD_D1_2, idParallel3_D_2, dd_2) 
3775
	= D_D1_en(idD_D1_1, idParallel3_D_1, dd_1, y, false);
3776
		
3777

    
3778
	(idParallel3_D, dd, idD_D1) 
3779
	=  (idParallel3_D_2, dd_2, idD_D1_2);
3780

    
3781
	--add unused variables
3782
	(idD_D2) 
3783
	= (idD_D2_1);
3784
	
3785

    
3786
	tel
3787

    
3788
	until true restart POINTParallel3_D
3789

    
3790

    
3791

    
3792
	state D_D2__TO__D_D1_1:
3793

    
3794
	 var 	idParallel3_D_2, idParallel3_D_3:int;
3795
	dd_2:int;
3796
	idD_D1_2:int;
3797
	idD_D2_2:int;
3798
	let
3799

    
3800
		-- transition trace :
3801
	--D_D2__To__D_D1_1
3802
		(idD_D2_2, idParallel3_D_2) 
3803
	= D_D2_ex(idD_D2_1, idParallel3_D_1, false);
3804
		
3805

    
3806
		(idD_D1_2, idParallel3_D_3, dd_2) 
3807
	= D_D1_en(idD_D1_1, idParallel3_D_2, dd_1, y, false);
3808
		
3809

    
3810
	(idParallel3_D, dd, idD_D1, idD_D2) 
3811
	=  (idParallel3_D_3, dd_2, idD_D1_2, idD_D2_2);
3812

    
3813

    
3814
	tel
3815

    
3816
	until true restart POINTParallel3_D
3817

    
3818

    
3819

    
3820
	state D_D1__TO__D_D2_1:
3821

    
3822
	 var 	idParallel3_D_2, idParallel3_D_3:int;
3823
	dd_2:int;
3824
	idD_D1_2:int;
3825
	idD_D2_2:int;
3826
	let
3827

    
3828
		-- transition trace :
3829
	--D_D1__To__D_D2_1
3830
		(idD_D1_2, idParallel3_D_2) 
3831
	= D_D1_ex(idD_D1_1, idParallel3_D_1, false);
3832
		
3833

    
3834
		(idD_D2_2, idParallel3_D_3, dd_2) 
3835
	= D_D2_en(idD_D2_1, idParallel3_D_2, dd_1, y, false);
3836
		
3837

    
3838
	(idParallel3_D, dd, idD_D1, idD_D2) 
3839
	=  (idParallel3_D_3, dd_2, idD_D1_2, idD_D2_2);
3840

    
3841

    
3842
	tel
3843

    
3844
	until true restart POINTParallel3_D
3845

    
3846

    
3847

    
3848
	state D_D2_IDL:
3849

    
3850
	 var 	dd_2:int;
3851
	idD_D2_2:int;
3852
	let
3853

    
3854
		
3855
	(idD_D2_2, dd_2) 
3856
	= D_D2_node(idD_D2_1, dd_1, y, S, R);
3857

    
3858
		
3859

    
3860

    
3861
	(idParallel3_D, dd, idD_D1, idD_D2) 
3862
	= (idParallel3_D_1, dd_2, idD_D1_1, idD_D2_2);
3863
	
3864

    
3865
	tel
3866

    
3867
	until true restart POINTParallel3_D
3868

    
3869

    
3870

    
3871
	state D_D1_IDL:
3872

    
3873
	 var 	dd_2:int;
3874
	idD_D1_2:int;
3875
	let
3876

    
3877
		
3878
	(idD_D1_2, dd_2) 
3879
	= D_D1_node(idD_D1_1, dd_1, y, S, R);
3880

    
3881
		
3882

    
3883

    
3884
	(idParallel3_D, dd, idD_D1, idD_D2) 
3885
	= (idParallel3_D_1, dd_2, idD_D1_2, idD_D2_1);
3886
	
3887

    
3888
	tel
3889

    
3890
	until true restart POINTParallel3_D
3891

    
3892

    
3893

    
3894
tel
3895

    
3896

    
3897
--***************************************************State :C_C2 Automaton***************************************************
3898

    
3899
node C_C2_node(idC_C2_1:int;
3900
	c_1:int;
3901
	y:int;
3902
	S:bool;
3903
	R:bool)
3904

    
3905
returns (idC_C2:int;
3906
	c:int);
3907

    
3908

    
3909
let
3910

    
3911
	 automaton c_c2
3912

    
3913
	state POINTC_C2:
3914
	unless (idC_C2_1=0) restart POINT__TO__C2_C2A_1
3915

    
3916

    
3917

    
3918
	unless (idC_C2_1=1508) and S restart C2_C2A__TO__C2_C2B_1
3919

    
3920

    
3921

    
3922
	unless (idC_C2_1=1509) and R restart C2_C2B__TO__C2_C2A_1
3923

    
3924

    
3925

    
3926
	unless (idC_C2_1=1508) restart C2_C2A_IDL
3927

    
3928
	unless (idC_C2_1=1509) restart C2_C2B_IDL
3929

    
3930
	let
3931

    
3932
		(idC_C2, c) 
3933
	= (idC_C2_1, c_1);
3934
	
3935

    
3936
	tel
3937

    
3938

    
3939

    
3940
	state POINT__TO__C2_C2A_1:
3941

    
3942
	 var 	idC_C2_2:int;
3943
	c_2:int;
3944
	let
3945

    
3946
		-- transition trace :
3947
	--POINT__To__C2_C2a_1
3948
		(idC_C2_2, c_2) 
3949
	= C2_C2a_en(idC_C2_1, y, c_1, false);
3950
		
3951

    
3952
	(idC_C2, c) 
3953
	=  (idC_C2_2, c_2);
3954

    
3955

    
3956
	tel
3957

    
3958
	until true restart POINTC_C2
3959

    
3960

    
3961

    
3962
	state C2_C2A__TO__C2_C2B_1:
3963

    
3964
	 var 	idC_C2_2, idC_C2_3:int;
3965
	c_2:int;
3966
	let
3967

    
3968
		-- transition trace :
3969
	--C2_C2a__To__C2_C2b_1
3970
		(idC_C2_2) 
3971
	= C2_C2a_ex(idC_C2_1, false);
3972
		
3973

    
3974
		(idC_C2_3, c_2) 
3975
	= C2_C2b_en(idC_C2_2, y, c_1, false);
3976
		
3977

    
3978
	(idC_C2, c) 
3979
	=  (idC_C2_3, c_2);
3980

    
3981

    
3982
	tel
3983

    
3984
	until true restart POINTC_C2
3985

    
3986

    
3987

    
3988
	state C2_C2B__TO__C2_C2A_1:
3989

    
3990
	 var 	idC_C2_2, idC_C2_3:int;
3991
	c_2:int;
3992
	let
3993

    
3994
		-- transition trace :
3995
	--C2_C2b__To__C2_C2a_1
3996
		(idC_C2_2) 
3997
	= C2_C2b_ex(idC_C2_1, false);
3998
		
3999

    
4000
		(idC_C2_3, c_2) 
4001
	= C2_C2a_en(idC_C2_2, y, c_1, false);
4002
		
4003

    
4004
	(idC_C2, c) 
4005
	=  (idC_C2_3, c_2);
4006

    
4007

    
4008
	tel
4009

    
4010
	until true restart POINTC_C2
4011

    
4012

    
4013

    
4014
	state C2_C2A_IDL:
4015

    
4016
	 	let
4017

    
4018
		
4019

    
4020
	(idC_C2, c) 
4021
	= (idC_C2_1, c_1);
4022
	
4023

    
4024
	tel
4025

    
4026
	until true restart POINTC_C2
4027

    
4028

    
4029

    
4030
	state C2_C2B_IDL:
4031

    
4032
	 	let
4033

    
4034
		
4035

    
4036
	(idC_C2, c) 
4037
	= (idC_C2_1, c_1);
4038
	
4039

    
4040
	tel
4041

    
4042
	until true restart POINTC_C2
4043

    
4044

    
4045

    
4046
tel
4047

    
4048

    
4049
--***************************************************State :C_C1 Automaton***************************************************
4050

    
4051
node C_C1_node(idC_C1_1:int;
4052
	c_1:int;
4053
	y:int;
4054
	S:bool;
4055
	R:bool)
4056

    
4057
returns (idC_C1:int;
4058
	c:int);
4059

    
4060

    
4061
let
4062

    
4063
	 automaton c_c1
4064

    
4065
	state POINTC_C1:
4066
	unless (idC_C1_1=0) restart POINT__TO__C1_C1A_1
4067

    
4068

    
4069

    
4070
	unless (idC_C1_1=1511) and S restart C1_C1A__TO__C1_C1B_1
4071

    
4072

    
4073

    
4074
	unless (idC_C1_1=1512) and R restart C1_C1B__TO__C1_C1A_1
4075

    
4076

    
4077

    
4078
	unless (idC_C1_1=1511) restart C1_C1A_IDL
4079

    
4080
	unless (idC_C1_1=1512) restart C1_C1B_IDL
4081

    
4082
	let
4083

    
4084
		(idC_C1, c) 
4085
	= (idC_C1_1, c_1);
4086
	
4087

    
4088
	tel
4089

    
4090

    
4091

    
4092
	state POINT__TO__C1_C1A_1:
4093

    
4094
	 var 	idC_C1_2:int;
4095
	c_2:int;
4096
	let
4097

    
4098
		-- transition trace :
4099
	--POINT__To__C1_C1a_1
4100
		(idC_C1_2, c_2) 
4101
	= C1_C1a_en(idC_C1_1, y, c_1, false);
4102
		
4103

    
4104
	(idC_C1, c) 
4105
	=  (idC_C1_2, c_2);
4106

    
4107

    
4108
	tel
4109

    
4110
	until true restart POINTC_C1
4111

    
4112

    
4113

    
4114
	state C1_C1A__TO__C1_C1B_1:
4115

    
4116
	 var 	idC_C1_2, idC_C1_3:int;
4117
	c_2:int;
4118
	let
4119

    
4120
		-- transition trace :
4121
	--C1_C1a__To__C1_C1b_1
4122
		(idC_C1_2) 
4123
	= C1_C1a_ex(idC_C1_1, false);
4124
		
4125

    
4126
		(idC_C1_3, c_2) 
4127
	= C1_C1b_en(idC_C1_2, y, c_1, false);
4128
		
4129

    
4130
	(idC_C1, c) 
4131
	=  (idC_C1_3, c_2);
4132

    
4133

    
4134
	tel
4135

    
4136
	until true restart POINTC_C1
4137

    
4138

    
4139

    
4140
	state C1_C1B__TO__C1_C1A_1:
4141

    
4142
	 var 	idC_C1_2, idC_C1_3:int;
4143
	c_2:int;
4144
	let
4145

    
4146
		-- transition trace :
4147
	--C1_C1b__To__C1_C1a_1
4148
		(idC_C1_2) 
4149
	= C1_C1b_ex(idC_C1_1, false);
4150
		
4151

    
4152
		(idC_C1_3, c_2) 
4153
	= C1_C1a_en(idC_C1_2, y, c_1, false);
4154
		
4155

    
4156
	(idC_C1, c) 
4157
	=  (idC_C1_3, c_2);
4158

    
4159

    
4160
	tel
4161

    
4162
	until true restart POINTC_C1
4163

    
4164

    
4165

    
4166
	state C1_C1A_IDL:
4167

    
4168
	 	let
4169

    
4170
		
4171

    
4172
	(idC_C1, c) 
4173
	= (idC_C1_1, c_1);
4174
	
4175

    
4176
	tel
4177

    
4178
	until true restart POINTC_C1
4179

    
4180

    
4181

    
4182
	state C1_C1B_IDL:
4183

    
4184
	 	let
4185

    
4186
		
4187

    
4188
	(idC_C1, c) 
4189
	= (idC_C1_1, c_1);
4190
	
4191

    
4192
	tel
4193

    
4194
	until true restart POINTC_C1
4195

    
4196

    
4197

    
4198
tel
4199

    
4200

    
4201
--***************************************************State :Parallel3_C Automaton***************************************************
4202

    
4203
node Parallel3_C_node(idParallel3_C_1:int;
4204
	c_1:int;
4205
	idC_C1_1:int;
4206
	y:int;
4207
	T:bool;
4208
	idC_C2_1:int;
4209
	R:bool;
4210
	S:bool)
4211

    
4212
returns (idParallel3_C:int;
4213
	c:int;
4214
	idC_C1:int;
4215
	idC_C2:int);
4216

    
4217

    
4218
let
4219

    
4220
	 automaton parallel3_c
4221

    
4222
	state POINTParallel3_C:
4223
	unless (idParallel3_C_1=0) restart POINT__TO__C_C1_1
4224

    
4225

    
4226

    
4227
	unless (idParallel3_C_1=1507) and T restart C_C2__TO__C_C1_1
4228

    
4229

    
4230

    
4231
	unless (idParallel3_C_1=1510) and T restart C_C1__TO__C_C2_1
4232

    
4233

    
4234

    
4235
	unless (idParallel3_C_1=1507) restart C_C2_IDL
4236

    
4237
	unless (idParallel3_C_1=1510) restart C_C1_IDL
4238

    
4239
	let
4240

    
4241
		(idParallel3_C, c, idC_C1, idC_C2) 
4242
	= (idParallel3_C_1, c_1, idC_C1_1, idC_C2_1);
4243
	
4244

    
4245
	tel
4246

    
4247

    
4248

    
4249
	state POINT__TO__C_C1_1:
4250

    
4251
	 var 	idParallel3_C_2:int;
4252
	c_2:int;
4253
	idC_C1_2:int;
4254
	let
4255

    
4256
		-- transition trace :
4257
	--POINT__To__C_C1_1
4258
		(idC_C1_2, idParallel3_C_2, c_2) 
4259
	= C_C1_en(idC_C1_1, idParallel3_C_1, c_1, y, false);
4260
		
4261

    
4262
	(idParallel3_C, c, idC_C1) 
4263
	=  (idParallel3_C_2, c_2, idC_C1_2);
4264

    
4265
	--add unused variables
4266
	(idC_C2) 
4267
	= (idC_C2_1);
4268
	
4269

    
4270
	tel
4271

    
4272
	until true restart POINTParallel3_C
4273

    
4274

    
4275

    
4276
	state C_C2__TO__C_C1_1:
4277

    
4278
	 var 	idParallel3_C_2, idParallel3_C_3:int;
4279
	c_2:int;
4280
	idC_C1_2:int;
4281
	idC_C2_2:int;
4282
	let
4283

    
4284
		-- transition trace :
4285
	--C_C2__To__C_C1_1
4286
		(idC_C2_2, idParallel3_C_2) 
4287
	= C_C2_ex(idC_C2_1, idParallel3_C_1, false);
4288
		
4289

    
4290
		(idC_C1_2, idParallel3_C_3, c_2) 
4291
	= C_C1_en(idC_C1_1, idParallel3_C_2, c_1, y, false);
4292
		
4293

    
4294
	(idParallel3_C, c, idC_C1, idC_C2) 
4295
	=  (idParallel3_C_3, c_2, idC_C1_2, idC_C2_2);
4296

    
4297

    
4298
	tel
4299

    
4300
	until true restart POINTParallel3_C
4301

    
4302

    
4303

    
4304
	state C_C1__TO__C_C2_1:
4305

    
4306
	 var 	idParallel3_C_2, idParallel3_C_3:int;
4307
	c_2:int;
4308
	idC_C1_2:int;
4309
	idC_C2_2:int;
4310
	let
4311

    
4312
		-- transition trace :
4313
	--C_C1__To__C_C2_1
4314
		(idC_C1_2, idParallel3_C_2) 
4315
	= C_C1_ex(idC_C1_1, idParallel3_C_1, false);
4316
		
4317

    
4318
		(idC_C2_2, idParallel3_C_3, c_2) 
4319
	= C_C2_en(idC_C2_1, idParallel3_C_2, c_1, y, false);
4320
		
4321

    
4322
	(idParallel3_C, c, idC_C1, idC_C2) 
4323
	=  (idParallel3_C_3, c_2, idC_C1_2, idC_C2_2);
4324

    
4325

    
4326
	tel
4327

    
4328
	until true restart POINTParallel3_C
4329

    
4330

    
4331

    
4332
	state C_C2_IDL:
4333

    
4334
	 var 	c_2:int;
4335
	idC_C2_2:int;
4336
	let
4337

    
4338
		
4339
	(idC_C2_2, c_2) 
4340
	= C_C2_node(idC_C2_1, c_1, y, S, R);
4341

    
4342
		
4343

    
4344

    
4345
	(idParallel3_C, c, idC_C1, idC_C2) 
4346
	= (idParallel3_C_1, c_2, idC_C1_1, idC_C2_2);
4347
	
4348

    
4349
	tel
4350

    
4351
	until true restart POINTParallel3_C
4352

    
4353

    
4354

    
4355
	state C_C1_IDL:
4356

    
4357
	 var 	c_2:int;
4358
	idC_C1_2:int;
4359
	let
4360

    
4361
		
4362
	(idC_C1_2, c_2) 
4363
	= C_C1_node(idC_C1_1, c_1, y, S, R);
4364

    
4365
		
4366

    
4367

    
4368
	(idParallel3_C, c, idC_C1, idC_C2) 
4369
	= (idParallel3_C_1, c_2, idC_C1_2, idC_C2_1);
4370
	
4371

    
4372
	tel
4373

    
4374
	until true restart POINTParallel3_C
4375

    
4376

    
4377

    
4378
tel
4379

    
4380

    
4381
--***************************************************State :A_A2 Automaton***************************************************
4382

    
4383
node A_A2_node(idA_A2_1:int;
4384
	a_1:int;
4385
	x:int;
4386
	S:bool;
4387
	R:bool)
4388

    
4389
returns (idA_A2:int;
4390
	a:int);
4391

    
4392

    
4393
let
4394

    
4395
	 automaton a_a2
4396

    
4397
	state POINTA_A2:
4398
	unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1
4399

    
4400

    
4401

    
4402
	unless (idA_A2_1=1497) and S restart A2_A2A__TO__A2_A2B_1
4403

    
4404

    
4405

    
4406
	unless (idA_A2_1=1498) and R restart A2_A2B__TO__A2_A2A_1
4407

    
4408

    
4409

    
4410
	unless (idA_A2_1=1497) restart A2_A2A_IDL
4411

    
4412
	unless (idA_A2_1=1498) restart A2_A2B_IDL
4413

    
4414
	let
4415

    
4416
		(idA_A2, a) 
4417
	= (idA_A2_1, a_1);
4418
	
4419

    
4420
	tel
4421

    
4422

    
4423

    
4424
	state POINT__TO__A2_A2A_1:
4425

    
4426
	 var 	idA_A2_2:int;
4427
	a_2:int;
4428
	let
4429

    
4430
		-- transition trace :
4431
	--POINT__To__A2_A2a_1
4432
		(idA_A2_2, a_2) 
4433
	= A2_A2a_en(idA_A2_1, x, a_1, false);
4434
		
4435

    
4436
	(idA_A2, a) 
4437
	=  (idA_A2_2, a_2);
4438

    
4439

    
4440
	tel
4441

    
4442
	until true restart POINTA_A2
4443

    
4444

    
4445

    
4446
	state A2_A2A__TO__A2_A2B_1:
4447

    
4448
	 var 	idA_A2_2, idA_A2_3:int;
4449
	a_2:int;
4450
	let
4451

    
4452
		-- transition trace :
4453
	--A2_A2a__To__A2_A2b_1
4454
		(idA_A2_2) 
4455
	= A2_A2a_ex(idA_A2_1, false);
4456
		
4457

    
4458
		(idA_A2_3, a_2) 
4459
	= A2_A2b_en(idA_A2_2, x, a_1, false);
4460
		
4461

    
4462
	(idA_A2, a) 
4463
	=  (idA_A2_3, a_2);
4464

    
4465

    
4466
	tel
4467

    
4468
	until true restart POINTA_A2
4469

    
4470

    
4471

    
4472
	state A2_A2B__TO__A2_A2A_1:
4473

    
4474
	 var 	idA_A2_2, idA_A2_3:int;
4475
	a_2:int;
4476
	let
4477

    
4478
		-- transition trace :
4479
	--A2_A2b__To__A2_A2a_1
4480
		(idA_A2_2) 
4481
	= A2_A2b_ex(idA_A2_1, false);
4482
		
4483

    
4484
		(idA_A2_3, a_2) 
4485
	= A2_A2a_en(idA_A2_2, x, a_1, false);
4486
		
4487

    
4488
	(idA_A2, a) 
4489
	=  (idA_A2_3, a_2);
4490

    
4491

    
4492
	tel
4493

    
4494
	until true restart POINTA_A2
4495

    
4496

    
4497

    
4498
	state A2_A2A_IDL:
4499

    
4500
	 	let
4501

    
4502
		
4503

    
4504
	(idA_A2, a) 
4505
	= (idA_A2_1, a_1);
4506
	
4507

    
4508
	tel
4509

    
4510
	until true restart POINTA_A2
4511

    
4512

    
4513

    
4514
	state A2_A2B_IDL:
4515

    
4516
	 	let
4517

    
4518
		
4519

    
4520
	(idA_A2, a) 
4521
	= (idA_A2_1, a_1);
4522
	
4523

    
4524
	tel
4525

    
4526
	until true restart POINTA_A2
4527

    
4528

    
4529

    
4530
tel
4531

    
4532

    
4533
--***************************************************State :A_A1 Automaton***************************************************
4534

    
4535
node A_A1_node(idA_A1_1:int;
4536
	a_1:int;
4537
	x:int;
4538
	S:bool;
4539
	R:bool)
4540

    
4541
returns (idA_A1:int;
4542
	a:int);
4543

    
4544

    
4545
let
4546

    
4547
	 automaton a_a1
4548

    
4549
	state POINTA_A1:
4550
	unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1
4551

    
4552

    
4553

    
4554
	unless (idA_A1_1=1494) and S restart A1_A1A__TO__A1_A1B_1
4555

    
4556

    
4557

    
4558
	unless (idA_A1_1=1495) and R restart A1_A1B__TO__A1_A1A_1
4559

    
4560

    
4561

    
4562
	unless (idA_A1_1=1494) restart A1_A1A_IDL
4563

    
4564
	unless (idA_A1_1=1495) restart A1_A1B_IDL
4565

    
4566
	let
4567

    
4568
		(idA_A1, a) 
4569
	= (idA_A1_1, a_1);
4570
	
4571

    
4572
	tel
4573

    
4574

    
4575

    
4576
	state POINT__TO__A1_A1A_1:
4577

    
4578
	 var 	idA_A1_2:int;
4579
	a_2:int;
4580
	let
4581

    
4582
		-- transition trace :
4583
	--POINT__To__A1_A1a_1
4584
		(idA_A1_2, a_2) 
4585
	= A1_A1a_en(idA_A1_1, x, a_1, false);
4586
		
4587

    
4588
	(idA_A1, a) 
4589
	=  (idA_A1_2, a_2);
4590

    
4591

    
4592
	tel
4593

    
4594
	until true restart POINTA_A1
4595

    
4596

    
4597

    
4598
	state A1_A1A__TO__A1_A1B_1:
4599

    
4600
	 var 	idA_A1_2, idA_A1_3:int;
4601
	a_2:int;
4602
	let
4603

    
4604
		-- transition trace :
4605
	--A1_A1a__To__A1_A1b_1
4606
		(idA_A1_2) 
4607
	= A1_A1a_ex(idA_A1_1, false);
4608
		
4609

    
4610
		(idA_A1_3, a_2) 
4611
	= A1_A1b_en(idA_A1_2, x, a_1, false);
4612
		
4613

    
4614
	(idA_A1, a) 
4615
	=  (idA_A1_3, a_2);
4616

    
4617

    
4618
	tel
4619

    
4620
	until true restart POINTA_A1
4621

    
4622

    
4623

    
4624
	state A1_A1B__TO__A1_A1A_1:
4625

    
4626
	 var 	idA_A1_2, idA_A1_3:int;
4627
	a_2:int;
4628
	let
4629

    
4630
		-- transition trace :
4631
	--A1_A1b__To__A1_A1a_1
4632
		(idA_A1_2) 
4633
	= A1_A1b_ex(idA_A1_1, false);
4634
		
4635

    
4636
		(idA_A1_3, a_2) 
4637
	= A1_A1a_en(idA_A1_2, x, a_1, false);
4638
		
4639

    
4640
	(idA_A1, a) 
4641
	=  (idA_A1_3, a_2);
4642

    
4643

    
4644
	tel
4645

    
4646
	until true restart POINTA_A1
4647

    
4648

    
4649

    
4650
	state A1_A1A_IDL:
4651

    
4652
	 	let
4653

    
4654
		
4655

    
4656
	(idA_A1, a) 
4657
	= (idA_A1_1, a_1);
4658
	
4659

    
4660
	tel
4661

    
4662
	until true restart POINTA_A1
4663

    
4664

    
4665

    
4666
	state A1_A1B_IDL:
4667

    
4668
	 	let
4669

    
4670
		
4671

    
4672
	(idA_A1, a) 
4673
	= (idA_A1_1, a_1);
4674
	
4675

    
4676
	tel
4677

    
4678
	until true restart POINTA_A1
4679

    
4680

    
4681

    
4682
tel
4683

    
4684

    
4685
--***************************************************State :Parallel3_A Automaton***************************************************
4686

    
4687
node Parallel3_A_node(idParallel3_A_1:int;
4688
	a_1:int;
4689
	idA_A1_1:int;
4690
	x:int;
4691
	T:bool;
4692
	idA_A2_1:int;
4693
	R:bool;
4694
	S:bool)
4695

    
4696
returns (idParallel3_A:int;
4697
	a:int;
4698
	idA_A1:int;
4699
	idA_A2:int);
4700

    
4701

    
4702
let
4703

    
4704
	 automaton parallel3_a
4705

    
4706
	state POINTParallel3_A:
4707
	unless (idParallel3_A_1=0) restart POINT__TO__A_A1_1
4708

    
4709

    
4710

    
4711
	unless (idParallel3_A_1=1493) and T restart A_A1__TO__A_A2_1
4712

    
4713

    
4714

    
4715
	unless (idParallel3_A_1=1496) and T restart A_A2__TO__A_A1_1
4716

    
4717

    
4718

    
4719
	unless (idParallel3_A_1=1493) restart A_A1_IDL
4720

    
4721
	unless (idParallel3_A_1=1496) restart A_A2_IDL
4722

    
4723
	let
4724

    
4725
		(idParallel3_A, a, idA_A1, idA_A2) 
4726
	= (idParallel3_A_1, a_1, idA_A1_1, idA_A2_1);
4727
	
4728

    
4729
	tel
4730

    
4731

    
4732

    
4733
	state POINT__TO__A_A1_1:
4734

    
4735
	 var 	idParallel3_A_2:int;
4736
	a_2:int;
4737
	idA_A1_2:int;
4738
	let
4739

    
4740
		-- transition trace :
4741
	--POINT__To__A_A1_1
4742
		(idA_A1_2, idParallel3_A_2, a_2) 
4743
	= A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false);
4744
		
4745

    
4746
	(idParallel3_A, a, idA_A1) 
4747
	=  (idParallel3_A_2, a_2, idA_A1_2);
4748

    
4749
	--add unused variables
4750
	(idA_A2) 
4751
	= (idA_A2_1);
4752
	
4753

    
4754
	tel
4755

    
4756
	until true restart POINTParallel3_A
4757

    
4758

    
4759

    
4760
	state A_A1__TO__A_A2_1:
4761

    
4762
	 var 	idParallel3_A_2, idParallel3_A_3:int;
4763
	a_2:int;
4764
	idA_A1_2:int;
4765
	idA_A2_2:int;
4766
	let
4767

    
4768
		-- transition trace :
4769
	--A_A1__To__A_A2_1
4770
		(idA_A1_2, idParallel3_A_2) 
4771
	= A_A1_ex(idA_A1_1, idParallel3_A_1, false);
4772
		
4773

    
4774
		(idA_A2_2, idParallel3_A_3, a_2) 
4775
	= A_A2_en(idA_A2_1, idParallel3_A_2, a_1, x, false);
4776
		
4777

    
4778
	(idParallel3_A, a, idA_A1, idA_A2) 
4779
	=  (idParallel3_A_3, a_2, idA_A1_2, idA_A2_2);
4780

    
4781

    
4782
	tel
4783

    
4784
	until true restart POINTParallel3_A
4785

    
4786

    
4787

    
4788
	state A_A2__TO__A_A1_1:
4789

    
4790
	 var 	idParallel3_A_2, idParallel3_A_3:int;
4791
	a_2:int;
4792
	idA_A1_2:int;
4793
	idA_A2_2:int;
4794
	let
4795

    
4796
		-- transition trace :
4797
	--A_A2__To__A_A1_1
4798
		(idA_A2_2, idParallel3_A_2) 
4799
	= A_A2_ex(idA_A2_1, idParallel3_A_1, false);
4800
		
4801

    
4802
		(idA_A1_2, idParallel3_A_3, a_2) 
4803
	= A_A1_en(idA_A1_1, idParallel3_A_2, a_1, x, false);
4804
		
4805

    
4806
	(idParallel3_A, a, idA_A1, idA_A2) 
4807
	=  (idParallel3_A_3, a_2, idA_A1_2, idA_A2_2);
4808

    
4809

    
4810
	tel
4811

    
4812
	until true restart POINTParallel3_A
4813

    
4814

    
4815

    
4816
	state A_A1_IDL:
4817

    
4818
	 var 	a_2:int;
4819
	idA_A1_2:int;
4820
	let
4821

    
4822
		
4823
	(idA_A1_2, a_2) 
4824
	= A_A1_node(idA_A1_1, a_1, x, S, R);
4825

    
4826
		
4827

    
4828

    
4829
	(idParallel3_A, a, idA_A1, idA_A2) 
4830
	= (idParallel3_A_1, a_2, idA_A1_2, idA_A2_1);
4831
	
4832

    
4833
	tel
4834

    
4835
	until true restart POINTParallel3_A
4836

    
4837

    
4838

    
4839
	state A_A2_IDL:
4840

    
4841
	 var 	a_2:int;
4842
	idA_A2_2:int;
4843
	let
4844

    
4845
		
4846
	(idA_A2_2, a_2) 
4847
	= A_A2_node(idA_A2_1, a_1, x, S, R);
4848

    
4849
		
4850

    
4851

    
4852
	(idParallel3_A, a, idA_A1, idA_A2) 
4853
	= (idParallel3_A_1, a_2, idA_A1_1, idA_A2_2);
4854
	
4855

    
4856
	tel
4857

    
4858
	until true restart POINTParallel3_A
4859

    
4860

    
4861

    
4862
tel
4863

    
4864

    
4865
--***************************************************State :Parallel3_Parallel3 Automaton***************************************************
4866

    
4867
node Parallel3_Parallel3_node(idParallel3_Parallel3_1:int;
4868
	a_1:int;
4869
	idA_A1_1:int;
4870
	idA_A2_1:int;
4871
	idParallel3_A_1:int;
4872
	x:int;
4873
	b_1:int;
4874
	idB_B1_1:int;
4875
	idB_B2_1:int;
4876
	idParallel3_B_1:int;
4877
	c_1:int;
4878
	idC_C1_1:int;
4879
	idC_C2_1:int;
4880
	idParallel3_C_1:int;
4881
	y:int;
4882
	dd_1:int;
4883
	idD_D1_1:int;
4884
	idD_D2_1:int;
4885
	idParallel3_D_1:int;
4886
	R:bool;
4887
	S:bool;
4888
	T:bool)
4889

    
4890
returns (idParallel3_Parallel3:int;
4891
	a:int;
4892
	idA_A1:int;
4893
	idA_A2:int;
4894
	idParallel3_A:int;
4895
	b:int;
4896
	idB_B1:int;
4897
	idB_B2:int;
4898
	idParallel3_B:int;
4899
	c:int;
4900
	idC_C1:int;
4901
	idC_C2:int;
4902
	idParallel3_C:int;
4903
	dd:int;
4904
	idD_D1:int;
4905
	idD_D2:int;
4906
	idParallel3_D:int);
4907

    
4908

    
4909
let
4910

    
4911
	 automaton parallel3_parallel3
4912

    
4913
	state POINTParallel3_Parallel3:
4914
	unless (idParallel3_Parallel3_1=0) restart PARALLEL3_PARALLEL3_PARALLEL_ENTRY
4915
	unless true  restart PARALLEL3_PARALLEL3_PARALLEL_IDL
4916

    
4917
	let
4918

    
4919
		(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D) 
4920
	= (idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, idC_C1_1, idC_C2_1, idParallel3_C_1, dd_1, idD_D1_1, idD_D2_1, idParallel3_D_1);
4921
	
4922

    
4923
	tel
4924

    
4925

    
4926

    
4927
	state PARALLEL3_PARALLEL3_PARALLEL_ENTRY:
4928

    
4929
	 var 	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4, idParallel3_Parallel3_5:int;
4930
	a_2:int;
4931
	idA_A1_2:int;
4932
	idA_A2_2:int;
4933
	idParallel3_A_2:int;
4934
	b_2:int;
4935
	idB_B1_2:int;
4936
	idB_B2_2:int;
4937
	idParallel3_B_2:int;
4938
	c_2:int;
4939
	idC_C1_2:int;
4940
	idC_C2_2:int;
4941
	idParallel3_C_2:int;
4942
	dd_2:int;
4943
	idD_D1_2:int;
4944
	idD_D2_2:int;
4945
	idParallel3_D_2:int;
4946
	let
4947

    
4948
		
4949
	(idParallel3_A_2, idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2) 
4950
	= Parallel3_A_en(idParallel3_A_1, idParallel3_Parallel3_1, a_1, idA_A1_1, x, idA_A2_1, false);
4951

    
4952
	(idParallel3_B_2, idParallel3_Parallel3_3, b_2, idB_B1_2, idB_B2_2) 
4953
	= Parallel3_B_en(idParallel3_B_1, idParallel3_Parallel3_2, b_1, idB_B1_1, x, idB_B2_1, false);
4954

    
4955
	(idParallel3_C_2, idParallel3_Parallel3_4, c_2, idC_C1_2, idC_C2_2) 
4956
	= Parallel3_C_en(idParallel3_C_1, idParallel3_Parallel3_3, c_1, idC_C1_1, y, idC_C2_1, false);
4957

    
4958
	(idParallel3_D_2, idParallel3_Parallel3_5, dd_2, idD_D1_2, idD_D2_2) 
4959
	= Parallel3_D_en(idParallel3_D_1, idParallel3_Parallel3_4, dd_1, idD_D1_1, y, idD_D2_1, false);
4960

    
4961

    
4962
	(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D) 
4963
	= (idParallel3_Parallel3_5, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2);
4964
	
4965

    
4966
	tel
4967

    
4968
	until true restart POINTParallel3_Parallel3
4969

    
4970

    
4971

    
4972
	state PARALLEL3_PARALLEL3_PARALLEL_IDL:
4973

    
4974
	 var 	a_2:int;
4975
	idA_A1_2:int;
4976
	idA_A2_2:int;
4977
	idParallel3_A_2:int;
4978
	b_2:int;
4979
	idB_B1_2:int;
4980
	idB_B2_2:int;
4981
	idParallel3_B_2:int;
4982
	c_2:int;
4983
	idC_C1_2:int;
4984
	idC_C2_2:int;
4985
	idParallel3_C_2:int;
4986
	dd_2:int;
4987
	idD_D1_2:int;
4988
	idD_D2_2:int;
4989
	idParallel3_D_2:int;
4990
	let
4991

    
4992
		
4993

    
4994
		(idParallel3_A_2, a_2, idA_A1_2, idA_A2_2)
4995
	= if not (idParallel3_A_1= 0 ) then Parallel3_A_node(idParallel3_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R, S)
4996

    
4997
		 else (idParallel3_A_1, a_1, idA_A1_1, idA_A2_1);
4998

    
4999
		
5000

    
5001
		
5002

    
5003
		(idParallel3_B_2, b_2, idB_B1_2, idB_B2_2)
5004
	= if not (idParallel3_B_1= 0 ) then Parallel3_B_node(idParallel3_B_1, b_1, idB_B1_1, x, T, idB_B2_1, R, S)
5005

    
5006
		 else (idParallel3_B_1, b_1, idB_B1_1, idB_B2_1);
5007

    
5008
		
5009

    
5010
		
5011

    
5012
		(idParallel3_C_2, c_2, idC_C1_2, idC_C2_2)
5013
	= if not (idParallel3_C_1= 0 ) then Parallel3_C_node(idParallel3_C_1, c_1, idC_C1_1, y, T, idC_C2_1, R, S)
5014

    
5015
		 else (idParallel3_C_1, c_1, idC_C1_1, idC_C2_1);
5016

    
5017
		
5018

    
5019
		
5020

    
5021
		(idParallel3_D_2, dd_2, idD_D1_2, idD_D2_2)
5022
	= if not (idParallel3_D_1= 0 ) then Parallel3_D_node(idParallel3_D_1, dd_1, idD_D1_1, y, T, idD_D2_1, R, S)
5023

    
5024
		 else (idParallel3_D_1, dd_1, idD_D1_1, idD_D2_1);
5025

    
5026
		
5027

    
5028
		
5029

    
5030
	(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D) 
5031
	= (idParallel3_Parallel3_1, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2);
5032
	
5033

    
5034
	tel
5035

    
5036
	until true restart POINTParallel3_Parallel3
5037

    
5038

    
5039

    
5040
tel
5041

    
5042

    
5043
--***************************************************State :Parallel3_Parallel3 Automaton***************************************************
5044

    
5045
node Parallel3_Parallel3(x:int;
5046
	y:int;
5047
	R:bool;
5048
	S:bool;
5049
	T:bool)
5050

    
5051
returns (a:int;
5052
	b:int;
5053
	dd:int;
5054
	c:int);
5055

    
5056

    
5057
var a_1: int;
5058

    
5059
	b_1: int;
5060

    
5061
	dd_1: int;
5062

    
5063
	c_1: int;
5064

    
5065
	idParallel3_Parallel3, idParallel3_Parallel3_1: int;
5066

    
5067
	idB_B2, idB_B2_1: int;
5068

    
5069
	idB_B1, idB_B1_1: int;
5070

    
5071
	idParallel3_B, idParallel3_B_1: int;
5072

    
5073
	idD_D2, idD_D2_1: int;
5074

    
5075
	idD_D1, idD_D1_1: int;
5076

    
5077
	idParallel3_D, idParallel3_D_1: int;
5078

    
5079
	idC_C2, idC_C2_1: int;
5080

    
5081
	idC_C1, idC_C1_1: int;
5082

    
5083
	idParallel3_C, idParallel3_C_1: int;
5084

    
5085
	idA_A2, idA_A2_1: int;
5086

    
5087
	idA_A1, idA_A1_1: int;
5088

    
5089
	idParallel3_A, idParallel3_A_1: int;
5090

    
5091
		idParallel3_Parallel3_2, idParallel3_Parallel3_3:int;
5092
	a_2, a_3:int;
5093
	idA_A1_2, idA_A1_3:int;
5094
	idA_A2_2, idA_A2_3:int;
5095
	idParallel3_A_2, idParallel3_A_3:int;
5096
	b_2, b_3:int;
5097
	idB_B1_2, idB_B1_3:int;
5098
	idB_B2_2, idB_B2_3:int;
5099
	idParallel3_B_2, idParallel3_B_3:int;
5100
	c_2, c_3:int;
5101
	idC_C1_2, idC_C1_3:int;
5102
	idC_C2_2, idC_C2_3:int;
5103
	idParallel3_C_2, idParallel3_C_3:int;
5104
	dd_2, dd_3:int;
5105
	idD_D1_2, idD_D1_3:int;
5106
	idD_D2_2, idD_D2_3:int;
5107
	idParallel3_D_2, idParallel3_D_3:int;
5108
let
5109

    
5110
	a_1 = 0 -> pre a;
5111

    
5112
	b_1 = 0 -> pre b;
5113

    
5114
	dd_1 = 0 -> pre dd;
5115

    
5116
	c_1 = 0 -> pre c;
5117

    
5118
	idParallel3_Parallel3_1 = 0 -> pre idParallel3_Parallel3;
5119

    
5120
	idB_B2_1 = 0 -> pre idB_B2;
5121

    
5122
	idB_B1_1 = 0 -> pre idB_B1;
5123

    
5124
	idParallel3_B_1 = 0 -> pre idParallel3_B;
5125

    
5126
	idD_D2_1 = 0 -> pre idD_D2;
5127

    
5128
	idD_D1_1 = 0 -> pre idD_D1;
5129

    
5130
	idParallel3_D_1 = 0 -> pre idParallel3_D;
5131

    
5132
	idC_C2_1 = 0 -> pre idC_C2;
5133

    
5134
	idC_C1_1 = 0 -> pre idC_C1;
5135

    
5136
	idParallel3_C_1 = 0 -> pre idParallel3_C;
5137

    
5138
	idA_A2_1 = 0 -> pre idA_A2;
5139

    
5140
	idA_A1_1 = 0 -> pre idA_A1;
5141

    
5142
	idParallel3_A_1 = 0 -> pre idParallel3_A;
5143

    
5144
	
5145

    
5146

    
5147

    
5148
	(idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2)
5149
	 = 
5150

    
5151
	 if R then Parallel3_Parallel3_node(idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, x, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, idC_C1_1, idC_C2_1, idParallel3_C_1, y, dd_1, idD_D1_1, idD_D2_1, idParallel3_D_1, R, false, false)
5152

    
5153
	 else (idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, idC_C1_1, idC_C2_1, idParallel3_C_1, dd_1, idD_D1_1, idD_D2_1, idParallel3_D_1);
5154

    
5155
	
5156

    
5157

    
5158

    
5159
	(idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, idC_C1_3, idC_C2_3, idParallel3_C_3, dd_3, idD_D1_3, idD_D2_3, idParallel3_D_3)
5160
	 = 
5161

    
5162
	 if S then Parallel3_Parallel3_node(idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, x, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, y, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2, false, S, false)
5163

    
5164
	 else (idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, idC_C1_2, idC_C2_2, idParallel3_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel3_D_2);
5165

    
5166
	
5167

    
5168

    
5169

    
5170
	(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, idC_C1, idC_C2, idParallel3_C, dd, idD_D1, idD_D2, idParallel3_D)
5171
	 = 
5172

    
5173
	 if T then Parallel3_Parallel3_node(idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, x, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, idC_C1_3, idC_C2_3, idParallel3_C_3, y, dd_3, idD_D1_3, idD_D2_3, idParallel3_D_3, false, false, T)
5174

    
5175
	 else (idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, idC_C1_3, idC_C2_3, idParallel3_C_3, dd_3, idD_D1_3, idD_D2_3, idParallel3_D_3);
5176

    
5177
	
5178

    
5179

    
5180
--unused outputs
5181
	
5182

    
5183
tel
5184

    
5185

    
5186

    
5187
node Parallel3 (x_1_1 : int; R_1_1 : real; y_1_1 : int; S_1_1 : real; T_1_1 : real)
5188
returns (a_1_1 : int;
5189
	b_2_1 : int;
5190
	dd_3_1 : int;
5191
	c_4_1 : int); 
5192
var
5193
	Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real;
5194
	Parallel3_1_1 : int; Parallel3_2_1 : int; Parallel3_3_1 : int; Parallel3_4_1 : int;
5195
	i_virtual_local : real;
5196
	Parallel3Mux_1_1_event: bool;
5197
	Parallel3Mux_1_2_event: bool;
5198
	Parallel3Mux_1_3_event: bool;
5199
let 
5200
	Mux_1_1 = R_1_1 ;
5201
	Mux_1_2 = S_1_1 ;
5202
	Mux_1_3 = T_1_1 ;
5203
	Parallel3Mux_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));
5204
	Parallel3Mux_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));
5205
	Parallel3Mux_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));
5206
	(Parallel3_1_1, Parallel3_2_1, Parallel3_3_1, Parallel3_4_1) =  Parallel3_Parallel3(x_1_1, y_1_1, Parallel3Mux_1_1_event, Parallel3Mux_1_2_event, Parallel3Mux_1_3_event);
5207
	a_1_1 = Parallel3_1_1;
5208
	b_2_1 = Parallel3_2_1;
5209
	dd_3_1 = Parallel3_3_1;
5210
	c_4_1 = Parallel3_4_1;
5211
	i_virtual_local= 0.0 -> 1.0;
5212
tel
5213