lustrectests / regression_tests / lustre_files / success / Stateflow / src_Flowchart5 / Flowchart5.lus @ eb639349
History  View  Annotate  Download (5.69 KB)
1 
 This file has been generated by cocoSim 

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9 
node Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action(x_1:int) 
10  
11 
returns (x:int); 
12  
13  
14 
var x_2:int; 
15  
16  
17 
let 
18  
19  
20  
21 
x_2 
22 
= x_1 + 1; 
23 

24  
25 
(x) 
26 
= (x_2); 
27 

28  
29 
tel 
30  
31  
32  
33  
34  
35  
36  
37  
38 
 Entry action for state :Flowchart5_A 
39 
node Flowchart5_A_en(idFlowchart5_A_1:int; 
40 
idFlowchart5_Flowchart5_1:int; 
41 
x_1:int; 
42 
isInner:bool) 
43  
44 
returns (idFlowchart5_A:int; 
45 
idFlowchart5_Flowchart5:int; 
46 
x:int); 
47  
48  
49 
var idFlowchart5_A_2, idFlowchart5_A_3, idFlowchart5_A_4:int; 
50 
idFlowchart5_Flowchart5_2, idFlowchart5_Flowchart5_3, idFlowchart5_Flowchart5_4:int; 
51 
x_2, x_3, x_4:int; 
52  
53  
54 
let 
55  
56  
57  
58 
 set state as active 
59 
idFlowchart5_Flowchart5_2 
60 
= 806; 
61 

62  
63 

64  
65  
66 
 transition trace : 
67 
POINT__To__Junction807_1, Junction807__To__Junction808_1 
68 
 condition Action : x++; 
69 

70 
(x_2) 
71 
= Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action(x_1); 
72 

73  
74 
(idFlowchart5_A_2, idFlowchart5_Flowchart5_3, x_3) 
75 
= 
76  
77 
if ( idFlowchart5_A_1 = 0) then 
78  
79 
(idFlowchart5_A_1, idFlowchart5_Flowchart5_2, x_2) 
80  
81 
else(idFlowchart5_A_1, idFlowchart5_Flowchart5_2, x_1); 
82  
83 

84  
85 
(idFlowchart5_A_3, idFlowchart5_Flowchart5_4, x_4) 
86 
= 
87 
if ( idFlowchart5_A_1 = 0) then 
88 
(idFlowchart5_A_2, idFlowchart5_Flowchart5_3, x_3) 
89 
else (idFlowchart5_A_1, idFlowchart5_Flowchart5_2, x_1); 
90 
 case of state without states but contains transitions 
91 
idFlowchart5_A_4 
92 
= 1; 
93 

94  
95 
(idFlowchart5_A, idFlowchart5_Flowchart5, x) 
96 
= (idFlowchart5_A_4, idFlowchart5_Flowchart5_4, x_4); 
97 

98  
99 
tel 
100  
101  
102  
103  
104  
105 
 Exit action for state :Flowchart5_A 
106 
node Flowchart5_A_ex(idFlowchart5_Flowchart5_1:int; 
107 
isInner:bool) 
108  
109 
returns (idFlowchart5_Flowchart5:int); 
110  
111  
112 
var idFlowchart5_Flowchart5_2:int; 
113  
114  
115 
let 
116  
117  
118  
119 
 set state as inactive 
120 
idFlowchart5_Flowchart5_2 
121 
= if (not isInner) then 0 else idFlowchart5_Flowchart5_1; 
122  
123  
124 
(idFlowchart5_Flowchart5) 
125 
= (idFlowchart5_Flowchart5_1); 
126 

127  
128 
tel 
129  
130  
131  
132  
133  
134 
During action for state :Flowchart5_A 
135 
node Flowchart5_A_du(x_1:int) 
136  
137 
returns (x:int); 
138  
139  
140  
141  
142 
let 
143  
144  
145  
146 
automaton flowchart5_a_INNER 
147  
148 
state POINTFlowchart5_A_INNER: 
149 
unless true restart FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1 
150  
151  
152  
153 
let 
154  
155 
(x) 
156 
= (x_1); 
157 

158  
159 
tel 
160  
161  
162  
163 
state FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1: 
164  
165 
var x_2:int; 
166 
let 
167  
168 

169  
170 
 transition trace : 
171 
Flowchart5_A__To__Junction807_1, Junction807__To__Junction808_1 
172 
 condition Action : x++; 
173 

174 
(x_2) 
175 
= Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action(x_1); 
176 

177  
178 
(x) 
179 
= (x_2); 
180  
181  
182 
tel 
183  
184 
until true restart POINTFlowchart5_A_INNER 
185  
186  
187  
188 
tel 
189  
190  
191 
***************************************************State :Flowchart5_A Automaton*************************************************** 
192  
193 
node Flowchart5_A_node(idFlowchart5_A_1:int; 
194 
x_1:int) 
195  
196 
returns (idFlowchart5_A:int; 
197 
x:int); 
198  
199  
200 
let 
201  
202 
automaton flowchart5_a 
203  
204 
state POINTFlowchart5_A: 
205 
unless (idFlowchart5_A_1=0) restart POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1 
206  
207  
208  
209 
let 
210  
211 
(idFlowchart5_A, x) 
212 
= (idFlowchart5_A_1, x_1); 
213 

