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

2  
3 
 External Stateflow functions 
4 
#open <math> 
5  
6 
 System nodes 
7  
8  
9  
10  
11 
node POINT__To__Chart_fJunction885_1_Condition_Action(x:real; 
12 
y:real; 
13 
z_1:real) 
14  
15 
returns (z:real); 
16  
17  
18 
var z_2:real; 
19  
20  
21 
let 
22  
23  
24  
25 
z_2 
26 
= sqrt(x*x+y*y); 
27 

28  
29 
(z) 
30 
= (z_2); 
31 

32  
33 
tel 
34  
35  
36 
***************************************************State :Chart_f Automaton*************************************************** 
37  
38 
node Chart_f_node(idChart_f_1:int; 
39 
x:real; 
40 
y:real; 
41 
z_1:real) 
42  
43 
returns (idChart_f:int; 
44 
z:real); 
45  
46  
47 
let 
48  
49 
automaton chart_f 
50  
51 
state POINTChart_f: 
52 
unless (idChart_f_1=0) restart POINT__TO__CHART_FJUNCTION885_1 
53  
54  
55  
56 
let 
57  
58 
(idChart_f, z) 
59 
= (idChart_f_1, z_1); 
60 

61  
62 
tel 
63  
64  
65  
66 
state POINT__TO__CHART_FJUNCTION885_1: 
67  
68 
var z_2:real; 
69 
let 
70  
71 
 transition trace : 
72 
POINT__To__Junction885_1 
73 
 condition Action : z=sqrt(x*x+y*y); 
74 

75 
(z_2) 
76 
= POINT__To__Chart_fJunction885_1_Condition_Action(x, y, z_1); 
77 

78  
79 
(idChart_f, z) 
80 
= (idChart_f_1, z_2); 
81  
82  
83 
tel 
84  
85 
until true restart POINTChart_f 
86  
87  
88  
89 
tel 
90  
91  
92 
***************************************************State :Chart_f Automaton*************************************************** 
93  
94 
node f(x:real; 
95 
y:real) 
96  
97 
returns (z:real); 
98  
99  
100 
var z_1: real; 
101  
102 
idChart_f, idChart_f_1: int; 
103  
104 
let 
105  
106 
z_1 = 0.0 > pre z; 
107  
108 
idChart_f_1 = 0 > pre idChart_f; 
109  
110 

111  
112  
113  
114 
(idChart_f, z) 
115 
= Chart_f_node(idChart_f_1, x, y, z_1); 
116  
117  
118 
unused outputs 
119 

120  
121 
tel 
122  
123  
124  
125  
126  
127  
128  
129 
node Chart_B__To__Chart_A_1_Condition_Action(a_1:real; 
130 
b_1:real; 
131 
c_1:real) 
132  
133 
returns (a:real; 
134 
b:real; 
135 
c:real); 
136  
137  
138 
var c_2:real; 
139  
140  
141 
let 
142  
143  
144  
145 
c_2 
146 
= f( a_1 , b_1 ); 
147 

148  
149 
(a, b, c) 
150 
= (a_1, b_1, c_2); 
151 

152  
153 
tel 
154  
155  
156  
157  
158  
159  
160  
161 
node Chart_A__To__Chart_B_1_Condition_Action(a_1:real; 
162 
b_1:real; 
163 
c_1:real) 
164  
165 
returns (a:real; 
166 
b:real; 
167 
c:real); 
168  
169  
170 
var c_2:real; 
171  
172  
173 
let 
174  
175  
176  
177 
c_2 
178 
= f( a_1 , b_1 ); 
179 

180  
181 
(a, b, c) 
182 
= (a_1, b_1, c_2); 
183 

184  
185 
tel 
186  
187  
188  
189  
190  
191  
192 
 Entry action for state :Chart_B 
193 
node Chart_B_en(idChart_Chart_1:int; 
194 
a_1:real; 
195 
b_1:real; 
196 
isInner:bool) 
197  
198 
returns (idChart_Chart:int; 
199 
a:real; 
200 
b:real); 
201  
202  
203 
var idChart_Chart_2:int; 
204 
a_2:real; 
205 
b_2:real; 
206  
207  
208 
let 
209  
210  
211  
212 
 set state as active 
213 
idChart_Chart_2 
214 
= 880; 
215 

