Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Junctions3 / Junctions3.lus @ eb639349

History | View | Annotate | Download (6.64 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9
node Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action(y_1:int)
10

    
11
returns (y:int);
12

    
13

    
14
var 	y_2:int;
15

    
16

    
17
let
18

    
19

    
20

    
21
	y_2 
22
	=  y_1  + 1;
23
	
24

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

    
29
tel
30

    
31

    
32

    
33

    
34

    
35

    
36
node Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action(y_1:int)
37

    
38
returns (y:int);
39

    
40

    
41
var 	y_2:int;
42

    
43

    
44
let
45

    
46

    
47

    
48
	y_2 
49
	=  y_1  + 1;
50
	
51

    
52
	(y) 
53
	= (y_2);
54
	
55

    
56
tel
57

    
58

    
59

    
60

    
61

    
62

    
63

    
64
node Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action(y_1:int)
65

    
66
returns (y:int);
67

    
68

    
69
var 	y_2:int;
70

    
71

    
72
let
73

    
74

    
75

    
76
	y_2 
77
	=  y_1  + 1;
78
	
79

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

    
84
tel
85

    
86

    
87

    
88

    
89

    
90

    
91
node Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action(y_1:int)
92

    
93
returns (y:int);
94

    
95

    
96
var 	y_2:int;
97

    
98

    
99
let
100

    
101

    
102

    
103
	y_2 
104
	= 0;
105
	
106

    
107
	(y) 
108
	= (y_2);
109
	
110

    
111
tel
112

    
113

    
114

    
115

    
116

    
117

    
118
node Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action(y_1:int)
119

    
120
returns (y:int);
121

    
122

    
123
var 	y_2:int;
124

    
125

    
126
let
127

    
128

    
129

    
130
	y_2 
131
	=  y_1  + 1;
132
	
133

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

    
138
tel
139

    
140

    
141

    
142

    
143

    
144

    
145
-- Entry action for state :Junctions3_B
146
node Junctions3_B_en(idJunctions3_Junctions3_1:int;
147
	isInner:bool)
148

    
149
returns (idJunctions3_Junctions3:int);
150

    
151

    
152
var 	idJunctions3_Junctions3_2:int;
153

    
154

    
155
let
156

    
157

    
158

    
159
	-- set state as active 
160
	idJunctions3_Junctions3_2 
161
	= 1225;
162
	
163

    
164
	(idJunctions3_Junctions3) 
165
	= (idJunctions3_Junctions3_2);
166
	
167

    
168
tel
169

    
170

    
171

    
172

    
173

    
174
-- Exit action for state :Junctions3_B
175
node Junctions3_B_ex(idJunctions3_Junctions3_1:int;
176
	isInner:bool)
177

    
178
returns (idJunctions3_Junctions3:int);
179

    
180

    
181
var 	idJunctions3_Junctions3_2:int;
182

    
183

    
184
let
185

    
186

    
187

    
188
	-- set state as inactive 
189
	idJunctions3_Junctions3_2
190
	 = if (not isInner) then 0 else idJunctions3_Junctions3_1;
191

    
192

    
193
	(idJunctions3_Junctions3) 
194
	= (idJunctions3_Junctions3_1);
195
	
196

    
197
tel
198

    
199

    
200

    
201

    
202

    
203

    
204
-- Entry action for state :Junctions3_A
205
node Junctions3_A_en(idJunctions3_Junctions3_1:int;
206
	isInner:bool)
207

    
208
returns (idJunctions3_Junctions3:int);
209

    
210

    
211
var 	idJunctions3_Junctions3_2:int;
212

    
213

    
214
let
215

    
216

    
217

    
218
	-- set state as active 
219
	idJunctions3_Junctions3_2 
220
	= 1224;
221
	
222

    
223
	(idJunctions3_Junctions3) 
224
	= (idJunctions3_Junctions3_2);
225
	
226

    
227
tel
228

    
229

    
230

    
231

    
232

    
233
-- Exit action for state :Junctions3_A
234
node Junctions3_A_ex(idJunctions3_Junctions3_1:int;
235
	isInner:bool)
236

    
237
returns (idJunctions3_Junctions3:int);
238

    
239

    
240
var 	idJunctions3_Junctions3_2:int;
241

    
242

    
243
let
244

    
245

    
246

    
247
	-- set state as inactive 
248
	idJunctions3_Junctions3_2
249
	 = if (not isInner) then 0 else idJunctions3_Junctions3_1;
250

    
251

    
252
	(idJunctions3_Junctions3) 
253
	= (idJunctions3_Junctions3_1);
254
	
255

    
256
tel
257

    
258

    
259
--***************************************************State :Junctions3_Junctions3 Automaton***************************************************
260

    
261
node Junctions3_Junctions3_node(idJunctions3_Junctions3_1:int;
262
	x:int;
263
	y_1:int)
264

    
265
returns (idJunctions3_Junctions3:int;
266
	y:int);
267

    
268

    
269
let
270

    
271
	 automaton junctions3_junctions3
272

    
273
	state POINTJunctions3_Junctions3:
274
	unless (idJunctions3_Junctions3_1=0) restart POINT__TO__JUNCTIONS3_A_1
275

    
276

    
277

    
278
	unless (idJunctions3_Junctions3_1=1224) and ( x=0 ) restart JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1
279

    
280

    
281

    
282
	unless (idJunctions3_Junctions3_1=1224) restart JUNCTIONS3_A_IDL
283

    
284
	unless (idJunctions3_Junctions3_1=1225) restart JUNCTIONS3_B_IDL
285

    
286
	let
287

    
288
		(idJunctions3_Junctions3, y) 
289
	= (idJunctions3_Junctions3_1, y_1);
290
	
291

    
292
	tel
293

    
294

    
295

    
296
	state POINT__TO__JUNCTIONS3_A_1:
297

    
298
	 var 	idJunctions3_Junctions3_2:int;
299
	let
300

    
301
		-- transition trace :
302
	--POINT__To__Junctions3_A_1
303
		(idJunctions3_Junctions3_2) 
304
	= Junctions3_A_en(idJunctions3_Junctions3_1, false);
305
		
306

    
307
	(idJunctions3_Junctions3) 
308
	=  (idJunctions3_Junctions3_2);
309

    
310
	--add unused variables
311
	(y) 
312
	= (y_1);
313
	
314

    
315
	tel
316

    
317
	until true restart POINTJunctions3_Junctions3
318

    
319

    
320

    
321
	state JUNCTIONS3_A__TO__JUNCTIONS3_JUNCTIONS3JUNCTION1228_1:
322

    
323
	 var 	idJunctions3_Junctions3_2, idJunctions3_Junctions3_3:int;
324
	y_2, y_3, y_4, y_5, y_6:int;
325
	let
326

    
327
		
328

    
329

    
330

    
331

    
332

    
333

    
334

    
335
-- transition trace :
336
	--Junctions3_A__To__Junction1228_1, Junction1228__To__Junction1229_1, Junction1229__To__Junction1230_1, Junction1230__To__Junction1231_1, Junction1231__To__Junctions3_B_1
337
		-- condition Action : y=0
338
		
339
		(y_2) 
340
	= Junctions3_A__To__Junctions3_Junctions3Junction1228_1_Condition_Action(y_1);
341
		
342

    
343
		-- condition Action : y++
344
		
345
		(y_3) 
346
	= 
347
		 if ((  y_2 =0 )) then 
348
		Junctions3_Junctions3Junction1228__To__Junctions3_Junctions3Junction1229_1_Condition_Action(y_2)
349
		 else (y_2);
350
		
351

    
352
		-- condition Action : y++
353
		
354
		(y_4) 
355
	= 
356
		 if ((  y_2 =0 ) and (  y_3 =1 )) then 
357
		Junctions3_Junctions3Junction1229__To__Junctions3_Junctions3Junction1230_1_Condition_Action(y_3)
358
		 else (y_3);
359
		
360

    
361
		-- condition Action : y++
362
		
363
		(y_5) 
364
	= 
365
		 if ((  y_2 =0 ) and (  y_3 =1 ) and (  y_4 =2 )) then 
366
		Junctions3_Junctions3Junction1230__To__Junctions3_Junctions3Junction1231_1_Condition_Action(y_4)
367
		 else (y_4);
368
		
369

    
370
		-- condition Action : y++
371
		
372
		(y_6) 
373
	= 
374
		 if ((  y_2 =0 ) and (  y_3 =1 ) and (  y_4 =2 )) then 
375
		Junctions3_Junctions3Junction1231__To__Junctions3_B_1_Condition_Action(y_5)
376
		 else (y_5);
377
		
378

    
379
		(idJunctions3_Junctions3_2) 
380
	= 
381
		 if ((  y_2 =0 ) and (  y_3 =1 ) and (  y_4 =2 )) then 
382
		Junctions3_A_ex(idJunctions3_Junctions3_1, false)
383
		 else (idJunctions3_Junctions3_1);
384
		
385

    
386
		(idJunctions3_Junctions3_3) 
387
	= 
388
		 if ((  y_2 =0 ) and (  y_3 =1 ) and (  y_4 =2 )) then 
389
		Junctions3_B_en(idJunctions3_Junctions3_2, false)
390
		 else (idJunctions3_Junctions3_2);
391
		
392

    
393
	(idJunctions3_Junctions3, y) 
394
	= 
395
		 if ((  y_2 =0 ) and (  y_3 =1 ) and (  y_4 =2 )) then 
396
		(idJunctions3_Junctions3_3, y_6)
397
		 else
398
		 if ((  y_2 =0 ) and (  y_3 =1 ) and (  y_4 =2 )) then 
399
		(idJunctions3_Junctions3_1, y_5)
400
		 else
401
		 if ((  y_2 =0 ) and (  y_3 =1 )) then 
402
		(idJunctions3_Junctions3_1, y_4)
403
		 else
404
		 if ((  y_2 =0 )) then 
405
		(idJunctions3_Junctions3_1, y_3)
406
		 else (idJunctions3_Junctions3_1, y_2);
407

    
408

    
409
	tel
410

    
411
	until true restart POINTJunctions3_Junctions3
412

    
413

    
414

    
415
	state JUNCTIONS3_A_IDL:
416

    
417
	 	let
418

    
419
		
420

    
421
	(idJunctions3_Junctions3, y) 
422
	= (idJunctions3_Junctions3_1, y_1);
423
	
424

    
425
	tel
426

    
427
	until true restart POINTJunctions3_Junctions3
428

    
429

    
430

    
431
	state JUNCTIONS3_B_IDL:
432

    
433
	 	let
434

    
435
		
436

    
437
	(idJunctions3_Junctions3, y) 
438
	= (idJunctions3_Junctions3_1, y_1);
439
	
440

    
441
	tel
442

    
443
	until true restart POINTJunctions3_Junctions3
444

    
445

    
446

    
447
tel
448

    
449

    
450
--***************************************************State :Junctions3_Junctions3 Automaton***************************************************
451

    
452
node Junctions3_Junctions3(x:int)
453

    
454
returns (y:int);
455

    
456

    
457
var y_1: int;
458

    
459
	idJunctions3_Junctions3, idJunctions3_Junctions3_1: int;
460

    
461
	let
462

    
463
	y_1 = 111111 -> pre y;
464

    
465
	idJunctions3_Junctions3_1 = 0 -> pre idJunctions3_Junctions3;
466

    
467
	
468

    
469

    
470

    
471
	(idJunctions3_Junctions3, y)
472
	 = Junctions3_Junctions3_node(idJunctions3_Junctions3_1, x, y_1);
473

    
474

    
475
--unused outputs
476
	
477

    
478
tel
479

    
480

    
481

    
482
node Junctions3 (x_1_1 : int)
483
returns (y_1_1 : int); 
484
var
485
	Junctions3_1_1 : int;
486
	i_virtual_local : real;
487
let 
488
	Junctions3_1_1 =  Junctions3_Junctions3(x_1_1);
489
	y_1_1 = Junctions3_1_1;
490
	i_virtual_local= 0.0 -> 1.0;
491
tel
492