## lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 9ae027f8

History | View | Annotate | Download (12.7 KB)

1 | 93119c3f | ploc | open Basetypes |
---|---|---|---|

2 | open ActiveStates |
||

3 | open CPS_transformer |
||

4 | |||

5 | let ff = Format.fprintf |
||

6 | |||

7 | module LustrePrinter ( |
||

8 | Vars : sig |
||

9 | val state_vars : ActiveStates.Vars.t |
||

10 | val global_vars : LustreSpec.var_decl list |
||

11 | end) : TransformerType = |
||

12 | struct |
||

13 | include TransformerStub |
||

14 | |||

15 | type name_t = string |
||

16 | type t_base = { statements : LustreSpec.statement list; assert_false: bool } |
||

17 | type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base) |
||

18 | |||

19 | 69c96b6c | ploc | |

20 | 93119c3f | ploc | let new_loc, reset_loc = |

21 | let cpt = ref 0 in |
||

22 | ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt), |
||

23 | (fun () -> cpt := 0)) |
||

24 | |||

25 | let new_aut, reset_aut = |
||

26 | let cpt = ref 0 in |
||

27 | ((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt), |
||

28 | (fun () -> cpt := 0)) |
||

29 | |||

30 | let pp_path prefix fmt path = |
||

31 | Format.fprintf fmt "%s%t" |
||

32 | prefix |
||

33 | (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path) |
||

34 | |||

35 | let pp_typed_path sin fmt path = |
||

36 | Format.fprintf fmt "%a : bool" (pp_path sin) path |
||

37 | |||

38 | let pp_vars sin fmt vars = |
||

39 | Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars)) |
||

40 | let pp_vars_decl sin fmt vars = |
||

41 | Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars)) |
||

42 | 74ca6b61 | ploc | |

43 | 93119c3f | ploc | let var_to_ident prefix p = |

44 | pp_path prefix Format.str_formatter p; |
||

45 | Format.flush_str_formatter () |
||

46 | |||

47 | let vars_to_ident_list ?(prefix="") vars = |
||

48 | List.map ( |
||

49 | fun p -> var_to_ident prefix p |
||

50 | ) (ActiveStates.Vars.elements vars) |
||

51 | |||

52 | let mkvar name typ = |
||

53 | let loc = Location.dummy_loc in |
||

54 | Corelang.mkvar_decl |
||

55 | loc |
||

56 | (name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None) |
||

57 | |||

58 | let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ |
||

59 | let state_vars_to_vdecl_list ?(prefix="") vars = |
||

60 | let bool_type = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_bool in |
||

61 | List.map |
||

62 | (fun v -> var_to_vdecl ~prefix:prefix v bool_type) |
||

63 | (ActiveStates.Vars.elements vars) |
||

64 | |||

65 | 69c96b6c | ploc | let mk_locals locs = |

66 | ActiveStates.Vars.fold (fun v accu -> |
||

67 | (state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars)@accu |
||

68 | ) locs [] |
||

69 | (* TODO: declare global vars *) |
||

70 | |||

71 | 93119c3f | ploc | let mkeq = Corelang.mkeq Location.dummy_loc |

72 | let mkexpr = Corelang.mkexpr Location.dummy_loc |
||

73 | let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc |
||

74 | let expr_of_bool b = mkexpr (LustreSpec.Expr_const (Corelang.const_of_bool b)) |
||

75 | let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs = |
||

76 | { statements = [ |
||

77 | LustreSpec.Eq ( |
||

78 | mkeq ( |
||

79 | vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *) |
||

80 | rhs (* rhs *) |
||

81 | ) |
||

82 | ) |
||

83 | ]; |
||

84 | assert_false = false |
||

85 | } |
||

86 | 69c96b6c | ploc | let base_to_assert b = |

87 | if b.assert_false then |
||

88 | [{LustreSpec.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}] |
||

89 | else |
||

90 | [] |
||

91 | |||

92 | 93119c3f | ploc | |

93 | let var_to_expr ?(prefix="") p = |
||

94 | let id = var_to_ident prefix p in |
||

95 | Corelang.expr_of_ident id Location.dummy_loc |
||

96 | |||

97 | let vars_to_exprl ?(prefix="") vars = |
||

98 | List.map |
||

99 | (fun p -> var_to_expr ~prefix:prefix p) |
||

100 | (ActiveStates.Vars.elements vars) |
||

101 | |||

