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

2  
3  
4 
 System nodes 
5  
6  
7  
8  
9 
node POINT__To__Flowchart2_Flowchart2Junction783_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 
 Entry action for state :Flowchart2_A 
37 
node Flowchart2_A_en(idFlowchart2_A_1:int; 
38 
idFlowchart2_Flowchart2_1:int; 
39 
x_1:int; 
40 
isInner:bool) 
41  
42 
returns (idFlowchart2_A:int; 
43 
idFlowchart2_Flowchart2:int; 
44 
x:int); 
45  
46  
47 
var idFlowchart2_A_2, idFlowchart2_A_3, idFlowchart2_A_4:int; 
48 
idFlowchart2_Flowchart2_2, idFlowchart2_Flowchart2_3, idFlowchart2_Flowchart2_4:int; 
49 
x_2, x_3, x_4, x_5:int; 
50  
51  
52 
let 
53  
54  
55  
56 
 set state as active 
57 
idFlowchart2_Flowchart2_2 
58 
= 782; 
59 

60  
61 
x_2 
62 
= if (not isInner) then 1000 
63 
else x_1; 
64 

65  
66 

67 
 transition trace : 
68 
POINT__To__Junction783_1 
69 
 condition Action : x++; 
70 

71 
(x_3) 
72 
= POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action(x_2); 
73 

74  
75 
(idFlowchart2_A_2, idFlowchart2_Flowchart2_3, x_4) 
76 
= 
77  
78 
if ( idFlowchart2_A_1 = 0) then 
79  
80 
(idFlowchart2_A_1, idFlowchart2_Flowchart2_2, x_3) 
81  
82 
else(idFlowchart2_A_1, idFlowchart2_Flowchart2_2, x_2); 
83  
84 

85  
86 
(idFlowchart2_A_3, idFlowchart2_Flowchart2_4, x_5) 
87 
= 
88 
if ( idFlowchart2_A_1 = 0) then 
89 
(idFlowchart2_A_2, idFlowchart2_Flowchart2_3, x_4) 
90 
else (idFlowchart2_A_1, idFlowchart2_Flowchart2_2, x_2); 
91 
 case of state without states but contains transitions 
92 
idFlowchart2_A_4 
93 
= 1; 
94 

95  
96 
(idFlowchart2_A, idFlowchart2_Flowchart2, x) 
97 
= (idFlowchart2_A_4, idFlowchart2_Flowchart2_4, x_5); 
98 

99  
100 
tel 
101  
102  
103  
104  
105  
106 
During action for state :Flowchart2_A 
107 
node Flowchart2_A_du(x_1:int) 
108  
109 
returns (x:int); 
110  
111  
112 
var x_2:int; 
113  
114  
115 
let 
116  
117  
118  
119 
x_2 
120 
= x_1  1; 
121 

122  
123 
(x) 
124 
= (x_2); 
125 

126  
127 
tel 
128  
129  
130  
131  
132  
133 
 Exit action for state :Flowchart2_A 
134 
node Flowchart2_A_ex(idFlowchart2_Flowchart2_1:int; 
135 
isInner:bool) 
136  
137 
returns (idFlowchart2_Flowchart2:int); 
138  
139  
140 
var idFlowchart2_Flowchart2_2:int; 
141  
142  
143 
let 
144  
145  
146  
147 
 set state as inactive 
148 
idFlowchart2_Flowchart2_2 
149 
= if (not isInner) then 0 else idFlowchart2_Flowchart2_1; 
150  
151  
152 
(idFlowchart2_Flowchart2) 
153 
= (idFlowchart2_Flowchart2_1); 
154 

155  
156 
tel 
157  
158  
159 
***************************************************State :Flowchart2_A Automaton*************************************************** 
160  
161 
node Flowchart2_A_node(idFlowchart2_A_1:int; 
162 
x_1:int) 
163  
164 
returns (idFlowchart2_A:int; 
165 
x:int); 
166  
167  
168 
let 
169  
170 
automaton flowchart2_a 
171  
172 
state POINTFlowchart2_A: 
173 
unless (idFlowchart2_A_1=0) restart POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1 
174  
175  
176  
177 
let 
178  
179 
(idFlowchart2_A, x) 
180 
= (idFlowchart2_A_1, x_1); 
181 

182  
183 
tel 
184  
185  
186  
187 
state POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1: 
188  
189 
var x_2:int; 
190 
let 
191  
192 
 transition trace : 
193 
POINT__To__Junction783_1 
194 
 condition Action : x++; 
195 

196 
(x_2) 
197 
= POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action(x_1); 
198 

