Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Parallel3V3 / Parallel3V3.lus @ eb639349

History | View | Annotate | Download (73.9 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9

    
10

    
11

    
12

    
13

    
14

    
15

    
16

    
17

    
18

    
19

    
20

    
21

    
22

    
23

    
24

    
25

    
26

    
27

    
28

    
29

    
30

    
31

    
32

    
33

    
34

    
35

    
36

    
37

    
38

    
39

    
40

    
41

    
42

    
43

    
44

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

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

    
55

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

    
59

    
60
let
61

    
62

    
63

    
64
	-- set state as active 
65
	idB_B2_2 
66
	= 1578;
67
	
68

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

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

    
78
tel
79

    
80

    
81

    
82

    
83

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

    
88
returns (idB_B2:int);
89

    
90

    
91
var 	idB_B2_2:int;
92

    
93

    
94
let
95

    
96

    
97

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

    
102

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

    
107
tel
108

    
109

    
110

    
111

    
112

    
113

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

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

    
124

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

    
128

    
129
let
130

    
131

    
132

    
133
	-- set state as active 
134
	idB_B2_2 
135
	= 1579;
136
	
137

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

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

    
147
tel
148

    
149

    
150

    
151

    
152

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

    
157
returns (idB_B2:int);
158

    
159

    
160
var 	idB_B2_2:int;
161

    
162

    
163
let
164

    
165

    
166

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

    
171

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

    
176
tel
177

    
178

    
179

    
180

    
181

    
182

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

    
190
returns (idB_B2:int;
191
	idParallel3_B:int;
192
	a:int;
193
	b:int);
194

    
195

    
196
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5, idB_B2_6:int;
197
	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4:int;
198
	a_2, a_3, a_4, a_5, a_6:int;
199
	b_2, b_3, b_4, b_5, b_6:int;
200

    
201

    
202
let
203

    
204

    
205

    
206
	-- set state as active 
207
	idParallel3_B_2 
208
	= 1577;
209
	
210

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

    
218
	(idB_B2_3, idParallel3_B_3, a_3, b_3) 
219
	= 
220

    
221
	if ( idB_B2_1 = 0) then
222

    
223
	 (idB_B2_2, idParallel3_B_2, a_2, b_2)
224

    
225
	 else(idB_B2_1, idParallel3_B_2, a_1, b_1);
226

    
227
	
228

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

    
235
	
236

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

    
243
	
244

    
245
	(idB_B2_6, idParallel3_B_4, a_6, b_6) 
246
	= 
247
		 if ( idB_B2_1 = 0) then 
248
		(idB_B2_3, idParallel3_B_3, a_3, b_3)
249
		 else
250
		 if ( idB_B2_1 = 1578) then 
251
		(idB_B2_4, idParallel3_B_3, a_4, b_4)
252
		 else
253
		 if ( idB_B2_1 = 1579) then 
254
		(idB_B2_5, idParallel3_B_3, a_5, b_5)
255
		 else (idB_B2_1, idParallel3_B_2, a_1, b_1);
256

    
257

    
258
	(idB_B2, idParallel3_B, a, b) 
259
	= (idB_B2_6, idParallel3_B_4, a_6, b_6);
260
	
261

    
262
tel
263

    
264

    
265

    
266

    
267

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

    
273
returns (idB_B2:int;
274
	idParallel3_B:int);
275

    
276

    
277
var 	idB_B2_2, idB_B2_3, idB_B2_4, idB_B2_5:int;
278
	idParallel3_B_2:int;
279

    
280

    
281
let
282

    
283

    
284

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

    
292
	
293

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

    
300
	
301

    
302
	(idB_B2_4) 
303
	= 
304
		 if ( idB_B2_1 = 1578) then 
305
		(idB_B2_2)
306
		 else
307
		 if ( idB_B2_1 = 1579) then 
308
		(idB_B2_3)
309
		 else (idB_B2_1);
310

    
311

    
312
	-- set state as inactive 
313
	idParallel3_B_2
314
	 = if (not isInner) then 0 else idParallel3_B_1;
315

    
316
	idB_B2_5 
317
	= 0;
318
	
319

    
320
	(idB_B2, idParallel3_B) 
321
	= (idB_B2_5, idParallel3_B_1);
322
	
323

    
324
tel
325

    
326

    
327

    
328

    
329

    
330

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

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

    
341

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

    
345

    
346
let
347

    
348

    
349

    
350
	-- set state as active 
351
	idB_B1_2 
352
	= 1581;
353
	
354

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

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

    
364
tel
365

    
366

    
367

    
368

    
369

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

    
374
returns (idB_B1:int);
375

    
376

    
377
var 	idB_B1_2:int;
378

    
379

    
380
let
381

    
382

    
383

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

    
388

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

    
393
tel
394

    
395

    
396

    
397

    
398

    
399

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

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

    
410

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

    
414

    
415
let
416

    
417

    
418

    
419
	-- set state as active 
420
	idB_B1_2 
421
	= 1582;
422
	
423

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

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

    
433
tel
434

    
435

    
436

    
437

    
438

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

    
443
returns (idB_B1:int);
444

    
445

    
446
var 	idB_B1_2:int;
447

    
448

    
449
let
450

    
451

    
452

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

    
457

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

    
462
tel
463

    
464

    
465

    
466

    
467

    
468

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

    
476
returns (idB_B1:int;
477
	idParallel3_B:int;
478
	a:int;
479
	b:int);
480

    
481

    
482
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5, idB_B1_6:int;
483
	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4:int;
484
	a_2, a_3, a_4, a_5, a_6:int;
485
	b_2, b_3, b_4, b_5, b_6:int;
486

    
487

    
488
let
489

    
490

    
491

    
492
	-- set state as active 
493
	idParallel3_B_2 
494
	= 1580;
495
	
496

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

    
504
	(idB_B1_3, idParallel3_B_3, a_3, b_3) 
505
	= 
506

    
507
	if ( idB_B1_1 = 0) then
508

    
509
	 (idB_B1_2, idParallel3_B_2, a_2, b_2)
510

    
511
	 else(idB_B1_1, idParallel3_B_2, a_1, b_1);
512

    
513
	
514

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

    
521
	
522

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

    
529
	
530

    
531
	(idB_B1_6, idParallel3_B_4, a_6, b_6) 
532
	= 
533
		 if ( idB_B1_1 = 0) then 
534
		(idB_B1_3, idParallel3_B_3, a_3, b_3)
535
		 else
536
		 if ( idB_B1_1 = 1581) then 
537
		(idB_B1_4, idParallel3_B_3, a_4, b_4)
538
		 else
539
		 if ( idB_B1_1 = 1582) then 
540
		(idB_B1_5, idParallel3_B_3, a_5, b_5)
541
		 else (idB_B1_1, idParallel3_B_2, a_1, b_1);
542

    
543

    
544
	(idB_B1, idParallel3_B, a, b) 
545
	= (idB_B1_6, idParallel3_B_4, a_6, b_6);
546
	
547

    
548
tel
549

    
550

    
551

    
552

    
553

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

    
559
returns (idB_B1:int;
560
	idParallel3_B:int);
561

    
562

    
563
var 	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
564
	idParallel3_B_2:int;
565

    
566

    
567
let
568

    
569

    
570

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

    
578
	
579

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

    
586
	
587

    
588
	(idB_B1_4) 
589
	= 
590
		 if ( idB_B1_1 = 1581) then 
591
		(idB_B1_2)
592
		 else
593
		 if ( idB_B1_1 = 1582) then 
594
		(idB_B1_3)
595
		 else (idB_B1_1);
596

    
597

    
598
	-- set state as inactive 
599
	idParallel3_B_2
600
	 = if (not isInner) then 0 else idParallel3_B_1;
601

    
602
	idB_B1_5 
603
	= 0;
604
	
605

    
606
	(idB_B1, idParallel3_B) 
607
	= (idB_B1_5, idParallel3_B_1);
608
	
609

    
610
tel
611

    
612

    
613

    
614

    
615

    
616

    
617
-- Entry action for state :Parallel3_B
618
node Parallel3_B_en(idParallel3_B_1:int;
619
	idParallel3_Parallel3_1:int;
620
	a_1:int;
621
	b_1:int;
622
	idB_B1_1:int;
623
	idB_B2_1:int;
624
	isInner:bool)
625

    
626
returns (idParallel3_B:int;
627
	idParallel3_Parallel3:int;
628
	a:int;
629
	b:int;
630
	idB_B1:int;
631
	idB_B2:int);
632

    
633

    
634
var 	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4, idParallel3_B_5, idParallel3_B_6:int;
635
	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int;
636
	a_2, a_3, a_4, a_5, a_6:int;
637
	b_2, b_3, b_4, b_5, b_6:int;
638
	idB_B1_2, idB_B1_3, idB_B1_4, idB_B1_5:int;
639
	idB_B2_2, idB_B2_3:int;
640

    
641

    
642
let
643

    
644

    
645

    
646
	-- set state as active 
647
	idParallel3_Parallel3_2 
648
	= 1576;
649
	
650

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

    
658
	(idParallel3_B_3, idParallel3_Parallel3_3, a_3, b_3, idB_B1_3) 
659
	= 
660

    
661
	if ( idParallel3_B_1 = 0) then
662

    
663
	 (idParallel3_B_2, idParallel3_Parallel3_2, a_2, b_2, idB_B1_2)
664

    
665
	 else(idParallel3_B_1, idParallel3_Parallel3_2, a_1, b_1, idB_B1_1);
666

    
667
	
668

    
669
	(idB_B2_2, idParallel3_B_4, a_4, b_4) 
670
	= 
671
	if ( idParallel3_B_1 = 1577) then
672
	B_B2_en(idB_B2_1, idParallel3_B_1, a_1, b_1, false)
673
	 else (idB_B2_1, idParallel3_B_1, a_1, b_1);
674

    
675
	
676

    
677
	(idB_B1_4, idParallel3_B_5, a_5, b_5) 
678
	= 
679
	if ( idParallel3_B_1 = 1580) then
680
	B_B1_en(idB_B1_1, idParallel3_B_1, a_1, b_1, false)
681
	 else (idB_B1_1, idParallel3_B_1, a_1, b_1);
682

    
683
	
684

    
685
	(idParallel3_B_6, idParallel3_Parallel3_4, a_6, b_6, idB_B1_5, idB_B2_3) 
686
	= 
687
		 if ( idParallel3_B_1 = 0) then 
688
		(idParallel3_B_3, idParallel3_Parallel3_3, a_3, b_3, idB_B1_3, idB_B2_1)
689
		 else
690
		 if ( idParallel3_B_1 = 1577) then 
691
		(idParallel3_B_4, idParallel3_Parallel3_3, a_4, b_4, idB_B1_1, idB_B2_2)
692
		 else
693
		 if ( idParallel3_B_1 = 1580) then 
694
		(idParallel3_B_5, idParallel3_Parallel3_3, a_5, b_5, idB_B1_4, idB_B2_1)
695
		 else (idParallel3_B_1, idParallel3_Parallel3_2, a_1, b_1, idB_B1_1, idB_B2_1);
696

    
697

    
698
	(idParallel3_B, idParallel3_Parallel3, a, b, idB_B1, idB_B2) 
699
	= (idParallel3_B_6, idParallel3_Parallel3_4, a_6, b_6, idB_B1_5, idB_B2_3);
700
	
701

    
702
tel
703

    
704

    
705

    
706

    
707

    
708
-- Exit action for state :Parallel3_B
709
node Parallel3_B_ex(idB_B2_1:int;
710
	idParallel3_B_1:int;
711
	idB_B1_1:int;
712
	idParallel3_Parallel3_1:int;
713
	isInner:bool)
714

    
715
returns (idB_B2:int;
716
	idParallel3_B:int;
717
	idB_B1:int;
718
	idParallel3_Parallel3:int);
719

    
720

    
721
var 	idB_B2_2, idB_B2_3:int;
722
	idParallel3_B_2, idParallel3_B_3, idParallel3_B_4, idParallel3_B_5:int;
723
	idB_B1_2, idB_B1_3:int;
724
	idParallel3_Parallel3_2:int;
725

    
726

    
727
let
728

    
729

    
730

    
731
	
732
	(idB_B2_2, idParallel3_B_2) 
733
	= 
734
	if ( idParallel3_B_1 = 1577) then
735
	B_B2_ex(idB_B2_1, idParallel3_B_1, false)
736
	 else (idB_B2_1, idParallel3_B_1);
737

    
738
	
739

    
740
	(idB_B1_2, idParallel3_B_3) 
741
	= 
742
	if ( idParallel3_B_1 = 1580) then
743
	B_B1_ex(idB_B1_1, idParallel3_B_1, false)
744
	 else (idB_B1_1, idParallel3_B_1);
745

    
746
	
747

    
748
	(idB_B2_3, idParallel3_B_4, idB_B1_3) 
749
	= 
750
		 if ( idParallel3_B_1 = 1577) then 
751
		(idB_B2_2, idParallel3_B_2, idB_B1_1)
752
		 else
753
		 if ( idParallel3_B_1 = 1580) then 
754
		(idB_B2_1, idParallel3_B_3, idB_B1_2)
755
		 else (idB_B2_1, idParallel3_B_1, idB_B1_1);
756

    
757

    
758
	-- set state as inactive 
759
	idParallel3_Parallel3_2
760
	 = if (not isInner) then 0 else idParallel3_Parallel3_1;
761

    
762
	idParallel3_B_5 
763
	= 0;
764
	
765

    
766
	(idB_B2, idParallel3_B, idB_B1, idParallel3_Parallel3) 
767
	= (idB_B2_3, idParallel3_B_5, idB_B1_3, idParallel3_Parallel3_1);
768
	
769

    
770
tel
771

    
772

    
773

    
774

    
775

    
776

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

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

    
787

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

    
791

    
792
let
793

    
794

    
795

    
796
	-- set state as active 
797
	idD_D2_2 
798
	= 1592;
799
	
800

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

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

    
810
tel
811

    
812

    
813

    
814

    
815

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

    
820
returns (idD_D2:int);
821

    
822

    
823
var 	idD_D2_2:int;
824

    
825

    
826
let
827

    
828

    
829

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

    
834

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

    
839
tel
840

    
841

    
842

    
843

    
844

    
845

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

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

    
856

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

    
860

    
861
let
862

    
863

    
864

    
865
	-- set state as active 
866
	idD_D2_2 
867
	= 1593;
868
	
869

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

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

    
879
tel
880

    
881

    
882

    
883

    
884

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

    
889
returns (idD_D2:int);
890

    
891

    
892
var 	idD_D2_2:int;
893

    
894

    
895
let
896

    
897

    
898

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

    
903

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

    
908
tel
909

    
910

    
911

    
912

    
913

    
914

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

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

    
927

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

    
933

    
934
let
935

    
936

    
937

    
938
	-- set state as active 
939
	idCD_D_2 
940
	= 1591;
941
	
942

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

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

    
953
	if ( idD_D2_1 = 0) then
954

    
955
	 (idD_D2_2, idCD_D_2, c_2, dd_2)
956

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

    
959
	
960

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

    
967
	
968

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

    
975
	
976

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

    
989

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

    
994
tel
995

    
996

    
997

    
998

    
999

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

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

    
1008

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

    
1012

    
1013
let
1014

    
1015

    
1016

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

    
1024
	
1025

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

    
1032
	
1033

    
1034
	(idD_D2_4) 
1035
	= 
1036
		 if ( idD_D2_1 = 1592) then 
1037
		(idD_D2_2)
1038
		 else
1039
		 if ( idD_D2_1 = 1593) then 
1040
		(idD_D2_3)
1041
		 else (idD_D2_1);
1042

    
1043

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

    
1048
	idD_D2_5 
1049
	= 0;
1050
	
1051

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

    
1056
tel
1057

    
1058

    
1059

    
1060

    
1061

    
1062

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

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

    
1073

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

    
1077

    
1078
let
1079

    
1080

    
1081

    
1082
	-- set state as active 
1083
	idD_D1_2 
1084
	= 1595;
1085
	
1086

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

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

    
1096
tel
1097

    
1098

    
1099

    
1100

    
1101

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

    
1106
returns (idD_D1:int);
1107

    
1108

    
1109
var 	idD_D1_2:int;
1110

    
1111

    
1112
let
1113

    
1114

    
1115

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

    
1120

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

    
1125
tel
1126

    
1127

    
1128

    
1129

    
1130

    
1131

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

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

    
1142

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

    
1146

    
1147
let
1148

    
1149

    
1150

    
1151
	-- set state as active 
1152
	idD_D1_2 
1153
	= 1596;
1154
	
1155

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

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

    
1165
tel
1166

    
1167

    
1168

    
1169

    
1170

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

    
1175
returns (idD_D1:int);
1176

    
1177

    
1178
var 	idD_D1_2:int;
1179

    
1180

    
1181
let
1182

    
1183

    
1184

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

    
1189

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

    
1194
tel
1195

    
1196

    
1197

    
1198

    
1199

    
1200

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

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

    
1213

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

    
1219

    
1220
let
1221

    
1222

    
1223

    
1224
	-- set state as active 
1225
	idCD_D_2 
1226
	= 1594;
1227
	
1228

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

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

    
1239
	if ( idD_D1_1 = 0) then
1240

    
1241
	 (idD_D1_2, idCD_D_2, c_2, dd_2)
1242

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

    
1245
	
1246

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

    
1253
	
1254

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

    
1261
	
1262

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

    
1275

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

    
1280
tel
1281

    
1282

    
1283

    
1284

    
1285

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

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

    
1294

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

    
1298

    
1299
let
1300

    
1301

    
1302

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

    
1310
	
1311

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

    
1318
	
1319

    
1320
	(idD_D1_4) 
1321
	= 
1322
		 if ( idD_D1_1 = 1595) then 
1323
		(idD_D1_2)
1324
		 else
1325
		 if ( idD_D1_1 = 1596) then 
1326
		(idD_D1_3)
1327
		 else (idD_D1_1);
1328

    
1329

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

    
1334
	idD_D1_5 
1335
	= 0;
1336
	
1337

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

    
1342
tel
1343

    
1344

    
1345

    
1346

    
1347

    
1348

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

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

    
1365

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

    
1373

    
1374
let
1375

    
1376

    
1377

    
1378
	-- set state as active 
1379
	idParallel3_CD_2 
1380
	= 1590;
1381
	
1382

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

    
1390
	(idCD_D_3, idParallel3_CD_3, c_3, dd_3, idD_D1_3) 
1391
	= 
1392

    
1393
	if ( idCD_D_1 = 0) then
1394

    
1395
	 (idCD_D_2, idParallel3_CD_2, c_2, dd_2, idD_D1_2)
1396

    
1397
	 else(idCD_D_1, idParallel3_CD_2, c_1, dd_1, idD_D1_1);
1398

    
1399
	
1400

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

    
1407
	
1408

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

    
1415
	
1416

    
1417
	(idCD_D_6, idParallel3_CD_4, c_6, dd_6, idD_D1_5, idD_D2_3) 
1418
	= 
1419
		 if ( idCD_D_1 = 0) then 
1420
		(idCD_D_3, idParallel3_CD_3, c_3, dd_3, idD_D1_3, idD_D2_1)
1421
		 else
1422
		 if ( idCD_D_1 = 1591) then 
1423
		(idCD_D_4, idParallel3_CD_3, c_4, dd_4, idD_D1_1, idD_D2_2)
1424
		 else
1425
		 if ( idCD_D_1 = 1594) then 
1426
		(idCD_D_5, idParallel3_CD_3, c_5, dd_5, idD_D1_4, idD_D2_1)
1427
		 else (idCD_D_1, idParallel3_CD_2, c_1, dd_1, idD_D1_1, idD_D2_1);
1428

    
1429

    
1430
	(idCD_D, idParallel3_CD, c, dd, idD_D1, idD_D2) 
1431
	= (idCD_D_6, idParallel3_CD_4, c_6, dd_6, idD_D1_5, idD_D2_3);
1432
	
1433

    
1434
tel
1435

    
1436

    
1437

    
1438

    
1439

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

    
1447
returns (idD_D2:int;
1448
	idCD_D:int;
1449
	idD_D1:int;
1450
	idParallel3_CD:int);
1451

    
1452

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

    
1458

    
1459
let
1460

    
1461

    
1462

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

    
1470
	
1471

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

    
1478
	
1479

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

    
1489

    
1490
	-- set state as inactive 
1491
	idParallel3_CD_2
1492
	 = if (not isInner) then 0 else idParallel3_CD_1;
1493

    
1494
	idCD_D_5 
1495
	= 0;
1496
	
1497

    
1498
	(idD_D2, idCD_D, idD_D1, idParallel3_CD) 
1499
	= (idD_D2_3, idCD_D_5, idD_D1_3, idParallel3_CD_1);
1500
	
1501

    
1502
tel
1503

    
1504

    
1505

    
1506

    
1507

    
1508

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

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

    
1519

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

    
1523

    
1524
let
1525

    
1526

    
1527

    
1528
	-- set state as active 
1529
	idC_C2_2 
1530
	= 1585;
1531
	
1532

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

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

    
1542
tel
1543

    
1544

    
1545

    
1546

    
1547

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

    
1552
returns (idC_C2:int);
1553

    
1554

    
1555
var 	idC_C2_2:int;
1556

    
1557

    
1558
let
1559

    
1560

    
1561

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

    
1566

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

    
1571
tel
1572

    
1573

    
1574

    
1575

    
1576

    
1577

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

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

    
1588

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

    
1592

    
1593
let
1594

    
1595

    
1596

    
1597
	-- set state as active 
1598
	idC_C2_2 
1599
	= 1586;
1600
	
1601

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

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

    
1611
tel
1612

    
1613

    
1614

    
1615

    
1616

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

    
1621
returns (idC_C2:int);
1622

    
1623

    
1624
var 	idC_C2_2:int;
1625

    
1626

    
1627
let
1628

    
1629

    
1630

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

    
1635

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

    
1640
tel
1641

    
1642

    
1643

    
1644

    
1645

    
1646

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

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

    
1659

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

    
1665

    
1666
let
1667

    
1668

    
1669

    
1670
	-- set state as active 
1671
	idCD_C_2 
1672
	= 1584;
1673
	
1674

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

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

    
1685
	if ( idC_C2_1 = 0) then
1686

    
1687
	 (idC_C2_2, idCD_C_2, b_2, c_2)
1688

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

    
1691
	
1692

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

    
1699
	
1700

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

    
1707
	
1708

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

    
1721

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

    
1726
tel
1727

    
1728

    
1729

    
1730

    
1731

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

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

    
1740

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

    
1744

    
1745
let
1746

    
1747

    
1748

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

    
1756
	
1757

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

    
1764
	
1765

    
1766
	(idC_C2_4) 
1767
	= 
1768
		 if ( idC_C2_1 = 1585) then 
1769
		(idC_C2_2)
1770
		 else
1771
		 if ( idC_C2_1 = 1586) then 
1772
		(idC_C2_3)
1773
		 else (idC_C2_1);
1774

    
1775

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

    
1780
	idC_C2_5 
1781
	= 0;
1782
	
1783

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

    
1788
tel
1789

    
1790

    
1791

    
1792

    
1793

    
1794

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

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

    
1805

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

    
1809

    
1810
let
1811

    
1812

    
1813

    
1814
	-- set state as active 
1815
	idC_C1_2 
1816
	= 1588;
1817
	
1818

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

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

    
1828
tel
1829

    
1830

    
1831

    
1832

    
1833

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

    
1838
returns (idC_C1:int);
1839

    
1840

    
1841
var 	idC_C1_2:int;
1842

    
1843

    
1844
let
1845

    
1846

    
1847

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

    
1852

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

    
1857
tel
1858

    
1859

    
1860

    
1861

    
1862

    
1863

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

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

    
1874

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

    
1878

    
1879
let
1880

    
1881

    
1882

    
1883
	-- set state as active 
1884
	idC_C1_2 
1885
	= 1589;
1886
	
1887

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

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

    
1897
tel
1898

    
1899

    
1900

    
1901

    
1902

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

    
1907
returns (idC_C1:int);
1908

    
1909

    
1910
var 	idC_C1_2:int;
1911

    
1912

    
1913
let
1914

    
1915

    
1916

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

    
1921

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

    
1926
tel
1927

    
1928

    
1929

    
1930

    
1931

    
1932

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

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

    
1945

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

    
1951

    
1952
let
1953

    
1954

    
1955

    
1956
	-- set state as active 
1957
	idCD_C_2 
1958
	= 1587;
1959
	
1960

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

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

    
1971
	if ( idC_C1_1 = 0) then
1972

    
1973
	 (idC_C1_2, idCD_C_2, b_2, c_2)
1974

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

    
1977
	
1978

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

    
1985
	
1986

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

    
1993
	
1994

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

    
2007

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

    
2012
tel
2013

    
2014

    
2015

    
2016

    
2017

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

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

    
2026

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

    
2030

    
2031
let
2032

    
2033

    
2034

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

    
2042
	
2043

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

    
2050
	
2051

    
2052
	(idC_C1_4) 
2053
	= 
2054
		 if ( idC_C1_1 = 1588) then 
2055
		(idC_C1_2)
2056
		 else
2057
		 if ( idC_C1_1 = 1589) then 
2058
		(idC_C1_3)
2059
		 else (idC_C1_1);
2060

    
2061

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

    
2066
	idC_C1_5 
2067
	= 0;
2068
	
2069

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

    
2074
tel
2075

    
2076

    
2077

    
2078

    
2079

    
2080

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

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

    
2097

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

    
2105

    
2106
let
2107

    
2108

    
2109

    
2110
	-- set state as active 
2111
	idParallel3_CD_2 
2112
	= 1583;
2113
	
2114

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

    
2122
	(idCD_C_3, idParallel3_CD_3, b_3, c_3, idC_C1_3) 
2123
	= 
2124

    
2125
	if ( idCD_C_1 = 0) then
2126

    
2127
	 (idCD_C_2, idParallel3_CD_2, b_2, c_2, idC_C1_2)
2128

    
2129
	 else(idCD_C_1, idParallel3_CD_2, b_1, c_1, idC_C1_1);
2130

    
2131
	
2132

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

    
2139
	
2140

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

    
2147
	
2148

    
2149
	(idCD_C_6, idParallel3_CD_4, b_6, c_6, idC_C1_5, idC_C2_3) 
2150
	= 
2151
		 if ( idCD_C_1 = 0) then 
2152
		(idCD_C_3, idParallel3_CD_3, b_3, c_3, idC_C1_3, idC_C2_1)
2153
		 else
2154
		 if ( idCD_C_1 = 1584) then 
2155
		(idCD_C_4, idParallel3_CD_3, b_4, c_4, idC_C1_1, idC_C2_2)
2156
		 else
2157
		 if ( idCD_C_1 = 1587) then 
2158
		(idCD_C_5, idParallel3_CD_3, b_5, c_5, idC_C1_4, idC_C2_1)
2159
		 else (idCD_C_1, idParallel3_CD_2, b_1, c_1, idC_C1_1, idC_C2_1);
2160

    
2161

    
2162
	(idCD_C, idParallel3_CD, b, c, idC_C1, idC_C2) 
2163
	= (idCD_C_6, idParallel3_CD_4, b_6, c_6, idC_C1_5, idC_C2_3);
2164
	
2165

    
2166
tel
2167

    
2168

    
2169

    
2170

    
2171

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

    
2179
returns (idC_C2:int;
2180
	idCD_C:int;
2181
	idC_C1:int;
2182
	idParallel3_CD:int);
2183

    
2184

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

    
2190

    
2191
let
2192

    
2193

    
2194

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

    
2202
	
2203

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

    
2210
	
2211

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

    
2221

    
2222
	-- set state as inactive 
2223
	idParallel3_CD_2
2224
	 = if (not isInner) then 0 else idParallel3_CD_1;
2225

    
2226
	idCD_C_5 
2227
	= 0;
2228
	
2229

    
2230
	(idC_C2, idCD_C, idC_C1, idParallel3_CD) 
2231
	= (idC_C2_3, idCD_C_5, idC_C1_3, idParallel3_CD_1);
2232
	
2233

    
2234
tel
2235

    
2236

    
2237

    
2238

    
2239

    
2240

    
2241
-- Entry action for state :Parallel3_CD
2242
node Parallel3_CD_en(idParallel3_CD_1:int;
2243
	idParallel3_Parallel3_1:int;
2244
	b_1:int;
2245
	c_1:int;
2246
	idCD_C_1:int;
2247
	idC_C1_1:int;
2248
	idC_C2_1:int;
2249
	dd_1:int;
2250
	idCD_D_1:int;
2251
	idD_D1_1:int;
2252
	idD_D2_1:int;
2253
	isInner:bool)
2254

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

    
2267

    
2268
var 	idParallel3_CD_2, idParallel3_CD_3:int;
2269
	idParallel3_Parallel3_2:int;
2270
	b_2:int;
2271
	c_2, c_3:int;
2272
	idCD_C_2:int;
2273
	idC_C1_2:int;
2274
	idC_C2_2:int;
2275
	dd_2:int;
2276
	idCD_D_2:int;
2277
	idD_D1_2:int;
2278
	idD_D2_2:int;
2279

    
2280

    
2281
let
2282

    
2283

    
2284

    
2285
	-- set state as active 
2286
	idParallel3_Parallel3_2 
2287
	= 1597;
2288
	
2289

    
2290
	
2291
	(idCD_C_2, idParallel3_CD_2, b_2, c_2, idC_C1_2, idC_C2_2) 
2292
	= CD_C_en(idCD_C_1, idParallel3_CD_1, b_1, c_1, idC_C1_1, idC_C2_1, false);
2293

    
2294
	(idCD_D_2, idParallel3_CD_3, c_3, dd_2, idD_D1_2, idD_D2_2) 
2295
	= CD_D_en(idCD_D_1, idParallel3_CD_2, c_2, dd_1, idD_D1_1, idD_D2_1, false);
2296

    
2297

    
2298
	(idParallel3_CD, idParallel3_Parallel3, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
2299
	= (idParallel3_CD_3, idParallel3_Parallel3_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);
2300
	
2301

    
2302
tel
2303

    
2304

    
2305

    
2306

    
2307

    
2308
-- Exit action for state :Parallel3_CD
2309
node Parallel3_CD_ex(idD_D2_1:int;
2310
	idCD_D_1:int;
2311
	idD_D1_1:int;
2312
	idParallel3_CD_1:int;
2313
	idCD_C_1:int;
2314
	idC_C1_1:int;
2315
	idC_C2_1:int;
2316
	idParallel3_Parallel3_1:int;
2317
	isInner:bool)
2318

    
2319
returns (idD_D2:int;
2320
	idCD_D:int;
2321
	idD_D1:int;
2322
	idParallel3_CD:int;
2323
	idCD_C:int;
2324
	idC_C1:int;
2325
	idC_C2:int;
2326
	idParallel3_Parallel3:int);
2327

    
2328

    
2329
var 	idD_D2_2:int;
2330
	idCD_D_2:int;
2331
	idD_D1_2:int;
2332
	idParallel3_CD_2, idParallel3_CD_3, idParallel3_CD_4:int;
2333
	idCD_C_2:int;
2334
	idC_C1_2:int;
2335
	idC_C2_2:int;
2336
	idParallel3_Parallel3_2:int;
2337

    
2338

    
2339
let
2340

    
2341

    
2342

    
2343
	
2344
	(idD_D2_2, idCD_D_2, idD_D1_2, idParallel3_CD_2) 
2345
	= CD_D_ex(idD_D2_1, idCD_D_1, idD_D1_1, idParallel3_CD_1, false);
2346

    
2347
	(idC_C2_2, idCD_C_2, idC_C1_2, idParallel3_CD_3) 
2348
	= CD_C_ex(idC_C2_1, idCD_C_1, idC_C1_1, idParallel3_CD_2, false);
2349

    
2350

    
2351
	-- set state as inactive 
2352
	idParallel3_Parallel3_2
2353
	 = if (not isInner) then 0 else idParallel3_Parallel3_1;
2354

    
2355
	idParallel3_CD_4 
2356
	= 0;
2357
	
2358

    
2359
	(idD_D2, idCD_D, idD_D1, idParallel3_CD, idCD_C, idC_C1, idC_C2, idParallel3_Parallel3) 
2360
	= (idD_D2_2, idCD_D_2, idD_D1_2, idParallel3_CD_4, idCD_C_2, idC_C1_2, idC_C2_2, idParallel3_Parallel3_1);
2361
	
2362

    
2363
tel
2364

    
2365

    
2366

    
2367

    
2368

    
2369

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

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

    
2379

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

    
2383

    
2384
let
2385

    
2386

    
2387

    
2388
	-- set state as active 
2389
	idA_A2_2 
2390
	= 1574;
2391
	
2392

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

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

    
2402
tel
2403

    
2404

    
2405

    
2406

    
2407

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

    
2412
returns (idA_A2:int);
2413

    
2414

    
2415
var 	idA_A2_2:int;
2416

    
2417

    
2418
let
2419

    
2420

    
2421

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

    
2426

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

    
2431
tel
2432

    
2433

    
2434

    
2435

    
2436

    
2437

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

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

    
2447

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

    
2451

    
2452
let
2453

    
2454

    
2455

    
2456
	-- set state as active 
2457
	idA_A2_2 
2458
	= 1575;
2459
	
2460

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

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

    
2470
tel
2471

    
2472

    
2473

    
2474

    
2475

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

    
2480
returns (idA_A2:int);
2481

    
2482

    
2483
var 	idA_A2_2:int;
2484

    
2485

    
2486
let
2487

    
2488

    
2489

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

    
2494

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

    
2499
tel
2500

    
2501

    
2502

    
2503

    
2504

    
2505

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

    
2513
returns (idA_A2:int;
2514
	idParallel3_A:int;
2515
	a:int);
2516

    
2517

    
2518
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int;
2519
	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4:int;
2520
	a_2, a_3, a_4, a_5, a_6:int;
2521

    
2522

    
2523
let
2524

    
2525

    
2526

    
2527
	-- set state as active 
2528
	idParallel3_A_2 
2529
	= 1573;
2530
	
2531

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

    
2539
	(idA_A2_3, idParallel3_A_3, a_3) 
2540
	= 
2541

    
2542
	if ( idA_A2_1 = 0) then
2543

    
2544
	 (idA_A2_2, idParallel3_A_2, a_2)
2545

    
2546
	 else(idA_A2_1, idParallel3_A_2, a_1);
2547

    
2548
	
2549

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

    
2556
	
2557

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

    
2564
	
2565

    
2566
	(idA_A2_6, idParallel3_A_4, a_6) 
2567
	= 
2568
		 if ( idA_A2_1 = 0) then 
2569
		(idA_A2_3, idParallel3_A_3, a_3)
2570
		 else
2571
		 if ( idA_A2_1 = 1574) then 
2572
		(idA_A2_4, idParallel3_A_3, a_4)
2573
		 else
2574
		 if ( idA_A2_1 = 1575) then 
2575
		(idA_A2_5, idParallel3_A_3, a_5)
2576
		 else (idA_A2_1, idParallel3_A_2, a_1);
2577

    
2578

    
2579
	(idA_A2, idParallel3_A, a) 
2580
	= (idA_A2_6, idParallel3_A_4, a_6);
2581
	
2582

    
2583
tel
2584

    
2585

    
2586

    
2587

    
2588

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

    
2594
returns (idA_A2:int;
2595
	idParallel3_A:int);
2596

    
2597

    
2598
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int;
2599
	idParallel3_A_2:int;
2600

    
2601

    
2602
let
2603

    
2604

    
2605

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

    
2613
	
2614

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

    
2621
	
2622

    
2623
	(idA_A2_4) 
2624
	= 
2625
		 if ( idA_A2_1 = 1574) then 
2626
		(idA_A2_2)
2627
		 else
2628
		 if ( idA_A2_1 = 1575) then 
2629
		(idA_A2_3)
2630
		 else (idA_A2_1);
2631

    
2632

    
2633
	-- set state as inactive 
2634
	idParallel3_A_2
2635
	 = if (not isInner) then 0 else idParallel3_A_1;
2636

    
2637
	idA_A2_5 
2638
	= 0;
2639
	
2640

    
2641
	(idA_A2, idParallel3_A) 
2642
	= (idA_A2_5, idParallel3_A_1);
2643
	
2644

    
2645
tel
2646

    
2647

    
2648

    
2649

    
2650

    
2651

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

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

    
2661

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

    
2665

    
2666
let
2667

    
2668

    
2669

    
2670
	-- set state as active 
2671
	idA_A1_2 
2672
	= 1571;
2673
	
2674

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

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

    
2684
tel
2685

    
2686

    
2687

    
2688

    
2689

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

    
2694
returns (idA_A1:int);
2695

    
2696

    
2697
var 	idA_A1_2:int;
2698

    
2699

    
2700
let
2701

    
2702

    
2703

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

    
2708

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

    
2713
tel
2714

    
2715

    
2716

    
2717

    
2718

    
2719

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

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

    
2729

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

    
2733

    
2734
let
2735

    
2736

    
2737

    
2738
	-- set state as active 
2739
	idA_A1_2 
2740
	= 1572;
2741
	
2742

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

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

    
2752
tel
2753

    
2754

    
2755

    
2756

    
2757

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

    
2762
returns (idA_A1:int);
2763

    
2764

    
2765
var 	idA_A1_2:int;
2766

    
2767

    
2768
let
2769

    
2770

    
2771

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

    
2776

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

    
2781
tel
2782

    
2783

    
2784

    
2785

    
2786

    
2787

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

    
2795
returns (idA_A1:int;
2796
	idParallel3_A:int;
2797
	a:int);
2798

    
2799

    
2800
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int;
2801
	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4:int;
2802
	a_2, a_3, a_4, a_5, a_6:int;
2803

    
2804

    
2805
let
2806

    
2807

    
2808

    
2809
	-- set state as active 
2810
	idParallel3_A_2 
2811
	= 1570;
2812
	
2813

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

    
2821
	(idA_A1_3, idParallel3_A_3, a_3) 
2822
	= 
2823

    
2824
	if ( idA_A1_1 = 0) then
2825

    
2826
	 (idA_A1_2, idParallel3_A_2, a_2)
2827

    
2828
	 else(idA_A1_1, idParallel3_A_2, a_1);
2829

    
2830
	
2831

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

    
2838
	
2839

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

    
2846
	
2847

    
2848
	(idA_A1_6, idParallel3_A_4, a_6) 
2849
	= 
2850
		 if ( idA_A1_1 = 0) then 
2851
		(idA_A1_3, idParallel3_A_3, a_3)
2852
		 else
2853
		 if ( idA_A1_1 = 1571) then 
2854
		(idA_A1_4, idParallel3_A_3, a_4)
2855
		 else
2856
		 if ( idA_A1_1 = 1572) then 
2857
		(idA_A1_5, idParallel3_A_3, a_5)
2858
		 else (idA_A1_1, idParallel3_A_2, a_1);
2859

    
2860

    
2861
	(idA_A1, idParallel3_A, a) 
2862
	= (idA_A1_6, idParallel3_A_4, a_6);
2863
	
2864

    
2865
tel
2866

    
2867

    
2868

    
2869

    
2870

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

    
2876
returns (idA_A1:int;
2877
	idParallel3_A:int);
2878

    
2879

    
2880
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2881
	idParallel3_A_2:int;
2882

    
2883

    
2884
let
2885

    
2886

    
2887

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

    
2895
	
2896

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

    
2903
	
2904

    
2905
	(idA_A1_4) 
2906
	= 
2907
		 if ( idA_A1_1 = 1571) then 
2908
		(idA_A1_2)
2909
		 else
2910
		 if ( idA_A1_1 = 1572) then 
2911
		(idA_A1_3)
2912
		 else (idA_A1_1);
2913

    
2914

    
2915
	-- set state as inactive 
2916
	idParallel3_A_2
2917
	 = if (not isInner) then 0 else idParallel3_A_1;
2918

    
2919
	idA_A1_5 
2920
	= 0;
2921
	
2922

    
2923
	(idA_A1, idParallel3_A) 
2924
	= (idA_A1_5, idParallel3_A_1);
2925
	
2926

    
2927
tel
2928

    
2929

    
2930

    
2931

    
2932

    
2933

    
2934
-- Entry action for state :Parallel3_A
2935
node Parallel3_A_en(idParallel3_A_1:int;
2936
	idParallel3_Parallel3_1:int;
2937
	a_1:int;
2938
	idA_A1_1:int;
2939
	x:int;
2940
	idA_A2_1:int;
2941
	isInner:bool)
2942

    
2943
returns (idParallel3_A:int;
2944
	idParallel3_Parallel3:int;
2945
	a:int;
2946
	idA_A1:int;
2947
	idA_A2:int);
2948

    
2949

    
2950
var 	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4, idParallel3_A_5, idParallel3_A_6:int;
2951
	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int;
2952
	a_2, a_3, a_4, a_5, a_6:int;
2953
	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2954
	idA_A2_2, idA_A2_3:int;
2955

    
2956

    
2957
let
2958

    
2959

    
2960

    
2961
	-- set state as active 
2962
	idParallel3_Parallel3_2 
2963
	= 1569;
2964
	
2965

    
2966
	
2967
-- transition trace :
2968
	--POINT__To__A_A1_1
2969
		(idA_A1_2, idParallel3_A_2, a_2) 
2970
	= A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false);
2971
		
2972

    
2973
	(idParallel3_A_3, idParallel3_Parallel3_3, a_3, idA_A1_3) 
2974
	= 
2975

    
2976
	if ( idParallel3_A_1 = 0) then
2977

    
2978
	 (idParallel3_A_2, idParallel3_Parallel3_2, a_2, idA_A1_2)
2979

    
2980
	 else(idParallel3_A_1, idParallel3_Parallel3_2, a_1, idA_A1_1);
2981

    
2982
	
2983

    
2984
	(idA_A2_2, idParallel3_A_4, a_4) 
2985
	= 
2986
	if ( idParallel3_A_1 = 1573) then
2987
	A_A2_en(idA_A2_1, idParallel3_A_1, a_1, x, false)
2988
	 else (idA_A2_1, idParallel3_A_1, a_1);
2989

    
2990
	
2991

    
2992
	(idA_A1_4, idParallel3_A_5, a_5) 
2993
	= 
2994
	if ( idParallel3_A_1 = 1570) then
2995
	A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false)