102 | |||

103 | (* Events *) |
||

104 | let event_type_decl = |
||

105 | Corelang.mktop |
||

106 | ( |
||

107 | LustreSpec.TypeDef { |
||

108 | LustreSpec.tydef_id = "event_type"; |
||

109 | tydef_desc = LustreSpec.Tydec_int |
||

110 | } |
||

111 | ) |
||

112 | |||

113 | let event_type = { |
||

114 | LustreSpec.ty_dec_desc = LustreSpec.Tydec_const "event_type"; |
||

115 | LustreSpec.ty_dec_loc = Location.dummy_loc; |
||

116 | } |
||

117 | |||

118 | let event_var = mkvar "event" event_type |
||

119 | |||

120 | |||

121 | let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13 |
||

122 | let get_event_const e = |
||

123 | try Hashtbl.find const_map e |
||

124 | with Not_found -> ( |
||

125 | let nb = Hashtbl.length const_map in |
||

126 | Hashtbl.add const_map e nb; |
||

127 | nb |
||

128 | ) |
||

129 | |||

130 | |||

131 | |||

132 | let null sin sout = |
||

133 | let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in |
||

134 | ActiveStates.Vars.empty, |
||

135 | ( |
||

136 | (* Nothing happen here: out_vars = in_vars *) |
||

137 | let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in |
||

138 | mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
||

139 | ) |
||

140 | |||

141 | let bot sin sout = |
||

142 | let (vars, tr) = null sin sout in |
||

143 | ( |
||

144 | ActiveStates.Vars.empty, |
||

145 | { tr with assert_false = true } |
||

146 | ) |
||

147 | |||

148 | let ( >> ) tr1 tr2 sin sout = |
||

149 | let l = new_loc () in |
||

150 | let (vars1, tr1) = tr1 sin l in |
||

151 | let (vars2, tr2) = tr2 l sout in |
||

152 | (ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2), |
||

153 | { |
||

154 | statements = tr1.statements @ tr2.statements; |
||

155 | assert_false = tr1.assert_false || tr2.assert_false |
||

156 | } |
||

157 | ) |
||

158 | 69c96b6c | ploc | |

159 | let pp_name : |
||

160 | type c. c call_t -> c -> unit = |
||

161 | fun call -> |
||

162 | match call with |
||