216  
217 
a_2 
218 
= if (not isInner) then 5. 
219 
else a_1; 
220 

221  
222 
b_2 
223 
= if (not isInner) then 12. 
224 
else b_1; 
225 

226  
227 
(idChart_Chart, a, b) 
228 
= (idChart_Chart_2, a_2, b_2); 
229 

230  
231 
tel 
232  
233  
234  
235  
236  
237 
 Exit action for state :Chart_B 
238 
node Chart_B_ex(idChart_Chart_1:int; 
239 
isInner:bool) 
240  
241 
returns (idChart_Chart:int); 
242  
243  
244 
var idChart_Chart_2:int; 
245  
246  
247 
let 
248  
249  
250  
251 
 set state as inactive 
252 
idChart_Chart_2 
253 
= if (not isInner) then 0 else idChart_Chart_1; 
254  
255  
256 
(idChart_Chart) 
257 
= (idChart_Chart_1); 
258 

259  
260 
tel 
261  
262  
263  
264  
265  
266  
267 
 Entry action for state :Chart_A 
268 
node Chart_A_en(idChart_Chart_1:int; 
269 
a_1:real; 
270 
b_1:real; 
271 
isInner:bool) 
272  
273 
returns (idChart_Chart:int; 
274 
a:real; 
275 
b:real); 
276  
277  
278 
var idChart_Chart_2:int; 
279 
a_2:real; 
280 
b_2:real; 
281  
282  
283 
let 
284  
285  
286  
287 
 set state as active 
288 
idChart_Chart_2 
289 
= 879; 
290 

291  
292 
a_2 
293 
= if (not isInner) then 3. 
294 
else a_1; 
295 

296  
297 
b_2 
298 
= if (not isInner) then 4. 
299 
else b_1; 
300 

301  
302 
(idChart_Chart, a, b) 
303 
= (idChart_Chart_2, a_2, b_2); 
304 

305  
306 
tel 
307  
308  
309  
310  
311  
312 
 Exit action for state :Chart_A 
313 
node Chart_A_ex(idChart_Chart_1:int; 
314 
isInner:bool) 
315  
316 
returns (idChart_Chart:int); 
317  
318  
319 
var idChart_Chart_2:int; 
320  
321  
322 
let 
323  
324  
325  
326 
 set state as inactive 
327 
idChart_Chart_2 
328 
= if (not isInner) then 0 else idChart_Chart_1; 
329  
330  
331 
(idChart_Chart) 
332 
= (idChart_Chart_1); 
333 

334  
335 
tel 
336  
337  
338 
***************************************************State :Chart_Chart Automaton*************************************************** 
339  
340 
node Chart_Chart_node(idChart_Chart_1:int; 
341 
a_1:real; 
342 
b_1:real; 
343 
c_1:real) 
344  
345 
returns (idChart_Chart:int; 
346 
a:real; 
347 
b:real; 
348 
c:real); 
349  
350  
351 
let 
352  
353 
automaton chart_chart 
354  
355 
state POINTChart_Chart: 
356 
unless (idChart_Chart_1=0) restart POINT__TO__CHART_A_1 
357  
358  
359  
360 
unless (idChart_Chart_1=879) restart CHART_A__TO__CHART_B_1 
361  
362  
363  
364 
unless (idChart_Chart_1=880) restart CHART_B__TO__CHART_A_1 
365  
366  
367  
368 
unless (idChart_Chart_1=879) restart CHART_A_IDL 
369  
370 
unless (idChart_Chart_1=880) restart CHART_B_IDL 
371  
372 
let 
373  
374 
(idChart_Chart, a, b, c) 
375 
= (idChart_Chart_1, a_1, b_1, c_1); 
376 

377  
378 
tel 
379  
380  
381  
382 
state POINT__TO__CHART_A_1: 
383  
384 
var idChart_Chart_2:int; 
385 
a_2:real; 
386 
b_2:real; 
387 
let 
388  
389 
 transition trace : 
390 
POINT__To__Chart_A_1 
391 
(idChart_Chart_2, a_2, b_2) 
392 
= Chart_A_en(idChart_Chart_1, a_1, b_1, false); 
393 

394  
395 
(idChart_Chart, a, b) 
396 
= (idChart_Chart_2, a_2, b_2); 
397  
398 
add unused variables 
399 
(c) 
400 
= (c_1); 
401 