2996
	 else (idA_A1_1, idParallel3_A_1, a_1);
2997

    
2998
	
2999

    
3000
	(idParallel3_A_6, idParallel3_Parallel3_4, a_6, idA_A1_5, idA_A2_3) 
3001
	= 
3002
		 if ( idParallel3_A_1 = 0) then 
3003
		(idParallel3_A_3, idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_1)
3004
		 else
3005
		 if ( idParallel3_A_1 = 1573) then 
3006
		(idParallel3_A_4, idParallel3_Parallel3_3, a_4, idA_A1_1, idA_A2_2)
3007
		 else
3008
		 if ( idParallel3_A_1 = 1570) then 
3009
		(idParallel3_A_5, idParallel3_Parallel3_3, a_5, idA_A1_4, idA_A2_1)
3010
		 else (idParallel3_A_1, idParallel3_Parallel3_2, a_1, idA_A1_1, idA_A2_1);
3011

    
3012

    
3013
	(idParallel3_A, idParallel3_Parallel3, a, idA_A1, idA_A2) 
3014
	= (idParallel3_A_6, idParallel3_Parallel3_4, a_6, idA_A1_5, idA_A2_3);
3015
	
3016

    
3017
tel
3018

    
3019

    
3020

    
3021

    
3022

    
3023
-- Exit action for state :Parallel3_A
3024
node Parallel3_A_ex(idA_A2_1:int;
3025
	idParallel3_A_1:int;
3026
	idA_A1_1:int;
3027
	idParallel3_Parallel3_1:int;
3028
	isInner:bool)
