Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_SetReset / SetReset.lus @ eb639349

History | View | Annotate | Download (5.1 KB)

1
-- This file has been generated by cocoSim
2

    
3

    
4
-- System nodes
5

    
6

    
7

    
8

    
9

    
10

    
11

    
12
-- Entry action for state :SetReset_On
13
node SetReset_On_en(idSetReset_SetReset_1:int;
14
	x_1:int;
15
	isInner:bool)
16

    
17
returns (idSetReset_SetReset:int;
18
	x:int);
19

    
20

    
21
var 	idSetReset_SetReset_2:int;
22
	x_2:int;
23

    
24

    
25
let
26

    
27

    
28

    
29
	-- set state as active 
30
	idSetReset_SetReset_2 
31
	= 1725;
32
	
33

    
34
	x_2 
35
	= if (not isInner) then 1
36
	 else x_1;
37
	
38

    
39
	(idSetReset_SetReset, x) 
40
	= (idSetReset_SetReset_2, x_2);
41
	
42

    
43
tel
44

    
45

    
46

    
47

    
48

    
49
-- Exit action for state :SetReset_On
50
node SetReset_On_ex(idSetReset_SetReset_1:int;
51
	isInner:bool)
52

    
53
returns (idSetReset_SetReset:int);
54

    
55

    
56
var 	idSetReset_SetReset_2:int;
57

    
58

    
59
let
60

    
61

    
62

    
63
	-- set state as inactive 
64
	idSetReset_SetReset_2
65
	 = if (not isInner) then 0 else idSetReset_SetReset_1;
66

    
67

    
68
	(idSetReset_SetReset) 
69
	= (idSetReset_SetReset_1);
70
	
71

    
72
tel
73

    
74

    
75

    
76

    
77

    
78

    
79
-- Entry action for state :SetReset_Off
80
node SetReset_Off_en(idSetReset_SetReset_1:int;
81
	x_1:int;
82
	isInner:bool)
83

    
84
returns (idSetReset_SetReset:int;
85
	x:int);
86

    
87

    
88
var 	idSetReset_SetReset_2:int;
89
	x_2:int;
90

    
91

    
92
let
93

    
94

    
95

    
96
	-- set state as active 
97
	idSetReset_SetReset_2 
98
	= 1724;
99
	
100

    
101
	x_2 
102
	= if (not isInner) then 0
103
	 else x_1;
104
	
105

    
106
	(idSetReset_SetReset, x) 
107
	= (idSetReset_SetReset_2, x_2);
108
	
109

    
110
tel
111

    
112

    
113

    
114

    
115

    
116
-- Exit action for state :SetReset_Off
117
node SetReset_Off_ex(idSetReset_SetReset_1:int;
118
	isInner:bool)
119

    
120
returns (idSetReset_SetReset:int);
121

    
122

    
123
var 	idSetReset_SetReset_2:int;
124

    
125

    
126
let
127

    
128

    
129

    
130
	-- set state as inactive 
131
	idSetReset_SetReset_2
132
	 = if (not isInner) then 0 else idSetReset_SetReset_1;
133

    
134

    
135
	(idSetReset_SetReset) 
136
	= (idSetReset_SetReset_1);
137
	
138

    
139
tel
140

    
141

    
142
--***************************************************State :SetReset_SetReset Automaton***************************************************
143

    
144
node SetReset_SetReset_node(idSetReset_SetReset_1:int;
145
	x_1:int;
146
	Set:bool;
147
	Reset:bool)
148

    
149
returns (idSetReset_SetReset:int;
150
	x:int);
151

    
152

    
153
let
154

    
155
	 automaton setreset_setreset
156

    
157
	state POINTSetReset_SetReset:
158
	unless (idSetReset_SetReset_1=0) restart POINT__TO__SETRESET_OFF_1
159

    
160

    
161

    
162
	unless (idSetReset_SetReset_1=1724) and Set restart SETRESET_OFF__TO__SETRESET_ON_1
163

    
164

    
165

    
166
	unless (idSetReset_SetReset_1=1725) and Reset restart SETRESET_ON__TO__SETRESET_OFF_1
167

    
168

    
169

    
170
	unless (idSetReset_SetReset_1=1724) restart SETRESET_OFF_IDL
171

    
172
	unless (idSetReset_SetReset_1=1725) restart SETRESET_ON_IDL
173

    
174
	let
175

    
176
		(idSetReset_SetReset, x) 
177
	= (idSetReset_SetReset_1, x_1);
178
	
179

    
180
	tel
181

    
182

    
183

    
184
	state POINT__TO__SETRESET_OFF_1:
185

    
186
	 var 	idSetReset_SetReset_2:int;
187
	x_2:int;
188
	let
189

    
190
		-- transition trace :
191
	--POINT__To__SetReset_Off_1
192
		(idSetReset_SetReset_2, x_2) 
193
	= SetReset_Off_en(idSetReset_SetReset_1, x_1, false);
194
		
