Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Temporal1 / Temporal1.lus @ eb639349

History | View | Annotate | Download (5.21 KB)

1
-- This file has been generated by cocoSim
2

    
3
-- External Stateflow functions
4
node after(n:int; E : bool; id:int ) returns ( Y : bool );
5
var count:int;
6
let
7
	count = 0 -> if (pre id != id) then
8
		 if E then 1 else 0 
9
	else
10
	 if E then (pre count) + 1 else pre count;
11
	 Y =  count >= n ;
12
tel
13
-- System nodes
14

    
15

    
16

    
17

    
18

    
19

    
20

    
21
-- Entry action for state :Temporal1_B
22
node Temporal1_B_en(idTemporal1_Temporal1_1:int;
23
	x_1:int;
24
	isInner:bool)
25

    
26
returns (idTemporal1_Temporal1:int;
27
	x:int);
28

    
29

    
30
var 	idTemporal1_Temporal1_2:int;
31
	x_2:int;
32

    
33

    
34
let
35

    
36

    
37

    
38
	-- set state as active 
39
	idTemporal1_Temporal1_2 
40
	= 123;
41
	
42

    
43
	x_2 
44
	= if (not isInner) then  x_1  + 1
45
	 else x_1;
46
	
47

    
48
	(idTemporal1_Temporal1, x) 
49
	= (idTemporal1_Temporal1_2, x_2);
50
	
51

    
52
tel
53

    
54

    
55

    
56

    
57

    
58
-- Exit action for state :Temporal1_B
59
node Temporal1_B_ex(idTemporal1_Temporal1_1:int;
60
	isInner:bool)
61

    
62
returns (idTemporal1_Temporal1:int);
63

    
64

    
65
var 	idTemporal1_Temporal1_2:int;
66

    
67

    
68
let
69

    
70

    
71

    
72
	-- set state as inactive 
73
	idTemporal1_Temporal1_2
74
	 = if (not isInner) then 0 else idTemporal1_Temporal1_1;
75

    
76

    
77
	(idTemporal1_Temporal1) 
78
	= (idTemporal1_Temporal1_1);
79
	
80

    
81
tel
82

    
83

    
84

    
85

    
86

    
87

    
88
-- Entry action for state :Temporal1_A
89
node Temporal1_A_en(idTemporal1_Temporal1_1:int;
90
	x_1:int;
91
	isInner:bool)
92

    
93
returns (idTemporal1_Temporal1:int;
94
	x:int);
95

    
96

    
97
var 	idTemporal1_Temporal1_2:int;
98
	x_2:int;
99

    
100

    
101
let
102

    
103

    
104

    
105
	-- set state as active 
106
	idTemporal1_Temporal1_2 
107
	= 122;
108
	
109

    
110
	x_2 
111
	= if (not isInner) then  x_1  + 1
112
	 else x_1;
113
	
114

    
115
	(idTemporal1_Temporal1, x) 
116
	= (idTemporal1_Temporal1_2, x_2);
117
	
118

    
119
tel
120

    
121

    
122

    
123

    
124

    
125
-- Exit action for state :Temporal1_A
126
node Temporal1_A_ex(idTemporal1_Temporal1_1:int;
127
	isInner:bool)
128

    
129
returns (idTemporal1_Temporal1:int);
130

    
131

    
132
var 	idTemporal1_Temporal1_2:int;
133

    
134

    
135
let
136

    
137

    
138

    
139
	-- set state as inactive 
140
	idTemporal1_Temporal1_2
141
	 = if (not isInner) then 0 else idTemporal1_Temporal1_1;
142

    
143

    
144
	(idTemporal1_Temporal1) 
145
	= (idTemporal1_Temporal1_1);
146
	
147

    
148
tel
149

    
150

    
151
--***************************************************State :Temporal1_Temporal1 Automaton***************************************************
152

    
153
node Temporal1_Temporal1_node(idTemporal1_Temporal1_1:int;
154
	x_1:int;
155
	E:bool)
156

    
157
returns (idTemporal1_Temporal1:int;
158
	x:int);
159
var 	after_E_2_output: bool;
160
 	after_E_3_output: bool;
161

    
162

    
163
let
164

    
165
	after_E_2_output =after(2,E,idTemporal1_Temporal1_1);
166
 	after_E_3_output =after(3,E,idTemporal1_Temporal1_1);
167
	 automaton temporal1_temporal1
168

    
169
	state POINTTemporal1_Temporal1:
170
	unless (idTemporal1_Temporal1_1=0) restart POINT__TO__TEMPORAL1_A_1
171

    
172

    
173

    
174
	unless (idTemporal1_Temporal1_1=122) and E and ( after_E_2_output ) restart TEMPORAL1_A__TO__TEMPORAL1_B_1
175

    
176

    
177

    
178
	unless (idTemporal1_Temporal1_1=123) and after_E_3_output restart TEMPORAL1_B__TO__TEMPORAL1_A_1
179

    
180

    
181

    
182
	unless (idTemporal1_Temporal1_1=122) restart TEMPORAL1_A_IDL