3029

    
3030
returns (idA_A2:int;
3031
	idParallel3_A:int;
3032
	idA_A1:int;
3033
	idParallel3_Parallel3:int);
3034

    
3035

    
3036
var 	idA_A2_2, idA_A2_3:int;
3037
	idParallel3_A_2, idParallel3_A_3, idParallel3_A_4, idParallel3_A_5:int;
3038
	idA_A1_2, idA_A1_3:int;
3039
	idParallel3_Parallel3_2:int;
3040

    
3041

    
3042
let
3043

    
3044

    
3045

    
3046
	
3047
	(idA_A2_2, idParallel3_A_2) 
3048
	= 
3049
	if ( idParallel3_A_1 = 1573) then
3050
	A_A2_ex(idA_A2_1, idParallel3_A_1, false)
3051
	 else (idA_A2_1, idParallel3_A_1);
3052

    
3053
	
3054

    
3055
	(idA_A1_2, idParallel3_A_3) 
3056
	= 
3057
	if ( idParallel3_A_1 = 1570) then
3058
	A_A1_ex(idA_A1_1, idParallel3_A_1, false)
3059
	 else (idA_A1_1, idParallel3_A_1);
3060

    
3061
	
3062

    
3063
	(idA_A2_3, idParallel3_A_4, idA_A1_3) 
