Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions1V0 / Junctions1V0.lus @ eb639349

History | View | Annotate | Download (7.9 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9

    
10
node Chart_A__To__Chart_ChartJunction1192_1_Condition_Action(y_1:int)
11

    
12
returns (y:int);
13

    
14

    
15
var 	y_2:int;
16

    
17

    
18
let
19

    
20

    
21

    
22
	y_2 
23
	=  y_1  + 1;
24
	
25

    
26
	(y) 
27
	= (y_2);
28
	
29

    
30
tel
31

    
32

    
33

    
34

    
35

    
36
node Chart_A__To__Chart_ChartJunction1192_1_Transition_Action(z_1:int)
37

    
38
returns (z:int);
39

    
40

    
41
var 	z_2:int;
42

    
43

    
44
let
45

    
46

    
47

    
48
	z_2 
49
	=  z_1 +2;
50
	
51

    
52
	(z) 
53
	= (z_2);
54
	
55

    
56
tel
57

    
58

    
59

    
60

    
61

    
62

    
63
node Chart_ChartJunction1192__To__Chart_C_2_Condition_Action(y_1:int)
64

    
65
returns (y:int);
66

    
67

    
68
var 	y_2:int;
69

    
70

    
71
let
72

    
73

    
74

    
75
	y_2 
76
	=  y_1  + 1;
77
	
78

    
79
	(y) 
80
	= (y_2);
81
	
82

    
83
tel
84

    
85

    
86

    
87

    
88

    
89
node Chart_ChartJunction1192__To__Chart_C_2_Transition_Action(z_1:int)
90

    
91
returns (z:int);
92

    
93

    
94
var 	z_2:int;
95

    
96

    
97
let
98

    
99

    
100

    
101
	z_2 
102
	=  z_1  + 1;
103
	
104

    
105
	(z) 
106
	= (z_2);
107
	
108

    
109
tel
110

    
111

    
112

    
113

    
114

    
115

    
116

    
117
node Chart_ChartJunction1192__To__Chart_B_1_Condition_Action(y_1:int)
118

    
119
returns (y:int);
120

    
121

    
122
var 	y_2:int;
123

    
124

    
125
let
126

    
127

    
128

    
129
	y_2 
130
	=  y_1 +2;
131
	
132

    
133
	(y) 
134
	= (y_2);
135
	
136

    
137
tel
138

    
139

    
140

    
141

    
142

    
143
node Chart_ChartJunction1192__To__Chart_B_1_Transition_Action(z_1:int)
144

    
145
returns (z:int);
146

    
147

    
148
var 	z_2, z_3:int;
149

    
150

    
151
let
152

    
153

    
154

    
155
	z_2 
156
	=  z_1  + 1;
157
	
158

    
159
	z_3 
160
	=  z_2  + 1;
161
	
162

    
163
	(z) 
164
	= (z_3);
165
	
166

    
167
tel
168

    
169

    
170

    
171

    
172

    
173

    
174

    
175
-- Entry action for state :Chart_B
176
node Chart_B_en(idChart_Chart_1:int;
177
	isInner:bool)
178

    
179
returns (idChart_Chart:int);
180

    
181

    
182
var 	idChart_Chart_2:int;
183

    
184

    
185
let
186

    
187

    
188

    
189
	-- set state as active 
190
	idChart_Chart_2 
191
	= 1186;
192
	
193

    
194
	(idChart_Chart) 
195
	= (idChart_Chart_2);
196
	
197

    
198
tel
199

    
200

    
201

    
202

    
203

    
204
-- Exit action for state :Chart_B
205
node Chart_B_ex(idChart_Chart_1:int;
206
	isInner:bool)
207

    
208
returns (idChart_Chart:int);
209

    
210

    
211
var 	idChart_Chart_2:int;
212

    
213

    
214
let
215

    
216

    
217

    
218
	-- set state as inactive 
219
	idChart_Chart_2
220
	 = if (not isInner) then 0 else idChart_Chart_1;
221

    
222

    
223
	(idChart_Chart) 
224
	= (idChart_Chart_1);
225
	
226

    
227
tel
228

    
229

    
230

    
231

    
232

    
233

    
234
-- Entry action for state :Chart_A
235
node Chart_A_en(idChart_Chart_1:int;
236
	isInner:bool)
237

    
238
returns (idChart_Chart:int);
239

    
240

    
241
var 	idChart_Chart_2:int;
242

    
243

    
244
let
245

    
246

    
247

    
248
	-- set state as active 
249
	idChart_Chart_2 
250
	= 1185;
251
	
252

    
253
	(idChart_Chart) 
254
	= (idChart_Chart_2);
255
	
256

    
257
tel
258

    
259

    
260

    
261

    
262

    
263
-- Exit action for state :Chart_A
264
node Chart_A_ex(idChart_Chart_1:int;
265
	isInner:bool)
266

    
267
returns (idChart_Chart:int);
268

    
269

    
270
var 	idChart_Chart_2:int;
271

    
272

    
273
let
274

    
275

    
276

    
277
	-- set state as inactive 
278
	idChart_Chart_2
279
	 = if (not isInner) then 0 else idChart_Chart_1;
280

    
281

    
282
	(idChart_Chart) 
283
	= (idChart_Chart_1);
284
	
285

    
286
tel
287

    
288

    
289

    
290

    
291

    
292

    
293
-- Entry action for state :Chart_C
294
node Chart_C_en(idChart_Chart_1:int;
295
	isInner:bool)
296

    
297
returns (idChart_Chart:int);
298

    
299

    
300
var 	idChart_Chart_2:int;
301

    
302

    
303
let
304

    
305

    
306

    
307
	-- set state as active 
308
	idChart_Chart_2 
309
	= 1187;
310
	
311

    
312
	(idChart_Chart) 
313
	= (idChart_Chart_2);
314
	
315

    
316
tel
317

    
318

    
319

    
320

    
321

    
322
-- Exit action for state :Chart_C
323
node Chart_C_ex(idChart_Chart_1:int;
324
	isInner:bool)
325

    
326
returns (idChart_Chart:int);
327

    
328

    
329
var 	idChart_Chart_2:int;
330

    
331

    
332
let
333

    
334

    
335

    
336
	-- set state as inactive 
337
	idChart_Chart_2
338
	 = if (not isInner) then 0 else idChart_Chart_1;
339

    
340

    
341
	(idChart_Chart) 
342
	= (idChart_Chart_1);
343
	
344

    
345
tel
346

    
347

    
348
--***************************************************State :Chart_Chart Automaton***************************************************
349

    
350
node Chart_Chart_node(idChart_Chart_1:int;
351
	E1:bool;
352
	x:int;
353
	y_1:int;
354
	z_1:int)
355

    
356
returns (idChart_Chart:int;
357
	y:int;
358
	z:int);
359

    
360

    
361
let
362

    
363
	 automaton chart_chart
364

    
365
	state POINTChart_Chart:
366
	unless (idChart_Chart_1=0) restart POINT__TO__CHART_A_1
367

    
368

    
369

    
370
	unless (idChart_Chart_1=1185) and E1 and ( x>0 ) restart CHART_A__TO__CHART_CHARTJUNCTION1192_1
371

    
372

    
373

    
374
	unless (idChart_Chart_1=1186) and ( x>3 ) restart CHART_B__TO__CHART_A_1
375

    
376

    
377

    
378
	unless (idChart_Chart_1=1187) and ( x>3 ) restart CHART_C__TO__CHART_A_1
379

    
380

    
381

    
382
	unless (idChart_Chart_1=1185) restart CHART_A_IDL
383

    
384
	unless (idChart_Chart_1=1186) restart CHART_B_IDL
385

    
386
	unless (idChart_Chart_1=1187) restart CHART_C_IDL
387

    
388
	let
389

    
390
		(idChart_Chart, y, z) 
391
	= (idChart_Chart_1, y_1, z_1);
392
	
393

    
394
	tel
395

    
396

    
397

    
398
	state POINT__TO__CHART_A_1:
399

    
400
	 var 	idChart_Chart_2:int;
401
	let
402

    
403
		-- transition trace :
404
	--POINT__To__Chart_A_1
405
		(idChart_Chart_2) 
406
	= Chart_A_en(idChart_Chart_1, false);
407
		
408

    
409
	(idChart_Chart) 
410
	=  (idChart_Chart_2);
411

    
412
	--add unused variables
413
	(y, z) 
414
	= (y_1, z_1);
415
	
416

    
417
	tel
418

    
419
	until true restart POINTChart_Chart
420

    
421

    
422

    
423
	state CHART_A__TO__CHART_CHARTJUNCTION1192_1:
424

    
425
	 var 	idChart_Chart_2, idChart_Chart_3, idChart_Chart_4, idChart_Chart_5:int;
426
	y_2, y_3, y_4, y_5:int;
427
	z_2, z_3, z_4, z_5:int;
428
	let
429

    
430
		
431

    
432
-- transition trace :
433
	--Chart_A__To__Junction1192_1, Junction1192__To__Chart_B_1
434
		-- condition Action : y++
435
		
436
		(y_2) 
437
	= Chart_A__To__Chart_ChartJunction1192_1_Condition_Action(y_1);
438
		
439

    
440
		-- condition Action : y+=2
441
		
442
		(y_3) 
443
	= 
444
		 if (( x>2 )) then 
445
		Chart_ChartJunction1192__To__Chart_B_1_Condition_Action(y_2)
446
		 else (y_2);
447
		
448

    
449
		(idChart_Chart_2) 
450
	= 
451
		 if (( x>2 )) then 
452
		Chart_A_ex(idChart_Chart_1, false)
453
		 else (idChart_Chart_1);
454
		
455

    
456
		(z_2) 
457
	= 
458
		 if (( x>2 )) then 
459
		Chart_A__To__Chart_ChartJunction1192_1_Transition_Action(z_1)
460
		 else (z_1);
461
		
462

    
463
		(z_3) 
464
	= 
465
		 if (( x>2 )) then 
466
		Chart_ChartJunction1192__To__Chart_B_1_Transition_Action(z_2)
467
		 else (z_2);
468
		
469

    
470
		(idChart_Chart_3) 
471
	= 
472
		 if (( x>2 )) then 
473
		Chart_B_en(idChart_Chart_2, false)
474
		 else (idChart_Chart_2);
475
		
476

    
477

    
478
-- transition trace :
479
	--Chart_A__To__Junction1192_1, Junction1192__To__Chart_C_2
480
		-- condition Action : y++
481
		
482
		(y_4) 
483
	= Chart_A__To__Chart_ChartJunction1192_1_Condition_Action(y_1);
484
		
485

    
486
		-- condition Action : y++
487
		
488
		(y_5) 
489
	= 
490
		 if (( x<=2 )) then 
491
		Chart_ChartJunction1192__To__Chart_C_2_Condition_Action(y_4)
492
		 else (y_4);
493
		
494

    
495
		(idChart_Chart_4) 
496
	= 
497
		 if (( x<=2 )) then 
498
		Chart_A_ex(idChart_Chart_1, false)
499
		 else (idChart_Chart_1);
500
		
501

    
502
		(z_4) 
503
	= 
504
		 if (( x<=2 )) then 
505
		Chart_A__To__Chart_ChartJunction1192_1_Transition_Action(z_1)
506
		 else (z_1);
507
		
508

    
509
		(z_5) 
510
	= 
511
		 if (( x<=2 )) then 
512
		Chart_ChartJunction1192__To__Chart_C_2_Transition_Action(z_4)
513
		 else (z_4);
514
		
515

    
516
		(idChart_Chart_5) 
517
	= 
518
		 if (( x<=2 )) then 
519
		Chart_C_en(idChart_Chart_4, false)
520
		 else (idChart_Chart_4);
521
		
522

    
523
	(idChart_Chart, y, z) 
524
	= 
525
		 if (( x>2 )) then 
526
		(idChart_Chart_3, y_3, z_3)
527
		 else
528
		 if (( x<=2 )) then 
529
		(idChart_Chart_5, y_5, z_5)
530
		 else (idChart_Chart_1, y_4, z_1);
531

    
532

    
533
	tel
534

    
535
	until true restart POINTChart_Chart
536

    
537

    
538

    
539
	state CHART_B__TO__CHART_A_1:
540

    
541
	 var 	idChart_Chart_2, idChart_Chart_3:int;
542
	let
543

    
544
		-- transition trace :
545
	--Chart_B__To__Chart_A_1
546
		(idChart_Chart_2) 
547
	= Chart_B_ex(idChart_Chart_1, false);
548
		
549

    
550
		(idChart_Chart_3) 
551
	= Chart_A_en(idChart_Chart_2, false);
552
		
553

    
554
	(idChart_Chart, y, z) 
555
	=  (idChart_Chart_3, y_1, z_1);
556

    
557

    
558
	tel
559

    
560
	until true restart POINTChart_Chart
561

    
562

    
563

    
564
	state CHART_C__TO__CHART_A_1:
565

    
566
	 var 	idChart_Chart_2, idChart_Chart_3:int;
567
	let
568

    
569
		-- transition trace :
570
	--Chart_C__To__Chart_A_1
571
		(idChart_Chart_2) 
572
	= Chart_C_ex(idChart_Chart_1, false);
573
		
574

    
575
		(idChart_Chart_3) 
576
	= Chart_A_en(idChart_Chart_2, false);
577
		
578

    
579
	(idChart_Chart, y, z) 
580
	=  (idChart_Chart_3, y_1, z_1);
581

    
582

    
583
	tel
584

    
585
	until true restart POINTChart_Chart
586

    
587

    
588

    
589
	state CHART_A_IDL:
590

    
591
	 	let
592

    
593
		
594

    
595
	(idChart_Chart, y, z) 
596
	= (idChart_Chart_1, y_1, z_1);
597
	
598

    
599
	tel
600

    
601
	until true restart POINTChart_Chart
602

    
603

    
604

    
605
	state CHART_B_IDL:
606

    
607
	 	let
608

    
609
		
610

    
611
	(idChart_Chart, y, z) 
612
	= (idChart_Chart_1, y_1, z_1);
613
	
614

    
615
	tel
616

    
617
	until true restart POINTChart_Chart
618

    
619

    
620

    
621
	state CHART_C_IDL:
622

    
623
	 	let
624

    
625
		
626

    
627
	(idChart_Chart, y, z) 
628
	= (idChart_Chart_1, y_1, z_1);
629
	
630

    
631
	tel
632

    
633
	until true restart POINTChart_Chart
634

    
635

    
636

    
637
tel
638

    
639

    
640
--***************************************************State :Chart_Chart Automaton***************************************************
641

    
642
node Junctions1V0_Chart(x:int;
643
	E1:bool)
644

    
645
returns (y:int;
646
	z:int);
647

    
648

    
649
var y_1: int;
650

    
651
	z_1: int;
652

    
653
	idChart_Chart, idChart_Chart_1: int;
654

    
655
	let
656

    
657
	y_1 = 1 -> pre y;
658

    
659
	z_1 = 2 -> pre z;
660

    
661
	idChart_Chart_1 = 0 -> pre idChart_Chart;
662

    
663
	
664

    
665

    
666

    
667
	(idChart_Chart, y, z)
668
	 = 
669

    
670
	 if E1 then Chart_Chart_node(idChart_Chart_1, E1, x, y_1, z_1)
671

    
672
	 else (idChart_Chart_1, y_1, z_1);
673

    
674
	
675

    
676

    
677
--unused outputs
678
	
679

    
680
tel
681

    
682

    
683

    
684
node Junctions1V0 (x_1_1 : int; E1_1_1 : real)
685
returns (y_1_1 : int;
686
	z_2_1 : int); 
687
var
688
	Chart_1_1 : int; Chart_2_1 : int;
689
	i_virtual_local : real;
690
	ChartE1_1_1_event: bool;
691
let 
692
	ChartE1_1_1_event = false -> ((pre(E1_1_1) > 0.0 and E1_1_1 <= 0.0) or (pre(E1_1_1) <= 0.0 and E1_1_1 > 0.0));
693
	(Chart_1_1, Chart_2_1) =  Junctions1V0_Chart(x_1_1, ChartE1_1_1_event);
694
	y_1_1 = Chart_1_1;
695
	z_2_1 = Chart_2_1;
696
	i_virtual_local= 0.0 -> 1.0;
697
tel
698