195

    
196
	(idSetReset_SetReset, x) 
197
	=  (idSetReset_SetReset_2, x_2);
198

    
199

    
200
	tel
201

    
202
	until true restart POINTSetReset_SetReset
203

    
204

    
205

    
206
	state SETRESET_OFF__TO__SETRESET_ON_1:
207

    
208
	 var 	idSetReset_SetReset_2, idSetReset_SetReset_3:int;
209
	x_2:int;
210
	let
211

    
212
		-- transition trace :
213
	--SetReset_Off__To__SetReset_On_1
214
		(idSetReset_SetReset_2) 
215
	= SetReset_Off_ex(idSetReset_SetReset_1, false);
216
		
217

    
218
		(idSetReset_SetReset_3, x_2) 
219
	= SetReset_On_en(idSetReset_SetReset_2, x_1, false);
220
		
221

    
222
	(idSetReset_SetReset, x) 
223
	=  (idSetReset_SetReset_3, x_2);
224

    
225

    
226
	tel
227

    
228
	until true restart POINTSetReset_SetReset
229

    
230

    
231

    
232
	state SETRESET_ON__TO__SETRESET_OFF_1:
233

    
234
	 var 	idSetReset_SetReset_2, idSetReset_SetReset_3:int;
235
	x_2:int;
236
	let
237

    
238
		-- transition trace :
239
	--SetReset_On__To__SetReset_Off_1
240
		(idSetReset_SetReset_2) 
241
	= SetReset_On_ex(idSetReset_SetReset_1, false);
242
		
243

    
244
		(idSetReset_SetReset_3, x_2) 
245
	= SetReset_Off_en(idSetReset_SetReset_2, x_1, false);
246
		
247

    
248
	(idSetReset_SetReset, x) 
249
	=  (idSetReset_SetReset_3, x_2);
250

    
251

    
252
	tel
253

    
254
	until true restart POINTSetReset_SetReset
255

    
256

    
257

    
258
	state SETRESET_OFF_IDL:
259

    
260
	 	let
261

    
262
		
263

    
264
	(idSetReset_SetReset, x) 
265
	= (idSetReset_SetReset_1, x_1);
266
	
267

    
268
	tel
269

    
270
	until true restart POINTSetReset_SetReset
271

    
272

    
273

    
274
	state SETRESET_ON_IDL:
275

    
276
	 	let
277

    
278
		
279

    
280
	(idSetReset_SetReset, x) 
281
	= (idSetReset_SetReset_1, x_1);
282
	
283

    
284
	tel
285

    
286
	until true restart POINTSetReset_SetReset
287

    
288

    
289

    
290
tel
291

    
292

    
293
--***************************************************State :SetReset_SetReset Automaton***************************************************
294

    
295
node SetReset_SetReset(Set:bool;
296
	Reset:bool)
297

    
298
returns (x:int);
299

    
300

    
301
var x_1: int;
302

    
303
	idSetReset_SetReset, idSetReset_SetReset_1: int;
304

    
305
		idSetReset_SetReset_2:int;
306
	x_2:int;
307
let
308

    
309
	x_1 = 0 -> pre x;
310

    
311
	idSetReset_SetReset_1 = 0 -> pre idSetReset_SetReset;
312

    
313
	
314

    
315

    
316

    
317
	(idSetReset_SetReset_2, x_2)
318
	 = 
319

    
320
	 if Set then SetReset_SetReset_node(idSetReset_SetReset_1, x_1, Set, false)
321

    
322
	 else (idSetReset_SetReset_1, x_1);
323

    
324
	
325

    
326

    
327

    
328
	(idSetReset_SetReset, x)
329
	 = 
330

    
331
	 if Reset then SetReset_SetReset_node(idSetReset_SetReset_2, x_2, false, Reset)
332

    
333
	 else (idSetReset_SetReset_2, x_2);
334

    
335
	
336

    
337

    
338
--unused outputs
339
	
340

    
341
tel
342

    
343

    
344

    
345
node SetReset (Set_1_1 : real; Reset_1_1 : real)
346
returns (output_1_1 : int); 
347
var
348
	Mux_1_1 : real; Mux_1_2 : real;
349
	SetReset_1_1 : int;
350
	i_virtual_local : real;
351
	SetResetMux_1_1_event: bool;
352
	SetResetMux_1_2_event: bool;
353
let 
354
	Mux_1_1 = Set_1_1 ;
355
	Mux_1_2 = Reset_1_1 ;
356
	SetResetMux_1_1_event = false -> (pre(Mux_1_1) <= 0.0 and Mux_1_1 > 0.0);
357
	SetResetMux_1_2_event = false -> (pre(Mux_1_2) <= 0.0 and Mux_1_2 > 0.0);
358
	SetReset_1_1 =  SetReset_SetReset(SetResetMux_1_1_event, SetResetMux_1_2_event);
359
	output_1_1 = SetReset_1_1;
360
	i_virtual_local= 0.0 -> 1.0;
361
tel
362