3064
	= 
3065
		 if ( idParallel3_A_1 = 1573) then 
3066
		(idA_A2_2, idParallel3_A_2, idA_A1_1)
3067
		 else
3068
		 if ( idParallel3_A_1 = 1570) then 
3069
		(idA_A2_1, idParallel3_A_3, idA_A1_2)
3070
		 else (idA_A2_1, idParallel3_A_1, idA_A1_1);
3071

    
3072

    
3073
	-- set state as inactive 
3074
	idParallel3_Parallel3_2
3075
	 = if (not isInner) then 0 else idParallel3_Parallel3_1;
3076

    
3077
	idParallel3_A_5 
3078
	= 0;
3079
	
3080

    
3081
	(idA_A2, idParallel3_A, idA_A1, idParallel3_Parallel3) 
3082
	= (idA_A2_3, idParallel3_A_5, idA_A1_3, idParallel3_Parallel3_1);
3083
	
3084

    
3085
tel
3086

    
3087

    
3088
--***************************************************State :B_B2 Automaton***************************************************
3089

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

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

    
3100

    
3101
let
3102

    
3103
	 automaton b_b2
3104

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

    
3108

    
3109

    
3110
	unless (idB_B2_1=1578) and S restart B2_B2A__TO__B2_B2B_1
3111

    
3112

    
3113

    
3114
	unless (idB_B2_1=1579) and R restart B2_B2B__TO__B2_B2A_1
3115

    
3116

    
3117

    
3118
	unless (idB_B2_1=1578) restart B2_B2A_IDL
3119

    
3120
	unless (idB_B2_1=1579) restart B2_B2B_IDL
3121

    
3122
	let
3123

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

    
3128
	tel
3129

    
3130

    
3131

    
3132
	state POINT__TO__B2_B2A_1:
3133

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

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

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

    
3148

    
3149
	tel
3150

    
3151
	until true restart POINTB_B2
3152

    
3153

    
3154

    
3155
	state B2_B2A__TO__B2_B2B_1:
3156

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

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

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

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

    
3175

    
3176
	tel
3177

    
3178
	until true restart POINTB_B2
3179

    
3180

    
3181

    
3182
	state B2_B2B__TO__B2_B2A_1:
3183

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

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

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

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

    
3202

    
3203
	tel
3204

    
3205
	until true restart POINTB_B2
3206

    
3207

    
3208

    
3209
	state B2_B2A_IDL:
3210

    
3211
	 	let
3212

    
3213
		
3214

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

    
3219
	tel
3220

    
3221
	until true restart POINTB_B2
3222

    
3223

    
3224

    
3225
	state B2_B2B_IDL:
3226

    
3227
	 	let
3228

    
3229
		
3230

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

    
3235
	tel
3236

    
3237
	until true restart POINTB_B2
3238

    
3239

    
3240

    
3241
tel
3242

    
3243

    
3244
--***************************************************State :B_B1 Automaton***************************************************
3245

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

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

    
3256

    
3257
let
3258

    
3259
	 automaton b_b1
