Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Parallel1 / Parallel1.lus @ eb639349

History | View | Annotate | Download (17.9 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9
node N1_A__To__N1_B_1_Condition_Action(x_1:int)
10

    
11
returns (x:int);
12

    
13

    
14
var 	x_2:int;
15

    
16

    
17
let
18

    
19

    
20

    
21
	x_2 
22
	=  x_1 +1;
23
	
24

    
25
	(x) 
26
	= (x_2);
27
	
28

    
29
tel
30

    
31

    
32

    
33

    
34

    
35

    
36
node N2_D__To__N2_C_1_Condition_Action(x_1:int)
37

    
38
returns (x:int);
39

    
40

    
41
var 	x_2:int;
42

    
43

    
44
let
45

    
46

    
47

    
48
	x_2 
49
	=  x_1 -100;
50
	
51

    
52
	(x) 
53
	= (x_2);
54
	
55

    
56
tel
57

    
58

    
59

    
60

    
61

    
62

    
63
node N2_C__To__N2_D_1_Condition_Action(x_1:int)
64

    
65
returns (x:int);
66

    
67

    
68
var 	x_2:int;
69

    
70

    
71
let
72

    
73

    
74

    
75
	x_2 
76
	=  x_1 +100;
77
	
78

    
79
	(x) 
80
	= (x_2);
81
	
82

    
83
tel
84

    
85

    
86

    
87

    
88

    
89

    
90

    
91

    
92
node N1_B__To__N1_A_1_Condition_Action(x_1:int)
93

    
94
returns (x:int);
95

    
96

    
97
var 	x_2:int;
98

    
99

    
100
let
101

    
102

    
103

    
104
	x_2 
105
	=  x_1 -1;
106
	
107

    
108
	(x) 
109
	= (x_2);
110
	
111

    
112
tel
113

    
114

    
115

    
116

    
117

    
118

    
119
-- Entry action for state :N2_C
120
node N2_C_en(idParallel1_N2_1:int;
121
	x_1:int;
122
	isInner:bool)
123

    
124
returns (idParallel1_N2:int;
125
	x:int);
126

    
127

    
128
var 	idParallel1_N2_2:int;
129
	x_2:int;
130

    
131

    
132
let
133

    
134

    
135

    
136
	-- set state as active 
137
	idParallel1_N2_2 
138
	= 1376;
139
	
140

    
141
	x_2 
142
	= if (not isInner) then  x_1 +1000
143
	 else x_1;
144
	
145

    
146
	(idParallel1_N2, x) 
147
	= (idParallel1_N2_2, x_2);
148
	
149

    
150
tel
151

    
152

    
153

    
154

    
155

    
156
-- Exit action for state :N2_C
157
node N2_C_ex(idParallel1_N2_1:int;
158
	isInner:bool)
159

    
160
returns (idParallel1_N2:int);
161

    
162

    
163
var 	idParallel1_N2_2:int;
164

    
165

    
166
let
167

    
168

    
169

    
170
	-- set state as inactive 
171
	idParallel1_N2_2
172
	 = if (not isInner) then 0 else idParallel1_N2_1;
173

    
174

    
175
	(idParallel1_N2) 
176
	= (idParallel1_N2_1);
177
	
178

    
179
tel
180

    
181

    
182

    
183

    
184

    
185

    
186
-- Entry action for state :N2_D
187
node N2_D_en(idParallel1_N2_1:int;
188
	x_1:int;
189
	isInner:bool)
190

    
191
returns (idParallel1_N2:int;
192
	x:int);
193

    
194

    
195
var 	idParallel1_N2_2:int;
196
	x_2:int;
197

    
198

    
199
let
200

    
201

    
202

    
203
	-- set state as active 
204
	idParallel1_N2_2 
205
	= 1377;
206
	
207

    
208
	x_2 
209
	= if (not isInner) then  x_1 -1000
210
	 else x_1;
211
	
212

    
213
	(idParallel1_N2, x) 
214
	= (idParallel1_N2_2, x_2);
215
	
216

    
217
tel
218

    
219

    
220

    
221

    
222

    
223
-- Exit action for state :N2_D
224
node N2_D_ex(idParallel1_N2_1:int;
225
	isInner:bool)
226

    
227
returns (idParallel1_N2:int);
228

    
229

    
230
var 	idParallel1_N2_2:int;
231

    
232

    
233
let
234

    
235

    
236

    
237
	-- set state as inactive 
238
	idParallel1_N2_2
239
	 = if (not isInner) then 0 else idParallel1_N2_1;
240

    
241

    
242
	(idParallel1_N2) 
243
	= (idParallel1_N2_1);
244
	
245

    
246
tel
247

    
248

    
249

    
250

    
251

    
252

    
253
-- Entry action for state :Parallel1_N2
254
node Parallel1_N2_en(idParallel1_N2_1:int;
255
	idParallel1_Parallel1_1:int;
256
	x_1:int;
257
	isInner:bool)
258

    
259
returns (idParallel1_N2:int;
260
	idParallel1_Parallel1:int;
261
	x:int);
262

    
263

    
264
var 	idParallel1_N2_2, idParallel1_N2_3, idParallel1_N2_4, idParallel1_N2_5, idParallel1_N2_6:int;
265
	idParallel1_Parallel1_2, idParallel1_Parallel1_3, idParallel1_Parallel1_4:int;
266
	x_2, x_3, x_4, x_5, x_6, x_7:int;
267

    
268

    
269
let
270

    
271

    
272

    
273
	-- set state as active 
274
	idParallel1_Parallel1_2 
275
	= 1373;
276
	
277

    
278
	x_2 
279
	= if (not isInner) then  x_1 +100000
280
	 else x_1;
281
	
282

    
283
	
284
-- transition trace :
285
	--POINT__To__N2_C_1
286
		(idParallel1_N2_2, x_3) 
287
	= N2_C_en(idParallel1_N2_1, x_2, false);
288
		
289

    
290
	(idParallel1_N2_3, idParallel1_Parallel1_3, x_4) 
291
	= 
292

    
293
	if ( idParallel1_N2_1 = 0) then
294

    
295
	 (idParallel1_N2_2, idParallel1_Parallel1_2, x_3)
296

    
297
	 else(idParallel1_N2_1, idParallel1_Parallel1_2, x_2);
298

    
299
	
300

    
301
	(idParallel1_N2_4, x_5) 
302
	= 
303
	if ( idParallel1_N2_1 = 1376) then
304
	N2_C_en(idParallel1_N2_1, x_2, false)
305
	 else (idParallel1_N2_1, x_2);
306

    
307
	
308

    
309
	(idParallel1_N2_5, x_6) 
310
	= 
311
	if ( idParallel1_N2_1 = 1377) then
312
	N2_D_en(idParallel1_N2_1, x_2, false)
313
	 else (idParallel1_N2_1, x_2);
314

    
315
	
316

    
317
	(idParallel1_N2_6, idParallel1_Parallel1_4, x_7) 
318
	= 
319
		 if ( idParallel1_N2_1 = 0) then 
320
		(idParallel1_N2_3, idParallel1_Parallel1_3, x_4)
321
		 else
322
		 if ( idParallel1_N2_1 = 1376) then 
323
		(idParallel1_N2_4, idParallel1_Parallel1_3, x_5)
324
		 else
325
		 if ( idParallel1_N2_1 = 1377) then 
326
		(idParallel1_N2_5, idParallel1_Parallel1_3, x_6)
327
		 else (idParallel1_N2_1, idParallel1_Parallel1_2, x_2);
328

    
329

    
330
	(idParallel1_N2, idParallel1_Parallel1, x) 
331
	= (idParallel1_N2_6, idParallel1_Parallel1_4, x_7);
332
	
333

    
334
tel
335

    
336

    
337

    
338

    
339

    
340
-- Exit action for state :Parallel1_N2
341
node Parallel1_N2_ex(idParallel1_N2_1:int;
342
	x_1:int;
343
	idParallel1_Parallel1_1:int;
344
	isInner:bool)
345

    
346
returns (idParallel1_N2:int;
347
	x:int;
348
	idParallel1_Parallel1:int);
349

    
350

    
351
var 	idParallel1_N2_2, idParallel1_N2_3, idParallel1_N2_4, idParallel1_N2_5:int;
352
	x_2:int;
353
	idParallel1_Parallel1_2:int;
354

    
355

    
356
let
357

    
358

    
359

    
360
	
361
	(idParallel1_N2_2) 
362
	= 
363
	if ( idParallel1_N2_1 = 1376) then
364
	N2_C_ex(idParallel1_N2_1, false)
365
	 else (idParallel1_N2_1);
366

    
367
	
368

    
369
	(idParallel1_N2_3) 
370
	= 
371
	if ( idParallel1_N2_1 = 1377) then
372
	N2_D_ex(idParallel1_N2_1, false)
373
	 else (idParallel1_N2_1);
374

    
375
	
376

    
377
	(idParallel1_N2_4) 
378
	= 
379
		 if ( idParallel1_N2_1 = 1376) then 
380
		(idParallel1_N2_2)
381
		 else
382
		 if ( idParallel1_N2_1 = 1377) then 
383
		(idParallel1_N2_3)
384
		 else (idParallel1_N2_1);
385

    
386

    
387
	x_2 
388
	= if (not isInner) then  x_1 -100000
389
	 else x_1;
390
	
391

    
392
	-- set state as inactive 
393
	idParallel1_Parallel1_2
394
	 = if (not isInner) then 0 else idParallel1_Parallel1_1;
395

    
396
	idParallel1_N2_5 
397
	= 0;
398
	
399

    
400
	(idParallel1_N2, x, idParallel1_Parallel1) 
401
	= (idParallel1_N2_5, x_2, idParallel1_Parallel1_1);
402
	
403

    
404
tel
405

    
406

    
407

    
408

    
409

    
410

    
411
-- Entry action for state :N1_A
412
node N1_A_en(idParallel1_N1_1:int;
413
	x_1:int;
414
	isInner:bool)
415

    
416
returns (idParallel1_N1:int;
417
	x:int);
418

    
419

    
420
var 	idParallel1_N1_2:int;
421
	x_2:int;
422

    
423

    
424
let
425

    
426

    
427

    
428
	-- set state as active 
429
	idParallel1_N1_2 
430
	= 1374;
431
	
432

    
433
	x_2 
434
	= if (not isInner) then  x_1 +10
435
	 else x_1;
436
	
437

    
438
	(idParallel1_N1, x) 
439
	= (idParallel1_N1_2, x_2);
440
	
441

    
442
tel
443

    
444

    
445

    
446

    
447

    
448
-- Exit action for state :N1_A
449
node N1_A_ex(idParallel1_N1_1:int;
450
	isInner:bool)
451

    
452
returns (idParallel1_N1:int);
453

    
454

    
455
var 	idParallel1_N1_2:int;
456

    
457

    
458
let
459

    
460

    
461

    
462
	-- set state as inactive 
463
	idParallel1_N1_2
464
	 = if (not isInner) then 0 else idParallel1_N1_1;
465

    
466

    
467
	(idParallel1_N1) 
468
	= (idParallel1_N1_1);
469
	
470

    
471
tel
472

    
473

    
474

    
475

    
476

    
477

    
478
-- Entry action for state :N1_B
479
node N1_B_en(idParallel1_N1_1:int;
480
	x_1:int;
481
	isInner:bool)
482

    
483
returns (idParallel1_N1:int;
484
	x:int);
485

    
486

    
487
var 	idParallel1_N1_2:int;
488
	x_2:int;
489

    
490

    
491
let
492

    
493

    
494

    
495
	-- set state as active 
496
	idParallel1_N1_2 
497
	= 1375;
498
	
499

    
500
	x_2 
501
	= if (not isInner) then  x_1 -10
502
	 else x_1;
503
	
504

    
505
	(idParallel1_N1, x) 
506
	= (idParallel1_N1_2, x_2);
507
	
508

    
509
tel
510

    
511

    
512

    
513

    
514

    
515
-- Exit action for state :N1_B
516
node N1_B_ex(idParallel1_N1_1:int;
517
	isInner:bool)
518

    
519
returns (idParallel1_N1:int);
520

    
521

    
522
var 	idParallel1_N1_2:int;
523

    
524

    
525
let
526

    
527

    
528

    
529
	-- set state as inactive 
530
	idParallel1_N1_2
531
	 = if (not isInner) then 0 else idParallel1_N1_1;
532

    
533

    
534
	(idParallel1_N1) 
535
	= (idParallel1_N1_1);
536
	
537

    
538
tel
539

    
540

    
541

    
542

    
543

    
544

    
545
-- Entry action for state :Parallel1_N1
546
node Parallel1_N1_en(idParallel1_N1_1:int;
547
	idParallel1_Parallel1_1:int;
548
	x_1:int;
549
	isInner:bool)
550

    
551
returns (idParallel1_N1:int;
552
	idParallel1_Parallel1:int;
553
	x:int);
554

    
555

    
556
var 	idParallel1_N1_2, idParallel1_N1_3, idParallel1_N1_4, idParallel1_N1_5, idParallel1_N1_6:int;
557
	idParallel1_Parallel1_2, idParallel1_Parallel1_3, idParallel1_Parallel1_4:int;
558
	x_2, x_3, x_4, x_5, x_6, x_7:int;
559

    
560

    
561
let
562

    
563

    
564

    
565
	-- set state as active 
566
	idParallel1_Parallel1_2 
567
	= 1372;
568
	
569

    
570
	x_2 
571
	= if (not isInner) then  x_1 +10000
572
	 else x_1;
573
	
574

    
575
	
576
-- transition trace :
577
	--POINT__To__N1_A_1
578
		(idParallel1_N1_2, x_3) 
579
	= N1_A_en(idParallel1_N1_1, x_2, false);
580
		
581

    
582
	(idParallel1_N1_3, idParallel1_Parallel1_3, x_4) 
583
	= 
584

    
585
	if ( idParallel1_N1_1 = 0) then
586

    
587
	 (idParallel1_N1_2, idParallel1_Parallel1_2, x_3)
588

    
589
	 else(idParallel1_N1_1, idParallel1_Parallel1_2, x_2);
590

    
591
	
592

    
593
	(idParallel1_N1_4, x_5) 
594
	= 
595
	if ( idParallel1_N1_1 = 1374) then
596
	N1_A_en(idParallel1_N1_1, x_2, false)
597
	 else (idParallel1_N1_1, x_2);
598

    
599
	
600

    
601
	(idParallel1_N1_5, x_6) 
602
	= 
603
	if ( idParallel1_N1_1 = 1375) then
604
	N1_B_en(idParallel1_N1_1, x_2, false)
605
	 else (idParallel1_N1_1, x_2);
606

    
607
	
608

    
609
	(idParallel1_N1_6, idParallel1_Parallel1_4, x_7) 
610
	= 
611
		 if ( idParallel1_N1_1 = 0) then 
612
		(idParallel1_N1_3, idParallel1_Parallel1_3, x_4)
613
		 else
614
		 if ( idParallel1_N1_1 = 1374) then 
615
		(idParallel1_N1_4, idParallel1_Parallel1_3, x_5)
616
		 else
617
		 if ( idParallel1_N1_1 = 1375) then 
618
		(idParallel1_N1_5, idParallel1_Parallel1_3, x_6)
619
		 else (idParallel1_N1_1, idParallel1_Parallel1_2, x_2);
620

    
621

    
622
	(idParallel1_N1, idParallel1_Parallel1, x) 
623
	= (idParallel1_N1_6, idParallel1_Parallel1_4, x_7);
624
	
625

    
626
tel
627

    
628

    
629

    
630

    
631

    
632
-- Exit action for state :Parallel1_N1
633
node Parallel1_N1_ex(idParallel1_N1_1:int;
634
	x_1:int;
635
	idParallel1_Parallel1_1:int;
636
	isInner:bool)
637

    
638
returns (idParallel1_N1:int;
639
	x:int;
640
	idParallel1_Parallel1:int);
641

    
642

    
643
var 	idParallel1_N1_2, idParallel1_N1_3, idParallel1_N1_4, idParallel1_N1_5:int;
644
	x_2:int;
645
	idParallel1_Parallel1_2:int;
646

    
647

    
648
let
649

    
650

    
651

    
652
	
653
	(idParallel1_N1_2) 
654
	= 
655
	if ( idParallel1_N1_1 = 1374) then
656
	N1_A_ex(idParallel1_N1_1, false)
657
	 else (idParallel1_N1_1);
658

    
659
	
660

    
661
	(idParallel1_N1_3) 
662
	= 
663
	if ( idParallel1_N1_1 = 1375) then
664
	N1_B_ex(idParallel1_N1_1, false)
665
	 else (idParallel1_N1_1);
666

    
667
	
668

    
669
	(idParallel1_N1_4) 
670
	= 
671
		 if ( idParallel1_N1_1 = 1374) then 
672
		(idParallel1_N1_2)
673
		 else
674
		 if ( idParallel1_N1_1 = 1375) then 
675
		(idParallel1_N1_3)
676
		 else (idParallel1_N1_1);
677

    
678

    
679
	x_2 
680
	= if (not isInner) then  x_1 -10000
681
	 else x_1;
682
	
683

    
684
	-- set state as inactive 
685
	idParallel1_Parallel1_2
686
	 = if (not isInner) then 0 else idParallel1_Parallel1_1;
687

    
688
	idParallel1_N1_5 
689
	= 0;
690
	
691

    
692
	(idParallel1_N1, x, idParallel1_Parallel1) 
693
	= (idParallel1_N1_5, x_2, idParallel1_Parallel1_1);
694
	
695

    
696
tel
697

    
698

    
699

    
700

    
701

    
702
--During action for state :Parallel1_N1
703
node Parallel1_N1_du(x_1:int)
704

    
705
returns (x:int);
706

    
707

    
708
var 	x_2:int;
709

    
710

    
711
let
712

    
713

    
714

    
715
	x_2 
716
	=  x_1 +1000000;
717
	
718

    
719
	(x) 
720
	= (x_2);
721
	
722

    
723
tel
724

    
725

    
726
--***************************************************State :Parallel1_N2 Automaton***************************************************
727

    
728
node Parallel1_N2_node(idParallel1_N2_1:int;
729
	x_1:int;
730
	S2:bool;
731
	R2:bool)
732

    
733
returns (idParallel1_N2:int;
734
	x:int);
735

    
736

    
737
let
738

    
739
	 automaton parallel1_n2
740

    
741
	state POINTParallel1_N2:
742
	unless (idParallel1_N2_1=0) restart POINT__TO__N2_C_1
743

    
744

    
745

    
746
	unless (idParallel1_N2_1=1376) and S2 restart N2_C__TO__N2_D_1
747

    
748

    
749

    
750
	unless (idParallel1_N2_1=1377) and R2 restart N2_D__TO__N2_C_1
751

    
752

    
753

    
754
	unless (idParallel1_N2_1=1376) restart N2_C_IDL
755

    
756
	unless (idParallel1_N2_1=1377) restart N2_D_IDL
757

    
758
	let
759

    
760
		(idParallel1_N2, x) 
761
	= (idParallel1_N2_1, x_1);
762
	
763

    
764
	tel
765

    
766

    
767

    
768
	state POINT__TO__N2_C_1:
769

    
770
	 var 	idParallel1_N2_2:int;
771
	x_2:int;
772
	let
773

    
774
		-- transition trace :
775
	--POINT__To__N2_C_1
776
		(idParallel1_N2_2, x_2) 
777
	= N2_C_en(idParallel1_N2_1, x_1, false);
778
		
779

    
780
	(idParallel1_N2, x) 
781
	=  (idParallel1_N2_2, x_2);
782

    
783

    
784
	tel
785

    
786
	until true restart POINTParallel1_N2
787

    
788

    
789

    
790
	state N2_C__TO__N2_D_1:
791

    
792
	 var 	idParallel1_N2_2, idParallel1_N2_3:int;
793
	x_2, x_3:int;
794
	let
795

    
796
		-- transition trace :
797
	--N2_C__To__N2_D_1
798
		-- condition Action : x+=100;
799
		
800
		(x_2) 
801
	= N2_C__To__N2_D_1_Condition_Action(x_1);
802
		
803

    
804
		(idParallel1_N2_2) 
805
	= N2_C_ex(idParallel1_N2_1, false);
806
		
807

    
808
		(idParallel1_N2_3, x_3) 
809
	= N2_D_en(idParallel1_N2_2, x_2, false);
810
		
811

    
812
	(idParallel1_N2, x) 
813
	=  (idParallel1_N2_3, x_3);
814

    
815

    
816
	tel
817

    
818
	until true restart POINTParallel1_N2
819

    
820

    
821

    
822
	state N2_D__TO__N2_C_1:
823

    
824
	 var 	idParallel1_N2_2, idParallel1_N2_3:int;
825
	x_2, x_3:int;
826
	let
827

    
828
		-- transition trace :
829
	--N2_D__To__N2_C_1
830
		-- condition Action : x-=100;
831
		
832
		(x_2) 
833
	= N2_D__To__N2_C_1_Condition_Action(x_1);
834
		
835

    
836
		(idParallel1_N2_2) 
837
	= N2_D_ex(idParallel1_N2_1, false);
838
		
839

    
840
		(idParallel1_N2_3, x_3) 
841
	= N2_C_en(idParallel1_N2_2, x_2, false);
842
		
843

    
844
	(idParallel1_N2, x) 
845
	=  (idParallel1_N2_3, x_3);
846

    
847

    
848
	tel
849

    
850
	until true restart POINTParallel1_N2
851

    
852

    
853

    
854
	state N2_C_IDL:
855

    
856
	 	let
857

    
858
		
859

    
860
	(idParallel1_N2, x) 
861
	= (idParallel1_N2_1, x_1);
862
	
863

    
864
	tel
865

    
866
	until true restart POINTParallel1_N2
867

    
868

    
869

    
870
	state N2_D_IDL:
871

    
872
	 	let
873

    
874
		
875

    
876
	(idParallel1_N2, x) 
877
	= (idParallel1_N2_1, x_1);
878
	
879

    
880
	tel
881

    
882
	until true restart POINTParallel1_N2
883

    
884

    
885

    
886
tel
887

    
888

    
889
--***************************************************State :Parallel1_N1 Automaton***************************************************
890

    
891
node Parallel1_N1_node(idParallel1_N1_1:int;
892
	x_1:int;
893
	S1:bool;
894
	R1:bool)
895

    
896
returns (idParallel1_N1:int;
897
	x:int);
898

    
899

    
900
let
901

    
902
	 automaton parallel1_n1
903

    
904
	state POINTParallel1_N1:
905
	unless (idParallel1_N1_1=0) restart POINT__TO__N1_A_1
906

    
907

    
908

    
909
	unless (idParallel1_N1_1=1374) and S1 restart N1_A__TO__N1_B_1
910

    
911

    
912

    
913
	unless (idParallel1_N1_1=1375) and R1 restart N1_B__TO__N1_A_1
914

    
915

    
916

    
917
	unless (idParallel1_N1_1=1374) restart N1_A_IDL
918

    
919
	unless (idParallel1_N1_1=1375) restart N1_B_IDL
920

    
921
	let
922

    
923
		(idParallel1_N1, x) 
924
	= (idParallel1_N1_1, x_1);
925
	
926

    
927
	tel
928

    
929

    
930

    
931
	state POINT__TO__N1_A_1:
932

    
933
	 var 	idParallel1_N1_2:int;
934
	x_2:int;
935
	let
936

    
937
		-- transition trace :
938
	--POINT__To__N1_A_1
939
		(idParallel1_N1_2, x_2) 
940
	= N1_A_en(idParallel1_N1_1, x_1, false);
941
		
942

    
943
	(idParallel1_N1, x) 
944
	=  (idParallel1_N1_2, x_2);
945

    
946

    
947
	tel
948

    
949
	until true restart POINTParallel1_N1
950

    
951

    
952

    
953
	state N1_A__TO__N1_B_1:
954

    
955
	 var 	idParallel1_N1_2, idParallel1_N1_3:int;
956
	x_2, x_3:int;
957
	let
958

    
959
		-- transition trace :
960
	--N1_A__To__N1_B_1
961
		-- condition Action : x+=1;
962
		
963
		(x_2) 
964
	= N1_A__To__N1_B_1_Condition_Action(x_1);
965
		
966

    
967
		(idParallel1_N1_2) 
968
	= N1_A_ex(idParallel1_N1_1, false);
969
		
970

    
971
		(idParallel1_N1_3, x_3) 
972
	= N1_B_en(idParallel1_N1_2, x_2, false);
973
		
974

    
975
	(idParallel1_N1, x) 
976
	=  (idParallel1_N1_3, x_3);
977

    
978

    
979
	tel
980

    
981
	until true restart POINTParallel1_N1
982

    
983

    
984

    
985
	state N1_B__TO__N1_A_1:
986

    
987
	 var 	idParallel1_N1_2, idParallel1_N1_3:int;
988
	x_2, x_3:int;
989
	let
990

    
991
		-- transition trace :
992
	--N1_B__To__N1_A_1
993
		-- condition Action : x-=1;
994
		
995
		(x_2) 
996
	= N1_B__To__N1_A_1_Condition_Action(x_1);
997
		
998

    
999
		(idParallel1_N1_2) 
1000
	= N1_B_ex(idParallel1_N1_1, false);
1001
		
1002

    
1003
		(idParallel1_N1_3, x_3) 
1004
	= N1_A_en(idParallel1_N1_2, x_2, false);
1005
		
1006

    
1007
	(idParallel1_N1, x) 
1008
	=  (idParallel1_N1_3, x_3);
1009

    
1010

    
1011
	tel
1012

    
1013
	until true restart POINTParallel1_N1
1014

    
1015

    
1016

    
1017
	state N1_A_IDL:
1018

    
1019
	 	let
1020

    
1021
		
1022

    
1023
	(idParallel1_N1, x) 
1024
	= (idParallel1_N1_1, x_1);
1025
	
1026

    
1027
	tel
1028

    
1029
	until true restart POINTParallel1_N1
1030

    
1031

    
1032

    
1033
	state N1_B_IDL:
1034

    
1035
	 	let
1036

    
1037
		
1038

    
1039
	(idParallel1_N1, x) 
1040
	= (idParallel1_N1_1, x_1);
1041
	
1042

    
1043
	tel
1044

    
1045
	until true restart POINTParallel1_N1
1046

    
1047

    
1048

    
1049
tel
1050

    
1051

    
1052
--***************************************************State :Parallel1_Parallel1 Automaton***************************************************
1053

    
1054
node Parallel1_Parallel1_node(idParallel1_Parallel1_1:int;
1055
	idParallel1_N1_1:int;
1056
	x_1:int;
1057
	idParallel1_N2_1:int;
1058
	R1:bool;
1059
	S1:bool;
1060
	R2:bool;
1061
	S2:bool)
1062

    
1063
returns (idParallel1_Parallel1:int;
1064
	idParallel1_N1:int;
1065
	x:int;
1066
	idParallel1_N2:int);
1067

    
1068

    
1069
let
1070

    
1071
	 automaton parallel1_parallel1
1072

    
1073
	state POINTParallel1_Parallel1:
1074
	unless (idParallel1_Parallel1_1=0) restart PARALLEL1_PARALLEL1_PARALLEL_ENTRY
1075
	unless true  restart PARALLEL1_PARALLEL1_PARALLEL_IDL
1076

    
1077
	let
1078

    
1079
		(idParallel1_Parallel1, idParallel1_N1, x, idParallel1_N2) 
1080
	= (idParallel1_Parallel1_1, idParallel1_N1_1, x_1, idParallel1_N2_1);
1081
	
1082

    
1083
	tel
1084

    
1085

    
1086

    
1087
	state PARALLEL1_PARALLEL1_PARALLEL_ENTRY:
1088

    
1089
	 var 	idParallel1_Parallel1_2, idParallel1_Parallel1_3:int;
1090
	idParallel1_N1_2:int;
1091
	x_2, x_3:int;
1092
	idParallel1_N2_2:int;
1093
	let
1094

    
1095
		
1096
	(idParallel1_N1_2, idParallel1_Parallel1_2, x_2) 
1097
	= Parallel1_N1_en(idParallel1_N1_1, idParallel1_Parallel1_1, x_1, false);
1098

    
1099
	(idParallel1_N2_2, idParallel1_Parallel1_3, x_3) 
1100
	= Parallel1_N2_en(idParallel1_N2_1, idParallel1_Parallel1_2, x_2, false);
1101

    
1102

    
1103
	(idParallel1_Parallel1, idParallel1_N1, x, idParallel1_N2) 
1104
	= (idParallel1_Parallel1_3, idParallel1_N1_2, x_3, idParallel1_N2_2);
1105
	
1106

    
1107
	tel
1108

    
1109
	until true restart POINTParallel1_Parallel1
1110

    
1111

    
1112

    
1113
	state PARALLEL1_PARALLEL1_PARALLEL_IDL:
1114

    
1115
	 var 	idParallel1_N1_2:int;
1116
	x_2, x_3, x_4:int;
1117
	idParallel1_N2_2:int;
1118
	let
1119

    
1120
		
1121
	(x_2) 
1122
	= if not (idParallel1_N1_1= 0 ) then Parallel1_N1_du(x_1)
1123

    
1124
		 else (x_1);
1125

    
1126
		
1127

    
1128

    
1129
		(idParallel1_N1_2, x_3)
1130
	= if not (idParallel1_N1_1= 0 ) then Parallel1_N1_node(idParallel1_N1_1, x_2, S1, R1)
1131

    
1132
		 else (idParallel1_N1_1, x_2);
1133

    
1134
		
1135

    
1136
		
1137

    
1138
		(idParallel1_N2_2, x_4)
1139
	= if not (idParallel1_N2_1= 0 ) then Parallel1_N2_node(idParallel1_N2_1, x_3, S2, R2)
1140

    
1141
		 else (idParallel1_N2_1, x_3);
1142

    
1143
		
1144

    
1145
		
1146

    
1147
	(idParallel1_Parallel1, idParallel1_N1, x, idParallel1_N2) 
1148
	= (idParallel1_Parallel1_1, idParallel1_N1_2, x_4, idParallel1_N2_2);
1149
	
1150

    
1151
	tel
1152

    
1153
	until true restart POINTParallel1_Parallel1
1154

    
1155

    
1156

    
1157
tel
1158

    
1159

    
1160
--***************************************************State :Parallel1_Parallel1 Automaton***************************************************
1161

    
1162
node Parallel1_Parallel1(S1:bool;
1163
	R1:bool;
1164
	S2:bool;
1165
	R2:bool)
1166

    
1167
returns (x:int);
1168

    
1169

    
1170
var x_1: int;
1171

    
1172
	idParallel1_Parallel1, idParallel1_Parallel1_1: int;
1173

    
1174
	idParallel1_N2, idParallel1_N2_1: int;
1175

    
1176
	idParallel1_N1, idParallel1_N1_1: int;
1177

    
1178
		idParallel1_Parallel1_2, idParallel1_Parallel1_3, idParallel1_Parallel1_4:int;
1179
	idParallel1_N1_2, idParallel1_N1_3, idParallel1_N1_4:int;
1180
	x_2, x_3, x_4:int;
1181
	idParallel1_N2_2, idParallel1_N2_3, idParallel1_N2_4:int;
1182
let
1183

    
1184
	x_1 = 0 -> pre x;
1185

    
1186
	idParallel1_Parallel1_1 = 0 -> pre idParallel1_Parallel1;
1187

    
1188
	idParallel1_N2_1 = 0 -> pre idParallel1_N2;
1189

    
1190
	idParallel1_N1_1 = 0 -> pre idParallel1_N1;
1191

    
1192
	
1193

    
1194

    
1195

    
1196
	(idParallel1_Parallel1_2, idParallel1_N1_2, x_2, idParallel1_N2_2)
1197
	 = 
1198

    
1199
	 if S1 then Parallel1_Parallel1_node(idParallel1_Parallel1_1, idParallel1_N1_1, x_1, idParallel1_N2_1, false, S1, false, false)
1200

    
1201
	 else (idParallel1_Parallel1_1, idParallel1_N1_1, x_1, idParallel1_N2_1);
1202

    
1203
	
1204

    
1205

    
1206

    
1207
	(idParallel1_Parallel1_3, idParallel1_N1_3, x_3, idParallel1_N2_3)
1208
	 = 
1209

    
1210
	 if R1 then Parallel1_Parallel1_node(idParallel1_Parallel1_2, idParallel1_N1_2, x_2, idParallel1_N2_2, R1, false, false, false)
1211

    
1212
	 else (idParallel1_Parallel1_2, idParallel1_N1_2, x_2, idParallel1_N2_2);
1213

    
1214
	
1215

    
1216

    
1217

    
1218
	(idParallel1_Parallel1_4, idParallel1_N1_4, x_4, idParallel1_N2_4)
1219
	 = 
1220

    
1221
	 if S2 then Parallel1_Parallel1_node(idParallel1_Parallel1_3, idParallel1_N1_3, x_3, idParallel1_N2_3, false, false, false, S2)
1222

    
1223
	 else (idParallel1_Parallel1_3, idParallel1_N1_3, x_3, idParallel1_N2_3);
1224

    
1225
	
1226

    
1227

    
1228

    
1229
	(idParallel1_Parallel1, idParallel1_N1, x, idParallel1_N2)
1230
	 = 
1231

    
1232
	 if R2 then Parallel1_Parallel1_node(idParallel1_Parallel1_4, idParallel1_N1_4, x_4, idParallel1_N2_4, false, false, R2, false)
1233

    
1234
	 else (idParallel1_Parallel1_4, idParallel1_N1_4, x_4, idParallel1_N2_4);
1235

    
1236
	
1237

    
1238

    
1239
--unused outputs
1240
	
1241

    
1242
tel
1243

    
1244

    
1245

    
1246
node Parallel1 (S1_1_1 : real; R1_1_1 : real; S2_1_1 : real; R2_1_1 : real)
1247
returns (x_1_1 : int); 
1248
var
1249
	Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real; Mux_1_4 : real;
1250
	Parallel1_1_1 : int;
1251
	i_virtual_local : real;
1252
	Parallel1Mux_1_1_event: bool;
1253
	Parallel1Mux_1_2_event: bool;
1254
	Parallel1Mux_1_3_event: bool;
1255
	Parallel1Mux_1_4_event: bool;
1256
let 
1257
	Mux_1_1 = S1_1_1 ;
1258
	Mux_1_2 = R1_1_1 ;
1259
	Mux_1_3 = S2_1_1 ;
1260
	Mux_1_4 = R2_1_1 ;
1261
	Parallel1Mux_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));
1262
	Parallel1Mux_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));
1263
	Parallel1Mux_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));
1264
	Parallel1Mux_1_4_event = false -> ((pre(Mux_1_4) > 0.0 and Mux_1_4 <= 0.0) or (pre(Mux_1_4) <= 0.0 and Mux_1_4 > 0.0));
1265
	Parallel1_1_1 =  Parallel1_Parallel1(Parallel1Mux_1_1_event, Parallel1Mux_1_2_event, Parallel1Mux_1_3_event, Parallel1Mux_1_4_event);
1266
	x_1_1 = Parallel1_1_1;
1267
	i_virtual_local= 0.0 -> 1.0;
1268
tel
1269