Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Parallel2V2 / Parallel2V2.lus @ eb639349

History | View | Annotate | Download (71.7 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
	= 1425;
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
	= 1426;
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
	idParallel2_B_1:int;
186
	a_1:int;
187
	b_1:int;
188
	isInner:bool)
189

    
190
returns (idB_B2:int;
191
	idParallel2_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
	idParallel2_B_2, idParallel2_B_3, idParallel2_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
	idParallel2_B_2 
208
	= 1424;
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, idParallel2_B_3, a_3, b_3) 
219
	= 
220

    
221
	if ( idB_B2_1 = 0) then
222

    
223
	 (idB_B2_2, idParallel2_B_2, a_2, b_2)
224

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

    
227
	
228

    
229
	(idB_B2_4, a_4, b_4) 
230
	= 
231
	if ( idB_B2_1 = 1425) 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 = 1426) 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, idParallel2_B_4, a_6, b_6) 
246
	= 
247
		 if ( idB_B2_1 = 0) then 
248
		(idB_B2_3, idParallel2_B_3, a_3, b_3)
249
		 else
250
		 if ( idB_B2_1 = 1425) then 
251
		(idB_B2_4, idParallel2_B_3, a_4, b_4)
252
		 else
253
		 if ( idB_B2_1 = 1426) then 
254
		(idB_B2_5, idParallel2_B_3, a_5, b_5)
255
		 else (idB_B2_1, idParallel2_B_2, a_1, b_1);
256

    
257

    
258
	(idB_B2, idParallel2_B, a, b) 
259
	= (idB_B2_6, idParallel2_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
	idParallel2_B_1:int;
271
	isInner:bool)
272

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

    
276

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

    
280

    
281
let
282

    
283

    
284

    
285
	
286
	(idB_B2_2) 
287
	= 
288
	if ( idB_B2_1 = 1425) 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 = 1426) 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 = 1425) then 
305
		(idB_B2_2)
306
		 else
307
		 if ( idB_B2_1 = 1426) then 
308
		(idB_B2_3)
309
		 else (idB_B2_1);
310

    
311

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

    
316
	idB_B2_5 
317
	= 0;
318
	
319

    
320
	(idB_B2, idParallel2_B) 
321
	= (idB_B2_5, idParallel2_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
	= 1428;
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
	= 1429;
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
	idParallel2_B_1:int;
472
	a_1:int;
473
	b_1:int;
474
	isInner:bool)
475

    
476
returns (idB_B1:int;
477
	idParallel2_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
	idParallel2_B_2, idParallel2_B_3, idParallel2_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
	idParallel2_B_2 
494
	= 1427;
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, idParallel2_B_3, a_3, b_3) 
505
	= 
506

    
507
	if ( idB_B1_1 = 0) then
508

    
509
	 (idB_B1_2, idParallel2_B_2, a_2, b_2)
510

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

    
513
	
514

    
515
	(idB_B1_4, a_4, b_4) 
516
	= 
517
	if ( idB_B1_1 = 1428) 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 = 1429) 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, idParallel2_B_4, a_6, b_6) 
532
	= 
533
		 if ( idB_B1_1 = 0) then 
534
		(idB_B1_3, idParallel2_B_3, a_3, b_3)
535
		 else
536
		 if ( idB_B1_1 = 1428) then 
537
		(idB_B1_4, idParallel2_B_3, a_4, b_4)
538
		 else
539
		 if ( idB_B1_1 = 1429) then 
540
		(idB_B1_5, idParallel2_B_3, a_5, b_5)
541
		 else (idB_B1_1, idParallel2_B_2, a_1, b_1);
542

    
543

    
544
	(idB_B1, idParallel2_B, a, b) 
545
	= (idB_B1_6, idParallel2_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
	idParallel2_B_1:int;
557
	isInner:bool)
558

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

    
562

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

    
566

    
567
let
568

    
569

    
570

    
571
	
572
	(idB_B1_2) 
573
	= 
574
	if ( idB_B1_1 = 1428) 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 = 1429) 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 = 1428) then 
591
		(idB_B1_2)
592
		 else
593
		 if ( idB_B1_1 = 1429) then 
594
		(idB_B1_3)
595
		 else (idB_B1_1);
596

    
597

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

    
602
	idB_B1_5 
603
	= 0;
604
	
605

    
606
	(idB_B1, idParallel2_B) 
607
	= (idB_B1_5, idParallel2_B_1);
608
	
609

    
610
tel
611

    
612

    
613

    
614

    
615

    
616

    
617
-- Entry action for state :Parallel2_B
618
node Parallel2_B_en(idParallel2_B_1:int;
619
	idParallel2_Parallel2_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 (idParallel2_B:int;
627
	idParallel2_Parallel2:int;
628
	a:int;
629
	b:int;
630
	idB_B1:int;
631
	idB_B2:int);
632

    
633

    
634
var 	idParallel2_B_2, idParallel2_B_3, idParallel2_B_4, idParallel2_B_5, idParallel2_B_6:int;
635
	idParallel2_Parallel2_2, idParallel2_Parallel2_3, idParallel2_Parallel2_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
	idParallel2_Parallel2_2 
648
	= 1423;
649
	
650

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

    
658
	(idParallel2_B_3, idParallel2_Parallel2_3, a_3, b_3, idB_B1_3) 
659
	= 
660

    
661
	if ( idParallel2_B_1 = 0) then
662

    
663
	 (idParallel2_B_2, idParallel2_Parallel2_2, a_2, b_2, idB_B1_2)
664

    
665
	 else(idParallel2_B_1, idParallel2_Parallel2_2, a_1, b_1, idB_B1_1);
666

    
667
	
668

    
669
	(idB_B2_2, idParallel2_B_4, a_4, b_4) 
670
	= 
671
	if ( idParallel2_B_1 = 1424) then
672
	B_B2_en(idB_B2_1, idParallel2_B_1, a_1, b_1, false)
673
	 else (idB_B2_1, idParallel2_B_1, a_1, b_1);
674

    
675
	
676

    
677
	(idB_B1_4, idParallel2_B_5, a_5, b_5) 
678
	= 
679
	if ( idParallel2_B_1 = 1427) then
680
	B_B1_en(idB_B1_1, idParallel2_B_1, a_1, b_1, false)
681
	 else (idB_B1_1, idParallel2_B_1, a_1, b_1);
682

    
683
	
684

    
685
	(idParallel2_B_6, idParallel2_Parallel2_4, a_6, b_6, idB_B1_5, idB_B2_3) 
686
	= 
687
		 if ( idParallel2_B_1 = 0) then 
688
		(idParallel2_B_3, idParallel2_Parallel2_3, a_3, b_3, idB_B1_3, idB_B2_1)
689
		 else
690
		 if ( idParallel2_B_1 = 1424) then 
691
		(idParallel2_B_4, idParallel2_Parallel2_3, a_4, b_4, idB_B1_1, idB_B2_2)
692
		 else
693
		 if ( idParallel2_B_1 = 1427) then 
694
		(idParallel2_B_5, idParallel2_Parallel2_3, a_5, b_5, idB_B1_4, idB_B2_1)
695
		 else (idParallel2_B_1, idParallel2_Parallel2_2, a_1, b_1, idB_B1_1, idB_B2_1);
696

    
697

    
698
	(idParallel2_B, idParallel2_Parallel2, a, b, idB_B1, idB_B2) 
699
	= (idParallel2_B_6, idParallel2_Parallel2_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 :Parallel2_B
709
node Parallel2_B_ex(idB_B2_1:int;
710
	idParallel2_B_1:int;
711
	idB_B1_1:int;
712
	idParallel2_Parallel2_1:int;
713
	isInner:bool)
714

    
715
returns (idB_B2:int;
716
	idParallel2_B:int;
717
	idB_B1:int;
718
	idParallel2_Parallel2:int);
719

    
720

    
721
var 	idB_B2_2, idB_B2_3:int;
722
	idParallel2_B_2, idParallel2_B_3, idParallel2_B_4, idParallel2_B_5:int;
723
	idB_B1_2, idB_B1_3:int;
724
	idParallel2_Parallel2_2:int;
725

    
726

    
727
let
728

    
729

    
730

    
731
	
732
	(idB_B2_2, idParallel2_B_2) 
733
	= 
734
	if ( idParallel2_B_1 = 1424) then
735
	B_B2_ex(idB_B2_1, idParallel2_B_1, false)
736
	 else (idB_B2_1, idParallel2_B_1);
737

    
738
	
739

    
740
	(idB_B1_2, idParallel2_B_3) 
741
	= 
742
	if ( idParallel2_B_1 = 1427) then
743
	B_B1_ex(idB_B1_1, idParallel2_B_1, false)
744
	 else (idB_B1_1, idParallel2_B_1);
745

    
746
	
747

    
748
	(idB_B2_3, idParallel2_B_4, idB_B1_3) 
749
	= 
750
		 if ( idParallel2_B_1 = 1424) then 
751
		(idB_B2_2, idParallel2_B_2, idB_B1_1)
752
		 else
753
		 if ( idParallel2_B_1 = 1427) then 
754
		(idB_B2_1, idParallel2_B_3, idB_B1_2)
755
		 else (idB_B2_1, idParallel2_B_1, idB_B1_1);
756

    
757

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

    
762
	idParallel2_B_5 
763
	= 0;
764
	
765

    
766
	(idB_B2, idParallel2_B, idB_B1, idParallel2_Parallel2) 
767
	= (idB_B2_3, idParallel2_B_5, idB_B1_3, idParallel2_Parallel2_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
	= 1439;
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
	= 1440;
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
	idParallel2_D_1:int;
918
	c_1:int;
919
	dd_1:int;
920
	isInner:bool)
921

    
922
returns (idD_D2:int;
923
	idParallel2_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
	idParallel2_D_2, idParallel2_D_3, idParallel2_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
	idParallel2_D_2 
940
	= 1438;
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, idParallel2_D_3, c_3, dd_3) 
951
	= 
952

    
953
	if ( idD_D2_1 = 0) then
954

    
955
	 (idD_D2_2, idParallel2_D_2, c_2, dd_2)
956

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

    
959
	
960

    
961
	(idD_D2_4, c_4, dd_4) 
962
	= 
963
	if ( idD_D2_1 = 1439) 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 = 1440) 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, idParallel2_D_4, c_6, dd_6) 
978
	= 
979
		 if ( idD_D2_1 = 0) then 
980
		(idD_D2_3, idParallel2_D_3, c_3, dd_3)
981
		 else
982
		 if ( idD_D2_1 = 1439) then 
983
		(idD_D2_4, idParallel2_D_3, c_4, dd_4)
984
		 else
985
		 if ( idD_D2_1 = 1440) then 
986
		(idD_D2_5, idParallel2_D_3, c_5, dd_5)
987
		 else (idD_D2_1, idParallel2_D_2, c_1, dd_1);
988

    
989

    
990
	(idD_D2, idParallel2_D, c, dd) 
991
	= (idD_D2_6, idParallel2_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
	idParallel2_D_1:int;
1003
	isInner:bool)
1004

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

    
1008

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

    
1012

    
1013
let
1014

    
1015

    
1016

    
1017
	
1018
	(idD_D2_2) 
1019
	= 
1020
	if ( idD_D2_1 = 1439) 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 = 1440) 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 = 1439) then 
1037
		(idD_D2_2)
1038
		 else
1039
		 if ( idD_D2_1 = 1440) then 
1040
		(idD_D2_3)
1041
		 else (idD_D2_1);
1042

    
1043

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

    
1048
	idD_D2_5 
1049
	= 0;
1050
	
1051

    
1052
	(idD_D2, idParallel2_D) 
1053
	= (idD_D2_5, idParallel2_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
	= 1442;
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
	= 1430;
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
	idParallel2_D_1:int;
1204
	c_1:int;
1205
	dd_1:int;
1206
	isInner:bool)
1207

    
1208
returns (idD_D1:int;
1209
	idParallel2_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
	idParallel2_D_2, idParallel2_D_3, idParallel2_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
	idParallel2_D_2 
1226
	= 1441;
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, idParallel2_D_3, c_3, dd_3) 
1237
	= 
1238

    
1239
	if ( idD_D1_1 = 0) then
1240

    
1241
	 (idD_D1_2, idParallel2_D_2, c_2, dd_2)
1242

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

    
1245
	
1246

    
1247
	(idD_D1_4, c_4, dd_4) 
1248
	= 
1249
	if ( idD_D1_1 = 1442) 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 = 1430) 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, idParallel2_D_4, c_6, dd_6) 
1264
	= 
1265
		 if ( idD_D1_1 = 0) then 
1266
		(idD_D1_3, idParallel2_D_3, c_3, dd_3)
1267
		 else
1268
		 if ( idD_D1_1 = 1442) then 
1269
		(idD_D1_4, idParallel2_D_3, c_4, dd_4)
1270
		 else
1271
		 if ( idD_D1_1 = 1430) then 
1272
		(idD_D1_5, idParallel2_D_3, c_5, dd_5)
1273
		 else (idD_D1_1, idParallel2_D_2, c_1, dd_1);
1274

    
1275

    
1276
	(idD_D1, idParallel2_D, c, dd) 
1277
	= (idD_D1_6, idParallel2_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
	idParallel2_D_1:int;
1289
	isInner:bool)
1290

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

    
1294

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

    
1298

    
1299
let
1300

    
1301

    
1302

    
1303
	
1304
	(idD_D1_2) 
1305
	= 
1306
	if ( idD_D1_1 = 1442) 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 = 1430) 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 = 1442) then 
1323
		(idD_D1_2)
1324
		 else
1325
		 if ( idD_D1_1 = 1430) then 
1326
		(idD_D1_3)
1327
		 else (idD_D1_1);
1328

    
1329

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

    
1334
	idD_D1_5 
1335
	= 0;
1336
	
1337

    
1338
	(idD_D1, idParallel2_D) 
1339
	= (idD_D1_5, idParallel2_D_1);
1340
	