3260

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

    
3264

    
3265

    
3266
	unless (idB_B1_1=1581) and S restart B1_B1A__TO__B1_B1B_1
3267

    
3268

    
3269

    
3270
	unless (idB_B1_1=1582) and R restart B1_B1B__TO__B1_B1A_1
3271

    
3272

    
3273

    
3274
	unless (idB_B1_1=1581) restart B1_B1A_IDL
3275

    
3276
	unless (idB_B1_1=1582) restart B1_B1B_IDL
3277

    
3278
	let
3279

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

    
3284
	tel
3285

    
3286

    
3287

    
3288
	state POINT__TO__B1_B1A_1:
3289

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

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

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

    
3304

    
3305
	tel
3306

    
3307
	until true restart POINTB_B1
3308

    
3309

    
3310

    
3311
	state B1_B1A__TO__B1_B1B_1:
3312

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

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

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

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

    
3331

    
3332
	tel
3333

    
3334
	until true restart POINTB_B1
3335

    
3336

    
3337

    
3338
	state B1_B1B__TO__B1_B1A_1:
3339

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

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

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

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

    
3358

    
3359
	tel
3360

    
3361
	until true restart POINTB_B1
3362

    
3363

    
3364

    
3365
	state B1_B1A_IDL:
3366

    
3367
	 	let
3368

    
3369
		
3370

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

    
3375
	tel
3376

    
3377
	until true restart POINTB_B1
3378

    
3379

    
3380

    
3381
	state B1_B1B_IDL:
3382

    
3383
	 	let
3384

    
3385
		
3386

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

    
3391
	tel
3392

    
3393
	until true restart POINTB_B1
3394

    
3395

    
3396

    
3397
tel
3398

    
3399

    
3400
--***************************************************State :Parallel3_B Automaton***************************************************
3401

    
3402
node Parallel3_B_node(idParallel3_B_1:int;
3403
	a_1:int;
3404
	b_1:int;
3405
	idB_B1_1:int;
3406
	T:bool;
3407
	idB_B2_1:int;
3408
	R:bool;
3409
	S:bool)
3410

    
3411
returns (idParallel3_B:int;
3412
	a:int;
3413
	b:int;
3414
	idB_B1:int;
3415
	idB_B2:int);
3416

    
3417

    
3418
let
3419

    
3420
	 automaton parallel3_b
3421

    
3422
	state POINTParallel3_B:
3423
	unless (idParallel3_B_1=0) restart POINT__TO__B_B1_1
3424

    
3425

    
3426

    
3427
	unless (idParallel3_B_1=1577) and T restart B_B2__TO__B_B1_1
3428

    
3429

    
3430

    
3431
	unless (idParallel3_B_1=1580) and T restart B_B1__TO__B_B2_1
3432

    
3433

    
3434

    
3435
	unless (idParallel3_B_1=1577) restart B_B2_IDL
3436

    
3437
	unless (idParallel3_B_1=1580) restart B_B1_IDL
3438

    
3439
	let
3440

    
3441
		(idParallel3_B, a, b, idB_B1, idB_B2) 
3442
	= (idParallel3_B_1, a_1, b_1, idB_B1_1, idB_B2_1);
3443
	
3444

    
3445
	tel
3446

    
3447

    
3448

    
3449
	state POINT__TO__B_B1_1:
3450

    
3451
	 var 	idParallel3_B_2:int;
3452
	a_2:int;
3453
	b_2:int;
3454
	idB_B1_2:int;
3455
	let
3456

    
3457
		-- transition trace :
3458
	--POINT__To__B_B1_1
3459
		(idB_B1_2, idParallel3_B_2, a_2, b_2) 
3460
	= B_B1_en(idB_B1_1, idParallel3_B_1, a_1, b_1, false);
3461
		
3462

    
3463
	(idParallel3_B, a, b, idB_B1) 
3464
	=  (idParallel3_B_2, a_2, b_2, idB_B1_2);
3465

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

    
3471
	tel
3472

    
3473
	until true restart POINTParallel3_B
3474

    
3475

    
3476

    
3477
	state B_B2__TO__B_B1_1:
3478

    
3479
	 var 	idParallel3_B_2, idParallel3_B_3:int;
3480
	a_2:int;
3481
	b_2:int;
3482
	idB_B1_2:int;
3483
	idB_B2_2:int;
3484
	let
3485

    
3486
		-- transition trace :
3487
	--B_B2__To__B_B1_1
3488
		(idB_B2_2, idParallel3_B_2) 
3489
	= B_B2_ex(idB_B2_1, idParallel3_B_1, false);
3490
		
3491

    
3492
		(idB_B1_2, idParallel3_B_3, a_2, b_2) 
3493
	= B_B1_en(idB_B1_1, idParallel3_B_2, a_1, b_1, false);
3494
		
3495

    
3496
	(idParallel3_B, a, b, idB_B1, idB_B2) 
3497
	=  (idParallel3_B_3, a_2, b_2, idB_B1_2, idB_B2_2);
3498

    
3499

    
3500
	tel
3501

    
3502
	until true restart POINTParallel3_B
3503

    
3504

    
3505

    
3506
	state B_B1__TO__B_B2_1:
3507

    
3508
	 var 	idParallel3_B_2, idParallel3_B_3:int;
3509
	a_2:int;
3510
	b_2:int;
3511
	idB_B1_2:int;
3512
	idB_B2_2:int;
3513
	let
3514

    
3515
		-- transition trace :
3516
	--B_B1__To__B_B2_1
3517
		(idB_B1_2, idParallel3_B_2) 
3518
	= B_B1_ex(idB_B1_1, idParallel3_B_1, false);
3519
		
3520

    
3521
		(idB_B2_2, idParallel3_B_3, a_2, b_2) 
3522
	= B_B2_en(idB_B2_1, idParallel3_B_2, a_1, b_1, false);
3523
		
3524

    
3525
	(idParallel3_B, a, b, idB_B1, idB_B2) 
3526
	=  (idParallel3_B_3, a_2, b_2, idB_B1_2, idB_B2_2);
3527

    
3528

    
3529
	tel
3530

    
3531
	until true restart POINTParallel3_B
3532

    
3533

    
3534

    
3535
	state B_B2_IDL:
3536

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

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

    
3546
		
3547

    
3548

    
3549
	(idParallel3_B, a, b, idB_B1, idB_B2) 
3550
	= (idParallel3_B_1, a_2, b_2, idB_B1_1, idB_B2_2);
3551
	
3552

    
3553
	tel
3554

    
3555
	until true restart POINTParallel3_B
3556

    
3557

    
3558

    
3559
	state B_B1_IDL:
3560

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

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

    
3570
		
3571

    
3572

    
3573
	(idParallel3_B, a, b, idB_B1, idB_B2) 
3574
	= (idParallel3_B_1, a_2, b_2, idB_B1_2, idB_B2_1);
3575
	
3576

    
3577
	tel
3578

    
3579
	until true restart POINTParallel3_B
3580

    
3581

    
3582

    
3583
tel
3584

    
3585

    
3586
--***************************************************State :D_D2 Automaton***************************************************
3587

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

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

    
3598

    
3599
let
3600

    
3601
	 automaton d_d2
3602

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

    
3606

    
3607

    
3608
	unless (idD_D2_1=1592) and S restart D2_D2A__TO__D2_D2B_1
3609

    
3610

    
3611

    
3612
	unless (idD_D2_1=1593) and R restart D2_D2B__TO__D2_D2A_1
3613

    
3614

    
3615

    
3616
	unless (idD_D2_1=1592) restart D2_D2A_IDL
3617

    
3618
	unless (idD_D2_1=1593) restart D2_D2B_IDL
3619

    
3620
	let
3621

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

    
3626
	tel
3627

    
3628

    
3629

    
3630
	state POINT__TO__D2_D2A_1:
3631

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

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

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

    
3646

    
3647
	tel
3648

    
3649
	until true restart POINTD_D2
3650

    
3651

    
3652

    
3653
	state D2_D2A__TO__D2_D2B_1:
3654

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

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

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

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

    
3673

    
3674
	tel
3675

    
3676
	until true restart POINTD_D2
3677

    
3678

    
3679

    
3680
	state D2_D2B__TO__D2_D2A_1:
3681

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

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

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

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

    
3700

    
3701
	tel
3702

    
3703
	until true restart POINTD_D2
3704

    
3705

    
3706

    
3707
	state D2_D2A_IDL:
3708

    
3709
	 	let
3710

    
3711
		
3712

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

    
3717
	tel
3718

    
3719
	until true restart POINTD_D2
3720

    
3721

    
3722

    
3723
	state D2_D2B_IDL:
3724

    
3725
	 	let
3726

    
3727
		
3728

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

    
3733
	tel
3734

    
3735
	until true restart POINTD_D2
3736

    
3737

    
3738

    
3739
tel
3740

    
3741

    
3742
--***************************************************State :D_D1 Automaton***************************************************
3743

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

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

    
3754

    
3755
let
3756

    
3757
	 automaton d_d1
3758

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

    
3762

    
3763

    
3764
	unless (idD_D1_1=1595) and S restart D1_D1A__TO__D1_D1B_1
3765

    
3766

    
3767

    
3768
	unless (idD_D1_1=1596) and R restart D1_D1B__TO__D1_D1A_1
3769

    
3770

    
3771

    
3772
	unless (idD_D1_1=1595) restart D1_D1A_IDL
3773

    
3774
	unless (idD_D1_1=1596) restart D1_D1B_IDL
3775

    
3776
	let
3777

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

    
3782
	tel
3783

    
3784

    
3785

    
3786
	state POINT__TO__D1_D1A_1:
3787

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

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

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

    
3802

    
3803
	tel
3804

    
3805
	until true restart POINTD_D1
3806

    
3807

    
3808

    
3809
	state D1_D1A__TO__D1_D1B_1:
3810

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

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

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

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

    
3829

    
3830
	tel
3831

    
3832
	until true restart POINTD_D1
3833

    
3834

    
3835

    
3836
	state D1_D1B__TO__D1_D1A_1:
3837

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

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

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

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

    
3856

    
3857
	tel
3858

    
3859
	until true restart POINTD_D1
3860

    
3861

    
3862

    
3863
	state D1_D1A_IDL:
3864

    
3865
	 	let
3866

    
3867
		
3868

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

    
3873
	tel
3874

    
3875
	until true restart POINTD_D1
3876

    
3877

    
3878

    
3879
	state D1_D1B_IDL:
3880

    
3881
	 	let
3882

    
3883
		
3884

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

    
3889
	tel
3890

    
3891
	until true restart POINTD_D1
3892

    
3893

    
3894

    
3895
tel
3896

    
3897

    
3898
--***************************************************State :CD_D Automaton***************************************************
3899

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

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

    
3915

    
3916
let
3917

    
3918
	 automaton cd_d
3919

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

    
3923

    
3924

    
3925
	unless (idCD_D_1=1591) and T restart D_D2__TO__D_D1_1
3926

    
3927

    
3928

    
3929
	unless (idCD_D_1=1594) and T restart D_D1__TO__D_D2_1
3930

    
3931

    
3932

    
3933
	unless (idCD_D_1=1591) restart D_D2_IDL
3934

    
3935
	unless (idCD_D_1=1594) restart D_D1_IDL
3936

    
3937
	let
3938

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

    
3943
	tel
3944

    
3945

    
3946

    
3947
	state POINT__TO__D_D1_1:
3948

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

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

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

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

    
3969
	tel
3970

    
3971
	until true restart POINTCD_D
3972

    
3973

    
3974

    
3975
	state D_D2__TO__D_D1_1:
3976

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

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

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

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

    
3997

    
3998
	tel
3999

    
4000
	until true restart POINTCD_D
4001

    
4002

    
4003

    
4004
	state D_D1__TO__D_D2_1:
4005

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

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

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

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

    
4026

    
4027
	tel
4028

    
4029
	until true restart POINTCD_D
4030

    
4031

    
4032

    
4033
	state D_D2_IDL:
4034

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

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

    
4044
		
4045

    
4046

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

    
4051
	tel