163 | | Ecall -> (fun (p, p', f) -> |
||

164 | Format.fprintf Format.str_formatter "theta%a%a%a_%a" |
||

165 | pp_call call |
||

166 | (pp_path "_from_") p |
||

167 | (pp_path "_to_") p' |
||

168 | pp_frontier f) |
||

169 | | Dcall -> (fun p -> |
||

170 | Format.fprintf Format.str_formatter "theta%a%a" |
||

171 | pp_call call |
||

172 | (pp_path "_from_") p) |
||

173 | | Xcall -> (fun (p, f) -> |
||

174 | Format.fprintf Format.str_formatter "theta%a%a_%a" |
||

175 | pp_call call |
||

176 | (pp_path "_from_") p |
||

177 | pp_frontier f) |
||

178 | |||

179 | |||

180 | 93119c3f | ploc | let mkcall' : |

181 | type c. name_t -> name_t -> c call_t -> c -> t_base = |
||

182 | 69c96b6c | ploc | fun sin sout call arg -> |

183 | pp_name call arg; |
||

184 | let funname = Format.flush_str_formatter () in |
||

185 | let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in |
||

186 | let rhs = mkpredef_call funname args in |
||

187 | mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
||

188 | |||

189 | 93119c3f | ploc | let mkact' action sin sout = |

190 | match action with |
||

191 | | Action.Call (c, a) -> mkcall' sin sout c a |
||

192 | | Action.Quote a -> |
||

193 | 9ae027f8 | ploc | (* TODO: check. This seems to be innappropriate *) |

194 | (* let funname = "action_" ^ a.ident in |
||

195 | 93119c3f | ploc | let args = vars_to_exprl ~prefix:sin Vars.state_vars in |

196 | let rhs = mkpredef_call funname args in |
||

197 | mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
||

198 | 9ae027f8 | ploc | *) |

199 | { |
||

200 | statements = a.defs; |
||

201 | assert_false = false |
||

202 | } |
||

203 | 93119c3f | ploc | | Action.Open p -> |

204 | let vars' = ActiveStates.Vars.remove p Vars.state_vars in |
||

205 | (* eq1: sout_p = true *) |
||

206 | let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in |
||

207 | (* eq2: sout_xx = sin_xx *) |
||

208 | let expr_list = vars_to_exprl ~prefix:sin vars' in |
||

209 | let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in |
||

210 | let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in |
||

211 | { |
||

212 | statements = [ |
||

213 | LustreSpec.Eq (eq1); |
||

214 | LustreSpec.Eq (eq2); |
||

215 | ]; |
||

216 | assert_false = false |
||

217 | } |
||

218 | |||

219 | | Action.Close p -> |
||

220 | let vars' = ActiveStates.Vars.remove p Vars.state_vars in |
||

221 | (* eq1: sout_p = false *) |
||

222 | let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in |
||

223 | (* eq2: sout_xx = sin_xx *) |
||

224 | let expr_list = vars_to_exprl ~prefix:sin vars' in |
||

225 | let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in |
||

226 | let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in |
||

227 | { |
||

228 | statements = [ |
||

229 | LustreSpec.Eq (eq1); |
||

230 | LustreSpec.Eq (eq2); |
||

231 | ]; |
||

232 | assert_false = false |
||

233 | } |
||

234 | |||

235 | | Action.Nil -> |
||

236 | let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in |
||

237 | let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in |
||

238 | mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
||

239 | |||

240 | let eval_act kenv (action : act_t) = |
||

241 | (*Format.printf "----- action = %a@." Action.pp_act action;*) |
||

242 | (fun sin sout -> (ActiveStates.Vars.empty, |
||

243 | mkact' action sin sout )) |
||

244 | |||

245 | let rec mkcond' sin condition = |
||

246 | (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*) |
||

247 | match condition with |
||

248 | | Condition.True -> expr_of_bool true |
||

249 | | Condition.Active p -> var_to_expr ~prefix:sin p |
||

250 | | Condition.Event e -> |
||

251 | mkpredef_call "=" [ |
||

252 | Corelang.expr_of_vdecl event_var; |
||

253 | mkexpr (LustreSpec.Expr_const (LustreSpec.Const_int (get_event_const e))) |
||

254 | ] |
||

255 | | Condition.Neg cond -> mkpredef_call "not" [mkcond' sin cond] |
||

256 | | Condition.And (cond1, cond2) -> mkpredef_call "&&" [mkcond' sin cond1; |
||

257 | mkcond' sin cond2] |
||

258 | 9ae027f8 | ploc | | Condition.Quote c -> c.expr (* TODO: shall we prefix with sin ? *) |

259 | 93119c3f | ploc | |

260 | 69c96b6c | ploc | let rec eval_cond condition (ok:t) ko sin sout = |

261 | 93119c3f | ploc | let open LustreSpec in |

262 | let loc = Location.dummy_loc in |
||

263 | (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*) |
||

264 | let (vars1, tr1) = ok sin sout in |
||

265 | let (vars2, tr2) = ko sin sout in |
||

266 | let (vars0, tr0) = bot sin sout in |
||

267 | let aut = new_aut () in |
||

268 | (ActiveStates.Vars.empty, |
||

269 | { |
||

270 | statements = [ |
||

271 | e0d6f1d1 | ploc | let handler_default_mode = (* Default mode : CenterPoint *) |

272 | let handler_default_mode_unless = [ |
||

273 | (loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut); |
||

274 | (loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut); |
||

275 | ] |
||

276 | in |
||

277 | Automata.mkhandler |
||

278 | loc (* location *) |
||

279 | ("CenterPoint_" ^ aut) (* state name *) |
||

280 | handler_default_mode_unless (* unless *) |
||

281 | [] (* until *) |
||

282 | [] (* locals *) |
||

283 | (tr0.statements, base_to_assert tr0, []) (* stmts, asserts, annots *) |
||

284 | in |
||

285 | let handler_cond_mode = (* Cond mode *) |
||

286 | let handler_cond_mode_until = [ |
||

287 | (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); |
||

288 | ] |
||

289 | in |
||

290 | Automata.mkhandler |
||

291 | loc (* location *) |
||

292 | ("Cond_" ^ aut) (* state name *) |
||

293 | [] (* unless *) |
||

294 | handler_cond_mode_until (* until *) |
||

295 | (mk_locals vars1) (* locals *) |
||

296 | (tr1.statements, base_to_assert tr1, []) (* stmts, asserts, annots *) |
||

297 | in |
||

298 | let handler_notcond_mode = (* NotCond mode *) |
||

299 | let handler_notcond_mode_until = [ |
||

300 | (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); |
||

301 | ] |
||

302 | in |
||

303 | Automata.mkhandler |
||

304 | loc (* location *) |
||

305 | ("NotCond_" ^ aut) (* state name *) |
||

306 | [] (* unless *) |
||

307 | handler_notcond_mode_until (* until *) |
||

308 | (mk_locals vars2) (* locals *) |
||

309 | (tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *) |
||

310 | in |
||

311 | let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in |
||

312 | Aut (Automata.mkautomata loc aut handlers) |
||

313 | 93119c3f | ploc | ]; |

314 | assert_false = false |
||

315 | } |
||

316 | ) |
||

317 | |||

318 | 69c96b6c | ploc | let mktransformer tr = |

319 | 93119c3f | ploc | let (vars, tr) = tr "sin_" "sout_" |

320 | 69c96b6c | ploc | in tr |

321 | 93119c3f | ploc | |

322 | let mkcomponent : |
||

323 | 69c96b6c | ploc | type c. c call_t -> c -> t -> LustreSpec.program = |

324 | fun call args -> |
||

325 | fun tr -> |
||

326 | reset_loc (); |
||

327 | let (vars', tr') = tr "sin_" "sout_" in |
||

328 | pp_name call args; |
||

329 | let funname = Format.flush_str_formatter () in |
||

330 | let node = |
||

331 | Corelang.mktop ( |
||

332 | LustreSpec.Node {LustreSpec.node_id = funname; |
||

333 | node_type = Types.new_var (); |
||

334 | node_clock = Clocks.new_var true; |
||

335 | node_inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars; |
||

336 | node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars; |
||

337 | node_locals = mk_locals vars'; (* TODO: add global vars *) |
||

338 | node_gencalls = []; |
||

339 | node_checks = []; |
||

340 | node_stmts = tr'.statements; |
||

341 | node_asserts = base_to_assert tr'; |
||

342 | node_dec_stateless = false; |
||

343 | node_stateless = None; |
||

344 | node_spec = None; |
||

345 | node_annot = []} |
||

346 | ) |
||

347 | in |
||

348 | [node] |
||

349 | |||

350 | 93119c3f | ploc | let mk_main_loop () = |

351 | 69c96b6c | ploc | (* let loc = Location.dummy_loc in *) |

352 | |||

353 | let call_stmt = |
||

354 | (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *) |
||

355 | let init = mkexpr |
||

356 | c5d45c13 | ploc | (LustreSpec.Expr_tuple (List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars))) |

357 | 69c96b6c | ploc | in |

358 | let args = (Corelang.expr_of_vdecl event_var):: |
||

359 | (vars_to_exprl ~prefix:"sout_" Vars.state_vars) |
||

360 | in |
||

361 | let call_expr = mkpredef_call "thetaCallD_from_principal" args in |
||

362 | let pre_call_expr = mkexpr (LustreSpec.Expr_pre (call_expr)) in |
||

363 | let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in |
||

364 | mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs |
||

365 | in |
||

366 | 93119c3f | ploc | let node_principal = |

367 | Corelang.mktop ( |
||

368 | LustreSpec.Node {LustreSpec.node_id = "principal_loop"; |
||

369 | node_type = Types.new_var (); |
||

370 | node_clock = Clocks.new_var true; |
||

371 | 68601cf5 | xthirioux | node_inputs = List.map Corelang.copy_var_decl [event_var]; |

372 | 69c96b6c | ploc | node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars; |

373 | 93119c3f | ploc | node_locals = []; (* TODO: add global vars *) |

374 | node_gencalls = []; |
||

375 | node_checks = []; |
||

376 | 69c96b6c | ploc | node_asserts = base_to_assert call_stmt; |

377 | node_stmts = call_stmt.statements; |
||

378 | 93119c3f | ploc | node_dec_stateless = false; |

379 | node_stateless = None; |
||

380 | node_spec = None; |
||

381 | node_annot = []} |
||

382 | ) |
||

383 | in |
||

384 | node_principal |
||

385 | 69c96b6c | ploc | |

386 | 93119c3f | ploc | |

387 | let mkprincipal tr = |
||

388 | 69c96b6c | ploc | event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()] |

389 | 93119c3f | ploc | |

390 | end |