1341

    
1342
tel
1343

    
1344

    
1345

    
1346

    
1347

    
1348

    
1349
-- Entry action for state :Parallel2_D
1350
node Parallel2_D_en(idParallel2_D_1:int;
1351
	idParallel2_Parallel2_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 (idParallel2_D:int;
1359
	idParallel2_Parallel2:int;
1360
	c:int;
1361
	dd:int;
1362
	idD_D1:int;
1363
	idD_D2:int);
1364

    
1365

    
1366
var 	idParallel2_D_2, idParallel2_D_3, idParallel2_D_4, idParallel2_D_5, idParallel2_D_6:int;
1367
	idParallel2_Parallel2_2, idParallel2_Parallel2_3, idParallel2_Parallel2_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
	idParallel2_Parallel2_2 
1380
	= 1437;
1381
	
1382

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

    
1390
	(idParallel2_D_3, idParallel2_Parallel2_3, c_3, dd_3, idD_D1_3) 
1391
	= 
1392

    
1393
	if ( idParallel2_D_1 = 0) then
1394

    
1395
	 (idParallel2_D_2, idParallel2_Parallel2_2, c_2, dd_2, idD_D1_2)
1396

    
1397
	 else(idParallel2_D_1, idParallel2_Parallel2_2, c_1, dd_1, idD_D1_1);
1398

    
1399
	
1400

    
1401
	(idD_D2_2, idParallel2_D_4, c_4, dd_4) 
1402
	= 
1403
	if ( idParallel2_D_1 = 1438) then
1404
	D_D2_en(idD_D2_1, idParallel2_D_1, c_1, dd_1, false)
1405
	 else (idD_D2_1, idParallel2_D_1, c_1, dd_1);
1406

    
1407
	
1408

    
1409
	(idD_D1_4, idParallel2_D_5, c_5, dd_5) 
1410
	= 
1411
	if ( idParallel2_D_1 = 1441) then
1412
	D_D1_en(idD_D1_1, idParallel2_D_1, c_1, dd_1, false)
1413
	 else (idD_D1_1, idParallel2_D_1, c_1, dd_1);
1414

    
1415
	
1416

    
1417
	(idParallel2_D_6, idParallel2_Parallel2_4, c_6, dd_6, idD_D1_5, idD_D2_3) 
1418
	= 
1419
		 if ( idParallel2_D_1 = 0) then 
1420
		(idParallel2_D_3, idParallel2_Parallel2_3, c_3, dd_3, idD_D1_3, idD_D2_1)
1421
		 else
1422
		 if ( idParallel2_D_1 = 1438) then 
1423
		(idParallel2_D_4, idParallel2_Parallel2_3, c_4, dd_4, idD_D1_1, idD_D2_2)
1424
		 else
1425
		 if ( idParallel2_D_1 = 1441) then 
1426
		(idParallel2_D_5, idParallel2_Parallel2_3, c_5, dd_5, idD_D1_4, idD_D2_1)
1427
		 else (idParallel2_D_1, idParallel2_Parallel2_2, c_1, dd_1, idD_D1_1, idD_D2_1);
1428

    
1429

    
1430
	(idParallel2_D, idParallel2_Parallel2, c, dd, idD_D1, idD_D2) 
1431
	= (idParallel2_D_6, idParallel2_Parallel2_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 :Parallel2_D
1441
node Parallel2_D_ex(idD_D2_1:int;
1442
	idParallel2_D_1:int;
1443
	idD_D1_1:int;
1444
	idParallel2_Parallel2_1:int;
1445
	isInner:bool)
1446

    
1447
returns (idD_D2:int;
1448
	idParallel2_D:int;
1449
	idD_D1:int;
1450
	idParallel2_Parallel2:int);
1451

    
1452

    
1453
var 	idD_D2_2, idD_D2_3:int;
1454
	idParallel2_D_2, idParallel2_D_3, idParallel2_D_4, idParallel2_D_5:int;
1455
	idD_D1_2, idD_D1_3:int;
1456
	idParallel2_Parallel2_2:int;
1457

    
1458

    
1459
let
1460

    
1461

    
1462

    
1463
	
1464
	(idD_D2_2, idParallel2_D_2) 
1465
	= 
1466
	if ( idParallel2_D_1 = 1438) then
1467
	D_D2_ex(idD_D2_1, idParallel2_D_1, false)
1468
	 else (idD_D2_1, idParallel2_D_1);
1469

    
1470
	
1471

    
1472
	(idD_D1_2, idParallel2_D_3) 
1473
	= 
1474
	if ( idParallel2_D_1 = 1441) then
1475
	D_D1_ex(idD_D1_1, idParallel2_D_1, false)
1476
	 else (idD_D1_1, idParallel2_D_1);
1477

    
1478
	
1479

    
1480
	(idD_D2_3, idParallel2_D_4, idD_D1_3) 
1481
	= 
1482
		 if ( idParallel2_D_1 = 1438) then 
1483
		(idD_D2_2, idParallel2_D_2, idD_D1_1)
1484
		 else
1485
		 if ( idParallel2_D_1 = 1441) then 
1486
		(idD_D2_1, idParallel2_D_3, idD_D1_2)
1487
		 else (idD_D2_1, idParallel2_D_1, idD_D1_1);
1488

    
1489

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

    
1494
	idParallel2_D_5 
1495
	= 0;
1496
	
1497

    
1498
	(idD_D2, idParallel2_D, idD_D1, idParallel2_Parallel2) 
1499
	= (idD_D2_3, idParallel2_D_5, idD_D1_3, idParallel2_Parallel2_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
	= 1432;
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
	= 1433;
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
	idParallel2_C_1:int;
1650
	b_1:int;
1651
	c_1:int;
1652
	isInner:bool)
1653

    
1654
returns (idC_C2:int;
1655
	idParallel2_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
	idParallel2_C_2, idParallel2_C_3, idParallel2_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
	idParallel2_C_2 
1672
	= 1431;
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, idParallel2_C_3, b_3, c_3) 
1683
	= 
1684

    
1685
	if ( idC_C2_1 = 0) then
1686

    
1687
	 (idC_C2_2, idParallel2_C_2, b_2, c_2)
1688

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

    
1691
	
1692

    
1693
	(idC_C2_4, b_4, c_4) 
1694
	= 
1695
	if ( idC_C2_1 = 1432) 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 = 1433) 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, idParallel2_C_4, b_6, c_6) 
1710
	= 
1711
		 if ( idC_C2_1 = 0) then 
1712
		(idC_C2_3, idParallel2_C_3, b_3, c_3)
1713
		 else
1714
		 if ( idC_C2_1 = 1432) then 
1715
		(idC_C2_4, idParallel2_C_3, b_4, c_4)
1716
		 else
1717
		 if ( idC_C2_1 = 1433) then 
1718
		(idC_C2_5, idParallel2_C_3, b_5, c_5)
1719
		 else (idC_C2_1, idParallel2_C_2, b_1, c_1);
1720

    
1721

    
1722
	(idC_C2, idParallel2_C, b, c) 
1723
	= (idC_C2_6, idParallel2_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
	idParallel2_C_1:int;
1735
	isInner:bool)
1736

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

    
1740

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

    
1744

    
1745
let
1746

    
1747

    
1748

    
1749
	
1750
	(idC_C2_2) 
1751
	= 
1752
	if ( idC_C2_1 = 1432) 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 = 1433) 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 = 1432) then 
1769
		(idC_C2_2)
1770
		 else
1771
		 if ( idC_C2_1 = 1433) then 
1772
		(idC_C2_3)
1773
		 else (idC_C2_1);
1774

    
1775

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

    
1780
	idC_C2_5 
1781
	= 0;
1782
	
1783

    
1784
	(idC_C2, idParallel2_C) 
1785
	= (idC_C2_5, idParallel2_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
	= 1435;
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
	= 1436;
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
	idParallel2_C_1:int;
1936
	b_1:int;
1937
	c_1:int;
1938
	isInner:bool)
1939

    
1940
returns (idC_C1:int;
1941
	idParallel2_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
	idParallel2_C_2, idParallel2_C_3, idParallel2_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
	idParallel2_C_2 
1958
	= 1434;
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, idParallel2_C_3, b_3, c_3) 
1969
	= 
1970

    
1971
	if ( idC_C1_1 = 0) then
1972

    
1973
	 (idC_C1_2, idParallel2_C_2, b_2, c_2)
1974

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

    
1977
	
1978

    
1979
	(idC_C1_4, b_4, c_4) 
1980
	= 
1981
	if ( idC_C1_1 = 1435) 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 = 1436) 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, idParallel2_C_4, b_6, c_6) 
1996
	= 
1997
		 if ( idC_C1_1 = 0) then 
1998
		(idC_C1_3, idParallel2_C_3, b_3, c_3)
1999
		 else
2000
		 if ( idC_C1_1 = 1435) then 
2001
		(idC_C1_4, idParallel2_C_3, b_4, c_4)
2002
		 else
2003
		 if ( idC_C1_1 = 1436) then 
2004
		(idC_C1_5, idParallel2_C_3, b_5, c_5)
2005
		 else (idC_C1_1, idParallel2_C_2, b_1, c_1);
2006

    
2007

    
2008
	(idC_C1, idParallel2_C, b, c) 
2009
	= (idC_C1_6, idParallel2_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
	idParallel2_C_1:int;
2021
	isInner:bool)
2022

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

    
2026

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

    
2030

    
2031
let
2032

    
2033

    
2034

    
2035
	
2036
	(idC_C1_2) 
2037
	= 
2038
	if ( idC_C1_1 = 1435) 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 = 1436) 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 = 1435) then 
2055
		(idC_C1_2)
2056
		 else
2057
		 if ( idC_C1_1 = 1436) then 
2058
		(idC_C1_3)
2059
		 else (idC_C1_1);
2060

    
2061

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

    
2066
	idC_C1_5 
2067
	= 0;
2068
	
2069

    
2070
	(idC_C1, idParallel2_C) 
2071
	= (idC_C1_5, idParallel2_C_1);
2072
	