4052

    
4053
	until true restart POINTCD_D
4054

    
4055

    
4056

    
4057
	state D_D1_IDL:
4058

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

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

    
4068
		
4069

    
4070

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

    
4075
	tel
4076

    
4077
	until true restart POINTCD_D
4078

    
4079

    
4080

    
4081
tel
4082

    
4083

    
4084
--***************************************************State :C_C2 Automaton***************************************************
4085

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

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

    
4096

    
4097
let
4098

    
4099
	 automaton c_c2
4100

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

    
4104

    
4105

    
4106
	unless (idC_C2_1=1585) and S restart C2_C2A__TO__C2_C2B_1
4107

    
4108

    
4109

    
4110
	unless (idC_C2_1=1586) and R restart C2_C2B__TO__C2_C2A_1
4111

    
4112

    
4113

    
4114
	unless (idC_C2_1=1585) restart C2_C2A_IDL
4115

    
4116
	unless (idC_C2_1=1586) restart C2_C2B_IDL
4117

    
4118
	let
4119

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

    
4124
	tel
4125

    
4126

    
4127

    
4128
	state POINT__TO__C2_C2A_1:
4129

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

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

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

    
4144

    
4145
	tel
4146

    
4147
	until true restart POINTC_C2
4148

    
4149

    
4150

    
4151
	state C2_C2A__TO__C2_C2B_1:
4152

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

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

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

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

    
4171

    
4172
	tel
4173

    
4174
	until true restart POINTC_C2
4175

    
4176

    
4177

    
4178
	state C2_C2B__TO__C2_C2A_1:
4179

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

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

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

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

    
4198

    
4199
	tel
4200

    
4201
	until true restart POINTC_C2
4202

    
4203

    
4204

    
4205
	state C2_C2A_IDL:
4206

    
4207
	 	let
4208

    
4209
		
4210

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

    
4215
	tel
4216

    
4217
	until true restart POINTC_C2
4218

    
4219

    
4220

    
4221
	state C2_C2B_IDL:
4222

    
4223
	 	let
4224

    
4225
		
4226

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

    
4231
	tel
4232

    
4233
	until true restart POINTC_C2
4234

    
4235

    
4236

    
4237
tel
4238

    
4239

    
4240
--***************************************************State :C_C1 Automaton***************************************************
4241

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

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

    
4252

    
4253
let
4254

    
4255
	 automaton c_c1
4256

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

    
4260

    
4261

    
4262
	unless (idC_C1_1=1588) and S restart C1_C1A__TO__C1_C1B_1
4263

    
4264

    
4265

    
4266
	unless (idC_C1_1=1589) and R restart C1_C1B__TO__C1_C1A_1
4267

    
4268

    
4269

    
4270
	unless (idC_C1_1=1588) restart C1_C1A_IDL
4271

    
4272
	unless (idC_C1_1=1589) restart C1_C1B_IDL
4273

    
4274
	let
4275

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

    
4280
	tel
4281

    
4282

    
4283

    
4284
	state POINT__TO__C1_C1A_1:
4285

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

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

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

    
4300

    
4301
	tel
4302

    
4303
	until true restart POINTC_C1
4304

    
4305

    
4306

    
4307
	state C1_C1A__TO__C1_C1B_1:
4308

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

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

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

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

    
4327

    
4328
	tel
4329

    
4330
	until true restart POINTC_C1
4331

    
4332

    
4333

    
4334
	state C1_C1B__TO__C1_C1A_1:
4335

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

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

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

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

    
4354

    
4355
	tel
4356

    
4357
	until true restart POINTC_C1
4358

    
4359

    
4360

    
4361
	state C1_C1A_IDL:
4362

    
4363
	 	let
4364

    
4365
		
4366

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

    
4371
	tel
4372

    
4373
	until true restart POINTC_C1
4374

    
4375

    
4376

    
4377
	state C1_C1B_IDL:
4378

    
4379
	 	let
4380

    
4381
		
4382

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

    
4387
	tel
4388

    
4389
	until true restart POINTC_C1
4390

    
4391

    
4392

    
4393
tel
4394

    
4395

    
4396
--***************************************************State :CD_C Automaton***************************************************
4397

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

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

    
4413

    
4414
let
4415

    
4416
	 automaton cd_c
4417

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

    
4421

    
4422

    
4423
	unless (idCD_C_1=1584) and T restart C_C2__TO__C_C1_1
4424

    
4425

    
4426

    
4427
	unless (idCD_C_1=1587) and T restart C_C1__TO__C_C2_1
4428

    
4429

    
4430

    
4431
	unless (idCD_C_1=1584) restart C_C2_IDL
4432

    
4433
	unless (idCD_C_1=1587) restart C_C1_IDL
4434

    
4435
	let
4436

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

    
4441
	tel
4442

    
4443

    
4444

    
4445
	state POINT__TO__C_C1_1:
4446

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

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

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

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

    
4467
	tel
4468

    
4469
	until true restart POINTCD_C
4470

    
4471

    
4472

    
4473
	state C_C2__TO__C_C1_1:
4474

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

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

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

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

    
4495

    
4496
	tel
4497

    
4498
	until true restart POINTCD_C
4499

    
4500

    
4501

    
4502
	state C_C1__TO__C_C2_1:
4503

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

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

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

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

    
4524

    
4525
	tel
4526

    
4527
	until true restart POINTCD_C
4528

    
4529

    
4530

    
4531
	state C_C2_IDL:
4532

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

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

    
4542
		
4543

    
4544

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

    
4549
	tel
4550

    
4551
	until true restart POINTCD_C
4552

    
4553

    
4554

    
4555
	state C_C1_IDL:
4556

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

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

    
4566
		
4567

    
4568

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

    
4573
	tel
4574

    
4575
	until true restart POINTCD_C
4576

    
4577

    
4578

    
4579
tel
4580

    
4581

    
4582
--***************************************************State :Parallel3_CD Automaton***************************************************
4583

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

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

    
4609

    
4610
let
4611

    
4612
	 automaton parallel3_cd
4613

    
4614
	state POINTParallel3_CD:
4615
	unless (idParallel3_CD_1=0) restart PARALLEL3_CD_PARALLEL_ENTRY
4616
	unless true  restart PARALLEL3_CD_PARALLEL_IDL
4617

    
4618
	let
4619

    
4620
		(idParallel3_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4621
	= (idParallel3_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);
4622
	
4623

    
4624
	tel
4625

    
4626

    
4627

    
4628
	state PARALLEL3_CD_PARALLEL_ENTRY:
4629

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

    
4642
		
4643
	(idCD_C_2, idParallel3_CD_2, b_2, c_2, idC_C1_2, idC_C2_2) 
4644
	= CD_C_en(idCD_C_1, idParallel3_CD_1, b_1, c_1, idC_C1_1, idC_C2_1, false);
4645

    
4646
	(idCD_D_2, idParallel3_CD_3, c_3, dd_2, idD_D1_2, idD_D2_2) 
4647
	= CD_D_en(idCD_D_1, idParallel3_CD_2, c_2, dd_1, idD_D1_1, idD_D2_1, false);
4648

    
4649

    
4650
	(idParallel3_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4651
	= (idParallel3_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);
4652
	
4653

    
4654
	tel
4655

    
4656
	until true restart POINTParallel3_CD
4657

    
4658

    
4659

    
4660
	state PARALLEL3_CD_PARALLEL_IDL:
4661

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

    
4673
		
4674

    
4675
		(idCD_C_2, b_2, c_2, idC_C1_2, idC_C2_2)
4676
	= 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)
4677

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

    
4680
		
4681

    
4682
		
4683

    
4684
		(idCD_D_2, c_3, dd_2, idD_D1_2, idD_D2_2)
4685
	= 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)
4686

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

    
4689
		
4690

    
4691
		
4692

    
4693
	(idParallel3_CD, b, c, idCD_C, idC_C1, idC_C2, dd, idCD_D, idD_D1, idD_D2) 
4694
	= (idParallel3_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);
4695
	
4696

    
4697
	tel
4698

    
4699
	until true restart POINTParallel3_CD
4700

    
4701

    
4702

    
4703
tel
4704

    
4705

    
4706
--***************************************************State :A_A2 Automaton***************************************************
4707

    
4708
node A_A2_node(idA_A2_1:int;
4709
	a_1:int;
4710
	x:int;
4711
	S:bool;
4712
	R:bool)
4713

    
4714
returns (idA_A2:int;
4715
	a:int);
4716

    
4717

    
4718
let
4719

    
4720
	 automaton a_a2
4721

    
4722
	state POINTA_A2:
4723
	unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1
4724

    
4725

    
4726

    
4727
	unless (idA_A2_1=1574) and S restart A2_A2A__TO__A2_A2B_1
4728

    
4729

    
4730

    
4731
	unless (idA_A2_1=1575) and R restart A2_A2B__TO__A2_A2A_1
4732

    
4733

    
4734

    
4735
	unless (idA_A2_1=1574) restart A2_A2A_IDL
4736

    
4737
	unless (idA_A2_1=1575) restart A2_A2B_IDL
4738

    
4739
	let
4740

    
4741
		(idA_A2, a) 
4742
	= (idA_A2_1, a_1);
4743
	
4744

    
4745
	tel
4746

    
4747

    
4748

    
4749
	state POINT__TO__A2_A2A_1:
4750

    
4751
	 var 	idA_A2_2:int;
4752
	a_2:int;
4753
	let
4754

    
4755
		-- transition trace :
4756
	--POINT__To__A2_A2a_1
4757
		(idA_A2_2, a_2) 
4758
	= A2_A2a_en(idA_A2_1, x, a_1, false);
4759
		
4760

    
4761
	(idA_A2, a) 
4762
	=  (idA_A2_2, a_2);
4763

    
4764

    
4765
	tel
4766

    
4767
	until true restart POINTA_A2
4768

    
4769

    
4770

    
4771
	state A2_A2A__TO__A2_A2B_1:
4772

    
4773
	 var 	idA_A2_2, idA_A2_3:int;
4774
	a_2:int;
4775
	let
4776

    
4777
		-- transition trace :
4778
	--A2_A2a__To__A2_A2b_1
4779
		(idA_A2_2) 
4780
	= A2_A2a_ex(idA_A2_1, false);
4781
		
4782

    
4783
		(idA_A2_3, a_2) 
4784
	= A2_A2b_en(idA_A2_2, x, a_1, false);
4785
		
4786

    
4787
	(idA_A2, a) 
4788
	=  (idA_A2_3, a_2);
4789

    
4790

    
4791
	tel
4792

    
4793
	until true restart POINTA_A2
4794

    
4795

    
4796

    
4797
	state A2_A2B__TO__A2_A2A_1:
4798

    
4799
	 var 	idA_A2_2, idA_A2_3:int;
4800
	a_2:int;
4801
	let
4802

    
4803
		-- transition trace :
4804
	--A2_A2b__To__A2_A2a_1
4805
		(idA_A2_2) 
4806
	= A2_A2b_ex(idA_A2_1, false);
4807
		
4808

    
4809
		(idA_A2_3, a_2) 
4810
	= A2_A2a_en(idA_A2_2, x, a_1, false);
4811
		
4812

    
4813
	(idA_A2, a) 
4814
	=  (idA_A2_3, a_2);
4815

    
4816

    
4817
	tel
4818

    
4819
	until true restart POINTA_A2
4820

    
4821

    
4822

    
4823
	state A2_A2A_IDL:
4824

    
4825
	 	let
4826

    
4827
		
4828

    
4829
	(idA_A2, a) 
4830
	= (idA_A2_1, a_1);
4831
	
4832

    
4833
	tel
4834

    
4835
	until true restart POINTA_A2
4836

    
4837

    
4838

    
4839
	state A2_A2B_IDL:
4840

    
4841
	 	let
4842

    
4843
		
4844

    
4845
	(idA_A2, a) 
4846
	= (idA_A2_1, a_1);
4847
	
4848

    
4849
	tel
4850

    
4851
	until true restart POINTA_A2
4852

    
4853

    
4854

    
4855
tel
4856

    
4857

    
4858
--***************************************************State :A_A1 Automaton***************************************************
4859

    
4860
node A_A1_node(idA_A1_1:int;
4861
	a_1:int;
4862
	x:int;
4863
	S:bool;
4864
	R:bool)