214  
215 
tel 
216  
217  
218  
219 
state POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1: 
220  
221 
var x_2:int; 
222 
let 
223  
224 

225  
226 
 transition trace : 
227 
POINT__To__Junction807_1, Junction807__To__Junction808_1 
228 
 condition Action : x++; 
229 

230 
(x_2) 
231 
= Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action(x_1); 
232 

233  
234 
(idFlowchart5_A, x) 
235 
= (idFlowchart5_A_1, x_2); 
236  
237  
238 
tel 
239  
240 
until true restart POINTFlowchart5_A 
241  
242  
243  
244 
tel 
245  
246  
247 
***************************************************State :Flowchart5_Flowchart5 Automaton*************************************************** 
248  
249 
node Flowchart5_Flowchart5_node(idFlowchart5_Flowchart5_1:int; 
250 
idFlowchart5_A_1:int; 
251 
x_1:int) 
252  
253 
returns (idFlowchart5_Flowchart5:int; 
254 
idFlowchart5_A:int; 
255 
x:int); 
256  
257  
258 
let 
259  
260 
automaton flowchart5_flowchart5 
261  
262 
state POINTFlowchart5_Flowchart5: 
263 
unless (idFlowchart5_Flowchart5_1=0) restart POINT__TO__FLOWCHART5_A_1 
264  
265  
266  
267 
unless true restart FLOWCHART5_FLOWCHART5_PARALLEL_IDL 
268  
269 
let 
270  
271 
(idFlowchart5_Flowchart5, idFlowchart5_A, x) 
272 
= (idFlowchart5_Flowchart5_1, idFlowchart5_A_1, x_1); 
273 

274  
275 
tel 
276  
277  
278  
279 
state POINT__TO__FLOWCHART5_A_1: 
280  
281 
var idFlowchart5_Flowchart5_2:int; 
282 
idFlowchart5_A_2:int; 
283 
x_2:int; 
284 
let 
285  
286 
 transition trace : 
287 
POINT__To__Flowchart5_A_1 
288 
(idFlowchart5_A_2, idFlowchart5_Flowchart5_2, x_2) 
289 
= Flowchart5_A_en(idFlowchart5_A_1, idFlowchart5_Flowchart5_1, x_1, false); 
290 

291  
292 
(idFlowchart5_Flowchart5, idFlowchart5_A, x) 
293 
= (idFlowchart5_Flowchart5_2, idFlowchart5_A_2, x_2); 
294  
295  
296 
tel 
297  
298 
until true restart POINTFlowchart5_Flowchart5 
299  
300  
301  
302 
state FLOWCHART5_FLOWCHART5_PARALLEL_IDL: 
303  
304 
var idFlowchart5_A_2:int; 
305 
x_2:int; 
306 
let 
307  
308 

309  
310 
(idFlowchart5_A_2, x_2) 
311 
= if not (idFlowchart5_A_1= 0 ) then Flowchart5_A_node(idFlowchart5_A_1, x_1) 
312  
313 
else (idFlowchart5_A_1, x_1); 
314  
315 

316  
317 

318  
319 
(idFlowchart5_Flowchart5, idFlowchart5_A, x) 
320 
= (idFlowchart5_Flowchart5_1, idFlowchart5_A_2, x_2); 
321 

322  
323 
tel 
324  
325 
until true restart POINTFlowchart5_Flowchart5 
326  
327  
328  
329 
tel 
330  
331  
332 
***************************************************State :Flowchart5_Flowchart5 Automaton*************************************************** 
333  
334 
node Flowchart5_Flowchart5(noInput :bool) 
335  
336 
returns (x:int); 
337  
338  
339 
var x_1: int; 
340  
341 
idFlowchart5_Flowchart5, idFlowchart5_Flowchart5_1: int; 
342  
343 
idFlowchart5_A, idFlowchart5_A_1: int; 
344  
345 
let 
346  
347 
x_1 = 0 > pre x; 
348  
349 
idFlowchart5_Flowchart5_1 = 0 > pre idFlowchart5_Flowchart5; 
350  
351 
idFlowchart5_A_1 = 0 > pre idFlowchart5_A; 
352  
353 

354  
355  
356  
357 
(idFlowchart5_Flowchart5, idFlowchart5_A, x) 
358 
= Flowchart5_Flowchart5_node(idFlowchart5_Flowchart5_1, idFlowchart5_A_1, x_1); 
359  
360  
361 
unused outputs 
362 

363  
364 
tel 
365  
366  
367  
368 
node Flowchart5 (i_virtual : real) 
369 
returns (Out1_1_1 : int); 
370 
var 
371 
Flowchart5_1_1 : int; 
372 
i_virtual_local : real; 
373 
let 
374 
Flowchart5_1_1 = Flowchart5_Flowchart5(true); 
375 
Out1_1_1 = Flowchart5_1_1; 
376 
i_virtual_local= 0.0 > 1.0; 
377 
tel 
378 