2073

    
2074
tel
2075

    
2076

    
2077

    
2078

    
2079

    
2080

    
2081
-- Entry action for state :Parallel2_C
2082
node Parallel2_C_en(idParallel2_C_1:int;
2083
	idParallel2_Parallel2_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 (idParallel2_C:int;
2091
	idParallel2_Parallel2:int;
2092
	b:int;
2093
	c:int;
2094
	idC_C1:int;
2095
	idC_C2:int);
2096

    
2097

    
2098
var 	idParallel2_C_2, idParallel2_C_3, idParallel2_C_4, idParallel2_C_5, idParallel2_C_6:int;
2099
	idParallel2_Parallel2_2, idParallel2_Parallel2_3, idParallel2_Parallel2_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
	idParallel2_Parallel2_2 
2112
	= 1443;
2113
	
2114

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

    
2122
	(idParallel2_C_3, idParallel2_Parallel2_3, b_3, c_3, idC_C1_3) 
2123
	= 
2124

    
2125
	if ( idParallel2_C_1 = 0) then
2126

    
2127
	 (idParallel2_C_2, idParallel2_Parallel2_2, b_2, c_2, idC_C1_2)
2128

    
2129
	 else(idParallel2_C_1, idParallel2_Parallel2_2, b_1, c_1, idC_C1_1);
2130

    
2131
	
2132

    
2133
	(idC_C2_2, idParallel2_C_4, b_4, c_4) 
2134
	= 
2135
	if ( idParallel2_C_1 = 1431) then
2136
	C_C2_en(idC_C2_1, idParallel2_C_1, b_1, c_1, false)
2137
	 else (idC_C2_1, idParallel2_C_1, b_1, c_1);
2138

    
2139
	
2140

    
2141
	(idC_C1_4, idParallel2_C_5, b_5, c_5) 
2142
	= 
2143
	if ( idParallel2_C_1 = 1434) then
2144
	C_C1_en(idC_C1_1, idParallel2_C_1, b_1, c_1, false)
2145
	 else (idC_C1_1, idParallel2_C_1, b_1, c_1);
2146

    
2147
	
2148

    
2149
	(idParallel2_C_6, idParallel2_Parallel2_4, b_6, c_6, idC_C1_5, idC_C2_3) 
2150
	= 
2151
		 if ( idParallel2_C_1 = 0) then 
2152
		(idParallel2_C_3, idParallel2_Parallel2_3, b_3, c_3, idC_C1_3, idC_C2_1)
2153
		 else
2154
		 if ( idParallel2_C_1 = 1431) then 
2155
		(idParallel2_C_4, idParallel2_Parallel2_3, b_4, c_4, idC_C1_1, idC_C2_2)
2156
		 else
2157
		 if ( idParallel2_C_1 = 1434) then 
2158
		(idParallel2_C_5, idParallel2_Parallel2_3, b_5, c_5, idC_C1_4, idC_C2_1)
2159
		 else (idParallel2_C_1, idParallel2_Parallel2_2, b_1, c_1, idC_C1_1, idC_C2_1);
2160

    
2161

    
2162
	(idParallel2_C, idParallel2_Parallel2, b, c, idC_C1, idC_C2) 
2163
	= (idParallel2_C_6, idParallel2_Parallel2_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 :Parallel2_C
2173
node Parallel2_C_ex(idC_C2_1:int;
2174
	idParallel2_C_1:int;
2175
	idC_C1_1:int;
2176
	idParallel2_Parallel2_1:int;
2177
	isInner:bool)
2178

    
2179
returns (idC_C2:int;
2180
	idParallel2_C:int;
2181
	idC_C1:int;
2182
	idParallel2_Parallel2:int);
2183

    
2184

    
2185
var 	idC_C2_2, idC_C2_3:int;
2186
	idParallel2_C_2, idParallel2_C_3, idParallel2_C_4, idParallel2_C_5:int;
2187
	idC_C1_2, idC_C1_3:int;
2188
	idParallel2_Parallel2_2:int;
2189

    
2190

    
2191
let
2192

    
2193

    
2194

    
2195
	
2196
	(idC_C2_2, idParallel2_C_2) 
2197
	= 
2198
	if ( idParallel2_C_1 = 1431) then
2199
	C_C2_ex(idC_C2_1, idParallel2_C_1, false)
2200
	 else (idC_C2_1, idParallel2_C_1);
2201

    
2202
	
2203

    
2204
	(idC_C1_2, idParallel2_C_3) 
2205
	= 
2206
	if ( idParallel2_C_1 = 1434) then
2207
	C_C1_ex(idC_C1_1, idParallel2_C_1, false)
2208
	 else (idC_C1_1, idParallel2_C_1);
2209

    
2210
	
2211

    
2212
	(idC_C2_3, idParallel2_C_4, idC_C1_3) 
2213
	= 
2214
		 if ( idParallel2_C_1 = 1431) then 
2215
		(idC_C2_2, idParallel2_C_2, idC_C1_1)
2216
		 else
2217
		 if ( idParallel2_C_1 = 1434) then 
2218
		(idC_C2_1, idParallel2_C_3, idC_C1_2)
2219
		 else (idC_C2_1, idParallel2_C_1, idC_C1_1);
2220

    
2221

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

    
2226
	idParallel2_C_5 
2227
	= 0;
2228
	
2229

    
2230
	(idC_C2, idParallel2_C, idC_C1, idParallel2_Parallel2) 
2231
	= (idC_C2_3, idParallel2_C_5, idC_C1_3, idParallel2_Parallel2_1);
2232
	
2233

    
2234
tel
2235

    
2236

    
2237

    
2238

    
2239

    
2240

    
2241
-- Entry action for state :A2_A2a
2242
node A2_A2a_en(idA_A2_1:int;
2243
	x:int;
2244
	a_1:int;
2245
	isInner:bool)
2246

    
2247
returns (idA_A2:int;
2248
	a:int);
2249

    
2250

    
2251
var 	idA_A2_2:int;
2252
	a_2:int;
2253

    
2254

    
2255
let
2256

    
2257

    
2258

    
2259
	-- set state as active 
2260
	idA_A2_2 
2261
	= 1421;
2262
	
2263

    
2264
	a_2 
2265
	= if (not isInner) then x+3
2266
	 else a_1;
2267
	
2268

    
2269
	(idA_A2, a) 
2270
	= (idA_A2_2, a_2);
2271
	
2272

    
2273
tel
2274

    
2275

    
2276

    
2277

    
2278

    
2279
-- Exit action for state :A2_A2a
2280
node A2_A2a_ex(idA_A2_1:int;
2281
	isInner:bool)
2282

    
2283
returns (idA_A2:int);
2284

    
2285

    
2286
var 	idA_A2_2:int;
2287

    
2288

    
2289
let
2290

    
2291

    
2292

    
2293
	-- set state as inactive 
2294
	idA_A2_2
2295
	 = if (not isInner) then 0 else idA_A2_1;
2296

    
2297

    
2298
	(idA_A2) 
2299
	= (idA_A2_1);
2300
	
2301

    
2302
tel
2303

    
2304

    
2305

    
2306

    
2307

    
2308

    
2309
-- Entry action for state :A2_A2b
2310
node A2_A2b_en(idA_A2_1:int;
2311
	x:int;
2312
	a_1:int;
2313
	isInner:bool)
2314

    
2315
returns (idA_A2:int;
2316
	a:int);
2317

    
2318

    
2319
var 	idA_A2_2:int;
2320
	a_2:int;
2321

    
2322

    
2323
let
2324

    
2325

    
2326

    
2327
	-- set state as active 
2328
	idA_A2_2 
2329
	= 1422;
2330
	
2331

    
2332
	a_2 
2333
	= if (not isInner) then x+4
2334
	 else a_1;
2335
	
2336

    
2337
	(idA_A2, a) 
2338
	= (idA_A2_2, a_2);
2339
	
2340

    
2341
tel
2342

    
2343

    
2344

    
2345

    
2346

    
2347
-- Exit action for state :A2_A2b
2348
node A2_A2b_ex(idA_A2_1:int;
2349
	isInner:bool)
2350

    
2351
returns (idA_A2:int);
2352

    
2353

    
2354
var 	idA_A2_2:int;
2355

    
2356

    
2357
let
2358

    
2359

    
2360

    
2361
	-- set state as inactive 
2362
	idA_A2_2
2363
	 = if (not isInner) then 0 else idA_A2_1;
2364

    
2365

    
2366
	(idA_A2) 
2367
	= (idA_A2_1);
2368
	
2369

    
2370
tel
2371

    
2372

    
2373

    
2374

    
2375

    
2376

    
2377
-- Entry action for state :A_A2
2378
node A_A2_en(idA_A2_1:int;
2379
	idParallel2_A_1:int;
2380
	a_1:int;
2381
	x:int;
2382
	isInner:bool)
2383

    
2384
returns (idA_A2:int;
2385
	idParallel2_A:int;
2386
	a:int);
2387

    
2388

    
2389
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int;
2390
	idParallel2_A_2, idParallel2_A_3, idParallel2_A_4:int;
2391
	a_2, a_3, a_4, a_5, a_6:int;
2392

    
2393

    
2394
let
2395

    
2396

    
2397

    
2398
	-- set state as active 
2399
	idParallel2_A_2 
2400
	= 1420;
2401
	
2402

    
2403
	
2404
-- transition trace :
2405
	--POINT__To__A2_A2a_1
2406
		(idA_A2_2, a_2) 
2407
	= A2_A2a_en(idA_A2_1, x, a_1, false);
2408
		
2409

    
2410
	(idA_A2_3, idParallel2_A_3, a_3) 
2411
	= 
2412

    
2413
	if ( idA_A2_1 = 0) then
2414

    
2415
	 (idA_A2_2, idParallel2_A_2, a_2)
2416

    
2417
	 else(idA_A2_1, idParallel2_A_2, a_1);
2418

    
2419
	
2420

    
2421
	(idA_A2_4, a_4) 
2422
	= 
2423
	if ( idA_A2_1 = 1421) then
2424
	A2_A2a_en(idA_A2_1, x, a_1, false)
2425
	 else (idA_A2_1, a_1);
2426

    
2427
	
2428

    
2429
	(idA_A2_5, a_5) 
2430
	= 
2431
	if ( idA_A2_1 = 1422) then
2432
	A2_A2b_en(idA_A2_1, x, a_1, false)
2433
	 else (idA_A2_1, a_1);
2434

    
2435
	
2436

    
2437
	(idA_A2_6, idParallel2_A_4, a_6) 
2438
	= 
2439
		 if ( idA_A2_1 = 0) then 
2440
		(idA_A2_3, idParallel2_A_3, a_3)
2441
		 else
2442
		 if ( idA_A2_1 = 1421) then 
2443
		(idA_A2_4, idParallel2_A_3, a_4)
2444
		 else
2445
		 if ( idA_A2_1 = 1422) then 
2446
		(idA_A2_5, idParallel2_A_3, a_5)
2447
		 else (idA_A2_1, idParallel2_A_2, a_1);
2448

    
2449

    
2450
	(idA_A2, idParallel2_A, a) 
2451
	= (idA_A2_6, idParallel2_A_4, a_6);
2452
	
2453

    
2454
tel
2455

    
2456

    
2457

    
2458

    
2459

    
2460
-- Exit action for state :A_A2
2461
node A_A2_ex(idA_A2_1:int;
2462
	idParallel2_A_1:int;
2463
	isInner:bool)
2464

    
2465
returns (idA_A2:int;
2466
	idParallel2_A:int);
2467

    
2468

    
2469
var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int;
2470
	idParallel2_A_2:int;
2471

    
2472

    
2473
let
2474

    
2475

    
2476

    
2477
	
2478
	(idA_A2_2) 
2479
	= 
2480
	if ( idA_A2_1 = 1421) then
2481
	A2_A2a_ex(idA_A2_1, false)
2482
	 else (idA_A2_1);
2483

    
2484
	
2485

    
2486
	(idA_A2_3) 
2487
	= 
2488
	if ( idA_A2_1 = 1422) then
2489
	A2_A2b_ex(idA_A2_1, false)
2490
	 else (idA_A2_1);
2491

    
2492
	
2493

    
2494
	(idA_A2_4) 
2495
	= 
2496
		 if ( idA_A2_1 = 1421) then 
2497
		(idA_A2_2)
2498
		 else
2499
		 if ( idA_A2_1 = 1422) then 
2500
		(idA_A2_3)
2501
		 else (idA_A2_1);
2502

    
2503

    
2504
	-- set state as inactive 
2505
	idParallel2_A_2
2506
	 = if (not isInner) then 0 else idParallel2_A_1;
2507

    
2508
	idA_A2_5 
2509
	= 0;
2510
	
2511

    
2512
	(idA_A2, idParallel2_A) 
2513
	= (idA_A2_5, idParallel2_A_1);
2514
	
2515

    
2516
tel
2517

    
2518

    
2519

    
2520

    
2521

    
2522

    
2523
-- Entry action for state :A1_A1a
2524
node A1_A1a_en(idA_A1_1:int;
2525
	x:int;
2526
	a_1:int;
2527
	isInner:bool)
2528

    
2529
returns (idA_A1:int;
2530
	a:int);
2531

    
2532

    
2533
var 	idA_A1_2:int;
2534
	a_2:int;
2535

    
2536

    
2537
let
2538

    
2539

    
2540

    
2541
	-- set state as active 
2542
	idA_A1_2 
2543
	= 1418;
2544
	
2545

    
2546
	a_2 
2547
	= if (not isInner) then x+1
2548
	 else a_1;
2549
	
2550

    
2551
	(idA_A1, a) 
2552
	= (idA_A1_2, a_2);
2553
	
2554

    
2555
tel
2556

    
2557

    
2558

    
2559

    
2560

    
2561
-- Exit action for state :A1_A1a
2562
node A1_A1a_ex(idA_A1_1:int;
2563
	isInner:bool)
2564

    
2565
returns (idA_A1:int);
2566

    
2567

    
2568
var 	idA_A1_2:int;
2569

    
2570

    
2571
let
2572

    
2573

    
2574

    
2575
	-- set state as inactive 
2576
	idA_A1_2
2577
	 = if (not isInner) then 0 else idA_A1_1;
2578

    
2579

    
2580
	(idA_A1) 
2581
	= (idA_A1_1);
2582
	
2583

    
2584
tel
2585

    
2586

    
2587

    
2588

    
2589

    
2590

    
2591
-- Entry action for state :A1_A1b
2592
node A1_A1b_en(idA_A1_1:int;
2593
	x:int;
2594
	a_1:int;
2595
	isInner:bool)
2596

    
2597
returns (idA_A1:int;
2598
	a:int);
2599

    
2600

    
2601
var 	idA_A1_2:int;
2602
	a_2:int;
2603

    
2604

    
2605
let
2606

    
2607

    
2608

    
2609
	-- set state as active 
2610
	idA_A1_2 
2611
	= 1419;
2612
	
2613

    
2614
	a_2 
2615
	= if (not isInner) then x+2
2616
	 else a_1;
2617
	
2618

    
2619
	(idA_A1, a) 
2620
	= (idA_A1_2, a_2);
2621
	
2622

    
2623
tel
2624

    
2625

    
2626

    
2627

    
2628

    
2629
-- Exit action for state :A1_A1b
2630
node A1_A1b_ex(idA_A1_1:int;
2631
	isInner:bool)
2632

    
2633
returns (idA_A1:int);
2634

    
2635

    
2636
var 	idA_A1_2:int;
2637

    
2638

    
2639
let
2640

    
2641

    
2642

    
2643
	-- set state as inactive 
2644
	idA_A1_2
2645
	 = if (not isInner) then 0 else idA_A1_1;
2646

    
2647

    
2648
	(idA_A1) 
2649
	= (idA_A1_1);
2650
	
2651

    
2652
tel
2653

    
2654

    
2655

    
2656

    
2657

    
2658

    
2659
-- Entry action for state :A_A1
2660
node A_A1_en(idA_A1_1:int;
2661
	idParallel2_A_1:int;
2662
	a_1:int;
2663
	x:int;
2664
	isInner:bool)
2665

    
2666
returns (idA_A1:int;
2667
	idParallel2_A:int;
2668
	a:int);
2669

    
2670

    
2671
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int;
2672
	idParallel2_A_2, idParallel2_A_3, idParallel2_A_4:int;
2673
	a_2, a_3, a_4, a_5, a_6:int;
2674

    
2675

    
2676
let
2677

    
2678

    
2679

    
2680
	-- set state as active 
2681
	idParallel2_A_2 
2682
	= 1417;
2683
	
2684

    
2685
	
2686
-- transition trace :
2687
	--POINT__To__A1_A1a_1
2688
		(idA_A1_2, a_2) 
2689
	= A1_A1a_en(idA_A1_1, x, a_1, false);
2690
		
2691

    
2692
	(idA_A1_3, idParallel2_A_3, a_3) 
2693
	= 
2694

    
2695
	if ( idA_A1_1 = 0) then
2696

    
2697
	 (idA_A1_2, idParallel2_A_2, a_2)
2698

    
2699
	 else(idA_A1_1, idParallel2_A_2, a_1);
2700

    
2701
	
2702

    
2703
	(idA_A1_4, a_4) 
2704
	= 
2705
	if ( idA_A1_1 = 1418) then
2706
	A1_A1a_en(idA_A1_1, x, a_1, false)
2707
	 else (idA_A1_1, a_1);
2708

    
2709
	
2710

    
2711
	(idA_A1_5, a_5) 
2712
	= 
2713
	if ( idA_A1_1 = 1419) then
2714
	A1_A1b_en(idA_A1_1, x, a_1, false)
2715
	 else (idA_A1_1, a_1);
2716

    
2717
	
2718

    
2719
	(idA_A1_6, idParallel2_A_4, a_6) 
2720
	= 
2721
		 if ( idA_A1_1 = 0) then 
2722
		(idA_A1_3, idParallel2_A_3, a_3)
2723
		 else
2724
		 if ( idA_A1_1 = 1418) then 
2725
		(idA_A1_4, idParallel2_A_3, a_4)
2726
		 else
2727
		 if ( idA_A1_1 = 1419) then 
2728
		(idA_A1_5, idParallel2_A_3, a_5)
2729
		 else (idA_A1_1, idParallel2_A_2, a_1);
2730

    
2731

    
2732
	(idA_A1, idParallel2_A, a) 
2733
	= (idA_A1_6, idParallel2_A_4, a_6);
2734
	
2735

    
2736
tel
2737

    
2738

    
2739

    
2740

    
2741

    
2742
-- Exit action for state :A_A1
2743
node A_A1_ex(idA_A1_1:int;
2744
	idParallel2_A_1:int;
2745
	isInner:bool)
2746

    
2747
returns (idA_A1:int;
2748
	idParallel2_A:int);
2749

    
2750

    
2751
var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2752
	idParallel2_A_2:int;
2753

    
2754

    
2755
let
2756

    
2757

    
2758

    
2759
	
2760
	(idA_A1_2) 
2761
	= 
2762
	if ( idA_A1_1 = 1418) then
2763
	A1_A1a_ex(idA_A1_1, false)
2764
	 else (idA_A1_1);
2765

    
2766
	
2767

    
2768
	(idA_A1_3) 
2769
	= 
2770
	if ( idA_A1_1 = 1419) then
2771
	A1_A1b_ex(idA_A1_1, false)
2772
	 else (idA_A1_1);
2773

    
2774
	
2775

    
2776
	(idA_A1_4) 
2777
	= 
2778
		 if ( idA_A1_1 = 1418) then 
2779
		(idA_A1_2)
2780
		 else
2781
		 if ( idA_A1_1 = 1419) then 
2782
		(idA_A1_3)
2783
		 else (idA_A1_1);
2784

    
2785

    
2786
	-- set state as inactive 
2787
	idParallel2_A_2
2788
	 = if (not isInner) then 0 else idParallel2_A_1;
2789

    
2790
	idA_A1_5 
2791
	= 0;
2792
	
2793

    
2794
	(idA_A1, idParallel2_A) 
2795
	= (idA_A1_5, idParallel2_A_1);
2796
	
2797

    
2798
tel
2799

    
2800

    
2801

    
2802

    
2803

    
2804

    
2805
-- Entry action for state :Parallel2_A
2806
node Parallel2_A_en(idParallel2_A_1:int;
2807
	idParallel2_Parallel2_1:int;
2808
	a_1:int;
2809
	idA_A1_1:int;
2810
	x:int;
2811
	idA_A2_1:int;
2812
	isInner:bool)
2813

    
2814
returns (idParallel2_A:int;
2815
	idParallel2_Parallel2:int;
2816
	a:int;
2817
	idA_A1:int;
2818
	idA_A2:int);
2819

    
2820

    
2821
var 	idParallel2_A_2, idParallel2_A_3, idParallel2_A_4, idParallel2_A_5, idParallel2_A_6:int;
2822
	idParallel2_Parallel2_2, idParallel2_Parallel2_3, idParallel2_Parallel2_4:int;
2823
	a_2, a_3, a_4, a_5, a_6:int;
2824
	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
2825
	idA_A2_2, idA_A2_3:int;
2826

    
2827

    
2828
let
2829

    
2830

    
2831

    
2832
	-- set state as active 
2833
	idParallel2_Parallel2_2 
2834
	= 1416;
2835
	
2836

    
2837
	
2838
-- transition trace :
2839
	--POINT__To__A_A1_1
2840
		(idA_A1_2, idParallel2_A_2, a_2) 
2841
	= A_A1_en(idA_A1_1, idParallel2_A_1, a_1, x, false);
2842
		
2843

    
2844
	(idParallel2_A_3, idParallel2_Parallel2_3, a_3, idA_A1_3) 
2845
	= 
2846

    
2847
	if ( idParallel2_A_1 = 0) then
2848

    
2849
	 (idParallel2_A_2, idParallel2_Parallel2_2, a_2, idA_A1_2)
2850

    
2851
	 else(idParallel2_A_1, idParallel2_Parallel2_2, a_1, idA_A1_1);
2852

    
2853
	
2854

    
2855
	(idA_A2_2, idParallel2_A_4, a_4) 
2856
	= 
2857
	if ( idParallel2_A_1 = 1420) then
2858
	A_A2_en(idA_A2_1, idParallel2_A_1, a_1, x, false)
2859
	 else (idA_A2_1, idParallel2_A_1, a_1);
2860

    
2861
	
2862

    
2863
	(idA_A1_4, idParallel2_A_5, a_5) 
2864
	= 
2865
	if ( idParallel2_A_1 = 1417) then
2866
	A_A1_en(idA_A1_1, idParallel2_A_1, a_1, x, false)
2867
	 else (idA_A1_1, idParallel2_A_1, a_1);
2868

    
2869
	
2870

    
2871
	(idParallel2_A_6, idParallel2_Parallel2_4, a_6, idA_A1_5, idA_A2_3) 
2872
	= 
2873
		 if ( idParallel2_A_1 = 0) then 
2874
		(idParallel2_A_3, idParallel2_Parallel2_3, a_3, idA_A1_3, idA_A2_1)
2875
		 else
2876
		 if ( idParallel2_A_1 = 1420) then 
2877
		(idParallel2_A_4, idParallel2_Parallel2_3, a_4, idA_A1_1, idA_A2_2)
2878
		 else
2879
		 if ( idParallel2_A_1 = 1417) then 
2880
		(idParallel2_A_5, idParallel2_Parallel2_3, a_5, idA_A1_4, idA_A2_1)
2881
		 else (idParallel2_A_1, idParallel2_Parallel2_2, a_1, idA_A1_1, idA_A2_1);
2882

    
2883

    
2884
	(idParallel2_A, idParallel2_Parallel2, a, idA_A1, idA_A2) 
2885
	= (idParallel2_A_6, idParallel2_Parallel2_4, a_6, idA_A1_5, idA_A2_3);
2886
	
2887

    
2888
tel
2889

    
2890

    
2891

    
2892

    
2893

    
2894
-- Exit action for state :Parallel2_A
2895
node Parallel2_A_ex(idA_A2_1:int;
2896
	idParallel2_A_1:int;
2897
	idA_A1_1:int;
2898
	idParallel2_Parallel2_1:int;
2899
	isInner:bool)
2900

    
2901
returns (idA_A2:int;
2902
	idParallel2_A:int;
2903
	idA_A1:int;
2904
	idParallel2_Parallel2:int);
2905

    
2906

    
2907
var 	idA_A2_2, idA_A2_3:int;
2908
	idParallel2_A_2, idParallel2_A_3, idParallel2_A_4, idParallel2_A_5:int;
2909
	idA_A1_2, idA_A1_3:int;
2910
	idParallel2_Parallel2_2:int;
2911

    
2912

    
2913
let
2914

    
2915

    
2916

    
2917
	
2918
	(idA_A2_2, idParallel2_A_2) 
2919
	= 
2920
	if ( idParallel2_A_1 = 1420) then
2921
	A_A2_ex(idA_A2_1, idParallel2_A_1, false)
2922
	 else (idA_A2_1, idParallel2_A_1);
2923

    
2924
	
2925

    
2926
	(idA_A1_2, idParallel2_A_3) 
2927
	= 
2928
	if ( idParallel2_A_1 = 1417) then
2929
	A_A1_ex(idA_A1_1, idParallel2_A_1, false)
2930
	 else (idA_A1_1, idParallel2_A_1);
2931

    
2932
	
2933

    
2934
	(idA_A2_3, idParallel2_A_4, idA_A1_3) 
2935
	= 
2936
		 if ( idParallel2_A_1 = 1420) then 
2937
		(idA_A2_2, idParallel2_A_2, idA_A1_1)
2938
		 else
2939
		 if ( idParallel2_A_1 = 1417) then 
2940
		(idA_A2_1, idParallel2_A_3, idA_A1_2)
2941
		 else (idA_A2_1, idParallel2_A_1, idA_A1_1);
2942

    
2943

    
2944
	-- set state as inactive 
2945
	idParallel2_Parallel2_2
2946
	 = if (not isInner) then 0 else idParallel2_Parallel2_1;
2947

    
2948
	idParallel2_A_5 
2949
	= 0;
2950
	
2951

    
2952
	(idA_A2, idParallel2_A, idA_A1, idParallel2_Parallel2) 
2953
	= (idA_A2_3, idParallel2_A_5, idA_A1_3, idParallel2_Parallel2_1);
2954
	
2955

    
2956
tel
2957

    
2958

    
2959
--***************************************************State :B_B2 Automaton***************************************************
2960

    
2961
node B_B2_node(idB_B2_1:int;
2962
	a_1:int;
2963
	b_1:int;
2964
	S:bool;
2965
	R:bool)
2966

    
2967
returns (idB_B2:int;
2968
	a:int;
2969
	b:int);
2970

    
2971

    
2972
let
2973

    
2974
	 automaton b_b2
2975

    
2976
	state POINTB_B2:
2977
	unless (idB_B2_1=0) restart POINT__TO__B2_B2A_1
2978

    
2979

    
2980

    
2981
	unless (idB_B2_1=1425) and S restart B2_B2A__TO__B2_B2B_1
2982

    
2983

    
2984

    
2985
	unless (idB_B2_1=1426) and R restart B2_B2B__TO__B2_B2A_1
2986

    
2987

    
2988

    
2989
	unless (idB_B2_1=1425) restart B2_B2A_IDL
2990

    
2991
	unless (idB_B2_1=1426) restart B2_B2B_IDL
2992

    
2993
	let
2994

    
2995
		(idB_B2, a, b) 
2996
	= (idB_B2_1, a_1, b_1);
2997
	
2998

    
2999
	tel
3000

    
3001

    
3002

    
3003
	state POINT__TO__B2_B2A_1:
3004

    
3005
	 var 	idB_B2_2:int;
3006
	a_2:int;
3007
	b_2:int;
3008
	let
3009

    
3010
		-- transition trace :
3011
	--POINT__To__B2_B2a_1
3012
		(idB_B2_2, a_2, b_2) 
3013
	= B2_B2a_en(idB_B2_1, a_1, b_1, false);
3014
		
3015

    
3016
	(idB_B2, a, b) 
3017
	=  (idB_B2_2, a_2, b_2);
3018

    
3019

    
3020
	tel
3021

    
3022
	until true restart POINTB_B2
3023

    
3024

    
3025

    
3026
	state B2_B2A__TO__B2_B2B_1:
3027

    
3028
	 var 	idB_B2_2, idB_B2_3:int;
3029
	a_2:int;
3030
	b_2:int;
3031
	let
3032

    
3033
		-- transition trace :
3034
	--B2_B2a__To__B2_B2b_1
3035
		(idB_B2_2) 
3036
	= B2_B2a_ex(idB_B2_1, false);
3037
		
3038

    
3039
		(idB_B2_3, a_2, b_2) 
3040
	= B2_B2b_en(idB_B2_2, a_1, b_1, false);
3041
		
3042

    
3043
	(idB_B2, a, b) 
3044
	=  (idB_B2_3, a_2, b_2);
3045

    
3046

    
3047
	tel
3048

    
3049
	until true restart POINTB_B2
3050

    
3051

    
3052

    
3053
	state B2_B2B__TO__B2_B2A_1:
3054

    
3055
	 var 	idB_B2_2, idB_B2_3:int;
3056
	a_2:int;
3057
	b_2:int;
3058
	let
3059

    
3060
		-- transition trace :
3061
	--B2_B2b__To__B2_B2a_1
3062
		(idB_B2_2) 
3063
	= B2_B2b_ex(idB_B2_1, false);
3064
		
3065

    
3066
		(idB_B2_3, a_2, b_2) 
3067
	= B2_B2a_en(idB_B2_2, a_1, b_1, false);
3068
		
3069

    
3070
	(idB_B2, a, b) 
3071
	=  (idB_B2_3, a_2, b_2);
3072

    
3073

    
3074
	tel
3075

    
3076
	until true restart POINTB_B2
3077

    
3078

    
3079

    
3080
	state B2_B2A_IDL:
3081

    
3082
	 	let
3083

    
3084
		
3085

    
3086
	(idB_B2, a, b) 
3087
	= (idB_B2_1, a_1, b_1);
3088
	
3089

    
3090
	tel
3091

    
3092
	until true restart POINTB_B2
3093

    
3094

    
3095

    
3096
	state B2_B2B_IDL:
3097

    
3098
	 	let
3099

    
3100
		
3101

    
3102
	(idB_B2, a, b) 
3103
	= (idB_B2_1, a_1, b_1);
3104
	
3105

    
3106
	tel
3107

    
3108
	until true restart POINTB_B2
3109

    
3110

    
3111

    
3112
tel
3113

    
3114

    
3115
--***************************************************State :B_B1 Automaton***************************************************
3116

    
3117
node B_B1_node(idB_B1_1:int;
3118
	a_1:int;
3119
	b_1:int;
3120
	S:bool;
3121
	R:bool)
3122

    
3123
returns (idB_B1:int;
3124
	a:int;
3125
	b:int);
3126

    
3127

    
3128
let
3129

    
3130
	 automaton b_b1
3131

    
3132
	state POINTB_B1:
3133
	unless (idB_B1_1=0) restart POINT__TO__B1_B1A_1
3134

    
3135

    
3136

    
3137
	unless (idB_B1_1=1428) and S restart B1_B1A__TO__B1_B1B_1
3138

    
3139

    
3140

    
3141
	unless (idB_B1_1=1429) and R restart B1_B1B__TO__B1_B1A_1
3142

    
3143

    
3144

    
3145
	unless (idB_B1_1=1428) restart B1_B1A_IDL
3146

    
3147
	unless (idB_B1_1=1429) restart B1_B1B_IDL
3148

    
3149
	let
3150

    
3151
		(idB_B1, a, b) 
3152
	= (idB_B1_1, a_1, b_1);
3153
	
3154

    
3155
	tel
3156

    
3157

    
3158

    
3159
	state POINT__TO__B1_B1A_1:
3160

    
3161
	 var 	idB_B1_2:int;
3162
	a_2:int;
3163
	b_2:int;
3164
	let
3165

    
3166
		-- transition trace :
3167
	--POINT__To__B1_B1a_1
3168
		(idB_B1_2, a_2, b_2) 
3169
	= B1_B1a_en(idB_B1_1, a_1, b_1, false);
3170
		
3171

    
3172
	(idB_B1, a, b) 
3173
	=  (idB_B1_2, a_2, b_2);
3174

    
3175

    
3176
	tel
3177

    
3178
	until true restart POINTB_B1
3179

    
3180

    
3181

    
3182
	state B1_B1A__TO__B1_B1B_1:
3183

    
3184
	 var 	idB_B1_2, idB_B1_3:int;
3185
	a_2:int;
3186
	b_2:int;
3187
	let
3188

    
3189
		-- transition trace :
3190
	--B1_B1a__To__B1_B1b_1
3191
		(idB_B1_2) 
3192
	= B1_B1a_ex(idB_B1_1, false);
3193
		
3194

    
3195
		(idB_B1_3, a_2, b_2) 
3196
	= B1_B1b_en(idB_B1_2, a_1, b_1, false);
3197
		
3198

    
3199
	(idB_B1, a, b) 
3200
	=  (idB_B1_3, a_2, b_2);
3201

    
3202

    
3203
	tel
3204

    
3205
	until true restart POINTB_B1
3206

    
3207

    
3208

    
3209
	state B1_B1B__TO__B1_B1A_1:
3210

    
3211
	 var 	idB_B1_2, idB_B1_3:int;
3212
	a_2:int;
3213
	b_2:int;
3214
	let
3215

    
3216
		-- transition trace :
3217
	--B1_B1b__To__B1_B1a_1
3218
		(idB_B1_2) 
3219
	= B1_B1b_ex(idB_B1_1, false);
3220
		
3221

    
3222
		(idB_B1_3, a_2, b_2) 
3223
	= B1_B1a_en(idB_B1_2, a_1, b_1, false);
3224
		
3225

    
3226
	(idB_B1, a, b) 
3227
	=  (idB_B1_3, a_2, b_2);
3228

    
3229

    
3230
	tel
3231

    
3232
	until true restart POINTB_B1
3233

    
3234

    
3235

    
3236
	state B1_B1A_IDL:
3237

    
3238
	 	let
3239

    
3240
		
3241

    
3242
	(idB_B1, a, b) 
3243
	= (idB_B1_1, a_1, b_1);
3244
	
3245

    
3246
	tel
3247

    
3248
	until true restart POINTB_B1
3249

    
3250

    
3251

    
3252
	state B1_B1B_IDL:
3253

    
3254
	 	let
3255

    
3256
		
3257

    
3258
	(idB_B1, a, b) 
3259
	= (idB_B1_1, a_1, b_1);
3260
	
3261

    
3262
	tel
3263

    
3264
	until true restart POINTB_B1
3265

    
3266

    
3267

    
3268
tel
3269

    
3270

    
3271
--***************************************************State :Parallel2_B Automaton***************************************************
3272

    
3273
node Parallel2_B_node(idParallel2_B_1:int;
3274
	a_1:int;
3275
	b_1:int;
3276
	idB_B1_1:int;
3277
	T:bool;
3278
	idB_B2_1:int;
3279
	R:bool;
3280
	S:bool)
3281

    
3282
returns (idParallel2_B:int;
3283
	a:int;
3284
	b:int;
3285
	idB_B1:int;
3286
	idB_B2:int);
3287

    
3288

    
3289
let
3290

    
3291
	 automaton parallel2_b
3292

    
3293
	state POINTParallel2_B:
3294
	unless (idParallel2_B_1=0) restart POINT__TO__B_B1_1
3295

    
3296

    
3297

    
3298
	unless (idParallel2_B_1=1424) and T restart B_B2__TO__B_B1_1
3299

    
3300

    
3301

    
3302
	unless (idParallel2_B_1=1427) and T restart B_B1__TO__B_B2_1
3303

    
3304

    
3305

    
3306
	unless (idParallel2_B_1=1424) restart B_B2_IDL
3307

    
3308
	unless (idParallel2_B_1=1427) restart B_B1_IDL
3309

    
3310
	let
3311

    
3312
		(idParallel2_B, a, b, idB_B1, idB_B2) 
3313
	= (idParallel2_B_1, a_1, b_1, idB_B1_1, idB_B2_1);
3314
	
3315

    
3316
	tel
3317

    
3318

    
3319

    
3320
	state POINT__TO__B_B1_1:
3321

    
3322
	 var 	idParallel2_B_2:int;
3323
	a_2:int;
3324
	b_2:int;
3325
	idB_B1_2:int;
3326
	let
3327

    
3328
		-- transition trace :
3329
	--POINT__To__B_B1_1
3330
		(idB_B1_2, idParallel2_B_2, a_2, b_2) 
3331
	= B_B1_en(idB_B1_1, idParallel2_B_1, a_1, b_1, false);
3332
		
3333

    
3334
	(idParallel2_B, a, b, idB_B1) 
3335
	=  (idParallel2_B_2, a_2, b_2, idB_B1_2);
3336

    
3337
	--add unused variables
3338
	(idB_B2) 
3339
	= (idB_B2_1);
3340
	
3341

    
3342
	tel
3343

    
3344
	until true restart POINTParallel2_B
3345

    
3346

    
3347

    
3348
	state B_B2__TO__B_B1_1:
3349

    
3350
	 var 	idParallel2_B_2, idParallel2_B_3:int;
3351
	a_2:int;
3352
	b_2:int;
3353
	idB_B1_2:int;
3354
	idB_B2_2:int;
3355
	let
3356

    
3357
		-- transition trace :
3358
	--B_B2__To__B_B1_1
3359
		(idB_B2_2, idParallel2_B_2) 
3360
	= B_B2_ex(idB_B2_1, idParallel2_B_1, false);
3361
		
3362

    
3363
		(idB_B1_2, idParallel2_B_3, a_2, b_2) 
3364
	= B_B1_en(idB_B1_1, idParallel2_B_2, a_1, b_1, false);
3365
		
3366

    
3367
	(idParallel2_B, a, b, idB_B1, idB_B2) 
3368
	=  (idParallel2_B_3, a_2, b_2, idB_B1_2, idB_B2_2);
3369

    
3370

    
3371
	tel
3372

    
3373
	until true restart POINTParallel2_B
3374

    
3375

    
3376

    
3377
	state B_B1__TO__B_B2_1:
3378

    
3379
	 var 	idParallel2_B_2, idParallel2_B_3:int;
3380
	a_2:int;
3381
	b_2:int;
3382
	idB_B1_2:int;
3383
	idB_B2_2:int;
3384
	let
3385

    
3386
		-- transition trace :
3387
	--B_B1__To__B_B2_1
3388
		(idB_B1_2, idParallel2_B_2) 
3389
	= B_B1_ex(idB_B1_1, idParallel2_B_1, false);
3390
		
3391

    
3392
		(idB_B2_2, idParallel2_B_3, a_2, b_2) 
3393
	= B_B2_en(idB_B2_1, idParallel2_B_2, a_1, b_1, false);
3394
		
3395

    
3396
	(idParallel2_B, a, b, idB_B1, idB_B2) 
3397
	=  (idParallel2_B_3, a_2, b_2, idB_B1_2, idB_B2_2);
3398

    
3399

    
3400
	tel
3401

    
3402
	until true restart POINTParallel2_B
3403

    
3404

    
3405

    
3406
	state B_B2_IDL:
3407

    
3408
	 var 	a_2:int;
3409
	b_2:int;
3410
	idB_B2_2:int;
3411
	let
3412

    
3413
		
3414
	(idB_B2_2, a_2, b_2) 
3415
	= B_B2_node(idB_B2_1, a_1, b_1, S, R);
3416

    
3417
		
3418

    
3419

    
3420
	(idParallel2_B, a, b, idB_B1, idB_B2) 
3421
	= (idParallel2_B_1, a_2, b_2, idB_B1_1, idB_B2_2);
3422
	
3423

    
3424
	tel
3425

    
3426
	until true restart POINTParallel2_B
3427

    
3428

    
3429

    
3430
	state B_B1_IDL:
3431

    
3432
	 var 	a_2:int;
3433
	b_2:int;
3434
	idB_B1_2:int;
3435
	let
3436

    
3437
		
3438
	(idB_B1_2, a_2, b_2) 
3439
	= B_B1_node(idB_B1_1, a_1, b_1, S, R);
3440

    
3441
		
3442

    
3443

    
3444
	(idParallel2_B, a, b, idB_B1, idB_B2) 
3445
	= (idParallel2_B_1, a_2, b_2, idB_B1_2, idB_B2_1);
3446
	
3447

    
3448
	tel
3449

    
3450
	until true restart POINTParallel2_B
3451

    
3452

    
3453

    
3454
tel
3455

    
3456

    
3457
--***************************************************State :D_D2 Automaton***************************************************
3458

    
3459
node D_D2_node(idD_D2_1:int;
3460
	c_1:int;
3461
	dd_1:int;
3462
	S:bool;
3463
	R:bool)
3464

    
3465
returns (idD_D2:int;
3466
	c:int;
3467
	dd:int);
3468

    
3469

    
3470
let
3471

    
3472
	 automaton d_d2
3473

    
3474
	state POINTD_D2:
3475
	unless (idD_D2_1=0) restart POINT__TO__D2_D2A_1
3476

    
3477

    
3478

    
3479
	unless (idD_D2_1=1439) and S restart D2_D2A__TO__D2_D2B_1
3480

    
3481

    
3482

    
3483
	unless (idD_D2_1=1440) and R restart D2_D2B__TO__D2_D2A_1
3484

    
3485

    
3486

    
3487
	unless (idD_D2_1=1439) restart D2_D2A_IDL
3488

    
3489
	unless (idD_D2_1=1440) restart D2_D2B_IDL
3490

    
3491
	let
3492

    
3493
		(idD_D2, c, dd) 
3494
	= (idD_D2_1, c_1, dd_1);
3495
	
3496

    
3497
	tel
3498

    
3499

    
3500

    
3501
	state POINT__TO__D2_D2A_1:
3502

    
3503
	 var 	idD_D2_2:int;
3504
	c_2:int;
3505
	dd_2:int;
3506
	let
3507

    
3508
		-- transition trace :
3509
	--POINT__To__D2_D2a_1
3510
		(idD_D2_2, c_2, dd_2) 
3511
	= D2_D2a_en(idD_D2_1, c_1, dd_1, false);
3512
		
3513

    
3514
	(idD_D2, c, dd) 
3515
	=  (idD_D2_2, c_2, dd_2);
3516

    
3517

    
3518
	tel
3519

    
3520
	until true restart POINTD_D2
3521

    
3522

    
3523

    
3524
	state D2_D2A__TO__D2_D2B_1:
3525

    
3526
	 var 	idD_D2_2, idD_D2_3:int;
3527
	c_2:int;
3528
	dd_2:int;
3529
	let
3530

    
3531
		-- transition trace :
3532
	--D2_D2a__To__D2_D2b_1
3533
		(idD_D2_2) 
3534
	= D2_D2a_ex(idD_D2_1, false);
3535
		
3536

    
3537
		(idD_D2_3, c_2, dd_2) 
3538
	= D2_D2b_en(idD_D2_2, c_1, dd_1, false);
3539
		
3540

    
3541
	(idD_D2, c, dd) 
3542
	=  (idD_D2_3, c_2, dd_2);
3543

    
3544

    
3545
	tel
3546

    
3547
	until true restart POINTD_D2
3548

    
3549

    
3550

    
3551
	state D2_D2B__TO__D2_D2A_1:
3552

    
3553
	 var 	idD_D2_2, idD_D2_3:int;
3554
	c_2:int;
3555
	dd_2:int;
3556
	let
3557

    
3558
		-- transition trace :
3559
	--D2_D2b__To__D2_D2a_1
3560
		(idD_D2_2) 
3561
	= D2_D2b_ex(idD_D2_1, false);
3562
		
3563

    
3564
		(idD_D2_3, c_2, dd_2) 
3565
	= D2_D2a_en(idD_D2_2, c_1, dd_1, false);
3566
		
3567

    
3568
	(idD_D2, c, dd) 
3569
	=  (idD_D2_3, c_2, dd_2);
3570

    
3571

    
3572
	tel
3573

    
3574
	until true restart POINTD_D2
3575

    
3576

    
3577

    
3578
	state D2_D2A_IDL:
3579

    
3580
	 	let
3581

    
3582
		
3583

    
3584
	(idD_D2, c, dd) 
3585
	= (idD_D2_1, c_1, dd_1);
3586
	
3587

    
3588
	tel
3589

    
3590
	until true restart POINTD_D2
3591

    
3592

    
3593

    
3594
	state D2_D2B_IDL:
3595

    
3596
	 	let
3597

    
3598
		
3599

    
3600
	(idD_D2, c, dd) 
3601
	= (idD_D2_1, c_1, dd_1);
3602
	
3603

    
3604
	tel
3605

    
3606
	until true restart POINTD_D2
3607

    
3608

    
3609

    
3610
tel
3611

    
3612

    
3613
--***************************************************State :D_D1 Automaton***************************************************
3614

    
3615
node D_D1_node(idD_D1_1:int;
3616
	c_1:int;
3617
	dd_1:int;
3618
	S:bool;
3619
	R:bool)
3620

    
3621
returns (idD_D1:int;
3622
	c:int;
3623
	dd:int);
3624

    
3625

    
3626
let
3627

    
3628
	 automaton d_d1
3629

    
3630
	state POINTD_D1:
3631
	unless (idD_D1_1=0) restart POINT__TO__D1_D1A_1
3632

    
3633

    
3634

    
3635
	unless (idD_D1_1=1442) and S restart D1_D1A__TO__D1_D1B_1
3636

    
3637

    
3638

    
3639
	unless (idD_D1_1=1430) and R restart D1_D1B__TO__D1_D1A_1
3640

    
3641

    
3642

    
3643
	unless (idD_D1_1=1442) restart D1_D1A_IDL
3644

    
3645
	unless (idD_D1_1=1430) restart D1_D1B_IDL
3646

    
3647
	let
3648

    
3649
		(idD_D1, c, dd) 
3650
	= (idD_D1_1, c_1, dd_1);
3651
	
3652

    
3653
	tel
3654

    
3655

    
3656

    
3657
	state POINT__TO__D1_D1A_1:
3658

    
3659
	 var 	idD_D1_2:int;
3660
	c_2:int;
3661
	dd_2:int;
3662
	let
3663

    
3664
		-- transition trace :
3665
	--POINT__To__D1_D1a_1
3666
		(idD_D1_2, c_2, dd_2) 
3667
	= D1_D1a_en(idD_D1_1, c_1, dd_1, false);
3668
		
3669

    
3670
	(idD_D1, c, dd) 
3671
	=  (idD_D1_2, c_2, dd_2);
3672

    
3673

    
3674
	tel
3675

    
3676
	until true restart POINTD_D1
3677

    
3678

    
3679

    
3680
	state D1_D1A__TO__D1_D1B_1:
3681

    
3682
	 var 	idD_D1_2, idD_D1_3:int;
3683
	c_2:int;
3684
	dd_2:int;
3685
	let
3686

    
3687
		-- transition trace :
3688
	--D1_D1a__To__D1_D1b_1
3689
		(idD_D1_2) 
3690
	= D1_D1a_ex(idD_D1_1, false);
3691
		
3692

    
3693
		(idD_D1_3, c_2, dd_2) 
3694
	= D1_D1b_en(idD_D1_2, c_1, dd_1, false);
3695
		
3696

    
3697
	(idD_D1, c, dd) 
3698
	=  (idD_D1_3, c_2, dd_2);
3699

    
3700

    
3701
	tel
3702

    
3703
	until true restart POINTD_D1
3704

    
3705

    
3706

    
3707
	state D1_D1B__TO__D1_D1A_1:
3708

    
3709
	 var 	idD_D1_2, idD_D1_3:int;
3710
	c_2:int;
3711
	dd_2:int;
3712
	let
3713

    
3714
		-- transition trace :
3715
	--D1_D1b__To__D1_D1a_1
3716
		(idD_D1_2) 
3717
	= D1_D1b_ex(idD_D1_1, false);
3718
		
3719

    
3720
		(idD_D1_3, c_2, dd_2) 
3721
	= D1_D1a_en(idD_D1_2, c_1, dd_1, false);
3722
		
3723

    
3724
	(idD_D1, c, dd) 
3725
	=  (idD_D1_3, c_2, dd_2);
3726

    
3727

    
3728
	tel
3729

    
3730
	until true restart POINTD_D1
3731

    
3732

    
3733

    
3734
	state D1_D1A_IDL:
3735

    
3736
	 	let
3737

    
3738
		
3739

    
3740
	(idD_D1, c, dd) 
3741
	= (idD_D1_1, c_1, dd_1);
3742
	
3743

    
3744
	tel
3745

    
3746
	until true restart POINTD_D1
3747

    
3748

    
3749

    
3750
	state D1_D1B_IDL:
3751

    
3752
	 	let
3753

    
3754
		
3755

    
3756
	(idD_D1, c, dd) 
3757
	= (idD_D1_1, c_1, dd_1);
3758
	
3759

    
3760
	tel
3761

    
3762
	until true restart POINTD_D1
3763

    
3764

    
3765

    
3766
tel
3767

    
3768

    
3769
--***************************************************State :Parallel2_D Automaton***************************************************
3770

    
3771
node Parallel2_D_node(idParallel2_D_1:int;
3772
	c_1:int;
3773
	dd_1:int;
3774
	idD_D1_1:int;
3775
	T:bool;
3776
	idD_D2_1:int;
3777
	R:bool;
3778
	S:bool)
3779

    
3780
returns (idParallel2_D:int;
3781
	c:int;
3782
	dd:int;
3783
	idD_D1:int;
3784
	idD_D2:int);
3785

    
3786

    
3787
let
3788

    
3789
	 automaton parallel2_d
3790

    
3791
	state POINTParallel2_D:
3792
	unless (idParallel2_D_1=0) restart POINT__TO__D_D1_1
3793

    
3794

    
3795

    
3796
	unless (idParallel2_D_1=1438) and T restart D_D2__TO__D_D1_1
3797

    
3798

    
3799

    
3800
	unless (idParallel2_D_1=1441) and T restart D_D1__TO__D_D2_1
3801

    
3802

    
3803

    
3804
	unless (idParallel2_D_1=1438) restart D_D2_IDL
3805

    
3806
	unless (idParallel2_D_1=1441) restart D_D1_IDL
3807

    
3808
	let
3809

    
3810
		(idParallel2_D, c, dd, idD_D1, idD_D2) 
3811
	= (idParallel2_D_1, c_1, dd_1, idD_D1_1, idD_D2_1);
3812
	
3813

    
3814
	tel
3815

    
3816

    
3817

    
3818
	state POINT__TO__D_D1_1:
3819

    
3820
	 var 	idParallel2_D_2:int;
3821
	c_2:int;
3822
	dd_2:int;
3823
	idD_D1_2:int;
3824
	let
3825

    
3826
		-- transition trace :
3827
	--POINT__To__D_D1_1
3828
		(idD_D1_2, idParallel2_D_2, c_2, dd_2) 
3829
	= D_D1_en(idD_D1_1, idParallel2_D_1, c_1, dd_1, false);
3830
		
3831

    
3832
	(idParallel2_D, c, dd, idD_D1) 
3833
	=  (idParallel2_D_2, c_2, dd_2, idD_D1_2);
3834

    
3835
	--add unused variables
3836
	(idD_D2) 
3837
	= (idD_D2_1);
3838
	
3839

    
3840
	tel
3841

    
3842
	until true restart POINTParallel2_D
3843

    
3844

    
3845

    
3846
	state D_D2__TO__D_D1_1:
3847

    
3848
	 var 	idParallel2_D_2, idParallel2_D_3:int;
3849
	c_2:int;
3850
	dd_2:int;
3851
	idD_D1_2:int;
3852
	idD_D2_2:int;
3853
	let
3854

    
3855
		-- transition trace :
3856
	--D_D2__To__D_D1_1
3857
		(idD_D2_2, idParallel2_D_2) 
3858
	= D_D2_ex(idD_D2_1, idParallel2_D_1, false);
3859
		
3860

    
3861
		(idD_D1_2, idParallel2_D_3, c_2, dd_2) 
3862
	= D_D1_en(idD_D1_1, idParallel2_D_2, c_1, dd_1, false);
3863
		
3864

    
3865
	(idParallel2_D, c, dd, idD_D1, idD_D2) 
3866
	=  (idParallel2_D_3, c_2, dd_2, idD_D1_2, idD_D2_2);
3867

    
3868

    
3869
	tel
3870

    
3871
	until true restart POINTParallel2_D
3872

    
3873

    
3874

    
3875
	state D_D1__TO__D_D2_1:
3876

    
3877
	 var 	idParallel2_D_2, idParallel2_D_3:int;
3878
	c_2:int;
3879
	dd_2:int;
3880
	idD_D1_2:int;
3881
	idD_D2_2:int;
3882
	let
3883

    
3884
		-- transition trace :
3885
	--D_D1__To__D_D2_1
3886
		(idD_D1_2, idParallel2_D_2) 
3887
	= D_D1_ex(idD_D1_1, idParallel2_D_1, false);
3888
		
3889

    
3890
		(idD_D2_2, idParallel2_D_3, c_2, dd_2) 
3891
	= D_D2_en(idD_D2_1, idParallel2_D_2, c_1, dd_1, false);
3892
		
3893

    
3894
	(idParallel2_D, c, dd, idD_D1, idD_D2) 
3895
	=  (idParallel2_D_3, c_2, dd_2, idD_D1_2, idD_D2_2);
3896

    
3897

    
3898
	tel
3899

    
3900
	until true restart POINTParallel2_D
3901

    
3902

    
3903

    
3904
	state D_D2_IDL:
3905

    
3906
	 var 	c_2:int;
3907
	dd_2:int;
3908
	idD_D2_2:int;
3909
	let
3910

    
3911
		
3912
	(idD_D2_2, c_2, dd_2) 
3913
	= D_D2_node(idD_D2_1, c_1, dd_1, S, R);
3914

    
3915
		
3916

    
3917

    
3918
	(idParallel2_D, c, dd, idD_D1, idD_D2) 
3919
	= (idParallel2_D_1, c_2, dd_2, idD_D1_1, idD_D2_2);
3920
	
3921

    
3922
	tel
3923

    
3924
	until true restart POINTParallel2_D
3925

    
3926

    
3927

    
3928
	state D_D1_IDL:
3929

    
3930
	 var 	c_2:int;
3931
	dd_2:int;
3932
	idD_D1_2:int;
3933
	let
3934

    
3935
		
3936
	(idD_D1_2, c_2, dd_2) 
3937
	= D_D1_node(idD_D1_1, c_1, dd_1, S, R);
3938

    
3939
		
3940

    
3941

    
3942
	(idParallel2_D, c, dd, idD_D1, idD_D2) 
3943
	= (idParallel2_D_1, c_2, dd_2, idD_D1_2, idD_D2_1);
3944
	
3945

    
3946
	tel
3947

    
3948
	until true restart POINTParallel2_D
3949

    
3950

    
3951

    
3952
tel
3953

    
3954

    
3955
--***************************************************State :C_C2 Automaton***************************************************
3956

    
3957
node C_C2_node(idC_C2_1:int;
3958
	b_1:int;
3959
	c_1:int;
3960
	S:bool;
3961
	R:bool)
3962

    
3963
returns (idC_C2:int;
3964
	b:int;
3965
	c:int);
3966

    
3967

    
3968
let
3969

    
3970
	 automaton c_c2
3971

    
3972
	state POINTC_C2:
3973
	unless (idC_C2_1=0) restart POINT__TO__C2_C2A_1
3974

    
3975

    
3976

    
3977
	unless (idC_C2_1=1432) and S restart C2_C2A__TO__C2_C2B_1
3978

    
3979

    
3980

    
3981
	unless (idC_C2_1=1433) and R restart C2_C2B__TO__C2_C2A_1
3982

    
3983

    
3984

    
3985
	unless (idC_C2_1=1432) restart C2_C2A_IDL
3986

    
3987
	unless (idC_C2_1=1433) restart C2_C2B_IDL
3988

    
3989
	let
3990

    
3991
		(idC_C2, b, c) 
3992
	= (idC_C2_1, b_1, c_1);
3993
	
3994

    
3995
	tel
3996

    
3997

    
3998

    
3999
	state POINT__TO__C2_C2A_1:
4000

    
4001
	 var 	idC_C2_2:int;
4002
	b_2:int;
4003
	c_2:int;
4004
	let
4005

    
4006
		-- transition trace :
4007
	--POINT__To__C2_C2a_1
4008
		(idC_C2_2, b_2, c_2) 
4009
	= C2_C2a_en(idC_C2_1, b_1, c_1, false);
4010
		
4011

    
4012
	(idC_C2, b, c) 
4013
	=  (idC_C2_2, b_2, c_2);
4014

    
4015

    
4016
	tel
4017

    
4018
	until true restart POINTC_C2
4019

    
4020

    
4021

    
4022
	state C2_C2A__TO__C2_C2B_1:
4023

    
4024
	 var 	idC_C2_2, idC_C2_3:int;
4025
	b_2:int;
4026
	c_2:int;
4027
	let
4028

    
4029
		-- transition trace :
4030
	--C2_C2a__To__C2_C2b_1
4031
		(idC_C2_2) 
4032
	= C2_C2a_ex(idC_C2_1, false);
4033
		
4034

    
4035
		(idC_C2_3, b_2, c_2) 
4036
	= C2_C2b_en(idC_C2_2, b_1, c_1, false);
4037
		
4038

    
4039
	(idC_C2, b, c) 
4040
	=  (idC_C2_3, b_2, c_2);
4041

    
4042

    
4043
	tel
4044

    
4045
	until true restart POINTC_C2
4046

    
4047

    
4048

    
4049
	state C2_C2B__TO__C2_C2A_1:
4050

    
4051
	 var 	idC_C2_2, idC_C2_3:int;
4052
	b_2:int;
4053
	c_2:int;
4054
	let
4055

    
4056
		-- transition trace :
4057
	--C2_C2b__To__C2_C2a_1
4058
		(idC_C2_2) 
4059
	= C2_C2b_ex(idC_C2_1, false);
4060
		
4061

    
4062
		(idC_C2_3, b_2, c_2) 
4063
	= C2_C2a_en(idC_C2_2, b_1, c_1, false);
4064
		
4065

    
4066
	(idC_C2, b, c) 
4067
	=  (idC_C2_3, b_2, c_2);
4068

    
4069

    
4070
	tel
4071

    
4072
	until true restart POINTC_C2
4073

    
4074

    
4075

    
4076
	state C2_C2A_IDL:
4077

    
4078
	 	let
4079

    
4080
		
4081

    
4082
	(idC_C2, b, c) 
4083
	= (idC_C2_1, b_1, c_1);
4084
	
4085

    
4086
	tel
4087

    
4088
	until true restart POINTC_C2
4089

    
4090

    
4091

    
4092
	state C2_C2B_IDL:
4093

    
4094
	 	let
4095

    
4096
		
4097

    
4098
	(idC_C2, b, c) 
4099
	= (idC_C2_1, b_1, c_1);
4100
	
4101

    
4102
	tel
4103

    
4104
	until true restart POINTC_C2
4105

    
4106

    
4107

    
4108
tel
4109

    
4110

    
4111
--***************************************************State :C_C1 Automaton***************************************************
4112

    
4113
node C_C1_node(idC_C1_1:int;
4114
	b_1:int;
4115
	c_1:int;
4116
	S:bool;
4117
	R:bool)
4118

    
4119
returns (idC_C1:int;
4120
	b:int;
4121
	c:int);
4122

    
4123

    
4124
let
4125

    
4126
	 automaton c_c1
4127

    
4128
	state POINTC_C1:
4129
	unless (idC_C1_1=0) restart POINT__TO__C1_C1A_1
4130

    
4131

    
4132

    
4133
	unless (idC_C1_1=1435) and S restart C1_C1A__TO__C1_C1B_1
4134

    
4135

    
4136

    
4137
	unless (idC_C1_1=1436) and R restart C1_C1B__TO__C1_C1A_1
4138

    
4139

    
4140

    
4141
	unless (idC_C1_1=1435) restart C1_C1A_IDL
4142

    
4143
	unless (idC_C1_1=1436) restart C1_C1B_IDL
4144

    
4145
	let
4146

    
4147
		(idC_C1, b, c) 
4148
	= (idC_C1_1, b_1, c_1);
4149
	
4150

    
4151
	tel
4152

    
4153

    
4154

    
4155
	state POINT__TO__C1_C1A_1:
4156

    
4157
	 var 	idC_C1_2:int;
4158
	b_2:int;
4159
	c_2:int;
4160
	let
4161

    
4162
		-- transition trace :
4163
	--POINT__To__C1_C1a_1
4164
		(idC_C1_2, b_2, c_2) 
4165
	= C1_C1a_en(idC_C1_1, b_1, c_1, false);
4166
		
4167

    
4168
	(idC_C1, b, c) 
4169
	=  (idC_C1_2, b_2, c_2);
4170

    
4171

    
4172
	tel
4173

    
4174
	until true restart POINTC_C1
4175

    
4176

    
4177

    
4178
	state C1_C1A__TO__C1_C1B_1:
4179

    
4180
	 var 	idC_C1_2, idC_C1_3:int;
4181
	b_2:int;
4182
	c_2:int;
4183
	let
4184

    
4185
		-- transition trace :
4186
	--C1_C1a__To__C1_C1b_1
4187
		(idC_C1_2) 
4188
	= C1_C1a_ex(idC_C1_1, false);
4189
		
4190

    
4191
		(idC_C1_3, b_2, c_2) 
4192
	= C1_C1b_en(idC_C1_2, b_1, c_1, false);
4193
		
4194

    
4195
	(idC_C1, b, c) 
4196
	=  (idC_C1_3, b_2, c_2);
4197

    
4198

    
4199
	tel
4200

    
4201
	until true restart POINTC_C1
4202

    
4203

    
4204

    
4205
	state C1_C1B__TO__C1_C1A_1:
4206

    
4207
	 var 	idC_C1_2, idC_C1_3:int;
4208
	b_2:int;
4209
	c_2:int;
4210
	let
4211

    
4212
		-- transition trace :
4213
	--C1_C1b__To__C1_C1a_1
4214
		(idC_C1_2) 
4215
	= C1_C1b_ex(idC_C1_1, false);
4216
		
4217

    
4218
		(idC_C1_3, b_2, c_2) 
4219
	= C1_C1a_en(idC_C1_2, b_1, c_1, false);
4220
		
4221

    
4222
	(idC_C1, b, c) 
4223
	=  (idC_C1_3, b_2, c_2);
4224

    
4225

    
4226
	tel
4227

    
4228
	until true restart POINTC_C1
4229

    
4230

    
4231

    
4232
	state C1_C1A_IDL:
4233

    
4234
	 	let
4235

    
4236
		
4237

    
4238
	(idC_C1, b, c) 
4239
	= (idC_C1_1, b_1, c_1);
4240
	
4241

    
4242
	tel
4243

    
4244
	until true restart POINTC_C1
4245

    
4246

    
4247

    
4248
	state C1_C1B_IDL:
4249

    
4250
	 	let
4251

    
4252
		
4253

    
4254
	(idC_C1, b, c) 
4255
	= (idC_C1_1, b_1, c_1);
4256
	
4257

    
4258
	tel
4259

    
4260
	until true restart POINTC_C1
4261

    
4262

    
4263

    
4264
tel
4265

    
4266

    
4267
--***************************************************State :Parallel2_C Automaton***************************************************
4268

    
4269
node Parallel2_C_node(idParallel2_C_1:int;
4270
	b_1:int;
4271
	c_1:int;
4272
	idC_C1_1:int;
4273
	T:bool;
4274
	idC_C2_1:int;
4275
	R:bool;
4276
	S:bool)
4277

    
4278
returns (idParallel2_C:int;
4279
	b:int;
4280
	c:int;
4281
	idC_C1:int;
4282
	idC_C2:int);
4283

    
4284

    
4285
let
4286

    
4287
	 automaton parallel2_c
4288

    
4289
	state POINTParallel2_C:
4290
	unless (idParallel2_C_1=0) restart POINT__TO__C_C1_1
4291

    
4292

    
4293

    
4294
	unless (idParallel2_C_1=1431) and T restart C_C2__TO__C_C1_1
4295

    
4296

    
4297

    
4298
	unless (idParallel2_C_1=1434) and T restart C_C1__TO__C_C2_1
4299

    
4300

    
4301

    
4302
	unless (idParallel2_C_1=1431) restart C_C2_IDL
4303

    
4304
	unless (idParallel2_C_1=1434) restart C_C1_IDL
4305

    
4306
	let
4307

    
4308
		(idParallel2_C, b, c, idC_C1, idC_C2) 
4309
	= (idParallel2_C_1, b_1, c_1, idC_C1_1, idC_C2_1);
4310
	
4311

    
4312
	tel
4313

    
4314

    
4315

    
4316
	state POINT__TO__C_C1_1:
4317

    
4318
	 var 	idParallel2_C_2:int;
4319
	b_2:int;
4320
	c_2:int;
4321
	idC_C1_2:int;
4322
	let
4323

    
4324
		-- transition trace :
4325
	--POINT__To__C_C1_1
4326
		(idC_C1_2, idParallel2_C_2, b_2, c_2) 
4327
	= C_C1_en(idC_C1_1, idParallel2_C_1, b_1, c_1, false);
4328
		
4329

    
4330
	(idParallel2_C, b, c, idC_C1) 
4331
	=  (idParallel2_C_2, b_2, c_2, idC_C1_2);
4332

    
4333
	--add unused variables
4334
	(idC_C2) 
4335
	= (idC_C2_1);
4336
	
4337

    
4338
	tel
4339

    
4340
	until true restart POINTParallel2_C
4341

    
4342

    
4343

    
4344
	state C_C2__TO__C_C1_1:
4345

    
4346
	 var 	idParallel2_C_2, idParallel2_C_3:int;
4347
	b_2:int;
4348
	c_2:int;
4349
	idC_C1_2:int;
4350
	idC_C2_2:int;
4351
	let
4352

    
4353
		-- transition trace :
4354
	--C_C2__To__C_C1_1
4355
		(idC_C2_2, idParallel2_C_2) 
4356
	= C_C2_ex(idC_C2_1, idParallel2_C_1, false);
4357
		
4358

    
4359
		(idC_C1_2, idParallel2_C_3, b_2, c_2) 
4360
	= C_C1_en(idC_C1_1, idParallel2_C_2, b_1, c_1, false);
4361
		
4362

    
4363
	(idParallel2_C, b, c, idC_C1, idC_C2) 
4364
	=  (idParallel2_C_3, b_2, c_2, idC_C1_2, idC_C2_2);
4365

    
4366

    
4367
	tel
4368

    
4369
	until true restart POINTParallel2_C
4370

    
4371

    
4372

    
4373
	state C_C1__TO__C_C2_1:
4374

    
4375
	 var 	idParallel2_C_2, idParallel2_C_3:int;
4376
	b_2:int;
4377
	c_2:int;
4378
	idC_C1_2:int;
4379
	idC_C2_2:int;
4380
	let
4381

    
4382
		-- transition trace :
4383
	--C_C1__To__C_C2_1
4384
		(idC_C1_2, idParallel2_C_2) 
4385
	= C_C1_ex(idC_C1_1, idParallel2_C_1, false);
4386
		
4387

    
4388
		(idC_C2_2, idParallel2_C_3, b_2, c_2) 
4389
	= C_C2_en(idC_C2_1, idParallel2_C_2, b_1, c_1, false);
4390
		
4391

    
4392
	(idParallel2_C, b, c, idC_C1, idC_C2) 
4393
	=  (idParallel2_C_3, b_2, c_2, idC_C1_2, idC_C2_2);
4394

    
4395

    
4396
	tel
4397

    
4398
	until true restart POINTParallel2_C
4399

    
4400

    
4401

    
4402
	state C_C2_IDL:
4403

    
4404
	 var 	b_2:int;
4405
	c_2:int;
4406
	idC_C2_2:int;
4407
	let
4408

    
4409
		
4410
	(idC_C2_2, b_2, c_2) 
4411
	= C_C2_node(idC_C2_1, b_1, c_1, S, R);
4412

    
4413
		
4414

    
4415

    
4416
	(idParallel2_C, b, c, idC_C1, idC_C2) 
4417
	= (idParallel2_C_1, b_2, c_2, idC_C1_1, idC_C2_2);
4418
	
4419

    
4420
	tel
4421

    
4422
	until true restart POINTParallel2_C
4423

    
4424

    
4425

    
4426
	state C_C1_IDL:
4427

    
4428
	 var 	b_2:int;
4429
	c_2:int;
4430
	idC_C1_2:int;
4431
	let
4432

    
4433
		
4434
	(idC_C1_2, b_2, c_2) 
4435
	= C_C1_node(idC_C1_1, b_1, c_1, S, R);
4436

    
4437
		
4438

    
4439

    
4440
	(idParallel2_C, b, c, idC_C1, idC_C2) 
4441
	= (idParallel2_C_1, b_2, c_2, idC_C1_2, idC_C2_1);
4442
	
4443

    
4444
	tel
4445

    
4446
	until true restart POINTParallel2_C
4447

    
4448

    
4449

    
4450
tel
4451

    
4452

    
4453
--***************************************************State :A_A2 Automaton***************************************************
4454

    
4455
node A_A2_node(idA_A2_1:int;
4456
	a_1:int;
4457
	x:int;
4458
	S:bool;
4459
	R:bool)
4460

    
4461
returns (idA_A2:int;
4462
	a:int);
4463

    
4464

    
4465
let
4466

    
4467
	 automaton a_a2
4468

    
4469
	state POINTA_A2:
4470
	unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1
4471

    
4472

    
4473

    
4474
	unless (idA_A2_1=1421) and S restart A2_A2A__TO__A2_A2B_1
4475

    
4476

    
4477

    
4478
	unless (idA_A2_1=1422) and R restart A2_A2B__TO__A2_A2A_1
4479

    
4480

    
4481

    
4482
	unless (idA_A2_1=1421) restart A2_A2A_IDL
4483

    
4484
	unless (idA_A2_1=1422) restart A2_A2B_IDL
4485

    
4486
	let
4487

    
4488
		(idA_A2, a) 
4489
	= (idA_A2_1, a_1);
4490
	
4491

    
4492
	tel
4493

    
4494

    
4495

    
4496
	state POINT__TO__A2_A2A_1:
4497

    
4498
	 var 	idA_A2_2:int;
4499
	a_2:int;
4500
	let
4501

    
4502
		-- transition trace :
4503
	--POINT__To__A2_A2a_1
4504
		(idA_A2_2, a_2) 
4505
	= A2_A2a_en(idA_A2_1, x, a_1, false);
4506
		
4507

    
4508
	(idA_A2, a) 
4509
	=  (idA_A2_2, a_2);
4510

    
4511

    
4512
	tel
4513

    
4514
	until true restart POINTA_A2
4515

    
4516

    
4517

    
4518
	state A2_A2A__TO__A2_A2B_1:
4519

    
4520
	 var 	idA_A2_2, idA_A2_3:int;
4521
	a_2:int;
4522
	let
4523

    
4524
		-- transition trace :
4525
	--A2_A2a__To__A2_A2b_1
4526
		(idA_A2_2) 
4527
	= A2_A2a_ex(idA_A2_1, false);
4528
		
4529

    
4530
		(idA_A2_3, a_2) 
4531
	= A2_A2b_en(idA_A2_2, x, a_1, false);
4532
		
4533

    
4534
	(idA_A2, a) 
4535
	=  (idA_A2_3, a_2);
4536

    
4537

    
4538
	tel
4539

    
4540
	until true restart POINTA_A2
4541

    
4542

    
4543

    
4544
	state A2_A2B__TO__A2_A2A_1:
4545

    
4546
	 var 	idA_A2_2, idA_A2_3:int;
4547
	a_2:int;
4548
	let
4549

    
4550
		-- transition trace :
4551
	--A2_A2b__To__A2_A2a_1
4552
		(idA_A2_2) 
4553
	= A2_A2b_ex(idA_A2_1, false);
4554
		
4555

    
4556
		(idA_A2_3, a_2) 
4557
	= A2_A2a_en(idA_A2_2, x, a_1, false);
4558
		
4559

    
4560
	(idA_A2, a) 
4561
	=  (idA_A2_3, a_2);
4562

    
4563

    
4564
	tel
4565

    
4566
	until true restart POINTA_A2
4567

    
4568

    
4569

    
4570
	state A2_A2A_IDL:
4571

    
4572
	 	let
4573

    
4574
		
4575

    
4576
	(idA_A2, a) 
4577
	= (idA_A2_1, a_1);
4578
	
4579

    
4580
	tel
4581

    
4582
	until true restart POINTA_A2
4583

    
4584

    
4585

    
4586
	state A2_A2B_IDL:
4587

    
4588
	 	let
4589

    
4590
		
4591

    
4592
	(idA_A2, a) 
4593
	= (idA_A2_1, a_1);
4594
	
4595

    
4596
	tel
4597

    
4598
	until true restart POINTA_A2
4599

    
4600

    
4601

    
4602
tel
4603

    
4604

    
4605
--***************************************************State :A_A1 Automaton***************************************************
4606

    
4607
node A_A1_node(idA_A1_1:int;
4608
	a_1:int;
4609
	x:int;
4610
	S:bool;
4611
	R:bool)
4612

    
4613
returns (idA_A1:int;
4614
	a:int);
4615

    
4616

    
4617
let
4618

    
4619
	 automaton a_a1
4620

    
4621
	state POINTA_A1:
4622
	unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1
4623

    
4624

    
4625

    
4626
	unless (idA_A1_1=1418) and S restart A1_A1A__TO__A1_A1B_1
4627

    
4628

    
4629

    
4630
	unless (idA_A1_1=1419) and R restart A1_A1B__TO__A1_A1A_1
4631

    
4632

    
4633

    
4634
	unless (idA_A1_1=1418) restart A1_A1A_IDL
4635

    
4636
	unless (idA_A1_1=1419) restart A1_A1B_IDL
4637

    
4638
	let
4639

    
4640
		(idA_A1, a) 
4641
	= (idA_A1_1, a_1);
4642
	
4643

    
4644
	tel
4645

    
4646

    
4647

    
4648
	state POINT__TO__A1_A1A_1:
4649

    
4650
	 var 	idA_A1_2:int;
4651
	a_2:int;
4652
	let
4653

    
4654
		-- transition trace :
4655
	--POINT__To__A1_A1a_1
4656
		(idA_A1_2, a_2) 
4657
	= A1_A1a_en(idA_A1_1, x, a_1, false);
4658
		
4659

    
4660
	(idA_A1, a) 
4661
	=  (idA_A1_2, a_2);
4662

    
4663

    
4664
	tel
4665

    
4666
	until true restart POINTA_A1
4667

    
4668

    
4669

    
4670
	state A1_A1A__TO__A1_A1B_1:
4671

    
4672
	 var 	idA_A1_2, idA_A1_3:int;
4673
	a_2:int;
4674
	let
4675

    
4676
		-- transition trace :
4677
	--A1_A1a__To__A1_A1b_1
4678
		(idA_A1_2) 
4679
	= A1_A1a_ex(idA_A1_1, false);
4680
		
4681

    
4682
		(idA_A1_3, a_2) 
4683
	= A1_A1b_en(idA_A1_2, x, a_1, false);
4684
		
4685

    
4686
	(idA_A1, a) 
4687
	=  (idA_A1_3, a_2);
4688

    
4689

    
4690
	tel
4691

    
4692
	until true restart POINTA_A1
4693

    
4694

    
4695

    
4696
	state A1_A1B__TO__A1_A1A_1:
4697

    
4698
	 var 	idA_A1_2, idA_A1_3:int;
4699
	a_2:int;
4700
	let
4701

    
4702
		-- transition trace :
4703
	--A1_A1b__To__A1_A1a_1
4704
		(idA_A1_2) 
4705
	= A1_A1b_ex(idA_A1_1, false);
4706
		
4707

    
4708
		(idA_A1_3, a_2) 
4709
	= A1_A1a_en(idA_A1_2, x, a_1, false);
4710
		
4711

    
4712
	(idA_A1, a) 
4713
	=  (idA_A1_3, a_2);
4714

    
4715

    
4716
	tel
4717

    
4718
	until true restart POINTA_A1
4719

    
4720

    
4721

    
4722
	state A1_A1A_IDL:
4723

    
4724
	 	let
4725

    
4726
		
4727

    
4728
	(idA_A1, a) 
4729
	= (idA_A1_1, a_1);
4730
	
4731

    
4732
	tel
4733

    
4734
	until true restart POINTA_A1
4735

    
4736

    
4737

    
4738
	state A1_A1B_IDL:
4739

    
4740
	 	let
4741

    
4742
		
4743

    
4744
	(idA_A1, a) 
4745
	= (idA_A1_1, a_1);
4746
	
4747

    
4748
	tel
4749

    
4750
	until true restart POINTA_A1
4751

    
4752

    
4753

    
4754
tel
4755

    
4756

    
4757
--***************************************************State :Parallel2_A Automaton***************************************************
4758

    
4759
node Parallel2_A_node(idParallel2_A_1:int;
4760
	a_1:int;
4761
	idA_A1_1:int;
4762
	x:int;
4763
	T:bool;
4764
	idA_A2_1:int;
4765
	R:bool;
4766
	S:bool)
4767

    
4768
returns (idParallel2_A:int;
4769
	a:int;
4770
	idA_A1:int;
4771
	idA_A2:int);
4772

    
4773

    
4774
let
4775

    
4776
	 automaton parallel2_a
4777

    
4778
	state POINTParallel2_A:
4779
	unless (idParallel2_A_1=0) restart POINT__TO__A_A1_1
4780

    
4781

    
4782

    
4783
	unless (idParallel2_A_1=1420) and T restart A_A2__TO__A_A1_1
4784

    
4785

    
4786

    
4787
	unless (idParallel2_A_1=1417) and T restart A_A1__TO__A_A2_1
4788

    
4789

    
4790

    
4791
	unless (idParallel2_A_1=1420) restart A_A2_IDL
4792

    
4793
	unless (idParallel2_A_1=1417) restart A_A1_IDL
4794

    
4795
	let
4796

    
4797
		(idParallel2_A, a, idA_A1, idA_A2) 
4798
	= (idParallel2_A_1, a_1, idA_A1_1, idA_A2_1);
4799
	
4800

    
4801
	tel
4802

    
4803

    
4804

    
4805
	state POINT__TO__A_A1_1:
4806

    
4807
	 var 	idParallel2_A_2:int;
4808
	a_2:int;
4809
	idA_A1_2:int;
4810
	let
4811

    
4812
		-- transition trace :
4813
	--POINT__To__A_A1_1
4814
		(idA_A1_2, idParallel2_A_2, a_2) 
4815
	= A_A1_en(idA_A1_1, idParallel2_A_1, a_1, x, false);
4816
		
4817

    
4818
	(idParallel2_A, a, idA_A1) 
4819
	=  (idParallel2_A_2, a_2, idA_A1_2);
4820

    
4821
	--add unused variables
4822
	(idA_A2) 
4823
	= (idA_A2_1);
4824
	
4825

    
4826
	tel
4827

    
4828
	until true restart POINTParallel2_A
4829

    
4830

    
4831

    
4832
	state A_A2__TO__A_A1_1:
4833

    
4834
	 var 	idParallel2_A_2, idParallel2_A_3:int;
4835
	a_2:int;
4836
	idA_A1_2:int;
4837
	idA_A2_2:int;
4838
	let
4839

    
4840
		-- transition trace :
4841
	--A_A2__To__A_A1_1
4842
		(idA_A2_2, idParallel2_A_2) 
4843
	= A_A2_ex(idA_A2_1, idParallel2_A_1, false);
4844
		
4845

    
4846
		(idA_A1_2, idParallel2_A_3, a_2) 
4847
	= A_A1_en(idA_A1_1, idParallel2_A_2, a_1, x, false);
4848
		
4849

    
4850
	(idParallel2_A, a, idA_A1, idA_A2) 
4851
	=  (idParallel2_A_3, a_2, idA_A1_2, idA_A2_2);
4852

    
4853

    
4854
	tel
4855

    
4856
	until true restart POINTParallel2_A
4857

    
4858

    
4859

    
4860
	state A_A1__TO__A_A2_1:
4861

    
4862
	 var 	idParallel2_A_2, idParallel2_A_3:int;
4863
	a_2:int;
4864
	idA_A1_2:int;
4865
	idA_A2_2:int;
4866
	let
4867

    
4868
		-- transition trace :
4869
	--A_A1__To__A_A2_1
4870
		(idA_A1_2, idParallel2_A_2) 
4871
	= A_A1_ex(idA_A1_1, idParallel2_A_1, false);
4872
		
4873

    
4874
		(idA_A2_2, idParallel2_A_3, a_2) 
4875
	= A_A2_en(idA_A2_1, idParallel2_A_2, a_1, x, false);
4876
		
4877

    
4878
	(idParallel2_A, a, idA_A1, idA_A2) 
4879
	=  (idParallel2_A_3, a_2, idA_A1_2, idA_A2_2);
4880

    
4881

    
4882
	tel
4883

    
4884
	until true restart POINTParallel2_A
4885

    
4886

    
4887

    
4888
	state A_A2_IDL:
4889

    
4890
	 var 	a_2:int;
4891
	idA_A2_2:int;
4892
	let
4893

    
4894
		
4895
	(idA_A2_2, a_2) 
4896
	= A_A2_node(idA_A2_1, a_1, x, S, R);
4897

    
4898
		
4899

    
4900

    
4901
	(idParallel2_A, a, idA_A1, idA_A2) 
4902
	= (idParallel2_A_1, a_2, idA_A1_1, idA_A2_2);
4903
	
4904

    
4905
	tel
4906

    
4907
	until true restart POINTParallel2_A
4908

    
4909

    
4910

    
4911
	state A_A1_IDL:
4912

    
4913
	 var 	a_2:int;
4914
	idA_A1_2:int;
4915
	let
4916

    
4917
		
4918
	(idA_A1_2, a_2) 
4919
	= A_A1_node(idA_A1_1, a_1, x, S, R);
4920

    
4921
		
4922

    
4923

    
4924
	(idParallel2_A, a, idA_A1, idA_A2) 
4925
	= (idParallel2_A_1, a_2, idA_A1_2, idA_A2_1);
4926
	
4927

    
4928
	tel
4929

    
4930
	until true restart POINTParallel2_A
4931

    
4932

    
4933

    
4934
tel
4935

    
4936

    
4937
--***************************************************State :Parallel2_Parallel2 Automaton***************************************************
4938

    
4939
node Parallel2_Parallel2_node(idParallel2_Parallel2_1:int;
4940
	a_1:int;
4941
	idA_A1_1:int;
4942
	idA_A2_1:int;
4943
	idParallel2_A_1:int;
4944
	x:int;
4945
	b_1:int;
4946
	idB_B1_1:int;
4947
	idB_B2_1:int;
4948
	idParallel2_B_1:int;
4949
	c_1:int;
4950
	idC_C1_1:int;
4951
	idC_C2_1:int;
4952
	idParallel2_C_1:int;
4953
	dd_1:int;
4954
	idD_D1_1:int;
4955
	idD_D2_1:int;
4956
	idParallel2_D_1:int;
4957
	R:bool;
4958
	S:bool;
4959
	T:bool)
4960

    
4961
returns (idParallel2_Parallel2:int;
4962
	a:int;
4963
	idA_A1:int;
4964
	idA_A2:int;
4965
	idParallel2_A:int;
4966
	b:int;
4967
	idB_B1:int;
4968
	idB_B2:int;
4969
	idParallel2_B:int;
4970
	c:int;
4971
	idC_C1:int;
4972
	idC_C2:int;
4973
	idParallel2_C:int;
4974
	dd:int;
4975
	idD_D1:int;
4976
	idD_D2:int;
4977
	idParallel2_D:int);
4978

    
4979

    
4980
let
4981

    
4982
	 automaton parallel2_parallel2
4983

    
4984
	state POINTParallel2_Parallel2:
4985
	unless (idParallel2_Parallel2_1=0) restart PARALLEL2_PARALLEL2_PARALLEL_ENTRY
4986
	unless true  restart PARALLEL2_PARALLEL2_PARALLEL_IDL
4987

    
4988
	let
4989

    
4990
		(idParallel2_Parallel2, a, idA_A1, idA_A2, idParallel2_A, b, idB_B1, idB_B2, idParallel2_B, c, idC_C1, idC_C2, idParallel2_C, dd, idD_D1, idD_D2, idParallel2_D) 
4991
	= (idParallel2_Parallel2_1, a_1, idA_A1_1, idA_A2_1, idParallel2_A_1, b_1, idB_B1_1, idB_B2_1, idParallel2_B_1, c_1, idC_C1_1, idC_C2_1, idParallel2_C_1, dd_1, idD_D1_1, idD_D2_1, idParallel2_D_1);
4992
	
4993

    
4994
	tel
4995

    
4996

    
4997

    
4998
	state PARALLEL2_PARALLEL2_PARALLEL_ENTRY:
4999

    
5000
	 var 	idParallel2_Parallel2_2, idParallel2_Parallel2_3, idParallel2_Parallel2_4, idParallel2_Parallel2_5:int;
5001
	a_2, a_3:int;
5002
	idA_A1_2:int;
5003
	idA_A2_2:int;
5004
	idParallel2_A_2:int;
5005
	b_2, b_3:int;
5006
	idB_B1_2:int;
5007
	idB_B2_2:int;
5008
	idParallel2_B_2:int;
5009
	c_2, c_3:int;
5010
	idC_C1_2:int;
5011
	idC_C2_2:int;
5012
	idParallel2_C_2:int;
5013
	dd_2:int;
5014
	idD_D1_2:int;
5015
	idD_D2_2:int;
5016
	idParallel2_D_2:int;
5017
	let
5018

    
5019
		
5020
	(idParallel2_A_2, idParallel2_Parallel2_2, a_2, idA_A1_2, idA_A2_2) 
5021
	= Parallel2_A_en(idParallel2_A_1, idParallel2_Parallel2_1, a_1, idA_A1_1, x, idA_A2_1, false);
5022

    
5023
	(idParallel2_B_2, idParallel2_Parallel2_3, a_3, b_2, idB_B1_2, idB_B2_2) 
5024
	= Parallel2_B_en(idParallel2_B_1, idParallel2_Parallel2_2, a_2, b_1, idB_B1_1, idB_B2_1, false);
5025

    
5026
	(idParallel2_C_2, idParallel2_Parallel2_4, b_3, c_2, idC_C1_2, idC_C2_2) 
5027
	= Parallel2_C_en(idParallel2_C_1, idParallel2_Parallel2_3, b_2, c_1, idC_C1_1, idC_C2_1, false);
5028

    
5029
	(idParallel2_D_2, idParallel2_Parallel2_5, c_3, dd_2, idD_D1_2, idD_D2_2) 
5030
	= Parallel2_D_en(idParallel2_D_1, idParallel2_Parallel2_4, c_2, dd_1, idD_D1_1, idD_D2_1, false);
5031

    
5032

    
5033
	(idParallel2_Parallel2, a, idA_A1, idA_A2, idParallel2_A, b, idB_B1, idB_B2, idParallel2_B, c, idC_C1, idC_C2, idParallel2_C, dd, idD_D1, idD_D2, idParallel2_D) 
5034
	= (idParallel2_Parallel2_5, a_3, idA_A1_2, idA_A2_2, idParallel2_A_2, b_3, idB_B1_2, idB_B2_2, idParallel2_B_2, c_3, idC_C1_2, idC_C2_2, idParallel2_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel2_D_2);
5035
	
5036

    
5037
	tel
5038

    
5039
	until true restart POINTParallel2_Parallel2
5040

    
5041

    
5042

    
5043
	state PARALLEL2_PARALLEL2_PARALLEL_IDL:
5044

    
5045
	 var 	a_2, a_3:int;
5046
	idA_A1_2:int;
5047
	idA_A2_2:int;
5048
	idParallel2_A_2:int;
5049
	b_2, b_3:int;
5050
	idB_B1_2:int;
5051
	idB_B2_2:int;
5052
	idParallel2_B_2:int;
5053
	c_2, c_3:int;
5054
	idC_C1_2:int;
5055
	idC_C2_2:int;
5056
	idParallel2_C_2:int;
5057
	dd_2:int;
5058
	idD_D1_2:int;
5059
	idD_D2_2:int;
5060
	idParallel2_D_2:int;
5061
	let
5062

    
5063
		
5064

    
5065
		(idParallel2_A_2, a_2, idA_A1_2, idA_A2_2)
5066
	= if not (idParallel2_A_1= 0 ) then Parallel2_A_node(idParallel2_A_1, a_1, idA_A1_1, x, T, idA_A2_1, R, S)
5067

    
5068
		 else (idParallel2_A_1, a_1, idA_A1_1, idA_A2_1);
5069

    
5070
		
5071

    
5072
		
5073

    
5074
		(idParallel2_B_2, a_3, b_2, idB_B1_2, idB_B2_2)
5075
	= if not (idParallel2_B_1= 0 ) then Parallel2_B_node(idParallel2_B_1, a_2, b_1, idB_B1_1, T, idB_B2_1, R, S)
5076

    
5077
		 else (idParallel2_B_1, a_2, b_1, idB_B1_1, idB_B2_1);
5078

    
5079
		
5080

    
5081
		
5082

    
5083
		(idParallel2_C_2, b_3, c_2, idC_C1_2, idC_C2_2)
5084
	= if not (idParallel2_C_1= 0 ) then Parallel2_C_node(idParallel2_C_1, b_2, c_1, idC_C1_1, T, idC_C2_1, R, S)
5085

    
5086
		 else (idParallel2_C_1, b_2, c_1, idC_C1_1, idC_C2_1);
5087

    
5088
		
5089

    
5090
		
5091

    
5092
		(idParallel2_D_2, c_3, dd_2, idD_D1_2, idD_D2_2)
5093
	= if not (idParallel2_D_1= 0 ) then Parallel2_D_node(idParallel2_D_1, c_2, dd_1, idD_D1_1, T, idD_D2_1, R, S)
5094

    
5095
		 else (idParallel2_D_1, c_2, dd_1, idD_D1_1, idD_D2_1);
5096

    
5097
		
5098

    
5099
		
5100

    
5101
	(idParallel2_Parallel2, a, idA_A1, idA_A2, idParallel2_A, b, idB_B1, idB_B2, idParallel2_B, c, idC_C1, idC_C2, idParallel2_C, dd, idD_D1, idD_D2, idParallel2_D) 
5102
	= (idParallel2_Parallel2_1, a_3, idA_A1_2, idA_A2_2, idParallel2_A_2, b_3, idB_B1_2, idB_B2_2, idParallel2_B_2, c_3, idC_C1_2, idC_C2_2, idParallel2_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel2_D_2);
5103
	
5104

    
5105
	tel
5106

    
5107
	until true restart POINTParallel2_Parallel2
5108

    
5109

    
5110

    
5111
tel
5112

    
5113

    
5114
--***************************************************State :Parallel2_Parallel2 Automaton***************************************************
5115

    
5116
node Parallel2V2_Parallel2(x:int;
5117
	R:bool;
5118
	S:bool;
5119
	T:bool)
5120

    
5121
returns (a:int;
5122
	b:int;
5123
	dd:int;
5124
	c:int);
5125

    
5126

    
5127
var a_1: int;
5128

    
5129
	b_1: int;
5130

    
5131
	dd_1: int;
5132

    
5133
	c_1: int;
5134

    
5135
	idParallel2_Parallel2, idParallel2_Parallel2_1: int;
5136

    
5137
	idB_B2, idB_B2_1: int;
5138

    
5139
	idB_B1, idB_B1_1: int;
5140

    
5141
	idParallel2_B, idParallel2_B_1: int;
5142

    
5143
	idD_D2, idD_D2_1: int;
5144

    
5145
	idD_D1, idD_D1_1: int;
5146

    
5147
	idParallel2_D, idParallel2_D_1: int;
5148

    
5149
	idC_C2, idC_C2_1: int;
5150

    
5151
	idC_C1, idC_C1_1: int;
5152

    
5153
	idParallel2_C, idParallel2_C_1: int;
5154

    
5155
	idA_A2, idA_A2_1: int;
5156

    
5157
	idA_A1, idA_A1_1: int;
5158

    
5159
	idParallel2_A, idParallel2_A_1: int;
5160

    
5161
		idParallel2_Parallel2_2, idParallel2_Parallel2_3:int;
5162
	a_2, a_3:int;
5163
	idA_A1_2, idA_A1_3:int;
5164
	idA_A2_2, idA_A2_3:int;
5165
	idParallel2_A_2, idParallel2_A_3:int;
5166
	b_2, b_3:int;
5167
	idB_B1_2, idB_B1_3:int;
5168
	idB_B2_2, idB_B2_3:int;
5169
	idParallel2_B_2, idParallel2_B_3:int;
5170
	c_2, c_3:int;
5171
	idC_C1_2, idC_C1_3:int;
5172
	idC_C2_2, idC_C2_3:int;
5173
	idParallel2_C_2, idParallel2_C_3:int;
5174
	dd_2, dd_3:int;
5175
	idD_D1_2, idD_D1_3:int;
5176
	idD_D2_2, idD_D2_3:int;
5177
	idParallel2_D_2, idParallel2_D_3:int;
5178
let
5179

    
5180
	a_1 = 0 -> pre a;
5181

    
5182
	b_1 = 0 -> pre b;
5183

    
5184
	dd_1 = 0 -> pre dd;
5185

    
5186
	c_1 = 0 -> pre c;
5187

    
5188
	idParallel2_Parallel2_1 = 0 -> pre idParallel2_Parallel2;
5189

    
5190
	idB_B2_1 = 0 -> pre idB_B2;
5191

    
5192
	idB_B1_1 = 0 -> pre idB_B1;
5193

    
5194
	idParallel2_B_1 = 0 -> pre idParallel2_B;
5195

    
5196
	idD_D2_1 = 0 -> pre idD_D2;
5197

    
5198
	idD_D1_1 = 0 -> pre idD_D1;
5199

    
5200
	idParallel2_D_1 = 0 -> pre idParallel2_D;
5201

    
5202
	idC_C2_1 = 0 -> pre idC_C2;
5203

    
5204
	idC_C1_1 = 0 -> pre idC_C1;
5205

    
5206
	idParallel2_C_1 = 0 -> pre idParallel2_C;
5207

    
5208
	idA_A2_1 = 0 -> pre idA_A2;
5209

    
5210
	idA_A1_1 = 0 -> pre idA_A1;
5211

    
5212
	idParallel2_A_1 = 0 -> pre idParallel2_A;
5213

    
5214
	
5215

    
5216

    
5217

    
5218
	(idParallel2_Parallel2_2, a_2, idA_A1_2, idA_A2_2, idParallel2_A_2, b_2, idB_B1_2, idB_B2_2, idParallel2_B_2, c_2, idC_C1_2, idC_C2_2, idParallel2_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel2_D_2)
5219
	 = 
5220

    
5221
	 if R then Parallel2_Parallel2_node(idParallel2_Parallel2_1, a_1, idA_A1_1, idA_A2_1, idParallel2_A_1, x, b_1, idB_B1_1, idB_B2_1, idParallel2_B_1, c_1, idC_C1_1, idC_C2_1, idParallel2_C_1, dd_1, idD_D1_1, idD_D2_1, idParallel2_D_1, R, false, false)
5222

    
5223
	 else (idParallel2_Parallel2_1, a_1, idA_A1_1, idA_A2_1, idParallel2_A_1, b_1, idB_B1_1, idB_B2_1, idParallel2_B_1, c_1, idC_C1_1, idC_C2_1, idParallel2_C_1, dd_1, idD_D1_1, idD_D2_1, idParallel2_D_1);
5224

    
5225
	
5226

    
5227

    
5228

    
5229
	(idParallel2_Parallel2_3, a_3, idA_A1_3, idA_A2_3, idParallel2_A_3, b_3, idB_B1_3, idB_B2_3, idParallel2_B_3, c_3, idC_C1_3, idC_C2_3, idParallel2_C_3, dd_3, idD_D1_3, idD_D2_3, idParallel2_D_3)
5230
	 = 
5231

    
5232
	 if S then Parallel2_Parallel2_node(idParallel2_Parallel2_2, a_2, idA_A1_2, idA_A2_2, idParallel2_A_2, x, b_2, idB_B1_2, idB_B2_2, idParallel2_B_2, c_2, idC_C1_2, idC_C2_2, idParallel2_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel2_D_2, false, S, false)
5233

    
5234
	 else (idParallel2_Parallel2_2, a_2, idA_A1_2, idA_A2_2, idParallel2_A_2, b_2, idB_B1_2, idB_B2_2, idParallel2_B_2, c_2, idC_C1_2, idC_C2_2, idParallel2_C_2, dd_2, idD_D1_2, idD_D2_2, idParallel2_D_2);
5235

    
5236
	
5237

    
5238

    
5239

    
5240
	(idParallel2_Parallel2, a, idA_A1, idA_A2, idParallel2_A, b, idB_B1, idB_B2, idParallel2_B, c, idC_C1, idC_C2, idParallel2_C, dd, idD_D1, idD_D2, idParallel2_D)
5241
	 = 
5242

    
5243
	 if T then Parallel2_Parallel2_node(idParallel2_Parallel2_3, a_3, idA_A1_3, idA_A2_3, idParallel2_A_3, x, b_3, idB_B1_3, idB_B2_3, idParallel2_B_3, c_3, idC_C1_3, idC_C2_3, idParallel2_C_3, dd_3, idD_D1_3, idD_D2_3, idParallel2_D_3, false, false, T)
5244

    
5245
	 else (idParallel2_Parallel2_3, a_3, idA_A1_3, idA_A2_3, idParallel2_A_3, b_3, idB_B1_3, idB_B2_3, idParallel2_B_3, c_3, idC_C1_3, idC_C2_3, idParallel2_C_3, dd_3, idD_D1_3, idD_D2_3, idParallel2_D_3);
5246

    
5247
	
5248

    
5249

    
5250
--unused outputs
5251
	
5252

    
5253
tel
5254

    
5255

    
5256

    
5257
node Parallel2V2 (x_1_1 : int; R_1_1 : real; S_1_1 : real; T_1_1 : real)
5258
returns (a_1_1 : int;
5259
	b_2_1 : int;
5260
	dd_3_1 : int;
5261
	c_4_1 : int); 
5262
var
5263
	Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real;
5264
	Parallel2_1_1 : int; Parallel2_2_1 : int; Parallel2_3_1 : int; Parallel2_4_1 : int;
5265
	i_virtual_local : real;
5266
	Parallel2Mux_1_1_event: bool;
5267
	Parallel2Mux_1_2_event: bool;
5268
	Parallel2Mux_1_3_event: bool;
5269
let 
5270
	Mux_1_1 = R_1_1 ;
5271
	Mux_1_2 = S_1_1 ;
5272
	Mux_1_3 = T_1_1 ;
5273
	Parallel2Mux_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));
5274
	Parallel2Mux_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));
5275
	Parallel2Mux_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));
5276
	(Parallel2_1_1, Parallel2_2_1, Parallel2_3_1, Parallel2_4_1) =  Parallel2V2_Parallel2(x_1_1, Parallel2Mux_1_1_event, Parallel2Mux_1_2_event, Parallel2Mux_1_3_event);
5277
	a_1_1 = Parallel2_1_1;
5278
	b_2_1 = Parallel2_2_1;
5279
	dd_3_1 = Parallel2_3_1;
5280
	c_4_1 = Parallel2_4_1;
5281
	i_virtual_local= 0.0 -> 1.0;
5282
tel
5283