4865

    
4866
returns (idA_A1:int;
4867
	a:int);
4868

    
4869

    
4870
let
4871

    
4872
	 automaton a_a1
4873

    
4874
	state POINTA_A1:
4875
	unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1
4876

    
4877

    
4878

    
4879
	unless (idA_A1_1=1571) and S restart A1_A1A__TO__A1_A1B_1
4880

    
4881

    
4882

    
4883
	unless (idA_A1_1=1572) and R restart A1_A1B__TO__A1_A1A_1
4884

    
4885

    
4886

    
4887
	unless (idA_A1_1=1571) restart A1_A1A_IDL
4888

    
4889
	unless (idA_A1_1=1572) restart A1_A1B_IDL
4890

    
4891
	let
4892

    
4893
		(idA_A1, a) 
4894
	= (idA_A1_1, a_1);
4895
	
4896

    
4897
	tel
4898

    
4899

    
4900

    
4901
	state POINT__TO__A1_A1A_1:
4902

    
4903
	 var 	idA_A1_2:int;
4904
	a_2:int;
4905
	let
4906

    
4907
		-- transition trace :
4908
	--POINT__To__A1_A1a_1
4909
		(idA_A1_2, a_2) 
4910
	= A1_A1a_en(idA_A1_1, x, a_1, false);
4911
		
4912

    
4913
	(idA_A1, a) 
4914
	=  (idA_A1_2, a_2);
4915

    
4916

    
4917
	tel
4918

    
4919
	until true restart POINTA_A1
4920

    
4921

    
4922

    
4923
	state A1_A1A__TO__A1_A1B_1:
4924

    
4925
	 var 	idA_A1_2, idA_A1_3:int;
4926
	a_2:int;
4927
	let
4928

    
4929
		-- transition trace :
4930
	--A1_A1a__To__A1_A1b_1
4931
		(idA_A1_2) 
4932
	= A1_A1a_ex(idA_A1_1, false);
4933
		
4934

    
4935
		(idA_A1_3, a_2) 
4936
	= A1_A1b_en(idA_A1_2, x, a_1, false);
4937
		
4938

    
4939
	(idA_A1, a) 
4940
	=  (idA_A1_3, a_2);
4941

    
4942

    
4943
	tel
4944

    
4945
	until true restart POINTA_A1
4946

    
4947

    
4948

    
4949
	state A1_A1B__TO__A1_A1A_1:
4950

    
4951
	 var 	idA_A1_2, idA_A1_3:int;
4952
	a_2:int;
4953
	let
4954

    
4955
		-- transition trace :
4956
	--A1_A1b__To__A1_A1a_1
4957
		(idA_A1_2) 
4958
	= A1_A1b_ex(idA_A1_1, false);
4959
		
4960

    
4961
		(idA_A1_3, a_2) 
4962
	= A1_A1a_en(idA_A1_2, x, a_1, false);
4963
		
4964

    
4965
	(idA_A1, a) 
4966
	=  (idA_A1_3, a_2);
4967

    
4968

    
4969
	tel
4970

    
4971
	until true restart POINTA_A1
4972

    
4973

    
4974

    
4975
	state A1_A1A_IDL:
4976

    
4977
	 	let
4978

    
4979
		
4980

    
4981
	(idA_A1, a) 
4982
	= (idA_A1_1, a_1);
4983
	
4984

    
4985
	tel
4986

    
4987
	until true restart POINTA_A1
4988

    
4989

    
4990

    
4991
	state A1_A1B_IDL:
4992

    
4993
	 	let
4994

    
4995
		
4996

    
4997
	(idA_A1, a) 
4998
	= (idA_A1_1, a_1);
4999
	
5000

    
5001
	tel
5002

    
5003
	until true restart POINTA_A1
5004

    
5005

    
5006

    
5007
tel
5008

    
5009

    
5010
--***************************************************State :Parallel3_A Automaton***************************************************
5011

    
5012
node Parallel3_A_node(idParallel3_A_1:int;
5013
	a_1:int;
5014
	idA_A1_1:int;
5015
	x:int;
5016
	T:bool;
5017
	idA_A2_1:int;
5018
	R:bool;
5019
	S:bool)
5020

    
5021
returns (idParallel3_A:int;
5022
	a:int;
5023
	idA_A1:int;
5024
	idA_A2:int);
5025

    
5026

    
5027
let
5028

    
5029
	 automaton parallel3_a
5030

    
5031
	state POINTParallel3_A:
5032
	unless (idParallel3_A_1=0) restart POINT__TO__A_A1_1
5033

    
5034

    
5035

    
5036
	unless (idParallel3_A_1=1573) and T restart A_A2__TO__A_A1_1
5037

    
5038

    
5039

    
5040
	unless (idParallel3_A_1=1570) and T restart A_A1__TO__A_A2_1
5041

    
5042

    
5043

    
5044
	unless (idParallel3_A_1=1573) restart A_A2_IDL
5045

    
5046
	unless (idParallel3_A_1=1570) restart A_A1_IDL
5047

    
5048
	let
5049

    
5050
		(idParallel3_A, a, idA_A1, idA_A2) 
5051
	= (idParallel3_A_1, a_1, idA_A1_1, idA_A2_1);
5052
	
5053

    
5054
	tel
5055

    
5056

    
5057

    
5058
	state POINT__TO__A_A1_1:
5059

    
5060
	 var 	idParallel3_A_2:int;
5061
	a_2:int;
5062
	idA_A1_2:int;
5063
	let
5064

    
5065
		-- transition trace :
5066
	--POINT__To__A_A1_1
5067
		(idA_A1_2, idParallel3_A_2, a_2) 
5068
	= A_A1_en(idA_A1_1, idParallel3_A_1, a_1, x, false);
5069
		
5070

    
5071
	(idParallel3_A, a, idA_A1) 
5072
	=  (idParallel3_A_2, a_2, idA_A1_2);
5073

    
5074
	--add unused variables
5075
	(idA_A2) 
5076
	= (idA_A2_1);
5077
	
5078

    
5079
	tel
5080

    
5081
	until true restart POINTParallel3_A
5082

    
5083

    
5084

    
5085
	state A_A2__TO__A_A1_1:
5086

    
5087
	 var 	idParallel3_A_2, idParallel3_A_3:int;
5088
	a_2:int;
5089
	idA_A1_2:int;
5090
	idA_A2_2:int;
5091
	let
5092

    
5093
		-- transition trace :
5094
	--A_A2__To__A_A1_1
5095
		(idA_A2_2, idParallel3_A_2) 
5096
	= A_A2_ex(idA_A2_1, idParallel3_A_1, false);
5097
		
5098

    
5099
		(idA_A1_2, idParallel3_A_3, a_2) 
5100
	= A_A1_en(idA_A1_1, idParallel3_A_2, a_1, x, false);
5101
		
5102

    
5103
	(idParallel3_A, a, idA_A1, idA_A2) 
5104
	=  (idParallel3_A_3, a_2, idA_A1_2, idA_A2_2);
5105

    
5106

    
5107
	tel
5108

    
5109
	until true restart POINTParallel3_A
5110

    
5111

    
5112

    
5113
	state A_A1__TO__A_A2_1:
5114

    
5115
	 var 	idParallel3_A_2, idParallel3_A_3:int;
5116
	a_2:int;
5117
	idA_A1_2:int;
5118
	idA_A2_2:int;
5119
	let
5120

    
5121
		-- transition trace :
5122
	--A_A1__To__A_A2_1
5123
		(idA_A1_2, idParallel3_A_2) 
5124
	= A_A1_ex(idA_A1_1, idParallel3_A_1, false);
5125
		
5126

    
5127
		(idA_A2_2, idParallel3_A_3, a_2) 
5128
	= A_A2_en(idA_A2_1, idParallel3_A_2, a_1, x, false);
5129
		
5130

    
5131
	(idParallel3_A, a, idA_A1, idA_A2) 
5132
	=  (idParallel3_A_3, a_2, idA_A1_2, idA_A2_2);
5133

    
5134

    
5135
	tel
5136

    
5137
	until true restart POINTParallel3_A
5138

    
5139

    
5140

    
5141
	state A_A2_IDL:
5142

    
5143
	 var 	a_2:int;
5144
	idA_A2_2:int;
5145
	let
5146

    
5147
		
5148
	(idA_A2_2, a_2) 
5149
	= A_A2_node(idA_A2_1, a_1, x, S, R);
5150

    
5151
		
5152

    
5153

    
5154
	(idParallel3_A, a, idA_A1, idA_A2) 
5155
	= (idParallel3_A_1, a_2, idA_A1_1, idA_A2_2);
5156
	
5157

    
5158
	tel
5159

    
5160
	until true restart POINTParallel3_A
5161

    
5162

    
5163

    
5164
	state A_A1_IDL:
5165

    
5166
	 var 	a_2:int;
5167
	idA_A1_2:int;
5168
	let
5169

    
5170
		
5171
	(idA_A1_2, a_2) 
5172
	= A_A1_node(idA_A1_1, a_1, x, S, R);
5173

    
5174
		
5175

    
5176

    
5177
	(idParallel3_A, a, idA_A1, idA_A2) 
5178
	= (idParallel3_A_1, a_2, idA_A1_2, idA_A2_1);
5179
	
5180

    
5181
	tel
5182

    
5183
	until true restart POINTParallel3_A
5184

    
5185

    
5186

    
5187
tel
5188

    
5189

    
5190
--***************************************************State :Parallel3_Parallel3 Automaton***************************************************
5191

    
5192
node Parallel3_Parallel3_node(idParallel3_Parallel3_1:int;
5193
	a_1:int;
5194
	idA_A1_1:int;
5195
	idA_A2_1:int;
5196
	idParallel3_A_1:int;
5197
	x:int;
5198
	b_1:int;
5199
	idB_B1_1:int;
5200
	idB_B2_1:int;
5201
	idParallel3_B_1:int;
5202
	c_1:int;
5203
	dd_1:int;
5204
	idCD_C_1:int;
5205
	idCD_D_1:int;
5206
	idC_C1_1:int;
5207
	idC_C2_1:int;
5208
	idD_D1_1:int;
5209
	idD_D2_1:int;
5210
	idParallel3_CD_1:int;
5211
	R:bool;
5212
	S:bool;
5213
	T:bool)
5214

    
5215
returns (idParallel3_Parallel3:int;
5216
	a:int;
5217
	idA_A1:int;
5218
	idA_A2:int;
5219
	idParallel3_A:int;
5220
	b:int;
5221
	idB_B1:int;
5222
	idB_B2:int;
5223
	idParallel3_B:int;
5224
	c:int;
5225
	dd:int;
5226
	idCD_C:int;
5227
	idCD_D:int;
5228
	idC_C1:int;
5229
	idC_C2:int;
5230
	idD_D1:int;
5231
	idD_D2:int;
5232
	idParallel3_CD:int);
5233

    
5234

    
5235
let
5236

    
5237
	 automaton parallel3_parallel3
5238

    
5239
	state POINTParallel3_Parallel3:
5240
	unless (idParallel3_Parallel3_1=0) restart PARALLEL3_PARALLEL3_PARALLEL_ENTRY
5241
	unless true  restart PARALLEL3_PARALLEL3_PARALLEL_IDL
5242

    
5243
	let
5244

    
5245
		(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel3_CD) 
5246
	= (idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel3_CD_1);
5247
	
5248

    
5249
	tel
5250

    
5251

    
5252

    
5253
	state PARALLEL3_PARALLEL3_PARALLEL_ENTRY:
5254

    
5255
	 var 	idParallel3_Parallel3_2, idParallel3_Parallel3_3, idParallel3_Parallel3_4:int;
5256
	a_2, a_3:int;
5257
	idA_A1_2:int;
5258
	idA_A2_2:int;
5259
	idParallel3_A_2:int;
5260
	b_2, b_3:int;
5261
	idB_B1_2:int;
5262
	idB_B2_2:int;
5263
	idParallel3_B_2:int;
5264
	c_2:int;
5265
	dd_2:int;
5266
	idCD_C_2:int;
