Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions1 / Junctions1.lus @ eb639349

History | View | Annotate | Download (7.29 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_ChartJunction1149_1_Condition_Action(y_1:int;
11
	z_1:int)
12

    
13
returns (y:int;
14
	z:int);
15

    
16

    
17
var 	y_2:int;
18
	z_2:int;
19

    
20

    
21
let
22

    
23

    
24

    
25
	y_2 
26
	=  y_1  + 1;
27
	
28

    
29
	z_2 
30
	=  z_1 +2;
31
	
32

    
33
	(y, z) 
34
	= (y_2, z_2);
35
	
36

    
37
tel
38

    
39

    
40

    
41

    
42

    
43

    
44
node Chart_ChartJunction1149__To__Chart_B_1_Condition_Action(y_1:int;
45
	z_1:int)
46

    
47
returns (y:int;
48
	z:int);
49

    
50

    
51
var 	y_2:int;
52
	z_2:int;
53

    
54

    
55
let
56

    
57

    
58

    
59
	y_2 
60
	=  y_1 +2;
61
	
62

    
63
	z_2 
64
	=  z_1  + 1;
65
	
66

    
67
	(y, z) 
68
	= (y_2, z_2);
69
	
70

    
71
tel
72

    
73

    
74

    
75

    
76

    
77

    
78
node Chart_ChartJunction1149__To__Chart_C_2_Condition_Action(y_1:int;
79
	z_1:int)
80

    
81
returns (y:int;
82
	z:int);
83

    
84

    
85
var 	y_2:int;
86
	z_2:int;
87

    
88

    
89
let
90

    
91

    
92

    
93
	y_2 
94
	=  y_1  + 1;
95
	
96

    
97
	z_2 
98
	=  z_1  + 1;
99
	
100

    
101
	(y, z) 
102
	= (y_2, z_2);
103
	
104

    
105
tel
106

    
107

    
108

    
109

    
110

    
111

    
112

    
113

    
114
-- Entry action for state :Chart_B
115
node Chart_B_en(idChart_Chart_1:int;
116
	isInner:bool)
117

    
118
returns (idChart_Chart:int);
119

    
120

    
121
var 	idChart_Chart_2:int;
122

    
123

    
124
let
125

    
126

    
127

    
128
	-- set state as active 
129
	idChart_Chart_2 
130
	= 1144;
131
	
132

    
133
	(idChart_Chart) 
134
	= (idChart_Chart_2);
135
	
136

    
137
tel
138

    
139

    
140

    
141

    
142

    
143
-- Exit action for state :Chart_B
144
node Chart_B_ex(idChart_Chart_1:int;
145
	isInner:bool)
146

    
147
returns (idChart_Chart:int);
148

    
149

    
150
var 	idChart_Chart_2:int;
151

    
152

    
153
let
154

    
155

    
156

    
157
	-- set state as inactive 
158
	idChart_Chart_2
159
	 = if (not isInner) then 0 else idChart_Chart_1;
160

    
161

    
162
	(idChart_Chart) 
163
	= (idChart_Chart_1);
164
	
165

    
166
tel
167

    
168

    
169

    
170

    
171

    
172

    
173
-- Exit action for state :Chart_A
174
node Chart_A_ex(y_1:int;
175
	idChart_Chart_1:int;
176
	isInner:bool)
177

    
178
returns (y:int;
179
	idChart_Chart:int);
180

    
181

    
182
var 	y_2:int;
183
	idChart_Chart_2:int;
184

    
185

    
186
let
187

    
188

    
189

    
190
	y_2 
191
	= if (not isInner) then  y_1 *2
192
	 else y_1;
193
	
194

    
195
	-- set state as inactive 
196
	idChart_Chart_2
197
	 = if (not isInner) then 0 else idChart_Chart_1;
198

    
199

    
200
	(y, idChart_Chart) 
201
	= (y_2, idChart_Chart_1);
202
	
203

    
204
tel
205

    
206

    
207

    
208

    
209

    
210
-- Entry action for state :Chart_A
211
node Chart_A_en(idChart_Chart_1:int;
212
	isInner:bool)
213

    
214
returns (idChart_Chart:int);
215

    
216

    
217
var 	idChart_Chart_2:int;
218

    
219

    
220
let
221

    
222

    
223

    
224
	-- set state as active 
225
	idChart_Chart_2 
226
	= 1142;
227
	
228

    
229
	(idChart_Chart) 
230
	= (idChart_Chart_2);
231
	
232

    
233
tel
234

    
235

    
236

    
237

    
238

    
239

    
240
-- Entry action for state :Chart_C
241
node Chart_C_en(idChart_Chart_1:int;
242
	isInner:bool)
243

    
244
returns (idChart_Chart:int);
245

    
246

    
247
var 	idChart_Chart_2:int;
248

    
249

    
250
let
251

    
252

    
253

    
254
	-- set state as active 
255
	idChart_Chart_2 
256
	= 1143;
257
	
258

    
259
	(idChart_Chart) 
260
	= (idChart_Chart_2);
261
	
262

    
263
tel
264

    
265

    
266

    
267

    
268

    
269
-- Exit action for state :Chart_C
270
node Chart_C_ex(idChart_Chart_1:int;
271
	isInner:bool)
272

    
273
returns (idChart_Chart:int);
274

    
275

    
276
var 	idChart_Chart_2:int;
277

    
278

    
279
let
280

    
281

    
282

    
283
	-- set state as inactive 
284
	idChart_Chart_2
285
	 = if (not isInner) then 0 else idChart_Chart_1;
286

    
287

    
288
	(idChart_Chart) 
289
	= (idChart_Chart_1);
290
	
291

    
292
tel
293

    
294

    
295
--***************************************************State :Chart_Chart Automaton***************************************************
296

    
297
node Chart_Chart_node(idChart_Chart_1:int;
298
	E1:bool;
299
	x:int;
300
	y_1:int;
301
	z_1:int)
302

    
303
returns (idChart_Chart:int;
304
	y:int;
305
	z:int);
306

    
307

    
308
let
309

    
310
	 automaton chart_chart
311

    
312
	state POINTChart_Chart:
313
	unless (idChart_Chart_1=0) restart POINT__TO__CHART_A_1
314

    
315

    
316

    
317
	unless (idChart_Chart_1=1142) and E1 and ( x>0 ) restart CHART_A__TO__CHART_CHARTJUNCTION1149_1
318

    
319

    
320

    
321
	unless (idChart_Chart_1=1143) and ( x>3 ) restart CHART_C__TO__CHART_A_1
322

    
323

    
324

    
325
	unless (idChart_Chart_1=1144) and ( x>3 ) restart CHART_B__TO__CHART_A_1
326

    
327

    
328

    
329
	unless (idChart_Chart_1=1142) restart CHART_A_IDL
330

    
331
	unless (idChart_Chart_1=1143) restart CHART_C_IDL
332

    
333
	unless (idChart_Chart_1=1144) restart CHART_B_IDL
334

    
335
	let
336

    
337
		(idChart_Chart, y, z) 
338
	= (idChart_Chart_1, y_1, z_1);
339
	
340

    
341
	tel
342

    
343

    
344

    
345
	state POINT__TO__CHART_A_1:
346

    
347
	 var 	idChart_Chart_2:int;
348
	let
349

    
350
		-- transition trace :
351
	--POINT__To__Chart_A_1
352
		(idChart_Chart_2) 
353
	= Chart_A_en(idChart_Chart_1, false);
354
		
355

    
356
	(idChart_Chart) 
357
	=  (idChart_Chart_2);
358

    
359
	--add unused variables
360
	(y, z) 
361
	= (y_1, z_1);
362
	
363

    
364
	tel
365

    
366
	until true restart POINTChart_Chart
367

    
368

    
369

    
370
	state CHART_A__TO__CHART_CHARTJUNCTION1149_1:
371

    
372
	 var 	idChart_Chart_2, idChart_Chart_3, idChart_Chart_4, idChart_Chart_5:int;
373
	y_2, y_3, y_4, y_5, y_6, y_7:int;
374
	z_2, z_3, z_4, z_5:int;
375
	let
376

    
377
		
378

    
379
-- transition trace :
380
	--Chart_A__To__Junction1149_1, Junction1149__To__Chart_B_1
381
		-- condition Action : y++;z+=2
382
		
383
		(y_2, z_2) 
384
	= Chart_A__To__Chart_ChartJunction1149_1_Condition_Action(y_1, z_1);
385
		
386

    
387
		-- condition Action : y+=2;z++
388
		
389
		(y_3, z_3) 
390
	= 
391
		 if (( x>=2 )) then 
392
		Chart_ChartJunction1149__To__Chart_B_1_Condition_Action(y_2, z_2)
393
		 else (y_2, z_2);
394
		
395

    
396
		(y_4, idChart_Chart_2) 
397
	= 
398
		 if (( x>=2 )) then 
399
		Chart_A_ex(y_3, idChart_Chart_1, false)
400
		 else (y_3, idChart_Chart_1);
401
		
402

    
403
		(idChart_Chart_3) 
404
	= 
405
		 if (( x>=2 )) then 
406
		Chart_B_en(idChart_Chart_2, false)
407
		 else (idChart_Chart_2);
408
		
409

    
410

    
411
-- transition trace :
412
	--Chart_A__To__Junction1149_1, Junction1149__To__Chart_C_2
413
		-- condition Action : y++;z+=2
414
		
415
		(y_5, z_4) 
416
	= Chart_A__To__Chart_ChartJunction1149_1_Condition_Action(y_1, z_1);
417
		
418

    
419
		-- condition Action : y++;z++
420
		
421
		(y_6, z_5) 
422
	= 
423
		 if (( x<2 )) then 
424
		Chart_ChartJunction1149__To__Chart_C_2_Condition_Action(y_5, z_4)
425
		 else (y_5, z_4);
426
		
427

    
428
		(y_7, idChart_Chart_4) 
429
	= 
430
		 if (( x<2 )) then 
431
		Chart_A_ex(y_6, idChart_Chart_1, false)
432
		 else (y_6, idChart_Chart_1);
433
		
434

    
435
		(idChart_Chart_5) 
436
	= 
437
		 if (( x<2 )) then 
438
		Chart_C_en(idChart_Chart_4, false)
439
		 else (idChart_Chart_4);
440
		
441

    
442
	(idChart_Chart, y, z) 
443
	= 
444
		 if (( x>=2 )) then 
445
		(idChart_Chart_3, y_4, z_3)
446
		 else
447
		 if (( x<2 )) then 
448
		(idChart_Chart_5, y_7, z_5)
449
		 else (idChart_Chart_1, y_5, z_4);
450

    
451

    
452
	tel
453

    
454
	until true restart POINTChart_Chart
455

    
456

    
457

    
458
	state CHART_C__TO__CHART_A_1:
459

    
460
	 var 	idChart_Chart_2, idChart_Chart_3:int;
461
	let
462

    
463
		-- transition trace :
464
	--Chart_C__To__Chart_A_1
465
		(idChart_Chart_2) 
466
	= Chart_C_ex(idChart_Chart_1, false);
467
		
468

    
469
		(idChart_Chart_3) 
470
	= Chart_A_en(idChart_Chart_2, false);
471
		
472

    
473
	(idChart_Chart, y, z) 
474
	=  (idChart_Chart_3, y_1, z_1);
475

    
476

    
477
	tel
478

    
479
	until true restart POINTChart_Chart
480

    
481

    
482

    
483
	state CHART_B__TO__CHART_A_1:
484

    
485
	 var 	idChart_Chart_2, idChart_Chart_3:int;
486
	let
487

    
488
		-- transition trace :
489
	--Chart_B__To__Chart_A_1
490
		(idChart_Chart_2) 
491
	= Chart_B_ex(idChart_Chart_1, false);
492
		
493

    
494
		(idChart_Chart_3) 
495
	= Chart_A_en(idChart_Chart_2, false);
496
		
497

    
498
	(idChart_Chart, y, z) 
499
	=  (idChart_Chart_3, y_1, z_1);
500

    
501

    
502
	tel
503

    
504
	until true restart POINTChart_Chart
505

    
506

    
507

    
508
	state CHART_A_IDL:
509

    
510
	 	let
511

    
512
		
513

    
514
	(idChart_Chart, y, z) 
515
	= (idChart_Chart_1, y_1, z_1);
516
	
517

    
518
	tel
519

    
520
	until true restart POINTChart_Chart
521

    
522

    
523

    
524
	state CHART_C_IDL:
525

    
526
	 	let
527

    
528
		
529

    
530
	(idChart_Chart, y, z) 
531
	= (idChart_Chart_1, y_1, z_1);
532
	
533

    
534
	tel
535

    
536
	until true restart POINTChart_Chart
537

    
538

    
539

    
540
	state CHART_B_IDL:
541

    
542
	 	let
543

    
544
		
545

    
546
	(idChart_Chart, y, z) 
547
	= (idChart_Chart_1, y_1, z_1);
548
	
549

    
550
	tel
551

    
552
	until true restart POINTChart_Chart
553

    
554

    
555

    
556
tel
557

    
558

    
559
--***************************************************State :Chart_Chart Automaton***************************************************
560

    
561
node Junctions1_Chart(x:int;
562
	E1:bool)
563

    
564
returns (y:int;
565
	z:int);
566

    
567

    
568
var y_1: int;
569

    
570
	z_1: int;
571

    
572
	idChart_Chart, idChart_Chart_1: int;
573

    
574
	let
575

    
576
	y_1 = 1 -> pre y;
577

    
578
	z_1 = 2 -> pre z;
579

    
580
	idChart_Chart_1 = 0 -> pre idChart_Chart;
581

    
582
	
583

    
584

    
585

    
586
	(idChart_Chart, y, z)
587
	 = 
588

    
589
	 if E1 then Chart_Chart_node(idChart_Chart_1, E1, x, y_1, z_1)
590

    
591
	 else (idChart_Chart_1, y_1, z_1);
592

    
593
	
594

    
595

    
596
--unused outputs
597
	
598

    
599
tel
600

    
601

    
602

    
603
node Junctions1 (x_1_1 : int; E1_1_1 : real)
604
returns (y_1_1 : int;
605
	z_2_1 : int); 
606
var
607
	Chart_1_1 : int; Chart_2_1 : int;
608
	i_virtual_local : real;
609
	ChartE1_1_1_event: bool;
610
let 
611
	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));
612
	(Chart_1_1, Chart_2_1) =  Junctions1_Chart(x_1_1, ChartE1_1_1_event);
613
	y_1_1 = Chart_1_1;
614
	z_2_1 = Chart_2_1;
615
	i_virtual_local= 0.0 -> 1.0;
616
tel
617