402  
403 
tel 
404  
405 
until true restart POINTChart_Chart 
406  
407  
408  
409 
state CHART_A__TO__CHART_B_1: 
410  
411 
var idChart_Chart_2, idChart_Chart_3:int; 
412 
a_2, a_3:real; 
413 
b_2, b_3:real; 
414 
c_2:real; 
415 
let 
416  
417 
 transition trace : 
418 
Chart_A__To__Chart_B_1 
419 
 condition Action : c=f(a,b) 
420 

421 
(a_2, b_2, c_2) 
422 
= Chart_A__To__Chart_B_1_Condition_Action(a_1, b_1, c_1); 
423 

424  
425 
(idChart_Chart_2) 
426 
= Chart_A_ex(idChart_Chart_1, false); 
427 

428  
429 
(idChart_Chart_3, a_3, b_3) 
430 
= Chart_B_en(idChart_Chart_2, a_2, b_2, false); 
431 

432  
433 
(idChart_Chart, a, b, c) 
434 
= (idChart_Chart_3, a_3, b_3, c_2); 
435  
436  
437 
tel 
438  
439 
until true restart POINTChart_Chart 
440  
441  
442  
443 
state CHART_B__TO__CHART_A_1: 
444  
445 
var idChart_Chart_2, idChart_Chart_3:int; 
446 
a_2, a_3:real; 
447 
b_2, b_3:real; 
448 
c_2:real; 
449 
let 
450  
451 
 transition trace : 
452 
Chart_B__To__Chart_A_1 
453 
 condition Action : c=f(a,b) 
454 

455 
(a_2, b_2, c_2) 
456 
= Chart_B__To__Chart_A_1_Condition_Action(a_1, b_1, c_1); 
457 

458  
459 
(idChart_Chart_2) 
460 
= Chart_B_ex(idChart_Chart_1, false); 
461 

462  
463 
(idChart_Chart_3, a_3, b_3) 
464 
= Chart_A_en(idChart_Chart_2, a_2, b_2, false); 
465 

466  
467 
(idChart_Chart, a, b, c) 
468 
= (idChart_Chart_3, a_3, b_3, c_2); 
469  
470  
471 
tel 
472  
473 
until true restart POINTChart_Chart 
474  
475  
476  
477 
state CHART_A_IDL: 
478  
479 
let 
480  
481 

482  
483 
(idChart_Chart, a, b, c) 
484 
= (idChart_Chart_1, a_1, b_1, c_1); 
485 

486  
487 
tel 
488  
489 
until true restart POINTChart_Chart 
490  
491  
492  
493 
state CHART_B_IDL: 
494  
495 
let 
496  
497 

498  
499 
(idChart_Chart, a, b, c) 
500 
= (idChart_Chart_1, a_1, b_1, c_1); 
501 

502  
503 
tel 
504  
505 
until true restart POINTChart_Chart 
506  
507  
508  
509 
tel 
510  
511  
512 
***************************************************State :Chart_Chart Automaton*************************************************** 
513  
514 
node GraphFun1_Chart(noInput :bool) 
515  
516 
returns (c:real); 
517  
518  
519 
var c_1: real; 
520  
521 
a, a_1: real; 
522  
523 
b, b_1: real; 
524  
525 
idChart_Chart, idChart_Chart_1: int; 
526  
527 
let 
528  
529 
c_1 = 0.0 > pre c; 
530  
531 
a_1 = 0.0 > pre a; 
532  
533 
b_1 = 0.0 > pre b; 
534  
535 
idChart_Chart_1 = 0 > pre idChart_Chart; 
536  
537 

538  
539  
540  
541 
(idChart_Chart, a, b, c) 
542 
= Chart_Chart_node(idChart_Chart_1, a_1, b_1, c_1); 
543  
544  
545 
unused outputs 
546 

547  
548 
tel 
549  
550  
551  
552 
node GraphFun1 (i_virtual : real) 
553 
returns (c_1_1 : real); 
554 
var 
555 
Chart_1_1 : real; 
556 
i_virtual_local : real; 
557 
let 
558 
Chart_1_1 = GraphFun1_Chart(true); 
559 
c_1_1 = Chart_1_1; 
560 
i_virtual_local= 0.0 > 1.0; 
561 
tel 
562 