5267
	idCD_D_2:int;
5268
	idC_C1_2:int;
5269
	idC_C2_2:int;
5270
	idD_D1_2:int;
5271
	idD_D2_2:int;
5272
	idParallel3_CD_2:int;
5273
	let
5274

    
5275
		
5276
	(idParallel3_A_2, idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2) 
5277
	= Parallel3_A_en(idParallel3_A_1, idParallel3_Parallel3_1, a_1, idA_A1_1, x, idA_A2_1, false);
5278

    
5279
	(idParallel3_B_2, idParallel3_Parallel3_3, a_3, b_2, idB_B1_2, idB_B2_2) 
5280
	= Parallel3_B_en(idParallel3_B_1, idParallel3_Parallel3_2, a_2, b_1, idB_B1_1, idB_B2_1, false);
5281

    
5282
	(idParallel3_CD_2, idParallel3_Parallel3_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) 
5283
	= Parallel3_CD_en(idParallel3_CD_1, idParallel3_Parallel3_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);
5284

    
5285

    
5286
	(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel3_CD) 
5287
	= (idParallel3_Parallel3_4, a_3, idA_A1_2, idA_A2_2, idParallel3_A_2, b_3, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel3_CD_2);
5288
	
5289

    
5290
	tel
5291

    
5292
	until true restart POINTParallel3_Parallel3
5293

    
5294

    
5295

    
5296
	state PARALLEL3_PARALLEL3_PARALLEL_IDL:
5297

    
5298
	 var 	a_2, a_3:int;
5299
	idA_A1_2:int;
5300
	idA_A2_2:int;
5301
	idParallel3_A_2:int;
5302
	b_2, b_3:int;
5303
	idB_B1_2:int;
5304
	idB_B2_2:int;
5305
	idParallel3_B_2:int;
5306
	c_2:int;
5307
	dd_2:int;
5308
	idCD_C_2:int;
5309
	idCD_D_2:int;
5310
	idC_C1_2:int;
5311
	idC_C2_2:int;
5312
	idD_D1_2:int;
5313
	idD_D2_2:int;
5314
	idParallel3_CD_2:int;
5315
	let
5316

    
5317
		
5318

    
5319
		(idParallel3_A_2, a_2, idA_A1_2, idA_A2_2)
5320
	= if not (idParallel3_A_1= 0 ) then Parallel3_A_node(idParallel3_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R, S)
5321

    
5322
		 else (idParallel3_A_1, a_1, idA_A1_1, idA_A2_1);
5323

    
5324
		
5325

    
5326
		
5327

    
5328
		(idParallel3_B_2, a_3, b_2, idB_B1_2, idB_B2_2)
5329
	= if not (idParallel3_B_1= 0 ) then Parallel3_B_node(idParallel3_B_1, a_2, b_1, idB_B1_1, T, idB_B2_1, R, S)
5330

    
5331
		 else (idParallel3_B_1, a_2, b_1, idB_B1_1, idB_B2_1);
5332

    
5333
		
5334

    
5335
		
5336

    
5337
		(idParallel3_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)
5338
	= if not (idParallel3_CD_1= 0 ) then Parallel3_CD_node(idParallel3_CD_1, b_2, c_1, idCD_C_1, idC_C1_1, idC_C2_1, dd_1, idCD_D_1, idD_D1_1, idD_D2_1, R, S, T)
5339

    
5340
		 else (idParallel3_CD_1, b_2, c_1, idCD_C_1, idC_C1_1, idC_C2_1, dd_1, idCD_D_1, idD_D1_1, idD_D2_1);
5341

    
5342
		
5343

    
5344
		
5345

    
5346
	(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel3_CD) 
5347
	= (idParallel3_Parallel3_1, a_3, idA_A1_2, idA_A2_2, idParallel3_A_2, b_3, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel3_CD_2);
5348
	
5349

    
5350
	tel
5351

    
5352
	until true restart POINTParallel3_Parallel3
5353

    
5354

    
5355

    
5356
tel
5357

    
5358

    
5359
--***************************************************State :Parallel3_Parallel3 Automaton***************************************************
5360

    
5361
node Parallel3V3_Parallel3(x:int;
5362
	R:bool;
5363
	S:bool;
5364
	T:bool)
5365

    
5366
returns (a:int;
5367
	b:int;
5368
	dd:int;
5369
	c:int);
5370

    
5371

    
5372
var a_1: int;
5373

    
5374
	b_1: int;
5375

    
5376
	dd_1: int;
5377

    
5378
	c_1: int;
5379

    
5380
	idParallel3_Parallel3, idParallel3_Parallel3_1: int;
5381

    
5382
	idB_B2, idB_B2_1: int;
5383

    
5384
	idB_B1, idB_B1_1: int;
5385

    
5386
	idParallel3_B, idParallel3_B_1: int;
5387

    
5388
	idD_D2, idD_D2_1: int;
5389

    
5390
	idD_D1, idD_D1_1: int;
5391

    
5392
	idCD_D, idCD_D_1: int;
5393

    
5394
	idC_C2, idC_C2_1: int;
5395

    
5396
	idC_C1, idC_C1_1: int;
5397

    
5398
	idCD_C, idCD_C_1: int;
5399

    
5400
	idParallel3_CD, idParallel3_CD_1: int;
5401

    
5402
	idA_A2, idA_A2_1: int;
5403

    
5404
	idA_A1, idA_A1_1: int;
5405

    
5406
	idParallel3_A, idParallel3_A_1: int;
5407

    
5408
		idParallel3_Parallel3_2, idParallel3_Parallel3_3:int;
5409
	a_2, a_3:int;
5410
	idA_A1_2, idA_A1_3:int;
5411
	idA_A2_2, idA_A2_3:int;
5412
	idParallel3_A_2, idParallel3_A_3:int;
5413
	b_2, b_3:int;
5414
	idB_B1_2, idB_B1_3:int;
5415
	idB_B2_2, idB_B2_3:int;
5416
	idParallel3_B_2, idParallel3_B_3:int;
5417
	c_2, c_3:int;
5418
	dd_2, dd_3:int;
5419
	idCD_C_2, idCD_C_3:int;
5420
	idCD_D_2, idCD_D_3:int;
5421
	idC_C1_2, idC_C1_3:int;
5422
	idC_C2_2, idC_C2_3:int;
5423
	idD_D1_2, idD_D1_3:int;
5424
	idD_D2_2, idD_D2_3:int;
5425
	idParallel3_CD_2, idParallel3_CD_3:int;
5426
let
5427

    
5428
	a_1 = 0 -> pre a;
5429

    
5430
	b_1 = 0 -> pre b;
5431

    
5432
	dd_1 = 0 -> pre dd;
5433

    
5434
	c_1 = 0 -> pre c;
5435

    
5436
	idParallel3_Parallel3_1 = 0 -> pre idParallel3_Parallel3;
5437

    
5438
	idB_B2_1 = 0 -> pre idB_B2;
5439

    
5440
	idB_B1_1 = 0 -> pre idB_B1;
5441

    
5442
	idParallel3_B_1 = 0 -> pre idParallel3_B;
5443

    
5444
	idD_D2_1 = 0 -> pre idD_D2;
5445

    
5446
	idD_D1_1 = 0 -> pre idD_D1;
5447

    
5448
	idCD_D_1 = 0 -> pre idCD_D;
5449

    
5450
	idC_C2_1 = 0 -> pre idC_C2;
5451

    
5452
	idC_C1_1 = 0 -> pre idC_C1;
5453

    
5454
	idCD_C_1 = 0 -> pre idCD_C;
5455

    
5456
	idParallel3_CD_1 = 0 -> pre idParallel3_CD;
5457

    
5458
	idA_A2_1 = 0 -> pre idA_A2;
5459

    
5460
	idA_A1_1 = 0 -> pre idA_A1;
5461

    
5462
	idParallel3_A_1 = 0 -> pre idParallel3_A;
5463

    
5464
	
5465

    
5466

    
5467

    
5468
	(idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel3_CD_2)
5469
	 = 
5470

    
5471
	 if R then Parallel3_Parallel3_node(idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, x, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel3_CD_1, R, false, false)
5472

    
5473
	 else (idParallel3_Parallel3_1, a_1, idA_A1_1, idA_A2_1, idParallel3_A_1, b_1, idB_B1_1, idB_B2_1, idParallel3_B_1, c_1, dd_1, idCD_C_1, idCD_D_1, idC_C1_1, idC_C2_1, idD_D1_1, idD_D2_1, idParallel3_CD_1);
5474

    
5475
	
5476

    
5477

    
5478

    
5479
	(idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel3_CD_3)
5480
	 = 
5481

    
5482
	 if S then Parallel3_Parallel3_node(idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, x, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel3_CD_2, false, S, false)
5483

    
5484
	 else (idParallel3_Parallel3_2, a_2, idA_A1_2, idA_A2_2, idParallel3_A_2, b_2, idB_B1_2, idB_B2_2, idParallel3_B_2, c_2, dd_2, idCD_C_2, idCD_D_2, idC_C1_2, idC_C2_2, idD_D1_2, idD_D2_2, idParallel3_CD_2);
5485

    
5486
	
5487

    
5488

    
5489

    
5490
	(idParallel3_Parallel3, a, idA_A1, idA_A2, idParallel3_A, b, idB_B1, idB_B2, idParallel3_B, c, dd, idCD_C, idCD_D, idC_C1, idC_C2, idD_D1, idD_D2, idParallel3_CD)
5491
	 = 
5492

    
5493
	 if T then Parallel3_Parallel3_node(idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, x, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel3_CD_3, false, false, T)
5494

    
5495
	 else (idParallel3_Parallel3_3, a_3, idA_A1_3, idA_A2_3, idParallel3_A_3, b_3, idB_B1_3, idB_B2_3, idParallel3_B_3, c_3, dd_3, idCD_C_3, idCD_D_3, idC_C1_3, idC_C2_3, idD_D1_3, idD_D2_3, idParallel3_CD_3);
5496

    
5497
	
5498

    
5499

    
5500
--unused outputs
5501
	
5502

    
5503
tel
5504

    
5505

    
5506

    
5507
node Parallel3V3 (x_1_1 : int; R_1_1 : real; S_1_1 : real; T_1_1 : real)
5508
returns (a_1_1 : int;
5509
	b_2_1 : int;
5510
	dd_3_1 : int;
5511
	c_4_1 : int); 
5512
var
5513
	Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real;
5514
	Parallel3_1_1 : int; Parallel3_2_1 : int; Parallel3_3_1 : int; Parallel3_4_1 : int;
5515
	i_virtual_local : real;
5516
	Parallel3Mux_1_1_event: bool;
5517
	Parallel3Mux_1_2_event: bool;
5518
	Parallel3Mux_1_3_event: bool;
5519
let 
5520
	Mux_1_1 = R_1_1 ;
5521
	Mux_1_2 = S_1_1 ;
5522
	Mux_1_3 = T_1_1 ;
5523
	Parallel3Mux_1_1_event = false -> ((pre(Mux_1_1) > 0.0 and Mux_1_1 <= 0.0) or (pre(Mux_1_1) <= 0.0 and Mux_1_1 > 0.0));
5524
	Parallel3Mux_1_2_event = false -> ((pre(Mux_1_2) > 0.0 and Mux_1_2 <= 0.0) or (pre(Mux_1_2) <= 0.0 and Mux_1_2 > 0.0));
5525
	Parallel3Mux_1_3_event = false -> ((pre(Mux_1_3) > 0.0 and Mux_1_3 <= 0.0) or (pre(Mux_1_3) <= 0.0 and Mux_1_3 > 0.0));
5526
	(Parallel3_1_1, Parallel3_2_1, Parallel3_3_1, Parallel3_4_1) =  Parallel3V3_Parallel3(x_1_1, Parallel3Mux_1_1_event, Parallel3Mux_1_2_event, Parallel3Mux_1_3_event);
5527
	a_1_1 = Parallel3_1_1;
5528
	b_2_1 = Parallel3_2_1;
5529
	dd_3_1 = Parallel3_3_1;
5530
	c_4_1 = Parallel3_4_1;
5531
	i_virtual_local= 0.0 -> 1.0;
5532
tel
5533