199  
200 
(idFlowchart2_A, x) 
201 
= (idFlowchart2_A_1, x_2); 
202  
203  
204 
tel 
205  
206 
until true restart POINTFlowchart2_A 
207  
208  
209  
210 
tel 
211  
212  
213 
***************************************************State :Flowchart2_Flowchart2 Automaton*************************************************** 
214  
215 
node Flowchart2_Flowchart2_node(idFlowchart2_Flowchart2_1:int; 
216 
idFlowchart2_A_1:int; 
217 
x_1:int) 
218  
219 
returns (idFlowchart2_Flowchart2:int; 
220 
idFlowchart2_A:int; 
221 
x:int); 
222  
223  
224 
let 
225  
226 
automaton flowchart2_flowchart2 
227  
228 
state POINTFlowchart2_Flowchart2: 
229 
unless (idFlowchart2_Flowchart2_1=0) restart POINT__TO__FLOWCHART2_A_1 
230  
231  
232  
233 
unless (idFlowchart2_Flowchart2_1=782) restart FLOWCHART2_A_IDL 
234  
235 
let 
236  
237 
(idFlowchart2_Flowchart2, idFlowchart2_A, x) 
238 
= (idFlowchart2_Flowchart2_1, idFlowchart2_A_1, x_1); 
239 

240  
241 
tel 
242  
243  
244  
245 
state POINT__TO__FLOWCHART2_A_1: 
246  
247 
var idFlowchart2_Flowchart2_2:int; 
248 
idFlowchart2_A_2:int; 
249 
x_2:int; 
250 
let 
251  
252 
 transition trace : 
253 
POINT__To__Flowchart2_A_1 
254 
(idFlowchart2_A_2, idFlowchart2_Flowchart2_2, x_2) 
255 
= Flowchart2_A_en(idFlowchart2_A_1, idFlowchart2_Flowchart2_1, x_1, false); 
256 

257  
258 
(idFlowchart2_Flowchart2, idFlowchart2_A, x) 
259 
= (idFlowchart2_Flowchart2_2, idFlowchart2_A_2, x_2); 
260  
261  
262 
tel 
263  
264 
until true restart POINTFlowchart2_Flowchart2 
265  
266  
267  
268 
state FLOWCHART2_A_IDL: 
269  
270 
var idFlowchart2_A_2:int; 
271 
x_2, x_3:int; 
272 
let 
273  
274 

275 
(x_2) 
276 
= Flowchart2_A_du(x_1); 
277  
278 

279  
280 
(idFlowchart2_A_2, x_3) 
281 
= Flowchart2_A_node(idFlowchart2_A_1, x_2); 
282  
283 

284  
285  
286 
(idFlowchart2_Flowchart2, idFlowchart2_A, x) 
287 
= (idFlowchart2_Flowchart2_1, idFlowchart2_A_2, x_3); 
288 

289  
290 
tel 
291  
292 
until true restart POINTFlowchart2_Flowchart2 
293  
294  
295  
296 
tel 
297  
298  
299 
***************************************************State :Flowchart2_Flowchart2 Automaton*************************************************** 
300  
301 
node Flowchart2_Flowchart2(noInput :bool) 
302  
303 
returns (x:int); 
304  
305  
306 
var x_1: int; 
307  
308 
idFlowchart2_Flowchart2, idFlowchart2_Flowchart2_1: int; 
309  
310 
idFlowchart2_A, idFlowchart2_A_1: int; 
311  
312 
let 
313  
314 
x_1 = 0 > pre x; 
315  
316 
idFlowchart2_Flowchart2_1 = 0 > pre idFlowchart2_Flowchart2; 
317  
318 
idFlowchart2_A_1 = 0 > pre idFlowchart2_A; 
319  
320 

321  
322  
323  
324 
(idFlowchart2_Flowchart2, idFlowchart2_A, x) 
325 
= Flowchart2_Flowchart2_node(idFlowchart2_Flowchart2_1, idFlowchart2_A_1, x_1); 
326  
327  
328 
unused outputs 
329 

330  
331 
tel 
332  
333  
334  
335 
node Flowchart2 (i_virtual : real) 
336 
returns (Out1_1_1 : int); 
337 
var 
338 
Flowchart2_1_1 : int; 
339 
i_virtual_local : real; 
340 
let 
341 
Flowchart2_1_1 = Flowchart2_Flowchart2(true); 
342 
Out1_1_1 = Flowchart2_1_1; 
343 
i_virtual_local= 0.0 > 1.0; 
344 
tel 
345 