183

    
184
	unless (idTemporal1_Temporal1_1=123) restart TEMPORAL1_B_IDL
185

    
186
	let
187

    
188
		(idTemporal1_Temporal1, x) 
189
	= (idTemporal1_Temporal1_1, x_1);
190
	
191

    
192
	tel
193

    
194

    
195

    
196
	state POINT__TO__TEMPORAL1_A_1:
197

    
198
	 var 	idTemporal1_Temporal1_2:int;
199
	x_2:int;
200
	let
201

    
202
		-- transition trace :
203
	--POINT__To__Temporal1_A_1
204
		(idTemporal1_Temporal1_2, x_2) 
205
	= Temporal1_A_en(idTemporal1_Temporal1_1, x_1, false);
206
		
207

    
208
	(idTemporal1_Temporal1, x) 
209
	=  (idTemporal1_Temporal1_2, x_2);
210

    
211

    
212
	tel
213

    
214
	until true restart POINTTemporal1_Temporal1
215

    
216

    
217

    
218
	state TEMPORAL1_A__TO__TEMPORAL1_B_1:
219

    
220
	 var 	idTemporal1_Temporal1_2, idTemporal1_Temporal1_3:int;
221
	x_2:int;
222
	let
223

    
224
		-- transition trace :
225
	--Temporal1_A__To__Temporal1_B_1
226
		(idTemporal1_Temporal1_2) 
227
	= Temporal1_A_ex(idTemporal1_Temporal1_1, false);
228
		
229

    
230
		(idTemporal1_Temporal1_3, x_2) 
231
	= Temporal1_B_en(idTemporal1_Temporal1_2, x_1, false);
232
		
233

    
234
	(idTemporal1_Temporal1, x) 
235
	=  (idTemporal1_Temporal1_3, x_2);
236

    
237

    
238
	tel
239

    
240
	until true restart POINTTemporal1_Temporal1
241

    
242

    
243

    
244
	state TEMPORAL1_B__TO__TEMPORAL1_A_1:
245

    
246
	 var 	idTemporal1_Temporal1_2, idTemporal1_Temporal1_3:int;
247
	x_2:int;
248
	let
249

    
250
		-- transition trace :
251
	--Temporal1_B__To__Temporal1_A_1
252
		(idTemporal1_Temporal1_2) 
253
	= Temporal1_B_ex(idTemporal1_Temporal1_1, false);
254
		
255

    
256
		(idTemporal1_Temporal1_3, x_2) 
257
	= Temporal1_A_en(idTemporal1_Temporal1_2, x_1, false);
258
		
259

    
260
	(idTemporal1_Temporal1, x) 
261
	=  (idTemporal1_Temporal1_3, x_2);
262

    
263

    
264
	tel
265

    
266
	until true restart POINTTemporal1_Temporal1
267

    
268

    
269

    
270
	state TEMPORAL1_A_IDL:
271

    
272
	 	let
273

    
274
		
275

    
276
	(idTemporal1_Temporal1, x) 
277
	= (idTemporal1_Temporal1_1, x_1);
278
	
279

    
280
	tel
281

    
282
	until true restart POINTTemporal1_Temporal1
283

    
284

    
285

    
286
	state TEMPORAL1_B_IDL:
287

    
288
	 	let
289

    
290
		
291

    
292
	(idTemporal1_Temporal1, x) 
293
	= (idTemporal1_Temporal1_1, x_1);
294
	
295

    
296
	tel
297

    
298
	until true restart POINTTemporal1_Temporal1
299

    
300

    
301

    
302
tel
303

    
304

    
305
--***************************************************State :Temporal1_Temporal1 Automaton***************************************************
306

    
307
node Temporal1_Temporal1(E:bool)
308

    
309
returns (x:int);
310

    
311

    
312
var x_1: int;
313

    
314
	idTemporal1_Temporal1, idTemporal1_Temporal1_1: int;
315

    
316
	let
317

    
318
	x_1 = 0 -> pre x;
319

    
320
	idTemporal1_Temporal1_1 = 0 -> pre idTemporal1_Temporal1;
321

    
322
	
323

    
324

    
325

    
326
	(idTemporal1_Temporal1, x)
327
	 = 
328

    
329
	 if E then Temporal1_Temporal1_node(idTemporal1_Temporal1_1, x_1, E)
330

    
331
	 else (idTemporal1_Temporal1_1, x_1);
332

    
333
	
334

    
335

    
336
--unused outputs
337
	
338

    
339
tel
340

    
341

    
342

    
343
node Temporal1 (E_1_1 : real)
344
returns (x_1_1 : int); 
345
var
346
	Temporal1_1_1 : int;
347
	i_virtual_local : real;
348
	Temporal1E_1_1_event: bool;
349
let 
350
	Temporal1E_1_1_event = false -> (pre(E_1_1) <= 0.0 and E_1_1 > 0.0);
351
	Temporal1_1_1 =  Temporal1_Temporal1(Temporal1E_1_1_event);
352
	x_1_1 = Temporal1_1_1;
353
	i_virtual_local= 0.0 -> 1.0;
354
tel
355