Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Parallel4 / Parallel4.lus @ eb639349

History | View | Annotate | Download (82.2 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9

    
10

    
11

    
12

    
13

    
14

    
15

    
16

    
17

    
18

    
19

    
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

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

    
52
returns (idB_B2:int;
53
	a:int;
54
	b:int);
55

    
56

    
57
var 	idB_B2_2:int;
58
	b_2:int;
59

    
60

    
61
let
62

    
63

    
64

    
65
	-- set state as active 
66
	idB_B2_2 
67
	= 1655;
68
	
69

    
70
	b_2 
71
	= if (not isInner) then  a_1 +7
72
	 else b_1;
73
	
74

    
75
	(idB_B2, a, b) 
76
	= (idB_B2_2, a_1, b_2);
77
	
78

    
79
tel
80

    
81

    
82

    
83

    
84

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

    
89
returns (idB_B2:int);
90

    
91

    
92
var 	idB_B2_2:int;
93

    
94

    
95
let
96

    
97

    
98

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

    
103

    
104
	(idB_B2) 
105
	= (idB_B2_1);
106
	
107

    
108
tel
109

    
110

    
111

    
112

    
113

    
114

    
115
-- Entry action for state :B2_B2b
116
node B2_B2b_en(idB_B2_1:int;
117
	a_1:int;
118
	b_1:int;
119
	isInner:bool)
120

    
121
returns (idB_B2:int;
122
	a:int;
123
	b:int);
124

    
125

    
126
var 	idB_B2_2:int;
127
	b_2:int;
128

    
129

    
130
let
131

    
132

    
133

    
134
	-- set state as active 
135
	idB_B2_2 
136
	= 1656;
137
	
138

    
139
	b_2 
140
	= if (not isInner) then  a_1 +8
141
	 else b_1;
142
	
143

    
144
	(idB_B2, a, b) 
145
	= (idB_B2_2, a_1, b_2);
146
	
147

    
148
tel
149

    
150

    
151

    
152

    
153

    
154
-- Exit action for state :B2_B2b
155
node B2_B2b_ex(idB_B2_1:int;
156
	isInner:bool)
157

    
158
returns (idB_B2:int);
159

    
160

    
161
var 	idB_B2_2:int;
162

    
163

    
164
let
165

    
166

    
167

    
168
	-- set state as inactive 
169
	idB_B2_2
170
	 = if (not isInner) then 0 else idB_B2_1;
171

    
172

    
173
	(idB_B2) 
174
	= (idB_B2_1);
175
	
176

    
177
tel
178

    
179

    
180

    
181

    
182

    
183

    
184
-- Entry action for state :B_B2
185
node B_B2_en(idB_B2_1:int;
186
	idParallel4_B_1:int;
187
	a_1:int;
188
	b_1:int;
189
	isInner:bool)
190

    
191
returns (idB_B2:int;
192
	idParallel4_B:int;
193
	a:int;
194
	b:int);
195

    
196

    
197
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5, idB_B2_6:int;
198
	idParallel4_B_2, idParallel4_B_3, idParallel4_B_4:int;
199
	a_2, a_3, a_4, a_5, a_6:int;
200
	b_2, b_3, b_4, b_5, b_6:int;
201

    
202

    
203
let
204

    
205

    
206

    
207
	-- set state as active 
208
	idParallel4_B_2 
209
	= 1654;
210
	
211

    
212
	
213
-- transition trace :
214
	--POINT__To__B2_B2a_1
215
		(idB_B2_2, a_2, b_2) 
216
	= B2_B2a_en(idB_B2_1, a_1, b_1, false);
217
		
218

    
219
	(idB_B2_3, idParallel4_B_3, a_3, b_3) 
220
	= 
221

    
222
	if ( idB_B2_1 = 0) then
223

    
224
	 (idB_B2_2, idParallel4_B_2, a_2, b_2)
225

    
226
	 else(idB_B2_1, idParallel4_B_2, a_1, b_1);
227

    
228
	
229

    
230
	(idB_B2_4, a_4, b_4) 
231
	= 
232
	if ( idB_B2_1 = 1655) then
233
	B2_B2a_en(idB_B2_1, a_1, b_1, false)
234
	 else (idB_B2_1, a_1, b_1);
235

    
236
	
237

    
238
	(idB_B2_5, a_5, b_5) 
239
	= 
240
	if ( idB_B2_1 = 1656) then
241
	B2_B2b_en(idB_B2_1, a_1, b_1, false)
242
	 else (idB_B2_1, a_1, b_1);
243

    
244
	
245

    
246
	(idB_B2_6, idParallel4_B_4, a_6, b_6) 
247
	= 
248
		 if ( idB_B2_1 = 0) then 
249
		(idB_B2_3, idParallel4_B_3, a_3, b_3)
250
		 else
251
		 if ( idB_B2_1 = 1655) then 
252
		(idB_B2_4, idParallel4_B_3, a_4, b_4)
253
		 else
254
		 if ( idB_B2_1 = 1656) then 
255
		(idB_B2_5, idParallel4_B_3, a_5, b_5)
256
		 else (idB_B2_1, idParallel4_B_2, a_1, b_1);
257

    
258

    
259
	(idB_B2, idParallel4_B, a, b) 
260
	= (idB_B2_6, idParallel4_B_4, a_6, b_6);
261
	
262

    
263
tel
264

    
265

    
266

    
267

    
268

    
269
-- Exit action for state :B_B2
270
node B_B2_ex(idB_B2_1:int;
271
	idParallel4_B_1:int;
272
	isInner:bool)
273

    
274
returns (idB_B2:int;
275
	idParallel4_B:int);
276

    
277

    
278
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5:int;
279
	idParallel4_B_2:int;
280

    
281

    
282
let
283

    
284

    
285

    
286
	
287
	(idB_B2_2) 
288
	= 
289
	if ( idB_B2_1 = 1655) then
290
	B2_B2a_ex(idB_B2_1, false)
291
	 else (idB_B2_1);
292

    
293
	
294

    
295
	(idB_B2_3) 
296
	= 
297
	if ( idB_B2_1 = 1656) then
298
	B2_B2b_ex(idB_B2_1, false)
299
	 else (idB_B2_1);
300

    
301
	
302

    
303
	(idB_B2_4) 
304
	= 
305
		 if ( idB_B2_1 = 1655) then 
306
		(idB_B2_2)
307
		 else
308
		 if ( idB_B2_1 = 1656) then 
309
		(idB_B2_3)
310
		 else (idB_B2_1);
311

    
312

    
313
	-- set state as inactive 
314
	idParallel4_B_2
315
	 = if (not isInner) then 0 else idParallel4_B_1;
316

    
317
	idB_B2_5 
318
	= 0;
319
	
320

    
321
	(idB_B2, idParallel4_B) 
322
	= (idB_B2_5, idParallel4_B_1);
323
	
324

    
325
tel
326

    
327

    
328

    
329

    
330

    
331

    
332
-- Entry action for state :B1_B1a
333
node B1_B1a_en(idB_B1_1:int;
334
	a_1:int;
335
	b_1:int;
336
	isInner:bool)
337

    
338
returns (idB_B1:int;
339
	a:int;
340
	b:int);
341

    
342

    
343
var 	idB_B1_2:int;
344
	b_2:int;
345

    
346

    
347
let
348

    
349

    
350

    
351
	-- set state as active 
352
	idB_B1_2 
353
	= 1658;
354
	
355

    
356
	b_2 
357
	= if (not isInner) then  a_1 +5
358
	 else b_1;
359
	
360

    
361
	(idB_B1, a, b) 
362
	= (idB_B1_2, a_1, b_2);
363
	
364

    
365
tel
366

    
367

    
368

    
369

    
370

    
371
-- Exit action for state :B1_B1a
372
node B1_B1a_ex(idB_B1_1:int;
373
	isInner:bool)
374

    
375
returns (idB_B1:int);
376

    
377

    
378
var 	idB_B1_2:int;
379

    
380

    
381
let
382

    
383

    
384

    
385
	-- set state as inactive 
386
	idB_B1_2
387
	 = if (not isInner) then 0 else idB_B1_1;
388

    
389

    
390
	(idB_B1) 
391
	= (idB_B1_1);
392
	
393

    
394
tel
395

    
396

    
397

    
398

    
399

    
400

    
401
-- Entry action for state :B1_B1b
402
node B1_B1b_en(idB_B1_1:int;
403
	a_1:int;
404
	b_1:int;
405
	isInner:bool)
406

    
407
returns (idB_B1:int;
408
	a:int;
409
	b:int);
410

    
411

    
412
var 	idB_B1_2:int;
413
	b_2:int;
414

    
415

    
416
let
417

    
418

    
419

    
420
	-- set state as active 
421
	idB_B1_2 
422
	= 1659;
423
	
424

    
425
	b_2 
426
	= if (not isInner) then  a_1 +6
427
	 else b_1;
428
	
429

    
430
	(idB_B1, a, b) 
431
	= (idB_B1_2, a_1, b_2);
432
	
433

    
434
tel
435

    
436

    
437

    
438

    
439

    
440
-- Exit action for state :B1_B1b
441
node B1_B1b_ex(idB_B1_1:int;
442
	isInner:bool)
443

    
444
returns (idB_B1:int);
445

    
446

    
447
var 	idB_B1_2:int;
448

    
449

    
450
let
451

    
452

    
453

    
454
	-- set state as inactive 
455
	idB_B1_2
456
	 = if (not isInner) then 0 else idB_B1_1;
457

    
458

    
459
	(idB_B1) 
460
	= (idB_B1_1);
461
	
462

    
463
tel
464

    
465

    
466

    
467

    
468

    
469

    
470
-- Entry action for state :B_B1
471
node B_B1_en(idB_B1_1:int;
472
	idParallel4_B_1:int;
473
	a_1:int;
474
	b_1:int;
475
	isInner:bool)
476

    
477
returns (idB_B1:int;
478
	idParallel4_B:int;
479
	a:int;
480
	b:int);
481

    
482

    
483
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5, idB_B1_6:int;
484
	idParallel4_B_2, idParallel4_B_3, idParallel4_B_4:int;
485
	a_2, a_3, a_4, a_5, a_6:int;
486
	b_2, b_3, b_4, b_5, b_6:int;
487

    
488

    
489
let
490

    
491

    
492

    
493
	-- set state as active 
494
	idParallel4_B_2 
495
	= 1657;
496
	
497

    
498
	
499
-- transition trace :
500
	--POINT__To__B1_B1a_1
501
		(idB_B1_2, a_2, b_2) 
502
	= B1_B1a_en(idB_B1_1, a_1, b_1, false);
503
		
504

    
505
	(idB_B1_3, idParallel4_B_3, a_3, b_3) 
506
	= 
507

    
508
	if ( idB_B1_1 = 0) then
509

    
510
	 (idB_B1_2, idParallel4_B_2, a_2, b_2)
511

    
512
	 else(idB_B1_1, idParallel4_B_2, a_1, b_1);
513

    
514
	
515

    
516
	(idB_B1_4, a_4, b_4) 
517
	= 
518
	if ( idB_B1_1 = 1658) then
519
	B1_B1a_en(idB_B1_1, a_1, b_1, false)
520
	 else (idB_B1_1, a_1, b_1);
521

    
522
	
523

    
524
	(idB_B1_5, a_5, b_5) 
525
	= 
526
	if ( idB_B1_1 = 1659) then
527
	B1_B1b_en(idB_B1_1, a_1, b_1, false)
528
	 else (idB_B1_1, a_1, b_1);
529

    
530
	
531

    
532
	(idB_B1_6, idParallel4_B_4, a_6, b_6) 
533
	= 
534
		 if ( idB_B1_1 = 0) then 
535
		(idB_B1_3, idParallel4_B_3, a_3, b_3)
536
		 else
537
		 if ( idB_B1_1 = 1658) then 
538
		(idB_B1_4, idParallel4_B_3, a_4, b_4)
539
		 else
540
		 if ( idB_B1_1 = 1659) then 
541
		(idB_B1_5, idParallel4_B_3, a_5, b_5)
542
		 else (idB_B1_1, idParallel4_B_2, a_1, b_1);
543

    
544

    
545
	(idB_B1, idParallel4_B, a, b) 
546
	= (idB_B1_6, idParallel4_B_4, a_6, b_6);
547
	
548

    
549
tel
550

    
551

    
552

    
553

    
554

    
555
-- Exit action for state :B_B1
556
node B_B1_ex(idB_B1_1:int;
557
	idParallel4_B_1:int;
558
	isInner:bool)
559

    
560
returns (idB_B1:int;
561
	idParallel4_B:int);
562

    
563

    
564
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
565
	idParallel4_B_2:int;
566

    
567

    
568
let
569

    
570

    
571

    
572
	
573
	(idB_B1_2) 
574
	= 
575
	if ( idB_B1_1 = 1658) then
576
	B1_B1a_ex(idB_B1_1, false)
577
	 else (idB_B1_1);
578

    
579
	
580

    
581
	(idB_B1_3) 
582
	= 
583
	if ( idB_B1_1 = 1659) then
584
	B1_B1b_ex(idB_B1_1, false)
585
	 else (idB_B1_1);
586

    
587
	
588

    
589
	(idB_B1_4) 
590
	= 
591
		 if ( idB_B1_1 = 1658) then 
592
		(idB_B1_2)
593
		 else
594
		 if ( idB_B1_1 = 1659) then 
595
		(idB_B1_3)
596
		 else (idB_B1_1);
597

    
598

    
599
	-- set state as inactive 
600
	idParallel4_B_2
601
	 = if (not isInner) then 0 else idParallel4_B_1;
602

    
603
	idB_B1_5 
604
	= 0;
605
	
606

    
607
	(idB_B1, idParallel4_B) 
608
	= (idB_B1_5, idParallel4_B_1);
609
	
610

    
611
tel
612

    
613

    
614

    
615

    
616

    
617

    
618
-- Entry action for state :Parallel4_B
619
node Parallel4_B_en(idParallel4_B_1:int;
620
	idParallel4_Parallel4_1:int;
621
	a_1:int;
622
	b_1:int;
623
	idB_B1_1:int;
624
	idB_B2_1:int;
625
	isInner:bool)
626

    
627
returns (idParallel4_B:int;
628
	idParallel4_Parallel4:int;
629
	a:int;
630
	b:int;
631
	idB_B1:int;
632
	idB_B2:int);
633

    
634

    
635
var 	idParallel4_B_2, idParallel4_B_3, idParallel4_B_4, idParallel4_B_5, idParallel4_B_6:int;
636
	idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4:int;
637
	a_2, a_3, a_4, a_5, a_6:int;
638
	b_2, b_3, b_4, b_5, b_6:int;
639
	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
640
	idB_B2_2, idB_B2_3:int;
641

    
642

    
643
let
644

    
645

    
646

    
647
	-- set state as active 
648
	idParallel4_Parallel4_2 
649
	= 1653;
650
	
651

    
652
	
653
-- transition trace :
654
	--POINT__To__B_B1_1
655
		(idB_B1_2, idParallel4_B_2, a_2, b_2) 
656
	= B_B1_en(idB_B1_1, idParallel4_B_1, a_1, b_1, false);
657
		
658

    
659
	(idParallel4_B_3, idParallel4_Parallel4_3, a_3, b_3, idB_B1_3) 
660
	= 
661

    
662
	if ( idParallel4_B_1 = 0) then
663

    
664
	 (idParallel4_B_2, idParallel4_Parallel4_2, a_2, b_2, idB_B1_2)
665

    
666
	 else(idParallel4_B_1, idParallel4_Parallel4_2, a_1, b_1, idB_B1_1);
667

    
668
	
669

    
670
	(idB_B2_2, idParallel4_B_4, a_4, b_4) 
671
	= 
672
	if ( idParallel4_B_1 = 1654) then
673
	B_B2_en(idB_B2_1, idParallel4_B_1, a_1, b_1, false)
674
	 else (idB_B2_1, idParallel4_B_1, a_1, b_1);
675

    
676
	
677

    
678
	(idB_B1_4, idParallel4_B_5, a_5, b_5) 
679
	= 
680
	if ( idParallel4_B_1 = 1657) then
681
	B_B1_en(idB_B1_1, idParallel4_B_1, a_1, b_1, false)
682
	 else (idB_B1_1, idParallel4_B_1, a_1, b_1);
683

    
684
	
685

    
686
	(idParallel4_B_6, idParallel4_Parallel4_4, a_6, b_6, idB_B1_5, idB_B2_3) 
687
	= 
688
		 if ( idParallel4_B_1 = 0) then 
689
		(idParallel4_B_3, idParallel4_Parallel4_3, a_3, b_3, idB_B1_3, idB_B2_1)
690
		 else
691
		 if ( idParallel4_B_1 = 1654) then 
692
		(idParallel4_B_4, idParallel4_Parallel4_3, a_4, b_4, idB_B1_1, idB_B2_2)
693
		 else
694
		 if ( idParallel4_B_1 = 1657) then 
695
		(idParallel4_B_5, idParallel4_Parallel4_3, a_5, b_5, idB_B1_4, idB_B2_1)
696
		 else (idParallel4_B_1, idParallel4_Parallel4_2, a_1, b_1, idB_B1_1, idB_B2_1);
697

    
698

    
699
	(idParallel4_B, idParallel4_Parallel4, a, b, idB_B1, idB_B2) 
700
	= (idParallel4_B_6, idParallel4_Parallel4_4, a_6, b_6, idB_B1_5, idB_B2_3);
701
	
702

    
703
tel
704

    
705

    
706

    
707

    
708

    
709
-- Exit action for state :Parallel4_B
710
node Parallel4_B_ex(idB_B2_1:int;
711
	idParallel4_B_1:int;
712
	idB_B1_1:int;
713
	idParallel4_Parallel4_1:int;
714
	isInner:bool)
715

    
716
returns (idB_B2:int;
717
	idParallel4_B:int;
718
	idB_B1:int;
719
	idParallel4_Parallel4:int);
720

    
721

    
722
var 	idB_B2_2, idB_B2_3:int;
723
	idParallel4_B_2, idParallel4_B_3, idParallel4_B_4, idParallel4_B_5:int;
724
	idB_B1_2, idB_B1_3:int;
725
	idParallel4_Parallel4_2:int;
726

    
727

    
728
let
729

    
730

    
731

    
732
	
733
	(idB_B2_2, idParallel4_B_2) 
734
	= 
735
	if ( idParallel4_B_1 = 1654) then
736
	B_B2_ex(idB_B2_1, idParallel4_B_1, false)
737
	 else (idB_B2_1, idParallel4_B_1);
738

    
739
	
740

    
741
	(idB_B1_2, idParallel4_B_3) 
742
	= 
743
	if ( idParallel4_B_1 = 1657) then
744
	B_B1_ex(idB_B1_1, idParallel4_B_1, false)
745
	 else (idB_B1_1, idParallel4_B_1);
746

    
747
	
748

    
749
	(idB_B2_3, idParallel4_B_4, idB_B1_3) 
750
	= 
751
		 if ( idParallel4_B_1 = 1654) then 
752
		(idB_B2_2, idParallel4_B_2, idB_B1_1)
753
		 else
754
		 if ( idParallel4_B_1 = 1657) then 
755
		(idB_B2_1, idParallel4_B_3, idB_B1_2)
756
		 else (idB_B2_1, idParallel4_B_1, idB_B1_1);
757

    
758

    
759
	-- set state as inactive 
760
	idParallel4_Parallel4_2
761
	 = if (not isInner) then 0 else idParallel4_Parallel4_1;
762

    
763
	idParallel4_B_5 
764
	= 0;
765
	
766

    
767
	(idB_B2, idParallel4_B, idB_B1, idParallel4_Parallel4) 
768
	= (idB_B2_3, idParallel4_B_5, idB_B1_3, idParallel4_Parallel4_1);
769
	
770

    
771
tel
772

    
773

    
774

    
775

    
776

    
777

    
778
-- Entry action for state :D2_D2a
779
node D2_D2a_en(idD_D2_1:int;
780
	c_1:int;
781
	dd_1:int;
782
	isInner:bool)
783

    
784
returns (idD_D2:int;
785
	c:int;
786
	dd:int);
787

    
788

    
789
var 	idD_D2_2:int;
790
	dd_2:int;
791

    
792

    
793
let
794

    
795

    
796

    
797
	-- set state as active 
798
	idD_D2_2 
799
	= 1669;
800
	
801

    
802
	dd_2 
803
	= if (not isInner) then  c_1 +7
804
	 else dd_1;
805
	
806

    
807
	(idD_D2, c, dd) 
808
	= (idD_D2_2, c_1, dd_2);
809
	
810

    
811
tel
812

    
813

    
814

    
815

    
816

    
817
-- Exit action for state :D2_D2a
818
node D2_D2a_ex(idD_D2_1:int;
819
	isInner:bool)
820

    
821
returns (idD_D2:int);
822

    
823

    
824
var 	idD_D2_2:int;
825

    
826

    
827
let
828

    
829

    
830

    
831
	-- set state as inactive 
832
	idD_D2_2
833
	 = if (not isInner) then 0 else idD_D2_1;
834

    
835

    
836
	(idD_D2) 
837
	= (idD_D2_1);
838
	
839

    
840
tel
841

    
842

    
843

    
844

    
845

    
846

    
847
-- Entry action for state :D2_D2b
848
node D2_D2b_en(idD_D2_1:int;
849
	c_1:int;
850
	dd_1:int;
851
	isInner:bool)
852

    
853
returns (idD_D2:int;
854
	c:int;
855
	dd:int);
856

    
857

    
858
var 	idD_D2_2:int;
859
	dd_2:int;
860

    
861

    
862
let
863

    
864

    
865

    
866
	-- set state as active 
867
	idD_D2_2 
868
	= 1670;
869
	
870

    
871
	dd_2 
872
	= if (not isInner) then  c_1 +8
873
	 else dd_1;
874
	
875

    
876
	(idD_D2, c, dd) 
877
	= (idD_D2_2, c_1, dd_2);
878
	
879

    
880
tel
881

    
882

    
883

    
884

    
885

    
886
-- Exit action for state :D2_D2b
887
node D2_D2b_ex(idD_D2_1:int;
888
	isInner:bool)
889

    
890
returns (idD_D2:int);
891

    
892

    
893
var 	idD_D2_2:int;
894

    
895

    
896
let
897

    
898

    
899

    
900
	-- set state as inactive 
901
	idD_D2_2
902
	 = if (not isInner) then 0 else idD_D2_1;
903

    
904

    
905
	(idD_D2) 
906
	= (idD_D2_1);
907
	
908

    
909
tel
910

    
911

    
912

    
913

    
914

    
915

    
916
-- Entry action for state :D_D2
917
node D_D2_en(idD_D2_1:int;
918
	idCD_D_1:int;
919
	c_1:int;
920
	dd_1:int;
921
	isInner:bool)
922

    
923
returns (idD_D2:int;
924
	idCD_D:int;
925
	c:int;
926
	dd:int);
927

    
928

    
929
var 	idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5, idD_D2_6:int;
930
	idCD_D_2, idCD_D_3, idCD_D_4:int;
931
	c_2, c_3, c_4, c_5, c_6:int;
932
	dd_2, dd_3, dd_4, dd_5, dd_6:int;
933

    
934

    
935
let
936

    
937

    
938

    
939
	-- set state as active 
940
	idCD_D_2 
941
	= 1668;
942
	
943

    
944
	
945
-- transition trace :
946
	--POINT__To__D2_D2a_1
947
		(idD_D2_2, c_2, dd_2) 
948
	= D2_D2a_en(idD_D2_1, c_1, dd_1, false);
949
		
950

    
951
	(idD_D2_3, idCD_D_3, c_3, dd_3) 
952
	= 
953

    
954
	if ( idD_D2_1 = 0) then
955

    
956
	 (idD_D2_2, idCD_D_2, c_2, dd_2)
957

    
958
	 else(idD_D2_1, idCD_D_2, c_1, dd_1);
959

    
960
	
961

    
962
	(idD_D2_4, c_4, dd_4) 
963
	= 
964
	if ( idD_D2_1 = 1669) then
965
	D2_D2a_en(idD_D2_1, c_1, dd_1, false)
966
	 else (idD_D2_1, c_1, dd_1);
967

    
968
	
969

    
970
	(idD_D2_5, c_5, dd_5) 
971
	= 
972
	if ( idD_D2_1 = 1670) then
973
	D2_D2b_en(idD_D2_1, c_1, dd_1, false)
974
	 else (idD_D2_1, c_1, dd_1);
975

    
976
	
977

    
978
	(idD_D2_6, idCD_D_4, c_6, dd_6) 
979
	= 
980
		 if ( idD_D2_1 = 0) then 
981
		(idD_D2_3, idCD_D_3, c_3, dd_3)
982
		 else
983
		 if ( idD_D2_1 = 1669) then 
984
		(idD_D2_4, idCD_D_3, c_4, dd_4)
985
		 else
986
		 if ( idD_D2_1 = 1670) then 
987
		(idD_D2_5, idCD_D_3, c_5, dd_5)
988
		 else (idD_D2_1, idCD_D_2, c_1, dd_1);
989

    
990

    
991
	(idD_D2, idCD_D, c, dd) 
992
	= (idD_D2_6, idCD_D_4, c_6, dd_6);
993
	
994

    
995
tel
996

    
997

    
998

    
999

    
1000

    
1001
-- Exit action for state :D_D2
1002
node D_D2_ex(idD_D2_1:int;
1003
	idCD_D_1:int;
1004
	isInner:bool)
1005

    
1006
returns (idD_D2:int;
1007
	idCD_D:int);
1008

    
1009

    
1010
var 	idD_D2_2, idD_D2_3, idD_D2_4, idD_D2_5:int;
1011
	idCD_D_2:int;
1012

    
1013

    
1014
let
1015

    
1016

    
1017

    
1018
	
1019
	(idD_D2_2) 
1020
	= 
1021
	if ( idD_D2_1 = 1669) then
1022
	D2_D2a_ex(idD_D2_1, false)
1023
	 else (idD_D2_1);
1024

    
1025
	
1026

    
1027
	(idD_D2_3) 
1028
	= 
1029
	if ( idD_D2_1 = 1670) then
1030
	D2_D2b_ex(idD_D2_1, false)
1031
	 else (idD_D2_1);
1032

    
1033
	
1034

    
1035
	(idD_D2_4) 
1036
	= 
1037
		 if ( idD_D2_1 = 1669) then 
1038
		(idD_D2_2)
1039
		 else
1040
		 if ( idD_D2_1 = 1670) then 
1041
		(idD_D2_3)
1042
		 else (idD_D2_1);
1043

    
1044

    
1045
	-- set state as inactive 
1046
	idCD_D_2
1047
	 = if (not isInner) then 0 else idCD_D_1;
1048

    
1049
	idD_D2_5 
1050
	= 0;
1051
	
1052

    
1053
	(idD_D2, idCD_D) 
1054
	= (idD_D2_5, idCD_D_1);
1055
	
1056

    
1057
tel
1058

    
1059

    
1060

    
1061

    
1062

    
1063

    
1064
-- Entry action for state :D1_D1a
1065
node D1_D1a_en(idD_D1_1:int;
1066
	c_1:int;
1067
	dd_1:int;
1068
	isInner:bool)
1069

    
1070
returns (idD_D1:int;
1071
	c:int;
1072
	dd:int);
1073

    
1074

    
1075
var 	idD_D1_2:int;
1076
	dd_2:int;
1077

    
1078

    
1079
let
1080

    
1081

    
1082

    
1083
	-- set state as active 
1084
	idD_D1_2 
1085
	= 1672;
1086
	
1087

    
1088
	dd_2 
1089
	= if (not isInner) then  c_1 +5
1090
	 else dd_1;
1091
	
1092

    
1093
	(idD_D1, c, dd) 
1094
	= (idD_D1_2, c_1, dd_2);
1095
	
1096

    
1097
tel
1098

    
1099

    
1100

    
1101

    
1102

    
1103
-- Exit action for state :D1_D1a
1104
node D1_D1a_ex(idD_D1_1:int;
1105
	isInner:bool)
1106

    
1107
returns (idD_D1:int);
1108

    
1109

    
1110
var 	idD_D1_2:int;
1111

    
1112

    
1113
let
1114

    
1115

    
1116

    
1117
	-- set state as inactive 
1118
	idD_D1_2
1119
	 = if (not isInner) then 0 else idD_D1_1;
1120

    
1121

    
1122
	(idD_D1) 
1123
	= (idD_D1_1);
1124
	
1125

    
1126
tel
1127

    
1128

    
1129

    
1130

    
1131

    
1132

    
1133
-- Entry action for state :D1_D1b
1134
node D1_D1b_en(idD_D1_1:int;
1135
	c_1:int;
1136
	dd_1:int;
1137
	isInner:bool)
1138

    
1139
returns (idD_D1:int;
1140
	c:int;
1141
	dd:int);
1142

    
1143

    
1144
var 	idD_D1_2:int;
1145
	dd_2:int;
1146

    
1147

    
1148
let
1149

    
1150

    
1151

    
1152
	-- set state as active 
1153
	idD_D1_2 
1154
	= 1673;
1155
	
1156

    
1157
	dd_2 
1158
	= if (not isInner) then  c_1 +6
1159
	 else dd_1;
1160
	
1161

    
1162
	(idD_D1, c, dd) 
1163
	= (idD_D1_2, c_1, dd_2);
1164
	
1165

    
1166
tel
1167

    
1168

    
1169

    
1170

    
1171

    
1172
-- Exit action for state :D1_D1b
1173
node D1_D1b_ex(idD_D1_1:int;
1174
	isInner:bool)
1175

    
1176
returns (idD_D1:int);
1177

    
1178

    
1179
var 	idD_D1_2:int;
1180

    
1181

    
1182
let
1183

    
1184

    
1185

    
1186
	-- set state as inactive 
1187
	idD_D1_2
1188
	 = if (not isInner) then 0 else idD_D1_1;
1189

    
1190

    
1191
	(idD_D1) 
1192
	= (idD_D1_1);
1193
	
1194

    
1195
tel
1196

    
1197

    
1198

    
1199

    
1200

    
1201

    
1202
-- Entry action for state :D_D1
1203
node D_D1_en(idD_D1_1:int;
1204
	idCD_D_1:int;
1205
	c_1:int;
1206
	dd_1:int;
1207
	isInner:bool)
1208

    
1209
returns (idD_D1:int;
1210
	idCD_D:int;
1211
	c:int;
1212
	dd:int);
1213

    
1214

    
1215
var 	idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5, idD_D1_6:int;
1216
	idCD_D_2, idCD_D_3, idCD_D_4:int;
1217
	c_2, c_3, c_4, c_5, c_6:int;
1218
	dd_2, dd_3, dd_4, dd_5, dd_6:int;
1219

    
1220

    
1221
let
1222

    
1223

    
1224

    
1225
	-- set state as active 
1226
	idCD_D_2 
1227
	= 1671;
1228
	
1229

    
1230
	
1231
-- transition trace :
1232
	--POINT__To__D1_D1a_1
1233
		(idD_D1_2, c_2, dd_2) 
1234
	= D1_D1a_en(idD_D1_1, c_1, dd_1, false);
1235
		
1236

    
1237
	(idD_D1_3, idCD_D_3, c_3, dd_3) 
1238
	= 
1239

    
1240
	if ( idD_D1_1 = 0) then
1241

    
1242
	 (idD_D1_2, idCD_D_2, c_2, dd_2)
1243

    
1244
	 else(idD_D1_1, idCD_D_2, c_1, dd_1);
1245

    
1246
	
1247

    
1248
	(idD_D1_4, c_4, dd_4) 
1249
	= 
1250
	if ( idD_D1_1 = 1672) then
1251
	D1_D1a_en(idD_D1_1, c_1, dd_1, false)
1252
	 else (idD_D1_1, c_1, dd_1);
1253

    
1254
	
1255

    
1256
	(idD_D1_5, c_5, dd_5) 
1257
	= 
1258
	if ( idD_D1_1 = 1673) then
1259
	D1_D1b_en(idD_D1_1, c_1, dd_1, false)
1260
	 else (idD_D1_1, c_1, dd_1);
1261

    
1262
	
1263

    
1264
	(idD_D1_6, idCD_D_4, c_6, dd_6) 
1265
	= 
1266
		 if ( idD_D1_1 = 0) then 
1267
		(idD_D1_3, idCD_D_3, c_3, dd_3)
1268
		 else
1269
		 if ( idD_D1_1 = 1672) then 
1270
		(idD_D1_4, idCD_D_3, c_4, dd_4)
1271
		 else
1272
		 if ( idD_D1_1 = 1673) then 
1273
		(idD_D1_5, idCD_D_3, c_5, dd_5)
1274
		 else (idD_D1_1, idCD_D_2, c_1, dd_1);
1275

    
1276

    
1277
	(idD_D1, idCD_D, c, dd) 
1278
	= (idD_D1_6, idCD_D_4, c_6, dd_6);
1279
	
1280

    
1281
tel
1282

    
1283

    
1284

    
1285

    
1286

    
1287
-- Exit action for state :D_D1
1288
node D_D1_ex(idD_D1_1:int;
1289
	idCD_D_1:int;
1290
	isInner:bool)
1291

    
1292
returns (idD_D1:int;
1293
	idCD_D:int);
1294

    
1295

    
1296
var 	idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int;
1297
	idCD_D_2:int;
1298

    
1299

    
1300
let
1301

    
1302

    
1303

    
1304
	
1305
	(idD_D1_2) 
1306
	= 
1307
	if ( idD_D1_1 = 1672) then
1308
	D1_D1a_ex(idD_D1_1, false)
1309
	 else (idD_D1_1);
1310

    
1311
	
1312

    
1313
	(idD_D1_3) 
1314
	= 
1315
	if ( idD_D1_1 = 1673) then
1316
	D1_D1b_ex(idD_D1_1, false)
1317
	 else (idD_D1_1);
1318

    
1319
	
1320

    
1321
	(idD_D1_4) 
1322
	= 
1323
		 if ( idD_D1_1 = 1672) then 
1324
		(idD_D1_2)
1325
		 else
1326
		 if ( idD_D1_1 = 1673) then 
1327
		(idD_D1_3)
1328
		 else (idD_D1_1);
1329

    
1330

    
1331
	-- set state as inactive 
1332
	idCD_D_2
1333
	 = if (not isInner) then 0 else idCD_D_1;
1334

    
1335
	idD_D1_5 
1336
	= 0;
1337
	
1338

    
1339
	(idD_D1, idCD_D) 
1340
	= (idD_D1_5, idCD_D_1);
1341
	
1342

    
1343
tel
1344

    
1345

    
1346

    
1347

    
1348

    
1349

    
1350
-- Entry action for state :CD_D
1351
node CD_D_en(idCD_D_1:int;
1352
	idParallel4_CD_1:int;
1353
	c_1:int;
1354
	dd_1:int;
1355
	idD_D1_1:int;
1356
	idD_D2_1:int;
1357
	isInner:bool)
1358

    
1359
returns (idCD_D:int;
1360
	idParallel4_CD:int;
1361
	c:int;
1362
	dd:int;
1363
	idD_D1:int;
1364
	idD_D2:int);
1365

    
1366

    
1367
var 	idCD_D_2, idCD_D_3, idCD_D_4, idCD_D_5, idCD_D_6:int;
1368
	idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4:int;
1369
	c_2, c_3, c_4, c_5, c_6:int;
1370
	dd_2, dd_3, dd_4, dd_5, dd_6:int;
1371
	idD_D1_2, idD_D1_3, idD_D1_4, idD_D1_5:int;
1372
	idD_D2_2, idD_D2_3:int;
1373

    
1374

    
1375
let
1376

    
1377

    
1378

    
1379
	-- set state as active 
1380
	idParallel4_CD_2 
1381
	= 1667;
1382
	
1383

    
1384
	
1385
-- transition trace :
1386
	--POINT__To__D_D1_1
1387
		(idD_D1_2, idCD_D_2, c_2, dd_2) 
1388
	= D_D1_en(idD_D1_1, idCD_D_1, c_1, dd_1, false);
1389
		
1390

    
1391
	(idCD_D_3, idParallel4_CD_3, c_3, dd_3, idD_D1_3) 
1392
	= 
1393

    
1394
	if ( idCD_D_1 = 0) then
1395

    
1396
	 (idCD_D_2, idParallel4_CD_2, c_2, dd_2, idD_D1_2)
1397

    
1398
	 else(idCD_D_1, idParallel4_CD_2, c_1, dd_1, idD_D1_1);
1399

    
1400
	
1401

    
1402
	(idD_D2_2, idCD_D_4, c_4, dd_4) 
1403
	= 
1404
	if ( idCD_D_1 = 1668) then
1405
	D_D2_en(idD_D2_1, idCD_D_1, c_1, dd_1, false)
1406
	 else (idD_D2_1, idCD_D_1, c_1, dd_1);
1407

    
1408
	
1409

    
1410
	(idD_D1_4, idCD_D_5, c_5, dd_5) 
1411
	= 
1412
	if ( idCD_D_1 = 1671) then
1413
	D_D1_en(idD_D1_1, idCD_D_1, c_1, dd_1, false)
1414
	 else (idD_D1_1, idCD_D_1, c_1, dd_1);
1415

    
1416
	
1417

    
1418
	(idCD_D_6, idParallel4_CD_4, c_6, dd_6, idD_D1_5, idD_D2_3) 
1419
	= 
1420
		 if ( idCD_D_1 = 0) then 
1421
		(idCD_D_3, idParallel4_CD_3, c_3, dd_3, idD_D1_3, idD_D2_1)
1422
		 else
1423
		 if ( idCD_D_1 = 1668) then 
1424
		(idCD_D_4, idParallel4_CD_3, c_4, dd_4, idD_D1_1, idD_D2_2)
1425
		 else
1426
		 if ( idCD_D_1 = 1671) then 
1427
		(idCD_D_5, idParallel4_CD_3, c_5, dd_5, idD_D1_4, idD_D2_1)
1428
		 else (idCD_D_1, idParallel4_CD_2, c_1, dd_1, idD_D1_1, idD_D2_1);
1429

    
1430

    
1431
	(idCD_D, idParallel4_CD, c, dd, idD_D1, idD_D2) 
1432
	= (idCD_D_6, idParallel4_CD_4, c_6, dd_6, idD_D1_5, idD_D2_3);
1433
	
1434

    
1435
tel
1436

    
1437

    
1438

    
1439

    
1440

    
1441
-- Exit action for state :CD_D
1442
node CD_D_ex(idD_D2_1:int;
1443
	idCD_D_1:int;
1444
	idD_D1_1:int;
1445
	idParallel4_CD_1:int;
1446
	isInner:bool)
1447

    
1448
returns (idD_D2:int;
1449
	idCD_D:int;
1450
	idD_D1:int;
1451
	idParallel4_CD:int);
1452

    
1453

    
1454
var 	idD_D2_2, idD_D2_3:int;
1455
	idCD_D_2, idCD_D_3, idCD_D_4, idCD_D_5:int;
1456
	idD_D1_2, idD_D1_3:int;
1457
	idParallel4_CD_2:int;
1458

    
1459

    
1460
let
1461

    
1462

    
1463

    
1464
	
1465
	(idD_D2_2, idCD_D_2) 
1466
	= 
1467
	if ( idCD_D_1 = 1668) then
1468
	D_D2_ex(idD_D2_1, idCD_D_1, false)
1469
	 else (idD_D2_1, idCD_D_1);
1470

    
1471
	
1472

    
1473
	(idD_D1_2, idCD_D_3) 
1474
	= 
1475
	if ( idCD_D_1 = 1671) then
1476
	D_D1_ex(idD_D1_1, idCD_D_1, false)
1477
	 else (idD_D1_1, idCD_D_1);
1478

    
1479
	
1480

    
1481
	(idD_D2_3, idCD_D_4, idD_D1_3) 
1482
	= 
1483
		 if ( idCD_D_1 = 1668) then 
1484
		(idD_D2_2, idCD_D_2, idD_D1_1)
1485
		 else
1486
		 if ( idCD_D_1 = 1671) then 
1487
		(idD_D2_1, idCD_D_3, idD_D1_2)
1488
		 else (idD_D2_1, idCD_D_1, idD_D1_1);
1489

    
1490

    
1491
	-- set state as inactive 
1492
	idParallel4_CD_2
1493
	 = if (not isInner) then 0 else idParallel4_CD_1;
1494

    
1495
	idCD_D_5 
1496
	= 0;
1497
	
1498

    
1499
	(idD_D2, idCD_D, idD_D1, idParallel4_CD) 
1500
	= (idD_D2_3, idCD_D_5, idD_D1_3, idParallel4_CD_1);
1501
	
1502

    
1503
tel
1504

    
1505

    
1506

    
1507

    
1508

    
1509

    
1510
-- Entry action for state :C2_C2a
1511
node C2_C2a_en(idC_C2_1:int;
1512
	b_1:int;
1513
	c_1:int;
1514
	isInner:bool)
1515

    
1516
returns (idC_C2:int;
1517
	b:int;
1518
	c:int);
1519

    
1520

    
1521
var 	idC_C2_2:int;
1522
	c_2:int;
1523

    
1524

    
1525
let
1526

    
1527

    
1528

    
1529
	-- set state as active 
1530
	idC_C2_2 
1531
	= 1662;
1532
	
1533

    
1534
	c_2 
1535
	= if (not isInner) then  b_1 +3
1536
	 else c_1;
1537
	
1538

    
1539
	(idC_C2, b, c) 
1540
	= (idC_C2_2, b_1, c_2);
1541
	
1542

    
1543
tel
1544

    
1545

    
1546

    
1547

    
1548

    
1549
-- Exit action for state :C2_C2a
1550
node C2_C2a_ex(idC_C2_1:int;
1551
	isInner:bool)
1552

    
1553
returns (idC_C2:int);
1554

    
1555

    
1556
var 	idC_C2_2:int;
1557

    
1558

    
1559
let
1560

    
1561

    
1562

    
1563
	-- set state as inactive 
1564
	idC_C2_2
1565
	 = if (not isInner) then 0 else idC_C2_1;
1566

    
1567

    
1568
	(idC_C2) 
1569
	= (idC_C2_1);
1570
	
1571

    
1572
tel
1573

    
1574

    
1575

    
1576

    
1577

    
1578

    
1579
-- Entry action for state :C2_C2b
1580
node C2_C2b_en(idC_C2_1:int;
1581
	b_1:int;
1582
	c_1:int;
1583
	isInner:bool)
1584

    
1585
returns (idC_C2:int;
1586
	b:int;
1587
	c:int);
1588

    
1589

    
1590
var 	idC_C2_2:int;
1591
	c_2:int;
1592

    
1593

    
1594
let
1595

    
1596

    
1597

    
1598
	-- set state as active 
1599
	idC_C2_2 
1600
	= 1663;
1601
	
1602

    
1603
	c_2 
1604
	= if (not isInner) then  b_1 +4
1605
	 else c_1;
1606
	
1607

    
1608
	(idC_C2, b, c) 
1609
	= (idC_C2_2, b_1, c_2);
1610
	
1611

    
1612
tel
1613

    
1614

    
1615

    
1616

    
1617

    
1618
-- Exit action for state :C2_C2b
1619
node C2_C2b_ex(idC_C2_1:int;
1620
	isInner:bool)
1621

    
1622
returns (idC_C2:int);
1623

    
1624

    
1625
var 	idC_C2_2:int;
1626

    
1627

    
1628
let
1629

    
1630

    
1631

    
1632
	-- set state as inactive 
1633
	idC_C2_2
1634
	 = if (not isInner) then 0 else idC_C2_1;
1635

    
1636

    
1637
	(idC_C2) 
1638
	= (idC_C2_1);
1639
	
1640

    
1641
tel
1642

    
1643

    
1644

    
1645

    
1646

    
1647

    
1648
-- Entry action for state :C_C2
1649
node C_C2_en(idC_C2_1:int;
1650
	idCD_C_1:int;
1651
	b_1:int;
1652
	c_1:int;
1653
	isInner:bool)
1654

    
1655
returns (idC_C2:int;
1656
	idCD_C:int;
1657
	b:int;
1658
	c:int);
1659

    
1660

    
1661
var 	idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5, idC_C2_6:int;
1662
	idCD_C_2, idCD_C_3, idCD_C_4:int;
1663
	b_2, b_3, b_4, b_5, b_6:int;
1664
	c_2, c_3, c_4, c_5, c_6:int;
1665

    
1666

    
1667
let
1668

    
1669

    
1670

    
1671
	-- set state as active 
1672
	idCD_C_2 
1673
	= 1661;
1674
	
1675

    
1676
	
1677
-- transition trace :
1678
	--POINT__To__C2_C2a_1
1679
		(idC_C2_2, b_2, c_2) 
1680
	= C2_C2a_en(idC_C2_1, b_1, c_1, false);
1681
		
1682

    
1683
	(idC_C2_3, idCD_C_3, b_3, c_3) 
1684
	= 
1685

    
1686
	if ( idC_C2_1 = 0) then
1687

    
1688
	 (idC_C2_2, idCD_C_2, b_2, c_2)
1689

    
1690
	 else(idC_C2_1, idCD_C_2, b_1, c_1);
1691

    
1692
	
1693

    
1694
	(idC_C2_4, b_4, c_4) 
1695
	= 
1696
	if ( idC_C2_1 = 1662) then
1697
	C2_C2a_en(idC_C2_1, b_1, c_1, false)
1698
	 else (idC_C2_1, b_1, c_1);
1699

    
1700
	
1701

    
1702
	(idC_C2_5, b_5, c_5) 
1703
	= 
1704
	if ( idC_C2_1 = 1663) then
1705
	C2_C2b_en(idC_C2_1, b_1, c_1, false)
1706
	 else (idC_C2_1, b_1, c_1);
1707

    
1708
	
1709

    
1710
	(idC_C2_6, idCD_C_4, b_6, c_6) 
1711
	= 
1712
		 if ( idC_C2_1 = 0) then 
1713
		(idC_C2_3, idCD_C_3, b_3, c_3)
1714
		 else
1715
		 if ( idC_C2_1 = 1662) then 
1716
		(idC_C2_4, idCD_C_3, b_4, c_4)
1717
		 else
1718
		 if ( idC_C2_1 = 1663) then 
1719
		(idC_C2_5, idCD_C_3, b_5, c_5)
1720
		 else (idC_C2_1, idCD_C_2, b_1, c_1);
1721

    
1722

    
1723
	(idC_C2, idCD_C, b, c) 
1724
	= (idC_C2_6, idCD_C_4, b_6, c_6);
1725
	
1726

    
1727
tel
1728

    
1729

    
1730

    
1731

    
1732

    
1733
-- Exit action for state :C_C2
1734
node C_C2_ex(idC_C2_1:int;
1735
	idCD_C_1:int;
1736
	isInner:bool)
1737

    
1738
returns (idC_C2:int;
1739
	idCD_C:int);
1740

    
1741

    
1742
var 	idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5:int;
1743
	idCD_C_2:int;
1744

    
1745

    
1746
let
1747

    
1748

    
1749

    
1750
	
1751
	(idC_C2_2) 
1752
	= 
1753
	if ( idC_C2_1 = 1662) then
1754
	C2_C2a_ex(idC_C2_1, false)
1755
	 else (idC_C2_1);
1756

    
1757
	
1758

    
1759
	(idC_C2_3) 
1760
	= 
1761
	if ( idC_C2_1 = 1663) then
1762
	C2_C2b_ex(idC_C2_1, false)
1763
	 else (idC_C2_1);
1764

    
1765
	
1766

    
1767
	(idC_C2_4) 
1768
	= 
1769
		 if ( idC_C2_1 = 1662) then 
1770
		(idC_C2_2)
1771
		 else
1772
		 if ( idC_C2_1 = 1663) then 
1773
		(idC_C2_3)
1774
		 else (idC_C2_1);
1775

    
1776

    
1777
	-- set state as inactive 
1778
	idCD_C_2
1779
	 = if (not isInner) then 0 else idCD_C_1;
1780

    
1781
	idC_C2_5 
1782
	= 0;
1783
	
1784

    
1785
	(idC_C2, idCD_C) 
1786
	= (idC_C2_5, idCD_C_1);
1787
	
1788

    
1789
tel
1790

    
1791

    
1792

    
1793

    
1794

    
1795

    
1796
-- Entry action for state :C1_C1a
1797
node C1_C1a_en(idC_C1_1:int;
1798
	b_1:int;
1799
	c_1:int;
1800
	isInner:bool)
1801

    
1802
returns (idC_C1:int;
1803
	b:int;
1804
	c:int);
1805

    
1806

    
1807
var 	idC_C1_2:int;
1808
	c_2:int;
1809

    
1810

    
1811
let
1812

    
1813

    
1814

    
1815
	-- set state as active 
1816
	idC_C1_2 
1817
	= 1665;
1818
	
1819

    
1820
	c_2 
1821
	= if (not isInner) then  b_1 +1
1822
	 else c_1;
1823
	
1824

    
1825
	(idC_C1, b, c) 
1826
	= (idC_C1_2, b_1, c_2);
1827
	
1828

    
1829
tel
1830

    
1831

    
1832

    
1833

    
1834

    
1835
-- Exit action for state :C1_C1a
1836
node C1_C1a_ex(idC_C1_1:int;
1837
	isInner:bool)
1838

    
1839
returns (idC_C1:int);
1840

    
1841

    
1842
var 	idC_C1_2:int;
1843

    
1844

    
1845
let
1846

    
1847

    
1848

    
1849
	-- set state as inactive 
1850
	idC_C1_2
1851
	 = if (not isInner) then 0 else idC_C1_1;
1852

    
1853

    
1854
	(idC_C1) 
1855
	= (idC_C1_1);
1856
	
1857

    
1858
tel
1859

    
1860

    
1861

    
1862

    
1863

    
1864

    
1865
-- Entry action for state :C1_C1b
1866
node C1_C1b_en(idC_C1_1:int;
1867
	b_1:int;
1868
	c_1:int;
1869
	isInner:bool)
1870

    
1871
returns (idC_C1:int;
1872
	b:int;
1873
	c:int);
1874

    
1875

    
1876
var 	idC_C1_2:int;
1877
	c_2:int;
1878

    
1879

    
1880
let
1881

    
1882

    
1883

    
1884
	-- set state as active 
1885
	idC_C1_2 
1886
	= 1666;
1887
	
1888

    
1889
	c_2 
1890
	= if (not isInner) then  b_1 +2
1891
	 else c_1;
1892
	
1893

    
1894
	(idC_C1, b, c) 
1895
	= (idC_C1_2, b_1, c_2);
1896
	
1897

    
1898
tel
1899

    
1900

    
1901

    
1902

    
1903

    
1904
-- Exit action for state :C1_C1b
1905
node C1_C1b_ex(idC_C1_1:int;
1906
	isInner:bool)
1907

    
1908
returns (idC_C1:int);
1909

    
1910

    
1911
var 	idC_C1_2:int;
1912

    
1913

    
1914
let
1915

    
1916

    
1917

    
1918
	-- set state as inactive 
1919
	idC_C1_2
1920
	 = if (not isInner) then 0 else idC_C1_1;
1921

    
1922

    
1923
	(idC_C1) 
1924
	= (idC_C1_1);
1925
	
1926

    
1927
tel
1928

    
1929

    
1930

    
1931

    
1932

    
1933

    
1934
-- Entry action for state :C_C1
1935
node C_C1_en(idC_C1_1:int;
1936
	idCD_C_1:int;
1937
	b_1:int;
1938
	c_1:int;
1939
	isInner:bool)
1940

    
1941
returns (idC_C1:int;
1942
	idCD_C:int;
1943
	b:int;
1944
	c:int);
1945

    
1946

    
1947
var 	idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5, idC_C1_6:int;
1948
	idCD_C_2, idCD_C_3, idCD_C_4:int;
1949
	b_2, b_3, b_4, b_5, b_6:int;
1950
	c_2, c_3, c_4, c_5, c_6:int;
1951

    
1952

    
1953
let
1954

    
1955

    
1956

    
1957
	-- set state as active 
1958
	idCD_C_2 
1959
	= 1664;
1960
	
1961

    
1962
	
1963
-- transition trace :
1964
	--POINT__To__C1_C1a_1
1965
		(idC_C1_2, b_2, c_2) 
1966
	= C1_C1a_en(idC_C1_1, b_1, c_1, false);
1967
		
1968

    
1969
	(idC_C1_3, idCD_C_3, b_3, c_3) 
1970
	= 
1971

    
1972
	if ( idC_C1_1 = 0) then
1973

    
1974
	 (idC_C1_2, idCD_C_2, b_2, c_2)
1975

    
1976
	 else(idC_C1_1, idCD_C_2, b_1, c_1);
1977

    
1978
	
1979

    
1980
	(idC_C1_4, b_4, c_4) 
1981
	= 
1982
	if ( idC_C1_1 = 1665) then
1983
	C1_C1a_en(idC_C1_1, b_1, c_1, false)
1984
	 else (idC_C1_1, b_1, c_1);
1985

    
1986
	
1987

    
1988
	(idC_C1_5, b_5, c_5) 
1989
	= 
1990
	if ( idC_C1_1 = 1666) then
1991
	C1_C1b_en(idC_C1_1, b_1, c_1, false)
1992
	 else (idC_C1_1, b_1, c_1);
1993

    
1994
	
1995

    
1996
	(idC_C1_6, idCD_C_4, b_6, c_6) 
1997
	= 
1998
		 if ( idC_C1_1 = 0) then 
1999
		(idC_C1_3, idCD_C_3, b_3, c_3)
2000
		 else
2001
		 if ( idC_C1_1 = 1665) then 
2002
		(idC_C1_4, idCD_C_3, b_4, c_4)
2003
		 else
2004
		 if ( idC_C1_1 = 1666) then 
2005
		(idC_C1_5, idCD_C_3, b_5, c_5)
2006
		 else (idC_C1_1, idCD_C_2, b_1, c_1);
2007

    
2008

    
2009
	(idC_C1, idCD_C, b, c) 
2010
	= (idC_C1_6, idCD_C_4, b_6, c_6);
2011
	
2012

    
2013
tel
2014

    
2015

    
2016

    
2017

    
2018

    
2019
-- Exit action for state :C_C1
2020
node C_C1_ex(idC_C1_1:int;
2021
	idCD_C_1:int;
2022
	isInner:bool)
2023

    
2024
returns (idC_C1:int;
2025
	idCD_C:int);
2026

    
2027

    
2028
var 	idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int;
2029
	idCD_C_2:int;
2030

    
2031

    
2032
let
2033

    
2034

    
2035

    
2036
	
2037
	(idC_C1_2) 
2038
	= 
2039
	if ( idC_C1_1 = 1665) then
2040
	C1_C1a_ex(idC_C1_1, false)
2041
	 else (idC_C1_1);
2042

    
2043
	
2044

    
2045
	(idC_C1_3) 
2046
	= 
2047
	if ( idC_C1_1 = 1666) then
2048
	C1_C1b_ex(idC_C1_1, false)
2049
	 else (idC_C1_1);
2050

    
2051
	
2052

    
2053
	(idC_C1_4) 
2054
	= 
2055
		 if ( idC_C1_1 = 1665) then 
2056
		(idC_C1_2)
2057
		 else
2058
		 if ( idC_C1_1 = 1666) then 
2059
		(idC_C1_3)
2060
		 else (idC_C1_1);
2061

    
2062

    
2063
	-- set state as inactive 
2064
	idCD_C_2
2065
	 = if (not isInner) then 0 else idCD_C_1;
2066

    
2067
	idC_C1_5 
2068
	= 0;
2069
	
2070

    
2071
	(idC_C1, idCD_C) 
2072
	= (idC_C1_5, idCD_C_1);
2073
	
2074

    
2075
tel
2076

    
2077

    
2078

    
2079

    
2080

    
2081

    
2082
-- Entry action for state :CD_C
2083
node CD_C_en(idCD_C_1:int;
2084
	idParallel4_CD_1:int;
2085
	b_1:int;
2086
	c_1:int;
2087
	idC_C1_1:int;
2088
	idC_C2_1:int;
2089
	isInner:bool)
2090

    
2091
returns (idCD_C:int;
2092
	idParallel4_CD:int;
2093
	b:int;
2094
	c:int;
2095
	idC_C1:int;
2096
	idC_C2:int);
2097

    
2098

    
2099
var 	idCD_C_2, idCD_C_3, idCD_C_4, idCD_C_5, idCD_C_6:int;
2100
	idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4:int;
2101
	b_2, b_3, b_4, b_5, b_6:int;
2102
	c_2, c_3, c_4, c_5, c_6:int;
2103
	idC_C1_2, idC_C1_3, idC_C1_4, idC_C1_5:int;
2104
	idC_C2_2, idC_C2_3:int;
2105

    
2106

    
2107
let
2108

    
2109

    
2110

    
2111
	-- set state as active 
2112
	idParallel4_CD_2 
2113
	= 1660;
2114
	
2115

    
2116
	
2117
-- transition trace :
2118
	--POINT__To__C_C1_1
2119
		(idC_C1_2, idCD_C_2, b_2, c_2) 
2120
	= C_C1_en(idC_C1_1, idCD_C_1, b_1, c_1, false);
2121
		
2122

    
2123
	(idCD_C_3, idParallel4_CD_3, b_3, c_3, idC_C1_3) 
2124
	= 
2125

    
2126
	if ( idCD_C_1 = 0) then
2127

    
2128
	 (idCD_C_2, idParallel4_CD_2, b_2, c_2, idC_C1_2)
2129

    
2130
	 else(idCD_C_1, idParallel4_CD_2, b_1, c_1, idC_C1_1);
2131

    
2132
	
2133

    
2134
	(idC_C2_2, idCD_C_4, b_4, c_4) 
2135
	= 
2136
	if ( idCD_C_1 = 1661) then
2137
	C_C2_en(idC_C2_1, idCD_C_1, b_1, c_1, false)
2138
	 else (idC_C2_1, idCD_C_1, b_1, c_1);
2139

    
2140
	
2141

    
2142
	(idC_C1_4, idCD_C_5, b_5, c_5) 
2143
	= 
2144
	if ( idCD_C_1 = 1664) then
2145
	C_C1_en(idC_C1_1, idCD_C_1, b_1, c_1, false)
2146
	 else (idC_C1_1, idCD_C_1, b_1, c_1);
2147

    
2148
	
2149

    
2150
	(idCD_C_6, idParallel4_CD_4, b_6, c_6, idC_C1_5, idC_C2_3) 
2151
	= 
2152
		 if ( idCD_C_1 = 0) then 
2153
		(idCD_C_3, idParallel4_CD_3, b_3, c_3, idC_C1_3, idC_C2_1)
2154
		 else
2155
		 if ( idCD_C_1 = 1661) then 
2156
		(idCD_C_4, idParallel4_CD_3, b_4, c_4, idC_C1_1, idC_C2_2)
2157
		 else
2158
		 if ( idCD_C_1 = 1664) then 
2159
		(idCD_C_5, idParallel4_CD_3, b_5, c_5, idC_C1_4, idC_C2_1)
2160
		 else (idCD_C_1, idParallel4_CD_2, b_1, c_1, idC_C1_1, idC_C2_1);
2161

    
2162

    
2163
	(idCD_C, idParallel4_CD, b, c, idC_C1, idC_C2) 
2164
	= (idCD_C_6, idParallel4_CD_4, b_6, c_6, idC_C1_5, idC_C2_3);
2165
	
2166

    
2167
tel
2168

    
2169

    
2170

    
2171

    
2172

    
2173
-- Exit action for state :CD_C
2174
node CD_C_ex(idC_C2_1:int;
2175
	idCD_C_1:int;
2176
	idC_C1_1:int;
2177
	idParallel4_CD_1:int;
2178
	isInner:bool)
2179

    
2180
returns (idC_C2:int;
2181
	idCD_C:int;
2182
	idC_C1:int;
2183
	idParallel4_CD:int);
2184

    
2185

    
2186
var 	idC_C2_2, idC_C2_3:int;
2187
	idCD_C_2, idCD_C_3, idCD_C_4, idCD_C_5:int;
2188
	idC_C1_2, idC_C1_3:int;
2189
	idParallel4_CD_2:int;
2190

    
2191

    
2192
let
2193

    
2194

    
2195

    
2196
	
2197
	(idC_C2_2, idCD_C_2) 
2198
	= 
2199
	if ( idCD_C_1 = 1661) then
2200
	C_C2_ex(idC_C2_1, idCD_C_1, false)
2201
	 else (idC_C2_1, idCD_C_1);
2202

    
2203
	
2204

    
2205
	(idC_C1_2, idCD_C_3) 
2206
	= 
2207
	if ( idCD_C_1 = 1664) then
2208
	C_C1_ex(idC_C1_1, idCD_C_1, false)
2209
	 else (idC_C1_1, idCD_C_1);
2210

    
2211
	
2212

    
2213
	(idC_C2_3, idCD_C_4, idC_C1_3) 
2214
	= 
2215
		 if ( idCD_C_1 = 1661) then 
2216
		(idC_C2_2, idCD_C_2, idC_C1_1)
2217
		 else
2218
		 if ( idCD_C_1 = 1664) then 
2219
		(idC_C2_1, idCD_C_3, idC_C1_2)
2220
		 else (idC_C2_1, idCD_C_1, idC_C1_1);
2221

    
2222

    
2223
	-- set state as inactive 
2224
	idParallel4_CD_2
2225
	 = if (not isInner) then 0 else idParallel4_CD_1;
2226

    
2227
	idCD_C_5 
2228
	= 0;
2229
	
2230

    
2231
	(idC_C2, idCD_C, idC_C1, idParallel4_CD) 
2232
	= (idC_C2_3, idCD_C_5, idC_C1_3, idParallel4_CD_1);
2233
	
2234

    
2235
tel
2236

    
2237

    
2238

    
2239

    
2240

    
2241

    
2242
-- Entry action for state :Parallel4_CD
2243
node Parallel4_CD_en(idParallel4_CD_1:int;
2244
	idParallel4_Parallel4_1:int;
2245
	b_1:int;
2246
	c_1:int;
2247
	idCD_C_1:int;
2248
	idC_C1_1:int;
2249
	idC_C2_1:int;
2250
	dd_1:int;
2251
	idCD_D_1:int;
2252
	idD_D1_1:int;
2253
	idD_D2_1:int;
2254
	isInner:bool)
2255

    
2256
returns (idParallel4_CD:int;
2257
	idParallel4_Parallel4:int;
2258
	b:int;
2259
	c:int;
2260
	idCD_C:int;
2261
	idC_C1:int;
2262
	idC_C2:int;
2263
	dd:int;
2264
	idCD_D:int;
2265
	idD_D1:int;
2266
	idD_D2:int);
2267

    
2268

    
2269
var 	idParallel4_CD_2, idParallel4_CD_3:int;
2270
	idParallel4_Parallel4_2:int;
2271
	b_2:int;
2272
	c_2, c_3:int;
2273
	idCD_C_2:int;
2274
	idC_C1_2:int;
2275
	idC_C2_2:int;
2276
	dd_2:int;
2277
	idCD_D_2:int;
2278
	idD_D1_2:int;
2279
	idD_D2_2:int;
2280

    
2281

    
2282
let
2283

    
2284

    
2285

    
2286
	-- set state as active 
2287
	idParallel4_Parallel4_2 
2288
	= 1674;
2289
	
2290

    
2291
	
2292
	(idCD_C_2, idParallel4_CD_2, b_2, c_2, idC_C1_2, idC_C2_2) 
2293
	= CD_C_en(idCD_C_1, idParallel4_CD_1, b_1, c_1, idC_C1_1, idC_C2_1, false);
2294

    
2295
	(idCD_D_2, idParallel4_CD_3, c_3, dd_2, idD_D1_2, idD_D2_2) 
2296
	= CD_D_en(idCD_D_1, idParallel4_CD_2, c_2, dd_1, idD_D1_1, idD_D2_1, false);
2297

    
2298

    
2299
	(idParallel4_CD, idParallel4_Parallel4, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
2300
	= (idParallel4_CD_3, idParallel4_Parallel4_2, b_2, c_3, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2);
2301
	
2302

    
2303
tel
2304

    
2305

    
2306

    
2307

    
2308

    
2309
-- Exit action for state :Parallel4_CD
2310
node Parallel4_CD_ex(idD_D2_1:int;
2311
	idCD_D_1:int;
2312
	idD_D1_1:int;
2313
	idParallel4_CD_1:int;
2314
	idCD_C_1:int;
2315
	idC_C1_1:int;
2316
	idC_C2_1:int;
2317
	idParallel4_Parallel4_1:int;
2318
	isInner:bool)
2319

    
2320
returns (idD_D2:int;
2321
	idCD_D:int;
2322
	idD_D1:int;
2323
	idParallel4_CD:int;
2324
	idCD_C:int;
2325
	idC_C1:int;
2326
	idC_C2:int;
2327
	idParallel4_Parallel4:int);
2328

    
2329

    
2330
var 	idD_D2_2:int;
2331
	idCD_D_2:int;
2332
	idD_D1_2:int;
2333
	idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4:int;
2334
	idCD_C_2:int;
2335
	idC_C1_2:int;
2336
	idC_C2_2:int;
2337
	idParallel4_Parallel4_2:int;
2338

    
2339

    
2340
let
2341

    
2342

    
2343

    
2344
	
2345
	(idD_D2_2, idCD_D_2, idD_D1_2, idParallel4_CD_2) 
2346
	= CD_D_ex(idD_D2_1, idCD_D_1, idD_D1_1, idParallel4_CD_1, false);
2347

    
2348
	(idC_C2_2, idCD_C_2, idC_C1_2, idParallel4_CD_3) 
2349
	= CD_C_ex(idC_C2_1, idCD_C_1, idC_C1_1, idParallel4_CD_2, false);
2350

    
2351

    
2352
	-- set state as inactive 
2353
	idParallel4_Parallel4_2
2354
	 = if (not isInner) then 0 else idParallel4_Parallel4_1;
2355

    
2356
	idParallel4_CD_4 
2357
	= 0;
2358
	
2359

    
2360
	(idD_D2, idCD_D, idD_D1, idParallel4_CD, idCD_C, idC_C1, idC_C2, idParallel4_Parallel4) 
2361
	= (idD_D2_2, idCD_D_2, idD_D1_2, idParallel4_CD_4, idCD_C_2, idC_C1_2, idC_C2_2, idParallel4_Parallel4_1);
2362
	
2363

    
2364
tel
2365

    
2366

    
2367

    
2368

    
2369

    
2370

    
2371
-- Entry action for state :A2_A2a
2372
node A2_A2a_en(idA_A2_1:int;
2373
	x:int;
2374
	a_1:int;
2375
	isInner:bool)
2376

    
2377
returns (idA_A2:int;
2378
	a:int);
2379

    
2380

    
2381
var 	idA_A2_2:int;
2382
	a_2:int;
2383

    
2384

    
2385
let
2386

    
2387

    
2388

    
2389
	-- set state as active 
2390
	idA_A2_2 
2391
	= 1651;
2392
	
2393

    
2394
	a_2 
2395
	= if (not isInner) then x+3
2396
	 else a_1;
2397
	
2398

    
2399
	(idA_A2, a) 
2400
	= (idA_A2_2, a_2);
2401
	
2402

    
2403
tel
2404

    
2405

    
2406

    
2407

    
2408

    
2409
-- Exit action for state :A2_A2a
2410
node A2_A2a_ex(idA_A2_1:int;
2411
	isInner:bool)
2412

    
2413
returns (idA_A2:int);
2414

    
2415

    
2416
var 	idA_A2_2:int;
2417

    
2418

    
2419
let
2420

    
2421

    
2422

    
2423
	-- set state as inactive 
2424
	idA_A2_2
2425
	 = if (not isInner) then 0 else idA_A2_1;
2426

    
2427

    
2428
	(idA_A2) 
2429
	= (idA_A2_1);
2430
	
2431

    
2432
tel
2433

    
2434

    
2435

    
2436

    
2437

    
2438

    
2439
-- Entry action for state :A2_A2b
2440
node A2_A2b_en(idA_A2_1:int;
2441
	x:int;
2442
	a_1:int;
2443
	isInner:bool)
2444

    
2445
returns (idA_A2:int;
2446
	a:int);
2447

    
2448

    
2449
var 	idA_A2_2:int;
2450
	a_2:int;
2451

    
2452

    
2453
let
2454

    
2455

    
2456

    
2457
	-- set state as active 
2458
	idA_A2_2 
2459
	= 1652;
2460
	
2461

    
2462
	a_2 
2463
	= if (not isInner) then x+4
2464
	 else a_1;
2465
	
2466

    
2467
	(idA_A2, a) 
2468
	= (idA_A2_2, a_2);
2469
	
2470

    
2471
tel
2472

    
2473

    
2474

    
2475

    
2476

    
2477
-- Exit action for state :A2_A2b
2478
node A2_A2b_ex(idA_A2_1:int;
2479
	isInner:bool)
2480

    
2481
returns (idA_A2:int);
2482

    
2483

    
2484
var 	idA_A2_2:int;
2485

    
2486

    
2487
let
2488

    
2489

    
2490

    
2491
	-- set state as inactive 
2492
	idA_A2_2
2493
	 = if (not isInner) then 0 else idA_A2_1;
2494

    
2495

    
2496
	(idA_A2) 
2497
	= (idA_A2_1);
2498
	
2499

    
2500
tel
2501

    
2502

    
2503

    
2504

    
2505

    
2506

    
2507
-- Entry action for state :A_A2
2508
node A_A2_en(idA_A2_1:int;
2509
	idParallel4_A_1:int;
2510
	a_1:int;
2511
	x:int;
2512
	isInner:bool)
2513

    
2514
returns (idA_A2:int;
2515
	idParallel4_A:int;
2516
	a:int);
2517

    
2518

    
2519
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int;
2520
	idParallel4_A_2, idParallel4_A_3, idParallel4_A_4:int;
2521
	a_2, a_3, a_4, a_5, a_6:int;
2522

    
2523

    
2524
let
2525

    
2526

    
2527

    
2528
	-- set state as active 
2529
	idParallel4_A_2 
2530
	= 1650;
2531
	
2532

    
2533
	
2534
-- transition trace :
2535
	--POINT__To__A2_A2a_1
2536
		(idA_A2_2, a_2) 
2537
	= A2_A2a_en(idA_A2_1, x, a_1, false);
2538
		
2539

    
2540
	(idA_A2_3, idParallel4_A_3, a_3) 
2541
	= 
2542

    
2543
	if ( idA_A2_1 = 0) then
2544

    
2545
	 (idA_A2_2, idParallel4_A_2, a_2)
2546

    
2547
	 else(idA_A2_1, idParallel4_A_2, a_1);
2548

    
2549
	
2550

    
2551
	(idA_A2_4, a_4) 
2552
	= 
2553
	if ( idA_A2_1 = 1651) then
2554
	A2_A2a_en(idA_A2_1, x, a_1, false)
2555
	 else (idA_A2_1, a_1);
2556

    
2557
	
2558

    
2559
	(idA_A2_5, a_5) 
2560
	= 
2561
	if ( idA_A2_1 = 1652) then
2562
	A2_A2b_en(idA_A2_1, x, a_1, false)
2563
	 else (idA_A2_1, a_1);
2564

    
2565
	
2566

    
2567
	(idA_A2_6, idParallel4_A_4, a_6) 
2568
	= 
2569
		 if ( idA_A2_1 = 0) then 
2570
		(idA_A2_3, idParallel4_A_3, a_3)
2571
		 else
2572
		 if ( idA_A2_1 = 1651) then 
2573
		(idA_A2_4, idParallel4_A_3, a_4)
2574
		 else
2575
		 if ( idA_A2_1 = 1652) then 
2576
		(idA_A2_5, idParallel4_A_3, a_5)
2577
		 else (idA_A2_1, idParallel4_A_2, a_1);
2578

    
2579

    
2580
	(idA_A2, idParallel4_A, a) 
2581
	= (idA_A2_6, idParallel4_A_4, a_6);
2582
	
2583

    
2584
tel
2585

    
2586

    
2587

    
2588

    
2589

    
2590
-- Exit action for state :A_A2
2591
node A_A2_ex(idA_A2_1:int;
2592
	idParallel4_A_1:int;
2593
	isInner:bool)
2594

    
2595
returns (idA_A2:int;
2596
	idParallel4_A:int);
2597

    
2598

    
2599
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int;
2600
	idParallel4_A_2:int;
2601

    
2602

    
2603
let
2604

    
2605

    
2606

    
2607
	
2608
	(idA_A2_2) 
2609
	= 
2610
	if ( idA_A2_1 = 1651) then
2611
	A2_A2a_ex(idA_A2_1, false)
2612
	 else (idA_A2_1);
2613

    
2614
	
2615

    
2616
	(idA_A2_3) 
2617
	= 
2618
	if ( idA_A2_1 = 1652) then
2619
	A2_A2b_ex(idA_A2_1, false)
2620
	 else (idA_A2_1);
2621

    
2622
	
2623

    
2624
	(idA_A2_4) 
2625
	= 
2626
		 if ( idA_A2_1 = 1651) then 
2627
		(idA_A2_2)
2628
		 else
2629
		 if ( idA_A2_1 = 1652) then 
2630
		(idA_A2_3)
2631
		 else (idA_A2_1);
2632

    
2633

    
2634
	-- set state as inactive 
2635
	idParallel4_A_2
2636
	 = if (not isInner) then 0 else idParallel4_A_1;
2637

    
2638
	idA_A2_5 
2639
	= 0;
2640
	
2641

    
2642
	(idA_A2, idParallel4_A) 
2643
	= (idA_A2_5, idParallel4_A_1);
2644
	
2645

    
2646
tel
2647

    
2648

    
2649

    
2650

    
2651

    
2652

    
2653
-- Entry action for state :A1_A1a
2654
node A1_A1a_en(idA_A1_1:int;
2655
	x:int;
2656
	a_1:int;
2657
	isInner:bool)
2658

    
2659
returns (idA_A1:int;
2660
	a:int);
2661

    
2662

    
2663
var 	idA_A1_2:int;
2664
	a_2:int;
2665

    
2666

    
2667
let
2668

    
2669

    
2670

    
2671
	-- set state as active 
2672
	idA_A1_2 
2673
	= 1648;
2674
	
2675

    
2676
	a_2 
2677
	= if (not isInner) then x+1
2678
	 else a_1;
2679
	
2680

    
2681
	(idA_A1, a) 
2682
	= (idA_A1_2, a_2);
2683
	
2684

    
2685
tel
2686

    
2687

    
2688

    
2689

    
2690

    
2691
-- Exit action for state :A1_A1a
2692
node A1_A1a_ex(idA_A1_1:int;
2693
	isInner:bool)
2694

    
2695
returns (idA_A1:int);
2696

    
2697

    
2698
var 	idA_A1_2:int;
2699

    
2700

    
2701
let
2702

    
2703

    
2704

    
2705
	-- set state as inactive 
2706
	idA_A1_2
2707
	 = if (not isInner) then 0 else idA_A1_1;
2708

    
2709

    
2710
	(idA_A1) 
2711
	= (idA_A1_1);
2712
	
2713

    
2714
tel
2715

    
2716

    
2717

    
2718

    
2719

    
2720

    
2721
-- Entry action for state :A1_A1b
2722
node A1_A1b_en(idA_A1_1:int;
2723
	x:int;
2724
	a_1:int;
2725
	isInner:bool)
2726

    
2727
returns (idA_A1:int;
2728
	a:int);
2729

    
2730

    
2731
var 	idA_A1_2:int;
2732
	a_2:int;
2733

    
2734

    
2735
let
2736

    
2737

    
2738

    
2739
	-- set state as active 
2740
	idA_A1_2 
2741
	= 1649;
2742
	
2743

    
2744
	a_2 
2745
	= if (not isInner) then x+2
2746
	 else a_1;
2747
	
2748

    
2749
	(idA_A1, a) 
2750
	= (idA_A1_2, a_2);
2751
	
2752

    
2753
tel
2754

    
2755

    
2756

    
2757

    
2758

    
2759
-- Exit action for state :A1_A1b
2760
node A1_A1b_ex(idA_A1_1:int;
2761
	isInner:bool)
2762

    
2763
returns (idA_A1:int);
2764

    
2765

    
2766
var 	idA_A1_2:int;
2767

    
2768

    
2769
let
2770

    
2771

    
2772

    
2773
	-- set state as inactive 
2774
	idA_A1_2
2775
	 = if (not isInner) then 0 else idA_A1_1;
2776

    
2777

    
2778
	(idA_A1) 
2779
	= (idA_A1_1);
2780
	
2781

    
2782
tel
2783

    
2784

    
2785

    
2786

    
2787

    
2788

    
2789
-- Entry action for state :A_A1
2790
node A_A1_en(idA_A1_1:int;
2791
	idParallel4_A_1:int;
2792
	a_1:int;
2793
	x:int;
2794
	isInner:bool)
2795

    
2796
returns (idA_A1:int;
2797
	idParallel4_A:int;
2798
	a:int);
2799

    
2800

    
2801
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int;
2802
	idParallel4_A_2, idParallel4_A_3, idParallel4_A_4:int;
2803
	a_2, a_3, a_4, a_5, a_6:int;
2804

    
2805

    
2806
let
2807

    
2808

    
2809

    
2810
	-- set state as active 
2811
	idParallel4_A_2 
2812
	= 1647;
2813
	
2814

    
2815
	
2816
-- transition trace :
2817
	--POINT__To__A1_A1a_1
2818
		(idA_A1_2, a_2) 
2819
	= A1_A1a_en(idA_A1_1, x, a_1, false);
2820
		
2821

    
2822
	(idA_A1_3, idParallel4_A_3, a_3) 
2823
	= 
2824

    
2825
	if ( idA_A1_1 = 0) then
2826

    
2827
	 (idA_A1_2, idParallel4_A_2, a_2)
2828

    
2829
	 else(idA_A1_1, idParallel4_A_2, a_1);
2830

    
2831
	
2832

    
2833
	(idA_A1_4, a_4) 
2834
	= 
2835
	if ( idA_A1_1 = 1648) then
2836
	A1_A1a_en(idA_A1_1, x, a_1, false)
2837
	 else (idA_A1_1, a_1);
2838

    
2839
	
2840

    
2841
	(idA_A1_5, a_5) 
2842
	= 
2843
	if ( idA_A1_1 = 1649) then
2844
	A1_A1b_en(idA_A1_1, x, a_1, false)
2845
	 else (idA_A1_1, a_1);
2846

    
2847
	
2848

    
2849
	(idA_A1_6, idParallel4_A_4, a_6) 
2850
	= 
2851
		 if ( idA_A1_1 = 0) then 
2852
		(idA_A1_3, idParallel4_A_3, a_3)
2853
		 else
2854
		 if ( idA_A1_1 = 1648) then 
2855
		(idA_A1_4, idParallel4_A_3, a_4)
2856
		 else
2857
		 if ( idA_A1_1 = 1649) then 
2858
		(idA_A1_5, idParallel4_A_3, a_5)
2859
		 else (idA_A1_1, idParallel4_A_2, a_1);
2860

    
2861

    
2862
	(idA_A1, idParallel4_A, a) 
2863
	= (idA_A1_6, idParallel4_A_4, a_6);
2864
	
2865

    
2866
tel
2867

    
2868

    
2869

    
2870

    
2871

    
2872
-- Exit action for state :A_A1
2873
node A_A1_ex(idA_A1_1:int;
2874
	idParallel4_A_1:int;
2875
	isInner:bool)
2876

    
2877
returns (idA_A1:int;
2878
	idParallel4_A:int);
2879

    
2880

    
2881
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2882
	idParallel4_A_2:int;
2883

    
2884

    
2885
let
2886

    
2887

    
2888

    
2889
	
2890
	(idA_A1_2) 
2891
	= 
2892
	if ( idA_A1_1 = 1648) then
2893
	A1_A1a_ex(idA_A1_1, false)
2894
	 else (idA_A1_1);
2895

    
2896
	
2897

    
2898
	(idA_A1_3) 
2899
	= 
2900
	if ( idA_A1_1 = 1649) then
2901
	A1_A1b_ex(idA_A1_1, false)
2902
	 else (idA_A1_1);
2903

    
2904
	
2905

    
2906
	(idA_A1_4) 
2907
	= 
2908
		 if ( idA_A1_1 = 1648) then 
2909
		(idA_A1_2)
2910
		 else
2911
		 if ( idA_A1_1 = 1649) then 
2912
		(idA_A1_3)
2913
		 else (idA_A1_1);
2914

    
2915

    
2916
	-- set state as inactive 
2917
	idParallel4_A_2
2918
	 = if (not isInner) then 0 else idParallel4_A_1;
2919

    
2920
	idA_A1_5 
2921
	= 0;
2922
	
2923

    
2924
	(idA_A1, idParallel4_A) 
2925
	= (idA_A1_5, idParallel4_A_1);
2926
	
2927

    
2928
tel
2929

    
2930

    
2931

    
2932

    
2933

    
2934

    
2935
-- Entry action for state :Parallel4_A
2936
node Parallel4_A_en(idParallel4_A_1:int;
2937
	idParallel4_Parallel4_1:int;
2938
	a_1:int;
2939
	idA_A1_1:int;
2940
	x:int;
2941
	idA_A2_1:int;
2942
	isInner:bool)
2943

    
2944
returns (idParallel4_A:int;
2945
	idParallel4_Parallel4:int;
2946
	a:int;
2947
	idA_A1:int;
2948
	idA_A2:int);
2949

    
2950

    
2951
var 	idParallel4_A_2, idParallel4_A_3, idParallel4_A_4, idParallel4_A_5, idParallel4_A_6:int;
2952
	idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4:int;
2953
	a_2, a_3, a_4, a_5, a_6:int;
2954
	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2955
	idA_A2_2, idA_A2_3:int;
2956

    
2957

    
2958
let
2959

    
2960

    
2961

    
2962
	-- set state as active 
2963
	idParallel4_Parallel4_2 
2964
	= 1646;
2965
	
2966

    
2967
	
2968
-- transition trace :
2969
	--POINT__To__A_A1_1
2970
		(idA_A1_2, idParallel4_A_2, a_2) 
2971
	= A_A1_en(idA_A1_1, idParallel4_A_1, a_1, x, false);
2972
		
2973

    
2974
	(idParallel4_A_3, idParallel4_Parallel4_3, a_3, idA_A1_3) 
2975
	= 
2976

    
2977
	if ( idParallel4_A_1 = 0) then
2978

    
2979
	 (idParallel4_A_2, idParallel4_Parallel4_2, a_2, idA_A1_2)
2980

    
2981
	 else(idParallel4_A_1, idParallel4_Parallel4_2, a_1, idA_A1_1);
2982

    
2983
	
2984

    
2985
	(idA_A2_2, idParallel4_A_4, a_4) 
2986
	= 
2987
	if ( idParallel4_A_1 = 1650) then
2988
	A_A2_en(idA_A2_1, idParallel4_A_1, a_1, x, false)
2989
	 else (idA_A2_1, idParallel4_A_1, a_1);
2990

    
2991
	
2992

    
2993
	(idA_A1_4, idParallel4_A_5, a_5) 
2994
	= 
2995
	if ( idParallel4_A_1 = 1647) then
2996
	A_A1_en(idA_A1_1, idParallel4_A_1, a_1, x, false)
2997
	 else (idA_A1_1, idParallel4_A_1, a_1);
2998

    
2999
	
3000

    
3001
	(idParallel4_A_6, idParallel4_Parallel4_4, a_6, idA_A1_5, idA_A2_3) 
3002
	= 
3003
		 if ( idParallel4_A_1 = 0) then 
3004
		(idParallel4_A_3, idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_1)
3005
		 else
3006
		 if ( idParallel4_A_1 = 1650) then 
3007
		(idParallel4_A_4, idParallel4_Parallel4_3, a_4, idA_A1_1, idA_A2_2)
3008
		 else
3009
		 if ( idParallel4_A_1 = 1647) then 
3010
		(idParallel4_A_5, idParallel4_Parallel4_3, a_5, idA_A1_4, idA_A2_1)
3011
		 else (idParallel4_A_1, idParallel4_Parallel4_2, a_1, idA_A1_1, idA_A2_1);
3012

    
3013

    
3014
	(idParallel4_A, idParallel4_Parallel4, a, idA_A1, idA_A2) 
3015
	= (idParallel4_A_6, idParallel4_Parallel4_4, a_6, idA_A1_5, idA_A2_3);
3016
	
3017

    
3018
tel
3019

    
3020

    
3021

    
3022

    
3023

    
3024
-- Exit action for state :Parallel4_A
3025
node Parallel4_A_ex(idA_A2_1:int;
3026
	idParallel4_A_1:int;
3027
	idA_A1_1:int;
3028
	idParallel4_Parallel4_1:int;
3029
	isInner:bool)
3030

    
3031
returns (idA_A2:int;
3032
	idParallel4_A:int;
3033
	idA_A1:int;
3034
	idParallel4_Parallel4:int);
3035

    
3036

    
3037
var 	idA_A2_2, idA_A2_3:int;
3038
	idParallel4_A_2, idParallel4_A_3, idParallel4_A_4, idParallel4_A_5:int;
3039
	idA_A1_2, idA_A1_3:int;
3040
	idParallel4_Parallel4_2:int;
3041

    
3042

    
3043
let
3044

    
3045

    
3046

    
3047
	
3048
	(idA_A2_2, idParallel4_A_2) 
3049
	= 
3050
	if ( idParallel4_A_1 = 1650) then
3051
	A_A2_ex(idA_A2_1, idParallel4_A_1, false)
3052
	 else (idA_A2_1, idParallel4_A_1);
3053

    
3054
	
3055

    
3056
	(idA_A1_2, idParallel4_A_3) 
3057
	= 
3058
	if ( idParallel4_A_1 = 1647) then
3059
	A_A1_ex(idA_A1_1, idParallel4_A_1, false)
3060
	 else (idA_A1_1, idParallel4_A_1);
3061

    
3062
	
3063

    
3064
	(idA_A2_3, idParallel4_A_4, idA_A1_3) 
3065
	= 
3066
		 if ( idParallel4_A_1 = 1650) then 
3067
		(idA_A2_2, idParallel4_A_2, idA_A1_1)
3068
		 else
3069
		 if ( idParallel4_A_1 = 1647) then 
3070
		(idA_A2_1, idParallel4_A_3, idA_A1_2)
3071
		 else (idA_A2_1, idParallel4_A_1, idA_A1_1);
3072

    
3073

    
3074
	-- set state as inactive 
3075
	idParallel4_Parallel4_2
3076
	 = if (not isInner) then 0 else idParallel4_Parallel4_1;
3077

    
3078
	idParallel4_A_5 
3079
	= 0;
3080
	
3081

    
3082
	(idA_A2, idParallel4_A, idA_A1, idParallel4_Parallel4) 
3083
	= (idA_A2_3, idParallel4_A_5, idA_A1_3, idParallel4_Parallel4_1);
3084
	
3085

    
3086
tel
3087

    
3088

    
3089
--***************************************************State :B_B2 Automaton***************************************************
3090

    
3091
node B_B2_node(idB_B2_1:int;
3092
	a_1:int;
3093
	b_1:int;
3094
	S:bool;
3095
	R:bool)
3096

    
3097
returns (idB_B2:int;
3098
	a:int;
3099
	b:int);
3100

    
3101

    
3102
let
3103

    
3104
	 automaton b_b2
3105

    
3106
	state POINTB_B2:
3107
	unless (idB_B2_1=0) restart POINT__TO__B2_B2A_1
3108

    
3109

    
3110

    
3111
	unless (idB_B2_1=1655) and S restart B2_B2A__TO__B2_B2B_1
3112

    
3113

    
3114

    
3115
	unless (idB_B2_1=1656) and R restart B2_B2B__TO__B2_B2A_1
3116

    
3117

    
3118

    
3119
	unless (idB_B2_1=1655) restart B2_B2A_IDL
3120

    
3121
	unless (idB_B2_1=1656) restart B2_B2B_IDL
3122

    
3123
	let
3124

    
3125
		(idB_B2, a, b) 
3126
	= (idB_B2_1, a_1, b_1);
3127
	
3128

    
3129
	tel
3130

    
3131

    
3132

    
3133
	state POINT__TO__B2_B2A_1:
3134

    
3135
	 var 	idB_B2_2:int;
3136
	a_2:int;
3137
	b_2:int;
3138
	let
3139

    
3140
		-- transition trace :
3141
	--POINT__To__B2_B2a_1
3142
		(idB_B2_2, a_2, b_2) 
3143
	= B2_B2a_en(idB_B2_1, a_1, b_1, false);
3144
		
3145

    
3146
	(idB_B2, a, b) 
3147
	=  (idB_B2_2, a_2, b_2);
3148

    
3149

    
3150
	tel
3151

    
3152
	until true restart POINTB_B2
3153

    
3154

    
3155

    
3156
	state B2_B2A__TO__B2_B2B_1:
3157

    
3158
	 var 	idB_B2_2, idB_B2_3:int;
3159
	a_2:int;
3160
	b_2:int;
3161
	let
3162

    
3163
		-- transition trace :
3164
	--B2_B2a__To__B2_B2b_1
3165
		(idB_B2_2) 
3166
	= B2_B2a_ex(idB_B2_1, false);
3167
		
3168

    
3169
		(idB_B2_3, a_2, b_2) 
3170
	= B2_B2b_en(idB_B2_2, a_1, b_1, false);
3171
		
3172

    
3173
	(idB_B2, a, b) 
3174
	=  (idB_B2_3, a_2, b_2);
3175

    
3176

    
3177
	tel
3178

    
3179
	until true restart POINTB_B2
3180

    
3181

    
3182

    
3183
	state B2_B2B__TO__B2_B2A_1:
3184

    
3185
	 var 	idB_B2_2, idB_B2_3:int;
3186
	a_2:int;
3187
	b_2:int;
3188
	let
3189

    
3190
		-- transition trace :
3191
	--B2_B2b__To__B2_B2a_1
3192
		(idB_B2_2) 
3193
	= B2_B2b_ex(idB_B2_1, false);
3194
		
3195

    
3196
		(idB_B2_3, a_2, b_2) 
3197
	= B2_B2a_en(idB_B2_2, a_1, b_1, false);
3198
		
3199

    
3200
	(idB_B2, a, b) 
3201
	=  (idB_B2_3, a_2, b_2);
3202

    
3203

    
3204
	tel
3205

    
3206
	until true restart POINTB_B2
3207

    
3208

    
3209

    
3210
	state B2_B2A_IDL:
3211

    
3212
	 	let
3213

    
3214
		
3215

    
3216
	(idB_B2, a, b) 
3217
	= (idB_B2_1, a_1, b_1);
3218
	
3219

    
3220
	tel
3221

    
3222
	until true restart POINTB_B2
3223

    
3224

    
3225

    
3226
	state B2_B2B_IDL:
3227

    
3228
	 	let
3229

    
3230
		
3231

    
3232
	(idB_B2, a, b) 
3233
	= (idB_B2_1, a_1, b_1);
3234
	
3235

    
3236
	tel
3237

    
3238
	until true restart POINTB_B2
3239

    
3240

    
3241

    
3242
tel
3243

    
3244

    
3245
--***************************************************State :B_B1 Automaton***************************************************
3246

    
3247
node B_B1_node(idB_B1_1:int;
3248
	a_1:int;
3249
	b_1:int;
3250
	S:bool;
3251
	R:bool)
3252

    
3253
returns (idB_B1:int;
3254
	a:int;
3255
	b:int);
3256

    
3257

    
3258
let
3259

    
3260
	 automaton b_b1
3261

    
3262
	state POINTB_B1:
3263
	unless (idB_B1_1=0) restart POINT__TO__B1_B1A_1
3264

    
3265

    
3266

    
3267
	unless (idB_B1_1=1658) and S restart B1_B1A__TO__B1_B1B_1
3268

    
3269

    
3270

    
3271
	unless (idB_B1_1=1659) and R restart B1_B1B__TO__B1_B1A_1
3272

    
3273

    
3274

    
3275
	unless (idB_B1_1=1658) restart B1_B1A_IDL
3276

    
3277
	unless (idB_B1_1=1659) restart B1_B1B_IDL
3278

    
3279
	let
3280

    
3281
		(idB_B1, a, b) 
3282
	= (idB_B1_1, a_1, b_1);
3283
	
3284

    
3285
	tel
3286

    
3287

    
3288

    
3289
	state POINT__TO__B1_B1A_1:
3290

    
3291
	 var 	idB_B1_2:int;
3292
	a_2:int;
3293
	b_2:int;
3294
	let
3295

    
3296
		-- transition trace :
3297
	--POINT__To__B1_B1a_1
3298
		(idB_B1_2, a_2, b_2) 
3299
	= B1_B1a_en(idB_B1_1, a_1, b_1, false);
3300
		
3301

    
3302
	(idB_B1, a, b) 
3303
	=  (idB_B1_2, a_2, b_2);
3304

    
3305

    
3306
	tel
3307

    
3308
	until true restart POINTB_B1
3309

    
3310

    
3311

    
3312
	state B1_B1A__TO__B1_B1B_1:
3313

    
3314
	 var 	idB_B1_2, idB_B1_3:int;
3315
	a_2:int;
3316
	b_2:int;
3317
	let
3318

    
3319
		-- transition trace :
3320
	--B1_B1a__To__B1_B1b_1
3321
		(idB_B1_2) 
3322
	= B1_B1a_ex(idB_B1_1, false);
3323
		
3324

    
3325
		(idB_B1_3, a_2, b_2) 
3326
	= B1_B1b_en(idB_B1_2, a_1, b_1, false);
3327
		
3328

    
3329
	(idB_B1, a, b) 
3330
	=  (idB_B1_3, a_2, b_2);
3331

    
3332

    
3333
	tel
3334

    
3335
	until true restart POINTB_B1
3336

    
3337

    
3338

    
3339
	state B1_B1B__TO__B1_B1A_1:
3340

    
3341
	 var 	idB_B1_2, idB_B1_3:int;
3342
	a_2:int;
3343
	b_2:int;
3344
	let
3345

    
3346
		-- transition trace :
3347
	--B1_B1b__To__B1_B1a_1
3348
		(idB_B1_2) 
3349
	= B1_B1b_ex(idB_B1_1, false);
3350
		
3351

    
3352
		(idB_B1_3, a_2, b_2) 
3353
	= B1_B1a_en(idB_B1_2, a_1, b_1, false);
3354
		
3355

    
3356
	(idB_B1, a, b) 
3357
	=  (idB_B1_3, a_2, b_2);
3358

    
3359

    
3360
	tel
3361

    
3362
	until true restart POINTB_B1
3363

    
3364

    
3365

    
3366
	state B1_B1A_IDL:
3367

    
3368
	 	let
3369

    
3370
		
3371

    
3372
	(idB_B1, a, b) 
3373
	= (idB_B1_1, a_1, b_1);
3374
	
3375

    
3376
	tel
3377

    
3378
	until true restart POINTB_B1
3379

    
3380

    
3381

    
3382
	state B1_B1B_IDL:
3383

    
3384
	 	let
3385

    
3386
		
3387

    
3388
	(idB_B1, a, b) 
3389
	= (idB_B1_1, a_1, b_1);
3390
	
3391

    
3392
	tel
3393

    
3394
	until true restart POINTB_B1
3395

    
3396

    
3397

    
3398
tel
3399

    
3400

    
3401
--***************************************************State :Parallel4_B Automaton***************************************************
3402

    
3403
node Parallel4_B_node(idParallel4_B_1:int;
3404
	a_1:int;
3405
	b_1:int;
3406
	idB_B1_1:int;
3407
	T:bool;
3408
	idB_B2_1:int;
3409
	R:bool;
3410
	S:bool)
3411

    
3412
returns (idParallel4_B:int;
3413
	a:int;
3414
	b:int;
3415
	idB_B1:int;
3416
	idB_B2:int);
3417

    
3418

    
3419
let
3420

    
3421
	 automaton parallel4_b
3422

    
3423
	state POINTParallel4_B:
3424
	unless (idParallel4_B_1=0) restart POINT__TO__B_B1_1
3425

    
3426

    
3427

    
3428
	unless (idParallel4_B_1=1654) and T restart B_B2__TO__B_B1_1
3429

    
3430

    
3431

    
3432
	unless (idParallel4_B_1=1657) and T restart B_B1__TO__B_B2_1
3433

    
3434

    
3435

    
3436
	unless (idParallel4_B_1=1654) restart B_B2_IDL
3437

    
3438
	unless (idParallel4_B_1=1657) restart B_B1_IDL
3439

    
3440
	let
3441

    
3442
		(idParallel4_B, a, b, idB_B1, idB_B2) 
3443
	= (idParallel4_B_1, a_1, b_1, idB_B1_1, idB_B2_1);
3444
	
3445

    
3446
	tel
3447

    
3448

    
3449

    
3450
	state POINT__TO__B_B1_1:
3451

    
3452
	 var 	idParallel4_B_2:int;
3453
	a_2:int;
3454
	b_2:int;
3455
	idB_B1_2:int;
3456
	let
3457

    
3458
		-- transition trace :
3459
	--POINT__To__B_B1_1
3460
		(idB_B1_2, idParallel4_B_2, a_2, b_2) 
3461
	= B_B1_en(idB_B1_1, idParallel4_B_1, a_1, b_1, false);
3462
		
3463

    
3464
	(idParallel4_B, a, b, idB_B1) 
3465
	=  (idParallel4_B_2, a_2, b_2, idB_B1_2);
3466

    
3467
	--add unused variables
3468
	(idB_B2) 
3469
	= (idB_B2_1);
3470
	
3471

    
3472
	tel
3473

    
3474
	until true restart POINTParallel4_B
3475

    
3476

    
3477

    
3478
	state B_B2__TO__B_B1_1:
3479

    
3480
	 var 	idParallel4_B_2, idParallel4_B_3:int;
3481
	a_2:int;
3482
	b_2:int;
3483
	idB_B1_2:int;
3484
	idB_B2_2:int;
3485
	let
3486

    
3487
		-- transition trace :
3488
	--B_B2__To__B_B1_1
3489
		(idB_B2_2, idParallel4_B_2) 
3490
	= B_B2_ex(idB_B2_1, idParallel4_B_1, false);
3491
		
3492

    
3493
		(idB_B1_2, idParallel4_B_3, a_2, b_2) 
3494
	= B_B1_en(idB_B1_1, idParallel4_B_2, a_1, b_1, false);
3495
		
3496

    
3497
	(idParallel4_B, a, b, idB_B1, idB_B2) 
3498
	=  (idParallel4_B_3, a_2, b_2, idB_B1_2, idB_B2_2);
3499

    
3500

    
3501
	tel
3502

    
3503
	until true restart POINTParallel4_B
3504

    
3505

    
3506

    
3507
	state B_B1__TO__B_B2_1:
3508

    
3509
	 var 	idParallel4_B_2, idParallel4_B_3:int;
3510
	a_2:int;
3511
	b_2:int;
3512
	idB_B1_2:int;
3513
	idB_B2_2:int;
3514
	let
3515

    
3516
		-- transition trace :
3517
	--B_B1__To__B_B2_1
3518
		(idB_B1_2, idParallel4_B_2) 
3519
	= B_B1_ex(idB_B1_1, idParallel4_B_1, false);
3520
		
3521

    
3522
		(idB_B2_2, idParallel4_B_3, a_2, b_2) 
3523
	= B_B2_en(idB_B2_1, idParallel4_B_2, a_1, b_1, false);
3524
		
3525

    
3526
	(idParallel4_B, a, b, idB_B1, idB_B2) 
3527
	=  (idParallel4_B_3, a_2, b_2, idB_B1_2, idB_B2_2);
3528

    
3529

    
3530
	tel
3531

    
3532
	until true restart POINTParallel4_B
3533

    
3534

    
3535

    
3536
	state B_B2_IDL:
3537

    
3538
	 var 	a_2:int;
3539
	b_2:int;
3540
	idB_B2_2:int;
3541
	let
3542

    
3543
		
3544
	(idB_B2_2, a_2, b_2) 
3545
	= B_B2_node(idB_B2_1, a_1, b_1, S, R);
3546

    
3547
		
3548

    
3549

    
3550
	(idParallel4_B, a, b, idB_B1, idB_B2) 
3551
	= (idParallel4_B_1, a_2, b_2, idB_B1_1, idB_B2_2);
3552
	
3553

    
3554
	tel
3555

    
3556
	until true restart POINTParallel4_B
3557

    
3558

    
3559

    
3560
	state B_B1_IDL:
3561

    
3562
	 var 	a_2:int;
3563
	b_2:int;
3564
	idB_B1_2:int;
3565
	let
3566

    
3567
		
3568
	(idB_B1_2, a_2, b_2) 
3569
	= B_B1_node(idB_B1_1, a_1, b_1, S, R);
3570

    
3571
		
3572

    
3573

    
3574
	(idParallel4_B, a, b, idB_B1, idB_B2) 
3575
	= (idParallel4_B_1, a_2, b_2, idB_B1_2, idB_B2_1);
3576
	
3577

    
3578
	tel
3579

    
3580
	until true restart POINTParallel4_B
3581

    
3582

    
3583

    
3584
tel
3585

    
3586

    
3587
--***************************************************State :D_D2 Automaton***************************************************
3588

    
3589
node D_D2_node(idD_D2_1:int;
3590
	c_1:int;
3591
	dd_1:int;
3592
	S:bool;
3593
	R:bool)
3594

    
3595
returns (idD_D2:int;
3596
	c:int;
3597
	dd:int);
3598

    
3599

    
3600
let
3601

    
3602
	 automaton d_d2
3603

    
3604
	state POINTD_D2:
3605
	unless (idD_D2_1=0) restart POINT__TO__D2_D2A_1
3606

    
3607

    
3608

    
3609
	unless (idD_D2_1=1669) and S restart D2_D2A__TO__D2_D2B_1
3610

    
3611

    
3612

    
3613
	unless (idD_D2_1=1670) and R restart D2_D2B__TO__D2_D2A_1
3614

    
3615

    
3616

    
3617
	unless (idD_D2_1=1669) restart D2_D2A_IDL
3618

    
3619
	unless (idD_D2_1=1670) restart D2_D2B_IDL
3620

    
3621
	let
3622

    
3623
		(idD_D2, c, dd) 
3624
	= (idD_D2_1, c_1, dd_1);
3625
	
3626

    
3627
	tel
3628

    
3629

    
3630

    
3631
	state POINT__TO__D2_D2A_1:
3632

    
3633
	 var 	idD_D2_2:int;
3634
	c_2:int;
3635
	dd_2:int;
3636
	let
3637

    
3638
		-- transition trace :
3639
	--POINT__To__D2_D2a_1
3640
		(idD_D2_2, c_2, dd_2) 
3641
	= D2_D2a_en(idD_D2_1, c_1, dd_1, false);
3642
		
3643

    
3644
	(idD_D2, c, dd) 
3645
	=  (idD_D2_2, c_2, dd_2);
3646

    
3647

    
3648
	tel
3649

    
3650
	until true restart POINTD_D2
3651

    
3652

    
3653

    
3654
	state D2_D2A__TO__D2_D2B_1:
3655

    
3656
	 var 	idD_D2_2, idD_D2_3:int;
3657
	c_2:int;
3658
	dd_2:int;
3659
	let
3660

    
3661
		-- transition trace :
3662
	--D2_D2a__To__D2_D2b_1
3663
		(idD_D2_2) 
3664
	= D2_D2a_ex(idD_D2_1, false);
3665
		
3666

    
3667
		(idD_D2_3, c_2, dd_2) 
3668
	= D2_D2b_en(idD_D2_2, c_1, dd_1, false);
3669
		
3670

    
3671
	(idD_D2, c, dd) 
3672
	=  (idD_D2_3, c_2, dd_2);
3673

    
3674

    
3675
	tel
3676

    
3677
	until true restart POINTD_D2
3678

    
3679

    
3680

    
3681
	state D2_D2B__TO__D2_D2A_1:
3682

    
3683
	 var 	idD_D2_2, idD_D2_3:int;
3684
	c_2:int;
3685
	dd_2:int;
3686
	let
3687

    
3688
		-- transition trace :
3689
	--D2_D2b__To__D2_D2a_1
3690
		(idD_D2_2) 
3691
	= D2_D2b_ex(idD_D2_1, false);
3692
		
3693

    
3694
		(idD_D2_3, c_2, dd_2) 
3695
	= D2_D2a_en(idD_D2_2, c_1, dd_1, false);
3696
		
3697

    
3698
	(idD_D2, c, dd) 
3699
	=  (idD_D2_3, c_2, dd_2);
3700

    
3701

    
3702
	tel
3703

    
3704
	until true restart POINTD_D2
3705

    
3706

    
3707

    
3708
	state D2_D2A_IDL:
3709

    
3710
	 	let
3711

    
3712
		
3713

    
3714
	(idD_D2, c, dd) 
3715
	= (idD_D2_1, c_1, dd_1);
3716
	
3717

    
3718
	tel
3719

    
3720
	until true restart POINTD_D2
3721

    
3722

    
3723

    
3724
	state D2_D2B_IDL:
3725

    
3726
	 	let
3727

    
3728
		
3729

    
3730
	(idD_D2, c, dd) 
3731
	= (idD_D2_1, c_1, dd_1);
3732
	
3733

    
3734
	tel
3735

    
3736
	until true restart POINTD_D2
3737

    
3738

    
3739

    
3740
tel
3741

    
3742

    
3743
--***************************************************State :D_D1 Automaton***************************************************
3744

    
3745
node D_D1_node(idD_D1_1:int;
3746
	c_1:int;
3747
	dd_1:int;
3748
	S:bool;
3749
	R:bool)
3750

    
3751
returns (idD_D1:int;
3752
	c:int;
3753
	dd:int);
3754

    
3755

    
3756
let
3757

    
3758
	 automaton d_d1
3759

    
3760
	state POINTD_D1:
3761
	unless (idD_D1_1=0) restart POINT__TO__D1_D1A_1
3762

    
3763

    
3764

    
3765
	unless (idD_D1_1=1672) and S restart D1_D1A__TO__D1_D1B_1
3766

    
3767

    
3768

    
3769
	unless (idD_D1_1=1673) and R restart D1_D1B__TO__D1_D1A_1
3770

    
3771

    
3772

    
3773
	unless (idD_D1_1=1672) restart D1_D1A_IDL
3774

    
3775
	unless (idD_D1_1=1673) restart D1_D1B_IDL
3776

    
3777
	let
3778

    
3779
		(idD_D1, c, dd) 
3780
	= (idD_D1_1, c_1, dd_1);
3781
	
3782

    
3783
	tel
3784

    
3785

    
3786

    
3787
	state POINT__TO__D1_D1A_1:
3788

    
3789
	 var 	idD_D1_2:int;
3790
	c_2:int;
3791
	dd_2:int;
3792
	let
3793

    
3794
		-- transition trace :
3795
	--POINT__To__D1_D1a_1
3796
		(idD_D1_2, c_2, dd_2) 
3797
	= D1_D1a_en(idD_D1_1, c_1, dd_1, false);
3798
		
3799

    
3800
	(idD_D1, c, dd) 
3801
	=  (idD_D1_2, c_2, dd_2);
3802

    
3803

    
3804
	tel
3805

    
3806
	until true restart POINTD_D1
3807

    
3808

    
3809

    
3810
	state D1_D1A__TO__D1_D1B_1:
3811

    
3812
	 var 	idD_D1_2, idD_D1_3:int;
3813
	c_2:int;
3814
	dd_2:int;
3815
	let
3816

    
3817
		-- transition trace :
3818
	--D1_D1a__To__D1_D1b_1
3819
		(idD_D1_2) 
3820
	= D1_D1a_ex(idD_D1_1, false);
3821
		
3822

    
3823
		(idD_D1_3, c_2, dd_2) 
3824
	= D1_D1b_en(idD_D1_2, c_1, dd_1, false);
3825
		
3826

    
3827
	(idD_D1, c, dd) 
3828
	=  (idD_D1_3, c_2, dd_2);
3829

    
3830

    
3831
	tel
3832

    
3833
	until true restart POINTD_D1
3834

    
3835

    
3836

    
3837
	state D1_D1B__TO__D1_D1A_1:
3838

    
3839
	 var 	idD_D1_2, idD_D1_3:int;
3840
	c_2:int;
3841
	dd_2:int;
3842
	let
3843

    
3844
		-- transition trace :
3845
	--D1_D1b__To__D1_D1a_1
3846
		(idD_D1_2) 
3847
	= D1_D1b_ex(idD_D1_1, false);
3848
		
3849

    
3850
		(idD_D1_3, c_2, dd_2) 
3851
	= D1_D1a_en(idD_D1_2, c_1, dd_1, false);
3852
		
3853

    
3854
	(idD_D1, c, dd) 
3855
	=  (idD_D1_3, c_2, dd_2);
3856

    
3857

    
3858
	tel
3859

    
3860
	until true restart POINTD_D1
3861

    
3862

    
3863

    
3864
	state D1_D1A_IDL:
3865

    
3866
	 	let
3867

    
3868
		
3869

    
3870
	(idD_D1, c, dd) 
3871
	= (idD_D1_1, c_1, dd_1);
3872
	
3873

    
3874
	tel
3875

    
3876
	until true restart POINTD_D1
3877

    
3878

    
3879

    
3880
	state D1_D1B_IDL:
3881

    
3882
	 	let
3883

    
3884
		
3885

    
3886
	(idD_D1, c, dd) 
3887
	= (idD_D1_1, c_1, dd_1);
3888
	
3889

    
3890
	tel
3891

    
3892
	until true restart POINTD_D1
3893

    
3894

    
3895

    
3896
tel
3897

    
3898

    
3899
--***************************************************State :CD_D Automaton***************************************************
3900

    
3901
node CD_D_node(idCD_D_1:int;
3902
	c_1:int;
3903
	dd_1:int;
3904
	idD_D1_1:int;
3905
	T:bool;
3906
	idD_D2_1:int;
3907
	R:bool;
3908
	S:bool)
3909

    
3910
returns (idCD_D:int;
3911
	c:int;
3912
	dd:int;
3913
	idD_D1:int;
3914
	idD_D2:int);
3915

    
3916

    
3917
let
3918

    
3919
	 automaton cd_d
3920

    
3921
	state POINTCD_D:
3922
	unless (idCD_D_1=0) restart POINT__TO__D_D1_1
3923

    
3924

    
3925

    
3926
	unless (idCD_D_1=1668) and T restart D_D2__TO__D_D1_1
3927

    
3928

    
3929

    
3930
	unless (idCD_D_1=1671) and T restart D_D1__TO__D_D2_1
3931

    
3932

    
3933

    
3934
	unless (idCD_D_1=1668) restart D_D2_IDL
3935

    
3936
	unless (idCD_D_1=1671) restart D_D1_IDL
3937

    
3938
	let
3939

    
3940
		(idCD_D, c, dd, idD_D1, idD_D2) 
3941
	= (idCD_D_1, c_1, dd_1, idD_D1_1, idD_D2_1);
3942
	
3943

    
3944
	tel
3945

    
3946

    
3947

    
3948
	state POINT__TO__D_D1_1:
3949

    
3950
	 var 	idCD_D_2:int;
3951
	c_2:int;
3952
	dd_2:int;
3953
	idD_D1_2:int;
3954
	let
3955

    
3956
		-- transition trace :
3957
	--POINT__To__D_D1_1
3958
		(idD_D1_2, idCD_D_2, c_2, dd_2) 
3959
	= D_D1_en(idD_D1_1, idCD_D_1, c_1, dd_1, false);
3960
		
3961

    
3962
	(idCD_D, c, dd, idD_D1) 
3963
	=  (idCD_D_2, c_2, dd_2, idD_D1_2);
3964

    
3965
	--add unused variables
3966
	(idD_D2) 
3967
	= (idD_D2_1);
3968
	
3969

    
3970
	tel
3971

    
3972
	until true restart POINTCD_D
3973

    
3974

    
3975

    
3976
	state D_D2__TO__D_D1_1:
3977

    
3978
	 var 	idCD_D_2, idCD_D_3:int;
3979
	c_2:int;
3980
	dd_2:int;
3981
	idD_D1_2:int;
3982
	idD_D2_2:int;
3983
	let
3984

    
3985
		-- transition trace :
3986
	--D_D2__To__D_D1_1
3987
		(idD_D2_2, idCD_D_2) 
3988
	= D_D2_ex(idD_D2_1, idCD_D_1, false);
3989
		
3990

    
3991
		(idD_D1_2, idCD_D_3, c_2, dd_2) 
3992
	= D_D1_en(idD_D1_1, idCD_D_2, c_1, dd_1, false);
3993
		
3994

    
3995
	(idCD_D, c, dd, idD_D1, idD_D2) 
3996
	=  (idCD_D_3, c_2, dd_2, idD_D1_2, idD_D2_2);
3997

    
3998

    
3999
	tel
4000

    
4001
	until true restart POINTCD_D
4002

    
4003

    
4004

    
4005
	state D_D1__TO__D_D2_1:
4006

    
4007
	 var 	idCD_D_2, idCD_D_3:int;
4008
	c_2:int;
4009
	dd_2:int;
4010
	idD_D1_2:int;
4011
	idD_D2_2:int;
4012
	let
4013

    
4014
		-- transition trace :
4015
	--D_D1__To__D_D2_1
4016
		(idD_D1_2, idCD_D_2) 
4017
	= D_D1_ex(idD_D1_1, idCD_D_1, false);
4018
		
4019

    
4020
		(idD_D2_2, idCD_D_3, c_2, dd_2) 
4021
	= D_D2_en(idD_D2_1, idCD_D_2, c_1, dd_1, false);
4022
		
4023

    
4024
	(idCD_D, c, dd, idD_D1, idD_D2) 
4025
	=  (idCD_D_3, c_2, dd_2, idD_D1_2, idD_D2_2);
4026

    
4027

    
4028
	tel
4029

    
4030
	until true restart POINTCD_D
4031

    
4032

    
4033

    
4034
	state D_D2_IDL:
4035

    
4036
	 var 	c_2:int;
4037
	dd_2:int;
4038
	idD_D2_2:int;
4039
	let
4040

    
4041
		
4042
	(idD_D2_2, c_2, dd_2) 
4043
	= D_D2_node(idD_D2_1, c_1, dd_1, S, R);
4044

    
4045
		
4046

    
4047

    
4048
	(idCD_D, c, dd, idD_D1, idD_D2) 
4049
	= (idCD_D_1, c_2, dd_2, idD_D1_1, idD_D2_2);
4050
	
4051

    
4052
	tel
4053

    
4054
	until true restart POINTCD_D
4055

    
4056

    
4057

    
4058
	state D_D1_IDL:
4059

    
4060
	 var 	c_2:int;
4061
	dd_2:int;
4062
	idD_D1_2:int;
4063
	let
4064

    
4065
		
4066
	(idD_D1_2, c_2, dd_2) 
4067
	= D_D1_node(idD_D1_1, c_1, dd_1, S, R);
4068

    
4069
		
4070

    
4071

    
4072
	(idCD_D, c, dd, idD_D1, idD_D2) 
4073
	= (idCD_D_1, c_2, dd_2, idD_D1_2, idD_D2_1);
4074
	
4075

    
4076
	tel
4077

    
4078
	until true restart POINTCD_D
4079

    
4080

    
4081

    
4082
tel
4083

    
4084

    
4085
--***************************************************State :C_C2 Automaton***************************************************
4086

    
4087
node C_C2_node(idC_C2_1:int;
4088
	b_1:int;
4089
	c_1:int;
4090
	S:bool;
4091
	R:bool)
4092

    
4093
returns (idC_C2:int;
4094
	b:int;
4095
	c:int);
4096

    
4097

    
4098
let
4099

    
4100
	 automaton c_c2
4101

    
4102
	state POINTC_C2:
4103
	unless (idC_C2_1=0) restart POINT__TO__C2_C2A_1
4104

    
4105

    
4106

    
4107
	unless (idC_C2_1=1662) and S restart C2_C2A__TO__C2_C2B_1
4108

    
4109

    
4110

    
4111
	unless (idC_C2_1=1663) and R restart C2_C2B__TO__C2_C2A_1
4112

    
4113

    
4114

    
4115
	unless (idC_C2_1=1662) restart C2_C2A_IDL
4116

    
4117
	unless (idC_C2_1=1663) restart C2_C2B_IDL
4118

    
4119
	let
4120

    
4121
		(idC_C2, b, c) 
4122
	= (idC_C2_1, b_1, c_1);
4123
	
4124

    
4125
	tel
4126

    
4127

    
4128

    
4129
	state POINT__TO__C2_C2A_1:
4130

    
4131
	 var 	idC_C2_2:int;
4132
	b_2:int;
4133
	c_2:int;
4134
	let
4135

    
4136
		-- transition trace :
4137
	--POINT__To__C2_C2a_1
4138
		(idC_C2_2, b_2, c_2) 
4139
	= C2_C2a_en(idC_C2_1, b_1, c_1, false);
4140
		
4141

    
4142
	(idC_C2, b, c) 
4143
	=  (idC_C2_2, b_2, c_2);
4144

    
4145

    
4146
	tel
4147

    
4148
	until true restart POINTC_C2
4149

    
4150

    
4151

    
4152
	state C2_C2A__TO__C2_C2B_1:
4153

    
4154
	 var 	idC_C2_2, idC_C2_3:int;
4155
	b_2:int;
4156
	c_2:int;
4157
	let
4158

    
4159
		-- transition trace :
4160
	--C2_C2a__To__C2_C2b_1
4161
		(idC_C2_2) 
4162
	= C2_C2a_ex(idC_C2_1, false);
4163
		
4164

    
4165
		(idC_C2_3, b_2, c_2) 
4166
	= C2_C2b_en(idC_C2_2, b_1, c_1, false);
4167
		
4168

    
4169
	(idC_C2, b, c) 
4170
	=  (idC_C2_3, b_2, c_2);
4171

    
4172

    
4173
	tel
4174

    
4175
	until true restart POINTC_C2
4176

    
4177

    
4178

    
4179
	state C2_C2B__TO__C2_C2A_1:
4180

    
4181
	 var 	idC_C2_2, idC_C2_3:int;
4182
	b_2:int;
4183
	c_2:int;
4184
	let
4185

    
4186
		-- transition trace :
4187
	--C2_C2b__To__C2_C2a_1
4188
		(idC_C2_2) 
4189
	= C2_C2b_ex(idC_C2_1, false);
4190
		
4191

    
4192
		(idC_C2_3, b_2, c_2) 
4193
	= C2_C2a_en(idC_C2_2, b_1, c_1, false);
4194
		
4195

    
4196
	(idC_C2, b, c) 
4197
	=  (idC_C2_3, b_2, c_2);
4198

    
4199

    
4200
	tel
4201

    
4202
	until true restart POINTC_C2
4203

    
4204

    
4205

    
4206
	state C2_C2A_IDL:
4207

    
4208
	 	let
4209

    
4210
		
4211

    
4212
	(idC_C2, b, c) 
4213
	= (idC_C2_1, b_1, c_1);
4214
	
4215

    
4216
	tel
4217

    
4218
	until true restart POINTC_C2
4219

    
4220

    
4221

    
4222
	state C2_C2B_IDL:
4223

    
4224
	 	let
4225

    
4226
		
4227

    
4228
	(idC_C2, b, c) 
4229
	= (idC_C2_1, b_1, c_1);
4230
	
4231

    
4232
	tel
4233

    
4234
	until true restart POINTC_C2
4235

    
4236

    
4237

    
4238
tel
4239

    
4240

    
4241
--***************************************************State :C_C1 Automaton***************************************************
4242

    
4243
node C_C1_node(idC_C1_1:int;
4244
	b_1:int;
4245
	c_1:int;
4246
	S:bool;
4247
	R:bool)
4248

    
4249
returns (idC_C1:int;
4250
	b:int;
4251
	c:int);
4252

    
4253

    
4254
let
4255

    
4256
	 automaton c_c1
4257

    
4258
	state POINTC_C1:
4259
	unless (idC_C1_1=0) restart POINT__TO__C1_C1A_1
4260

    
4261

    
4262

    
4263
	unless (idC_C1_1=1665) and S restart C1_C1A__TO__C1_C1B_1
4264

    
4265

    
4266

    
4267
	unless (idC_C1_1=1666) and R restart C1_C1B__TO__C1_C1A_1
4268

    
4269

    
4270

    
4271
	unless (idC_C1_1=1665) restart C1_C1A_IDL
4272

    
4273
	unless (idC_C1_1=1666) restart C1_C1B_IDL
4274

    
4275
	let
4276

    
4277
		(idC_C1, b, c) 
4278
	= (idC_C1_1, b_1, c_1);
4279
	
4280

    
4281
	tel
4282

    
4283

    
4284

    
4285
	state POINT__TO__C1_C1A_1:
4286

    
4287
	 var 	idC_C1_2:int;
4288
	b_2:int;
4289
	c_2:int;
4290
	let
4291

    
4292
		-- transition trace :
4293
	--POINT__To__C1_C1a_1
4294
		(idC_C1_2, b_2, c_2) 
4295
	= C1_C1a_en(idC_C1_1, b_1, c_1, false);
4296
		
4297

    
4298
	(idC_C1, b, c) 
4299
	=  (idC_C1_2, b_2, c_2);
4300

    
4301

    
4302
	tel
4303

    
4304
	until true restart POINTC_C1
4305

    
4306

    
4307

    
4308
	state C1_C1A__TO__C1_C1B_1:
4309

    
4310
	 var 	idC_C1_2, idC_C1_3:int;
4311
	b_2:int;
4312
	c_2:int;
4313
	let
4314

    
4315
		-- transition trace :
4316
	--C1_C1a__To__C1_C1b_1
4317
		(idC_C1_2) 
4318
	= C1_C1a_ex(idC_C1_1, false);
4319
		
4320

    
4321
		(idC_C1_3, b_2, c_2) 
4322
	= C1_C1b_en(idC_C1_2, b_1, c_1, false);
4323
		
4324

    
4325
	(idC_C1, b, c) 
4326
	=  (idC_C1_3, b_2, c_2);
4327

    
4328

    
4329
	tel
4330

    
4331
	until true restart POINTC_C1
4332

    
4333

    
4334

    
4335
	state C1_C1B__TO__C1_C1A_1:
4336

    
4337
	 var 	idC_C1_2, idC_C1_3:int;
4338
	b_2:int;
4339
	c_2:int;
4340
	let
4341

    
4342
		-- transition trace :
4343
	--C1_C1b__To__C1_C1a_1
4344
		(idC_C1_2) 
4345
	= C1_C1b_ex(idC_C1_1, false);
4346
		
4347

    
4348
		(idC_C1_3, b_2, c_2) 
4349
	= C1_C1a_en(idC_C1_2, b_1, c_1, false);
4350
		
4351

    
4352
	(idC_C1, b, c) 
4353
	=  (idC_C1_3, b_2, c_2);
4354

    
4355

    
4356
	tel
4357

    
4358
	until true restart POINTC_C1
4359

    
4360

    
4361

    
4362
	state C1_C1A_IDL:
4363

    
4364
	 	let
4365

    
4366
		
4367

    
4368
	(idC_C1, b, c) 
4369
	= (idC_C1_1, b_1, c_1);
4370
	
4371

    
4372
	tel
4373

    
4374
	until true restart POINTC_C1
4375

    
4376

    
4377

    
4378
	state C1_C1B_IDL:
4379

    
4380
	 	let
4381

    
4382
		
4383

    
4384
	(idC_C1, b, c) 
4385
	= (idC_C1_1, b_1, c_1);
4386
	
4387

    
4388
	tel
4389

    
4390
	until true restart POINTC_C1
4391

    
4392

    
4393

    
4394
tel
4395

    
4396

    
4397
--***************************************************State :CD_C Automaton***************************************************
4398

    
4399
node CD_C_node(idCD_C_1:int;
4400
	b_1:int;
4401
	c_1:int;
4402
	idC_C1_1:int;
4403
	T:bool;
4404
	idC_C2_1:int;
4405
	R:bool;
4406
	S:bool)
4407

    
4408
returns (idCD_C:int;
4409
	b:int;
4410
	c:int;
4411
	idC_C1:int;
4412
	idC_C2:int);
4413

    
4414

    
4415
let
4416

    
4417
	 automaton cd_c
4418

    
4419
	state POINTCD_C:
4420
	unless (idCD_C_1=0) restart POINT__TO__C_C1_1
4421

    
4422

    
4423

    
4424
	unless (idCD_C_1=1661) and T restart C_C2__TO__C_C1_1
4425

    
4426

    
4427

    
4428
	unless (idCD_C_1=1664) and T restart C_C1__TO__C_C2_1
4429

    
4430

    
4431

    
4432
	unless (idCD_C_1=1661) restart C_C2_IDL
4433

    
4434
	unless (idCD_C_1=1664) restart C_C1_IDL
4435

    
4436
	let
4437

    
4438
		(idCD_C, b, c, idC_C1, idC_C2) 
4439
	= (idCD_C_1, b_1, c_1, idC_C1_1, idC_C2_1);
4440
	
4441

    
4442
	tel
4443

    
4444

    
4445

    
4446
	state POINT__TO__C_C1_1:
4447

    
4448
	 var 	idCD_C_2:int;
4449
	b_2:int;
4450
	c_2:int;
4451
	idC_C1_2:int;
4452
	let
4453

    
4454
		-- transition trace :
4455
	--POINT__To__C_C1_1
4456
		(idC_C1_2, idCD_C_2, b_2, c_2) 
4457
	= C_C1_en(idC_C1_1, idCD_C_1, b_1, c_1, false);
4458
		
4459

    
4460
	(idCD_C, b, c, idC_C1) 
4461
	=  (idCD_C_2, b_2, c_2, idC_C1_2);
4462

    
4463
	--add unused variables
4464
	(idC_C2) 
4465
	= (idC_C2_1);
4466
	
4467

    
4468
	tel
4469

    
4470
	until true restart POINTCD_C
4471

    
4472

    
4473

    
4474
	state C_C2__TO__C_C1_1:
4475

    
4476
	 var 	idCD_C_2, idCD_C_3:int;
4477
	b_2:int;
4478
	c_2:int;
4479
	idC_C1_2:int;
4480
	idC_C2_2:int;
4481
	let
4482

    
4483
		-- transition trace :
4484
	--C_C2__To__C_C1_1
4485
		(idC_C2_2, idCD_C_2) 
4486
	= C_C2_ex(idC_C2_1, idCD_C_1, false);
4487
		
4488

    
4489
		(idC_C1_2, idCD_C_3, b_2, c_2) 
4490
	= C_C1_en(idC_C1_1, idCD_C_2, b_1, c_1, false);
4491
		
4492

    
4493
	(idCD_C, b, c, idC_C1, idC_C2) 
4494
	=  (idCD_C_3, b_2, c_2, idC_C1_2, idC_C2_2);
4495

    
4496

    
4497
	tel
4498

    
4499
	until true restart POINTCD_C
4500

    
4501

    
4502

    
4503
	state C_C1__TO__C_C2_1:
4504

    
4505
	 var 	idCD_C_2, idCD_C_3:int;
4506
	b_2:int;
4507
	c_2:int;
4508
	idC_C1_2:int;
4509
	idC_C2_2:int;
4510
	let
4511

    
4512
		-- transition trace :
4513
	--C_C1__To__C_C2_1
4514
		(idC_C1_2, idCD_C_2) 
4515
	= C_C1_ex(idC_C1_1, idCD_C_1, false);
4516
		
4517

    
4518
		(idC_C2_2, idCD_C_3, b_2, c_2) 
4519
	= C_C2_en(idC_C2_1, idCD_C_2, b_1, c_1, false);
4520
		
4521

    
4522
	(idCD_C, b, c, idC_C1, idC_C2) 
4523
	=  (idCD_C_3, b_2, c_2, idC_C1_2, idC_C2_2);
4524

    
4525

    
4526
	tel
4527

    
4528
	until true restart POINTCD_C
4529

    
4530

    
4531

    
4532
	state C_C2_IDL:
4533

    
4534
	 var 	b_2:int;
4535
	c_2:int;
4536
	idC_C2_2:int;
4537
	let
4538

    
4539
		
4540
	(idC_C2_2, b_2, c_2) 
4541
	= C_C2_node(idC_C2_1, b_1, c_1, S, R);
4542

    
4543
		
4544

    
4545

    
4546
	(idCD_C, b, c, idC_C1, idC_C2) 
4547
	= (idCD_C_1, b_2, c_2, idC_C1_1, idC_C2_2);
4548
	
4549

    
4550
	tel
4551

    
4552
	until true restart POINTCD_C
4553

    
4554

    
4555

    
4556
	state C_C1_IDL:
4557

    
4558
	 var 	b_2:int;
4559
	c_2:int;
4560
	idC_C1_2:int;
4561
	let
4562

    
4563
		
4564
	(idC_C1_2, b_2, c_2) 
4565
	= C_C1_node(idC_C1_1, b_1, c_1, S, R);
4566

    
4567
		
4568

    
4569

    
4570
	(idCD_C, b, c, idC_C1, idC_C2) 
4571
	= (idCD_C_1, b_2, c_2, idC_C1_2, idC_C2_1);
4572
	
4573

    
4574
	tel
4575

    
4576
	until true restart POINTCD_C
4577

    
4578

    
4579

    
4580
tel
4581

    
4582

    
4583
--***************************************************State :Parallel4_CD Automaton***************************************************
4584

    
4585
node Parallel4_CD_node(idParallel4_CD_1:int;
4586
	b_1:int;
4587
	c_1:int;
4588
	idCD_C_1:int;
4589
	idC_C1_1:int;
4590
	idC_C2_1:int;
4591
	dd_1:int;
4592
	idCD_D_1:int;
4593
	idD_D1_1:int;
4594
	idD_D2_1:int;
4595
	R:bool;
4596
	S:bool;
4597
	T:bool)
4598

    
4599
returns (idParallel4_CD:int;
4600
	b:int;
4601
	c:int;
4602
	idCD_C:int;
4603
	idC_C1:int;
4604
	idC_C2:int;
4605
	dd:int;
4606
	idCD_D:int;
4607
	idD_D1:int;
4608
	idD_D2:int);
4609

    
4610

    
4611
let
4612

    
4613
	 automaton parallel4_cd
4614

    
4615
	state POINTParallel4_CD:
4616
	unless (idParallel4_CD_1=0) restart PARALLEL4_CD_PARALLEL_ENTRY
4617
	unless true  restart PARALLEL4_CD_PARALLEL_IDL
4618

    
4619
	let
4620

    
4621
		(idParallel4_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4622
	= (idParallel4_CD_1, b_1, c_1, idCD_C_1, idC_C1_1, idC_C2_1, dd_1, idCD_D_1, idD_D1_1, idD_D2_1);
4623
	
4624

    
4625
	tel
4626

    
4627

    
4628

    
4629
	state PARALLEL4_CD_PARALLEL_ENTRY:
4630

    
4631
	 var 	idParallel4_CD_2, idParallel4_CD_3:int;
4632
	b_2:int;
4633
	c_2, c_3:int;
4634
	idCD_C_2:int;
4635
	idC_C1_2:int;
4636
	idC_C2_2:int;
4637
	dd_2:int;
4638
	idCD_D_2:int;
4639
	idD_D1_2:int;
4640
	idD_D2_2:int;
4641
	let
4642

    
4643
		
4644
	(idCD_C_2, idParallel4_CD_2, b_2, c_2, idC_C1_2, idC_C2_2) 
4645
	= CD_C_en(idCD_C_1, idParallel4_CD_1, b_1, c_1, idC_C1_1, idC_C2_1, false);
4646

    
4647
	(idCD_D_2, idParallel4_CD_3, c_3, dd_2, idD_D1_2, idD_D2_2) 
4648
	= CD_D_en(idCD_D_1, idParallel4_CD_2, c_2, dd_1, idD_D1_1, idD_D2_1, false);
4649

    
4650

    
4651
	(idParallel4_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4652
	= (idParallel4_CD_3, b_2, c_3, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2);
4653
	
4654

    
4655
	tel
4656

    
4657
	until true restart POINTParallel4_CD
4658

    
4659

    
4660

    
4661
	state PARALLEL4_CD_PARALLEL_IDL:
4662

    
4663
	 var 	b_2:int;
4664
	c_2, c_3:int;
4665
	idCD_C_2:int;
4666
	idC_C1_2:int;
4667
	idC_C2_2:int;
4668
	dd_2:int;
4669
	idCD_D_2:int;
4670
	idD_D1_2:int;
4671
	idD_D2_2:int;
4672
	let
4673

    
4674
		
4675

    
4676
		(idCD_C_2, b_2, c_2, idC_C1_2, idC_C2_2)
4677
	= if not (idCD_C_1= 0 ) then CD_C_node(idCD_C_1, b_1, c_1, idC_C1_1, T, idC_C2_1, R, S)
4678

    
4679
		 else (idCD_C_1, b_1, c_1, idC_C1_1, idC_C2_1);
4680

    
4681
		
4682

    
4683
		
4684

    
4685
		(idCD_D_2, c_3, dd_2, idD_D1_2, idD_D2_2)
4686
	= if not (idCD_D_1= 0 ) then CD_D_node(idCD_D_1, c_2, dd_1, idD_D1_1, T, idD_D2_1, R, S)
4687

    
4688
		 else (idCD_D_1, c_2, dd_1, idD_D1_1, idD_D2_1);
4689

    
4690
		
4691

    
4692
		
4693

    
4694
	(idParallel4_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4695
	= (idParallel4_CD_1, b_2, c_3, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2);
4696
	
4697

    
4698
	tel
4699

    
4700
	until true restart POINTParallel4_CD
4701

    
4702

    
4703

    
4704
tel
4705

    
4706

    
4707
--***************************************************State :A_A2 Automaton***************************************************
4708

    
4709
node A_A2_node(idA_A2_1:int;
4710
	a_1:int;
4711
	x:int;
4712
	S:bool;
4713
	idCD_C_1:int;
4714
	idCD_D_1:int;
4715
	idC_C1_1:int;
4716
	idC_C2_1:int;
4717
	idD_D1_1:int;
4718
	idD_D2_1:int;
4719
	idParallel4_CD_1:int;
4720
	idParallel4_Parallel4_1:int;
4721
	idB_B1_1:int;
4722
	idB_B2_1:int;
4723
	idParallel4_B_1:int;
4724
	idA_A1_1:int;
4725
	idParallel4_A_1:int;
4726
	b_1:int;
4727
	c_1:int;
4728
	dd_1:int;
4729
	R:bool)
4730

    
4731
returns (idA_A2:int;
4732
	a:int;
4733
	idCD_C:int;
4734
	idCD_D:int;
4735
	idC_C1:int;
4736
	idC_C2:int;
4737
	idD_D1:int;
4738
	idD_D2:int;
4739
	idParallel4_CD:int;
4740
	idParallel4_Parallel4:int;
4741
	idB_B1:int;
4742
	idB_B2:int;
4743
	idParallel4_B:int;
4744
	idA_A1:int;
4745
	idParallel4_A:int;
4746
	b:int;
4747
	c:int;
4748
	dd:int);
4749

    
4750

    
4751
let
4752

    
4753
	 automaton a_a2
4754

    
4755
	state POINTA_A2:
4756
	unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1
4757

    
4758

    
4759

    
4760
	unless (idA_A2_1=1651) and S restart A2_A2A__TO__A2_A2B_1
4761

    
4762

    
4763

    
4764
	unless (idA_A2_1=1652) and S restart A2_A2B__TO__C2_C2A_1
4765

    
4766

    
4767

    
4768
	unless (idA_A2_1=1652) and R restart A2_A2B__TO__A2_A2A_2
4769

    
4770

    
4771

    
4772
	unless (idA_A2_1=1651) restart A2_A2A_IDL
4773

    
4774
	unless (idA_A2_1=1652) restart A2_A2B_IDL
4775

    
4776
	let
4777

    
4778
		(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4779
	= (idA_A2_1, a_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1);
4780
	
4781

    
4782
	tel
4783

    
4784

    
4785

    
4786
	state POINT__TO__A2_A2A_1:
4787

    
4788
	 var 	idA_A2_2:int;
4789
	a_2:int;
4790
	let
4791

    
4792
		-- transition trace :
4793
	--POINT__To__A2_A2a_1
4794
		(idA_A2_2, a_2) 
4795
	= A2_A2a_en(idA_A2_1, x, a_1, false);
4796
		
4797

    
4798
	(idA_A2, a) 
4799
	=  (idA_A2_2, a_2);
4800

    
4801
	--add unused variables
4802
	(b, c, dd, idA_A1, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_A, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
4803
	= (b_1, c_1, dd_1, idA_A1_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_A_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
4804
	
4805

    
4806
	tel
4807

    
4808
	until true restart POINTA_A2
4809

    
4810

    
4811

    
4812
	state A2_A2A__TO__A2_A2B_1:
4813

    
4814
	 var 	idA_A2_2, idA_A2_3:int;
4815
	a_2:int;
4816
	let
4817

    
4818
		-- transition trace :
4819
	--A2_A2a__To__A2_A2b_1
4820
		(idA_A2_2) 
4821
	= A2_A2a_ex(idA_A2_1, false);
4822
		
4823

    
4824
		(idA_A2_3, a_2) 
4825
	= A2_A2b_en(idA_A2_2, x, a_1, false);
4826
		
4827

    
4828
	(idA_A2, a) 
4829
	=  (idA_A2_3, a_2);
4830

    
4831
	--add unused variables
4832
	(b, c, dd, idA_A1, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_A, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
4833
	= (b_1, c_1, dd_1, idA_A1_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_A_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
4834
	
4835

    
4836
	tel
4837

    
4838
	until true restart POINTA_A2
4839

    
4840

    
4841

    
4842
	state A2_A2B__TO__C2_C2A_1:
4843

    
4844
	 var 	idA_A2_2, idA_A2_3:int;
4845
	a_2, a_3:int;
4846
	idCD_C_2, idCD_C_3, idCD_C_4, idCD_C_5:int;
4847
	idCD_D_2, idCD_D_3:int;
4848
	idC_C1_2, idC_C1_3:int;
4849
	idC_C2_2, idC_C2_3, idC_C2_4, idC_C2_5:int;
4850
	idD_D1_2, idD_D1_3:int;
4851
	idD_D2_2, idD_D2_3:int;
4852
	idParallel4_CD_2, idParallel4_CD_3, idParallel4_CD_4, idParallel4_CD_5:int;
4853
	idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4, idParallel4_Parallel4_5, idParallel4_Parallel4_6, idParallel4_Parallel4_7:int;
4854
	idB_B1_2, idB_B1_3:int;
4855
	idB_B2_2, idB_B2_3:int;
4856
	idParallel4_B_2, idParallel4_B_3:int;
4857
	idA_A1_2, idA_A1_3:int;
4858
	idParallel4_A_2, idParallel4_A_3:int;
4859
	b_2, b_3:int;
4860
	c_2:int;
4861
	dd_2:int;
4862
	let
4863

    
4864
		-- transition trace :
4865
	--A2_A2b__To__C2_C2a_1
4866
		(idD_D2_2, idCD_D_2, idD_D1_2, idParallel4_CD_2, idCD_C_2, idC_C1_2, idC_C2_2, idParallel4_Parallel4_2) 
4867
	= Parallel4_CD_ex(idD_D2_1, idCD_D_1, idD_D1_1, idParallel4_CD_1, idCD_C_1, idC_C1_1, idC_C2_1, idParallel4_Parallel4_1, false);
4868
		
4869

    
4870
		(idB_B2_2, idParallel4_B_2, idB_B1_2, idParallel4_Parallel4_3) 
4871
	= Parallel4_B_ex(idB_B2_1, idParallel4_B_1, idB_B1_1, idParallel4_Parallel4_2, false);
4872
		
4873

    
4874
		(idA_A2_2, idParallel4_A_2, idA_A1_2, idParallel4_Parallel4_4) 
4875
	= Parallel4_A_ex(idA_A2_1, idParallel4_A_1, idA_A1_1, idParallel4_Parallel4_3, false);
4876
		
4877

    
4878
		idC_C2_3 
4879
	= 1662;
4880
	
4881
		idCD_C_3 
4882
	= 1661;
4883
	
4884
		idParallel4_CD_3 
4885
	= 1660;
4886
	
4887
		(idParallel4_A_3, idParallel4_Parallel4_5, a_2, idA_A1_3, idA_A2_3) 
4888
	= Parallel4_A_en(idParallel4_A_2, idParallel4_Parallel4_4, a_1, idA_A1_2, x, idA_A2_2, false);
4889
		
4890

    
4891
		(idParallel4_B_3, idParallel4_Parallel4_6, a_3, b_2, idB_B1_3, idB_B2_3) 
4892
	= Parallel4_B_en(idParallel4_B_2, idParallel4_Parallel4_5, a_2, b_1, idB_B1_2, idB_B2_2, false);
4893
		
4894

    
4895
		idC_C2_4 
4896
	= 1662;
4897
	
4898
		idCD_C_4 
4899
	= 1661;
4900
	
4901
		idParallel4_CD_4 
4902
	= 1660;
4903
	
4904
		(idParallel4_CD_5, idParallel4_Parallel4_7, b_3, c_2, idCD_C_5, idC_C1_3, idC_C2_5, dd_2, idCD_D_3, idD_D1_3, idD_D2_3) 
4905
	= Parallel4_CD_en(idParallel4_CD_4, idParallel4_Parallel4_6, b_2, c_1, idCD_C_4, idC_C1_2, idC_C2_4, dd_1, idCD_D_2, idD_D1_2, idD_D2_2, false);
4906
		
4907

    
4908
	(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4909
	=  (idA_A2_3, a_3, idCD_C_5, idCD_D_3, idC_C1_3, idC_C2_5, idD_D1_3, idD_D2_3, idParallel4_CD_5, idParallel4_Parallel4_7, idB_B1_3, idB_B2_3, idParallel4_B_3, idA_A1_3, idParallel4_A_3, b_3, c_2, dd_2);
4910

    
4911

    
4912
	tel
4913

    
4914
	until true restart POINTA_A2
4915

    
4916

    
4917

    
4918
	state A2_A2B__TO__A2_A2A_2:
4919

    
4920
	 var 	idA_A2_2, idA_A2_3:int;
4921
	a_2:int;
4922
	let
4923

    
4924
		-- transition trace :
4925
	--A2_A2b__To__A2_A2a_2
4926
		(idA_A2_2) 
4927
	= A2_A2b_ex(idA_A2_1, false);
4928
		
4929

    
4930
		(idA_A2_3, a_2) 
4931
	= A2_A2a_en(idA_A2_2, x, a_1, false);
4932
		
4933

    
4934
	(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4935
	=  (idA_A2_3, a_2, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1);
4936

    
4937

    
4938
	tel
4939

    
4940
	until true restart POINTA_A2
4941

    
4942

    
4943

    
4944
	state A2_A2A_IDL:
4945

    
4946
	 	let
4947

    
4948
		
4949

    
4950
	(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4951
	= (idA_A2_1, a_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1);
4952
	
4953

    
4954
	tel
4955

    
4956
	until true restart POINTA_A2
4957

    
4958

    
4959

    
4960
	state A2_A2B_IDL:
4961

    
4962
	 	let
4963

    
4964
		
4965

    
4966
	(idA_A2, a, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD, idParallel4_Parallel4, idB_B1, idB_B2, idParallel4_B, idA_A1, idParallel4_A, b, c, dd) 
4967
	= (idA_A2_1, a_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1);
4968
	
4969

    
4970
	tel
4971

    
4972
	until true restart POINTA_A2
4973

    
4974

    
4975

    
4976
tel
4977

    
4978

    
4979
--***************************************************State :A_A1 Automaton***************************************************
4980

    
4981
node A_A1_node(idA_A1_1:int;
4982
	a_1:int;
4983
	x:int;
4984
	S:bool;
4985
	R:bool)
4986

    
4987
returns (idA_A1:int;
4988
	a:int);
4989

    
4990

    
4991
let
4992

    
4993
	 automaton a_a1
4994

    
4995
	state POINTA_A1:
4996
	unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1
4997

    
4998

    
4999

    
5000
	unless (idA_A1_1=1648) and S restart A1_A1A__TO__A1_A1B_1
5001

    
5002

    
5003

    
5004
	unless (idA_A1_1=1649) and R restart A1_A1B__TO__A1_A1A_1
5005

    
5006

    
5007

    
5008
	unless (idA_A1_1=1648) restart A1_A1A_IDL
5009

    
5010
	unless (idA_A1_1=1649) restart A1_A1B_IDL
5011

    
5012
	let
5013

    
5014
		(idA_A1, a) 
5015
	= (idA_A1_1, a_1);
5016
	
5017

    
5018
	tel
5019

    
5020

    
5021

    
5022
	state POINT__TO__A1_A1A_1:
5023

    
5024
	 var 	idA_A1_2:int;
5025
	a_2:int;
5026
	let
5027

    
5028
		-- transition trace :
5029
	--POINT__To__A1_A1a_1
5030
		(idA_A1_2, a_2) 
5031
	= A1_A1a_en(idA_A1_1, x, a_1, false);
5032
		
5033

    
5034
	(idA_A1, a) 
5035
	=  (idA_A1_2, a_2);
5036

    
5037

    
5038
	tel
5039

    
5040
	until true restart POINTA_A1
5041

    
5042

    
5043

    
5044
	state A1_A1A__TO__A1_A1B_1:
5045

    
5046
	 var 	idA_A1_2, idA_A1_3:int;
5047
	a_2:int;
5048
	let
5049

    
5050
		-- transition trace :
5051
	--A1_A1a__To__A1_A1b_1
5052
		(idA_A1_2) 
5053
	= A1_A1a_ex(idA_A1_1, false);
5054
		
5055

    
5056
		(idA_A1_3, a_2) 
5057
	= A1_A1b_en(idA_A1_2, x, a_1, false);
5058
		
5059

    
5060
	(idA_A1, a) 
5061
	=  (idA_A1_3, a_2);
5062

    
5063

    
5064
	tel
5065

    
5066
	until true restart POINTA_A1
5067

    
5068

    
5069

    
5070
	state A1_A1B__TO__A1_A1A_1:
5071

    
5072
	 var 	idA_A1_2, idA_A1_3:int;
5073
	a_2:int;
5074
	let
5075

    
5076
		-- transition trace :
5077
	--A1_A1b__To__A1_A1a_1
5078
		(idA_A1_2) 
5079
	= A1_A1b_ex(idA_A1_1, false);
5080
		
5081

    
5082
		(idA_A1_3, a_2) 
5083
	= A1_A1a_en(idA_A1_2, x, a_1, false);
5084
		
5085

    
5086
	(idA_A1, a) 
5087
	=  (idA_A1_3, a_2);
5088

    
5089

    
5090
	tel
5091

    
5092
	until true restart POINTA_A1
5093

    
5094

    
5095

    
5096
	state A1_A1A_IDL:
5097

    
5098
	 	let
5099

    
5100
		
5101

    
5102
	(idA_A1, a) 
5103
	= (idA_A1_1, a_1);
5104
	
5105

    
5106
	tel
5107

    
5108
	until true restart POINTA_A1
5109

    
5110

    
5111

    
5112
	state A1_A1B_IDL:
5113

    
5114
	 	let
5115

    
5116
		
5117

    
5118
	(idA_A1, a) 
5119
	= (idA_A1_1, a_1);
5120
	
5121

    
5122
	tel
5123

    
5124
	until true restart POINTA_A1
5125

    
5126

    
5127

    
5128
tel
5129

    
5130

    
5131
--***************************************************State :Parallel4_A Automaton***************************************************
5132

    
5133
node Parallel4_A_node(idParallel4_A_1:int;
5134
	a_1:int;
5135
	idA_A1_1:int;
5136
	x:int;
5137
	T:bool;
5138
	idA_A2_1:int;
5139
	R:bool;
5140
	S:bool;
5141
	b_1:int;
5142
	c_1:int;
5143
	dd_1:int;
5144
	idB_B1_1:int;
5145
	idB_B2_1:int;
5146
	idCD_C_1:int;
5147
	idCD_D_1:int;
5148
	idC_C1_1:int;
5149
	idC_C2_1:int;
5150
	idD_D1_1:int;
5151
	idD_D2_1:int;
5152
	idParallel4_B_1:int;
5153
	idParallel4_CD_1:int;
5154
	idParallel4_Parallel4_1:int)
5155

    
5156
returns (idParallel4_A:int;
5157
	a:int;
5158
	idA_A1:int;
5159
	idA_A2:int;
5160
	b:int;
5161
	c:int;
5162
	dd:int;
5163
	idB_B1:int;
5164
	idB_B2:int;
5165
	idCD_C:int;
5166
	idCD_D:int;
5167
	idC_C1:int;
5168
	idC_C2:int;
5169
	idD_D1:int;
5170
	idD_D2:int;
5171
	idParallel4_B:int;
5172
	idParallel4_CD:int;
5173
	idParallel4_Parallel4:int);
5174

    
5175

    
5176
let
5177

    
5178
	 automaton parallel4_a
5179

    
5180
	state POINTParallel4_A:
5181
	unless (idParallel4_A_1=0) restart POINT__TO__A_A1_1
5182

    
5183

    
5184

    
5185
	unless (idParallel4_A_1=1650) and T restart A_A2__TO__A_A1_1
5186

    
5187

    
5188

    
5189
	unless (idParallel4_A_1=1647) and T restart A_A1__TO__A_A2_1
5190

    
5191

    
5192

    
5193
	unless (idParallel4_A_1=1650) restart A_A2_IDL
5194

    
5195
	unless (idParallel4_A_1=1647) restart A_A1_IDL
5196

    
5197
	let
5198

    
5199
		(idParallel4_A, a, idA_A1, idA_A2, b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5200
	= (idParallel4_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
5201
	
5202

    
5203
	tel
5204

    
5205

    
5206

    
5207
	state POINT__TO__A_A1_1:
5208

    
5209
	 var 	idParallel4_A_2:int;
5210
	a_2:int;
5211
	idA_A1_2:int;
5212
	let
5213

    
5214
		-- transition trace :
5215
	--POINT__To__A_A1_1
5216
		(idA_A1_2, idParallel4_A_2, a_2) 
5217
	= A_A1_en(idA_A1_1, idParallel4_A_1, a_1, x, false);
5218
		
5219

    
5220
	(idParallel4_A, a, idA_A1) 
5221
	=  (idParallel4_A_2, a_2, idA_A1_2);
5222

    
5223
	--add unused variables
5224
	(b, c, dd, idA_A2, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5225
	= (b_1, c_1, dd_1, idA_A2_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
5226
	
5227

    
5228
	tel
5229

    
5230
	until true restart POINTParallel4_A
5231

    
5232

    
5233

    
5234
	state A_A2__TO__A_A1_1:
5235

    
5236
	 var 	idParallel4_A_2, idParallel4_A_3:int;
5237
	a_2:int;
5238
	idA_A1_2:int;
5239
	idA_A2_2:int;
5240
	let
5241

    
5242
		-- transition trace :
5243
	--A_A2__To__A_A1_1
5244
		(idA_A2_2, idParallel4_A_2) 
5245
	= A_A2_ex(idA_A2_1, idParallel4_A_1, false);
5246
		
5247

    
5248
		(idA_A1_2, idParallel4_A_3, a_2) 
5249
	= A_A1_en(idA_A1_1, idParallel4_A_2, a_1, x, false);
5250
		
5251

    
5252
	(idParallel4_A, a, idA_A1, idA_A2) 
5253
	=  (idParallel4_A_3, a_2, idA_A1_2, idA_A2_2);
5254

    
5255
	--add unused variables
5256
	(b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5257
	= (b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
5258
	
5259

    
5260
	tel
5261

    
5262
	until true restart POINTParallel4_A
5263

    
5264

    
5265

    
5266
	state A_A1__TO__A_A2_1:
5267

    
5268
	 var 	idParallel4_A_2, idParallel4_A_3:int;
5269
	a_2:int;
5270
	idA_A1_2:int;
5271
	idA_A2_2:int;
5272
	let
5273

    
5274
		-- transition trace :
5275
	--A_A1__To__A_A2_1
5276
		(idA_A1_2, idParallel4_A_2) 
5277
	= A_A1_ex(idA_A1_1, idParallel4_A_1, false);
5278
		
5279

    
5280
		(idA_A2_2, idParallel4_A_3, a_2) 
5281
	= A_A2_en(idA_A2_1, idParallel4_A_2, a_1, x, false);
5282
		
5283

    
5284
	(idParallel4_A, a, idA_A1, idA_A2) 
5285
	=  (idParallel4_A_3, a_2, idA_A1_2, idA_A2_2);
5286

    
5287
	--add unused variables
5288
	(b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5289
	= (b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
5290
	
5291

    
5292
	tel
5293

    
5294
	until true restart POINTParallel4_A
5295

    
5296

    
5297

    
5298
	state A_A2_IDL:
5299

    
5300
	 var 	idParallel4_A_2:int;
5301
	a_2:int;
5302
	idA_A1_2:int;
5303
	idA_A2_2:int;
5304
	b_2:int;
5305
	c_2:int;
5306
	dd_2:int;
5307
	idB_B1_2:int;
5308
	idB_B2_2:int;
5309
	idCD_C_2:int;
5310
	idCD_D_2:int;
5311
	idC_C1_2:int;
5312
	idC_C2_2:int;
5313
	idD_D1_2:int;
5314
	idD_D2_2:int;
5315
	idParallel4_B_2:int;
5316
	idParallel4_CD_2:int;
5317
	idParallel4_Parallel4_2:int;
5318
	let
5319

    
5320
		
5321
	(idA_A2_2, a_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2, idParallel4_Parallel4_2, idB_B1_2, idB_B2_2, idParallel4_B_2, idA_A1_2, idParallel4_A_2, b_2, c_2, dd_2) 
5322
	= A_A2_node(idA_A2_1, a_1, x, S, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, idParallel4_Parallel4_1, idB_B1_1, idB_B2_1, idParallel4_B_1, idA_A1_1, idParallel4_A_1, b_1, c_1, dd_1, R);
5323

    
5324
		
5325

    
5326

    
5327
	(idParallel4_A, a, idA_A1, idA_A2, b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5328
	= (idParallel4_A_2, a_2, idA_A1_2, idA_A2_2, b_2, c_2, dd_2, idB_B1_2, idB_B2_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_B_2, idParallel4_CD_2, idParallel4_Parallel4_2);
5329
	
5330

    
5331
	tel
5332

    
5333
	until true restart POINTParallel4_A
5334

    
5335

    
5336

    
5337
	state A_A1_IDL:
5338

    
5339
	 var 	a_2:int;
5340
	idA_A1_2:int;
5341
	let
5342

    
5343
		
5344
	(idA_A1_2, a_2) 
5345
	= A_A1_node(idA_A1_1, a_1, x, S, R);
5346

    
5347
		
5348

    
5349

    
5350
	(idParallel4_A, a, idA_A1, idA_A2, b, c, dd, idB_B1, idB_B2, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_B, idParallel4_CD, idParallel4_Parallel4) 
5351
	= (idParallel4_A_1, a_2, idA_A1_2, idA_A2_1, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
5352
	
5353

    
5354
	tel
5355

    
5356
	until true restart POINTParallel4_A
5357

    
5358

    
5359

    
5360
tel
5361

    
5362

    
5363
--***************************************************State :Parallel4_Parallel4 Automaton***************************************************
5364

    
5365
node Parallel4_Parallel4_node(idParallel4_Parallel4_1:int;
5366
	a_1:int;
5367
	idA_A1_1:int;
5368
	idA_A2_1:int;
5369
	idParallel4_A_1:int;
5370
	x:int;
5371
	b_1:int;
5372
	idB_B1_1:int;
5373
	idB_B2_1:int;
5374
	idParallel4_B_1:int;
5375
	c_1:int;
5376
	dd_1:int;
5377
	idCD_C_1:int;
5378
	idCD_D_1:int;
5379
	idC_C1_1:int;
5380
	idC_C2_1:int;
5381
	idD_D1_1:int;
5382
	idD_D2_1:int;
5383
	idParallel4_CD_1:int;
5384
	R:bool;
5385
	S:bool;
5386
	T:bool)
5387

    
5388
returns (idParallel4_Parallel4:int;
5389
	a:int;
5390
	idA_A1:int;
5391
	idA_A2:int;
5392
	idParallel4_A:int;
5393
	b:int;
5394
	idB_B1:int;
5395
	idB_B2:int;
5396
	idParallel4_B:int;
5397
	c:int;
5398
	dd:int;
5399
	idCD_C:int;
5400
	idCD_D:int;
5401
	idC_C1:int;
5402
	idC_C2:int;
5403
	idD_D1:int;
5404
	idD_D2:int;
5405
	idParallel4_CD:int);
5406

    
5407

    
5408
let
5409

    
5410
	 automaton parallel4_parallel4
5411

    
5412
	state POINTParallel4_Parallel4:
5413
	unless (idParallel4_Parallel4_1=0) restart PARALLEL4_PARALLEL4_PARALLEL_ENTRY
5414
	unless true  restart PARALLEL4_PARALLEL4_PARALLEL_IDL
5415

    
5416
	let
5417

    
5418
		(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD) 
5419
	= (idParallel4_Parallel4_1, a_1, idA_A1_1, idA_A2_1, idParallel4_A_1, b_1, idB_B1_1, idB_B2_1, idParallel4_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1);
5420
	
5421

    
5422
	tel
5423

    
5424

    
5425

    
5426
	state PARALLEL4_PARALLEL4_PARALLEL_ENTRY:
5427

    
5428
	 var 	idParallel4_Parallel4_2, idParallel4_Parallel4_3, idParallel4_Parallel4_4:int;
5429
	a_2, a_3:int;
5430
	idA_A1_2:int;
5431
	idA_A2_2:int;
5432
	idParallel4_A_2:int;
5433
	b_2, b_3:int;
5434
	idB_B1_2:int;
5435
	idB_B2_2:int;
5436
	idParallel4_B_2:int;
5437
	c_2:int;
5438
	dd_2:int;
5439
	idCD_C_2:int;
5440
	idCD_D_2:int;
5441
	idC_C1_2:int;
5442
	idC_C2_2:int;
5443
	idD_D1_2:int;
5444
	idD_D2_2:int;
5445
	idParallel4_CD_2:int;
5446
	let
5447

    
5448
		
5449
	(idParallel4_A_2, idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2) 
5450
	= Parallel4_A_en(idParallel4_A_1, idParallel4_Parallel4_1, a_1, idA_A1_1, x, idA_A2_1, false);
5451

    
5452
	(idParallel4_B_2, idParallel4_Parallel4_3, a_3, b_2, idB_B1_2, idB_B2_2) 
5453
	= Parallel4_B_en(idParallel4_B_1, idParallel4_Parallel4_2, a_2, b_1, idB_B1_1, idB_B2_1, false);
5454

    
5455
	(idParallel4_CD_2, idParallel4_Parallel4_4, b_3, c_2, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2) 
5456
	= Parallel4_CD_en(idParallel4_CD_1, idParallel4_Parallel4_3, b_2, c_1, idCD_C_1, idC_C1_1, idC_C2_1, dd_1, idCD_D_1, idD_D1_1, idD_D2_1, false);
5457

    
5458

    
5459
	(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD) 
5460
	= (idParallel4_Parallel4_4, a_3, idA_A1_2, idA_A2_2, idParallel4_A_2, b_3, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2);
5461
	
5462

    
5463
	tel
5464

    
5465
	until true restart POINTParallel4_Parallel4
5466

    
5467

    
5468

    
5469
	state PARALLEL4_PARALLEL4_PARALLEL_IDL:
5470

    
5471
	 var 	idParallel4_Parallel4_2:int;
5472
	a_2, a_3:int;
5473
	idA_A1_2:int;
5474
	idA_A2_2:int;
5475
	idParallel4_A_2:int;
5476
	b_2, b_3, b_4:int;
5477
	idB_B1_2, idB_B1_3:int;
5478
	idB_B2_2, idB_B2_3:int;
5479
	idParallel4_B_2, idParallel4_B_3:int;
5480
	c_2, c_3:int;
5481
	dd_2, dd_3:int;
5482
	idCD_C_2, idCD_C_3:int;
5483
	idCD_D_2, idCD_D_3:int;
5484
	idC_C1_2, idC_C1_3:int;
5485
	idC_C2_2, idC_C2_3:int;
5486
	idD_D1_2, idD_D1_3:int;
5487
	idD_D2_2, idD_D2_3:int;
5488
	idParallel4_CD_2, idParallel4_CD_3:int;
5489
	let
5490

    
5491
		
5492

    
5493
		(idParallel4_A_2, a_2, idA_A1_2, idA_A2_2, b_2, c_2, dd_2, idB_B1_2, idB_B2_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_B_2, idParallel4_CD_2, idParallel4_Parallel4_2)
5494
	= if not (idParallel4_A_1= 0 ) then Parallel4_A_node(idParallel4_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R, S, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1)
5495

    
5496
		 else (idParallel4_A_1, a_1, idA_A1_1, idA_A2_1, b_1, c_1, dd_1, idB_B1_1, idB_B2_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_B_1, idParallel4_CD_1, idParallel4_Parallel4_1);
5497

    
5498
		
5499

    
5500
		
5501

    
5502
		(idParallel4_B_3, a_3, b_3, idB_B1_3, idB_B2_3)
5503
	= if not (idParallel4_B_2= 0 ) then Parallel4_B_node(idParallel4_B_2, a_2, b_2, idB_B1_2, T, idB_B2_2, R, S)
5504

    
5505
		 else (idParallel4_B_2, a_2, b_2, idB_B1_2, idB_B2_2);
5506

    
5507
		
5508

    
5509
		
5510

    
5511
		(idParallel4_CD_3, b_4, c_3, idCD_C_3, idC_C1_3, idC_C2_3, dd_3, idCD_D_3, idD_D1_3, idD_D2_3)
5512
	= if not (idParallel4_CD_2= 0 ) then Parallel4_CD_node(idParallel4_CD_2, b_3, c_2, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2, R, S, T)
5513

    
5514
		 else (idParallel4_CD_2, b_3, c_2, idCD_C_2, idC_C1_2, idC_C2_2, dd_2, idCD_D_2, idD_D1_2, idD_D2_2);
5515

    
5516
		
5517

    
5518
		
5519

    
5520
	(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD) 
5521
	= (idParallel4_Parallel4_2, a_3, idA_A1_2, idA_A2_2, idParallel4_A_2, b_4, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3);
5522
	
5523

    
5524
	tel
5525

    
5526
	until true restart POINTParallel4_Parallel4
5527

    
5528

    
5529

    
5530
tel
5531

    
5532

    
5533
--***************************************************State :Parallel4_Parallel4 Automaton***************************************************
5534

    
5535
node Parallel4_Parallel4(x:int;
5536
	R:bool;
5537
	S:bool;
5538
	T:bool)
5539

    
5540
returns (a:int;
5541
	b:int;
5542
	dd:int;
5543
	c:int);
5544

    
5545

    
5546
var a_1: int;
5547

    
5548
	b_1: int;
5549

    
5550
	dd_1: int;
5551

    
5552
	c_1: int;
5553

    
5554
	idParallel4_Parallel4, idParallel4_Parallel4_1: int;
5555

    
5556
	idB_B2, idB_B2_1: int;
5557

    
5558
	idB_B1, idB_B1_1: int;
5559

    
5560
	idParallel4_B, idParallel4_B_1: int;
5561

    
5562
	idD_D2, idD_D2_1: int;
5563

    
5564
	idD_D1, idD_D1_1: int;
5565

    
5566
	idCD_D, idCD_D_1: int;
5567

    
5568
	idC_C2, idC_C2_1: int;
5569

    
5570
	idC_C1, idC_C1_1: int;
5571

    
5572
	idCD_C, idCD_C_1: int;
5573

    
5574
	idParallel4_CD, idParallel4_CD_1: int;
5575

    
5576
	idA_A2, idA_A2_1: int;
5577

    
5578
	idA_A1, idA_A1_1: int;
5579

    
5580
	idParallel4_A, idParallel4_A_1: int;
5581

    
5582
		idParallel4_Parallel4_2, idParallel4_Parallel4_3:int;
5583
	a_2, a_3:int;
5584
	idA_A1_2, idA_A1_3:int;
5585
	idA_A2_2, idA_A2_3:int;
5586
	idParallel4_A_2, idParallel4_A_3:int;
5587
	b_2, b_3:int;
5588
	idB_B1_2, idB_B1_3:int;
5589
	idB_B2_2, idB_B2_3:int;
5590
	idParallel4_B_2, idParallel4_B_3:int;
5591
	c_2, c_3:int;
5592
	dd_2, dd_3:int;
5593
	idCD_C_2, idCD_C_3:int;
5594
	idCD_D_2, idCD_D_3:int;
5595
	idC_C1_2, idC_C1_3:int;
5596
	idC_C2_2, idC_C2_3:int;
5597
	idD_D1_2, idD_D1_3:int;
5598
	idD_D2_2, idD_D2_3:int;
5599
	idParallel4_CD_2, idParallel4_CD_3:int;
5600
let
5601

    
5602
	a_1 = 0 -> pre a;
5603

    
5604
	b_1 = 0 -> pre b;
5605

    
5606
	dd_1 = 0 -> pre dd;
5607

    
5608
	c_1 = 0 -> pre c;
5609

    
5610
	idParallel4_Parallel4_1 = 0 -> pre idParallel4_Parallel4;
5611

    
5612
	idB_B2_1 = 0 -> pre idB_B2;
5613

    
5614
	idB_B1_1 = 0 -> pre idB_B1;
5615

    
5616
	idParallel4_B_1 = 0 -> pre idParallel4_B;
5617

    
5618
	idD_D2_1 = 0 -> pre idD_D2;
5619

    
5620
	idD_D1_1 = 0 -> pre idD_D1;
5621

    
5622
	idCD_D_1 = 0 -> pre idCD_D;
5623

    
5624
	idC_C2_1 = 0 -> pre idC_C2;
5625

    
5626
	idC_C1_1 = 0 -> pre idC_C1;
5627

    
5628
	idCD_C_1 = 0 -> pre idCD_C;
5629

    
5630
	idParallel4_CD_1 = 0 -> pre idParallel4_CD;
5631

    
5632
	idA_A2_1 = 0 -> pre idA_A2;
5633

    
5634
	idA_A1_1 = 0 -> pre idA_A1;
5635

    
5636
	idParallel4_A_1 = 0 -> pre idParallel4_A;
5637

    
5638
	
5639

    
5640

    
5641

    
5642
	(idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2, idParallel4_A_2, b_2, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2)
5643
	 = 
5644

    
5645
	 if R then Parallel4_Parallel4_node(idParallel4_Parallel4_1, a_1, idA_A1_1, idA_A2_1, idParallel4_A_1, x, b_1, idB_B1_1, idB_B2_1, idParallel4_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1, R, false, false)
5646

    
5647
	 else (idParallel4_Parallel4_1, a_1, idA_A1_1, idA_A2_1, idParallel4_A_1, b_1, idB_B1_1, idB_B2_1, idParallel4_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel4_CD_1);
5648

    
5649
	
5650

    
5651

    
5652

    
5653
	(idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_3, idParallel4_A_3, b_3, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3)
5654
	 = 
5655

    
5656
	 if S then Parallel4_Parallel4_node(idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2, idParallel4_A_2, x, b_2, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2, false, S, false)
5657

    
5658
	 else (idParallel4_Parallel4_2, a_2, idA_A1_2, idA_A2_2, idParallel4_A_2, b_2, idB_B1_2, idB_B2_2, idParallel4_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel4_CD_2);
5659

    
5660
	
5661

    
5662

    
5663

    
5664
	(idParallel4_Parallel4, a, idA_A1, idA_A2, idParallel4_A, b, idB_B1, idB_B2, idParallel4_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel4_CD)
5665
	 = 
5666

    
5667
	 if T then Parallel4_Parallel4_node(idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_3, idParallel4_A_3, x, b_3, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3, false, false, T)
5668

    
5669
	 else (idParallel4_Parallel4_3, a_3, idA_A1_3, idA_A2_3, idParallel4_A_3, b_3, idB_B1_3, idB_B2_3, idParallel4_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel4_CD_3);
5670

    
5671
	
5672

    
5673

    
5674
--unused outputs
5675
	
5676

    
5677
tel
5678

    
5679

    
5680

    
5681
node Parallel4 (x_1_1 : int; R_1_1 : real; S_1_1 : real; T_1_1 : real)
5682
returns (a_1_1 : int;
5683
	b_2_1 : int;
5684
	dd_3_1 : int;
5685
	c_4_1 : int); 
5686
var
5687
	Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real;
5688
	Parallel4_1_1 : int; Parallel4_2_1 : int; Parallel4_3_1 : int; Parallel4_4_1 : int;
5689
	i_virtual_local : real;
5690
	Parallel4Mux_1_1_event: bool;
5691
	Parallel4Mux_1_2_event: bool;
5692
	Parallel4Mux_1_3_event: bool;
5693
let 
5694
	Mux_1_1 = R_1_1 ;
5695
	Mux_1_2 = S_1_1 ;
5696
	Mux_1_3 = T_1_1 ;
5697
	Parallel4Mux_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));
5698
	Parallel4Mux_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));
5699
	Parallel4Mux_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));
5700
	(Parallel4_1_1, Parallel4_2_1, Parallel4_3_1, Parallel4_4_1) =  Parallel4_Parallel4(x_1_1, Parallel4Mux_1_1_event, Parallel4Mux_1_2_event, Parallel4Mux_1_3_event);
5701
	a_1_1 = Parallel4_1_1;
5702
	b_2_1 = Parallel4_2_1;
5703
	dd_3_1 = Parallel4_3_1;
5704
	c_4_1 = Parallel4_4_1;
5705
	i_virtual_local= 0.0 -> 1.0;
5706
tel
5707