## lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_GraphFun1 / GraphFun1.lus @ eb639349

History | View | Annotate | Download (6.33 KB)

1 | eb639349 | bourbouh | -- 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 |