## lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 93119c3f

History | View | Annotate | Download (12.3 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 | let new_loc, reset_loc = |
||

20 | let cpt = ref 0 in |
||

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

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

23 | |||

24 | let new_aut, reset_aut = |
||

25 | let cpt = ref 0 in |
||

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

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

28 | |||

29 | let pp_path prefix fmt path = |
||

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

31 | prefix |
||

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

33 | |||

34 | let pp_typed_path sin fmt path = |
||

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

36 | |||

37 | let pp_vars sin fmt vars = |
||

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

39 | let pp_vars_decl sin fmt vars = |
||

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

41 | |||

42 | let pp_locals fmt locs = |
||

43 | ActiveStates.Vars.iter (fun v -> Format.fprintf fmt "%a;@ " (pp_vars_decl (List.hd v)) Vars.state_vars) locs; |
||

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

45 | |||

46 | let var_to_ident prefix p = |
||

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

48 | Format.flush_str_formatter () |
||

49 | |||

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

51 | List.map ( |
||

52 | fun p -> var_to_ident prefix p |
||

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

54 | |||

55 | let mkvar name typ = |
||

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

57 | Corelang.mkvar_decl |
||

58 | loc |
||

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

60 | |||

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

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

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

64 | List.map |
||

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

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

67 | |||

68 | let mkeq = Corelang.mkeq Location.dummy_loc |
||

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

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

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

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

73 | { statements = [ |
||

74 | LustreSpec.Eq ( |
||

75 | mkeq ( |
||

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

77 | rhs (* rhs *) |
||

78 | ) |
||

79 | ) |
||

80 | ]; |
||

81 | assert_false = false |
||

82 | } |
||

83 | |||

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

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

86 | Corelang.expr_of_ident id Location.dummy_loc |
||

87 | |||

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

89 | List.map |
||

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

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

92 | |||

93 | |||

94 | (* Events *) |
||

95 | let event_type_decl = |
||

96 | Corelang.mktop |
||

97 | ( |
||

98 | LustreSpec.TypeDef { |
||

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

100 | tydef_desc = LustreSpec.Tydec_int |
||

101 | } |
||

102 | ) |
||

103 | |||

104 | let event_type = { |
||

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

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

107 | } |
||

108 | |||

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

110 | |||

111 | |||

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

113 | let get_event_const e = |
||

114 | try Hashtbl.find const_map e |
||

115 | with Not_found -> ( |
||

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

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

118 | nb |
||

119 | ) |
||

120 | |||

121 | |||

122 | |||

123 | let null sin sout = |
||

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

125 | ActiveStates.Vars.empty, |
||

126 | ( |
||

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

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

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

130 | ) |
||

131 | |||

132 | let bot sin sout = |
||

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

134 | ( |
||

135 | ActiveStates.Vars.empty, |
||

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

137 | ) |
||

138 | |||

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

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

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

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

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

144 | { |
||

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

146 | assert_false = tr1.assert_false || tr2.assert_false |
||

147 | } |
||

148 | ) |
||

149 | |||

150 | let mkcall' : |
||

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

152 | fun sin sout call -> |
||

153 | let pp_name : type c. c call_t -> c -> unit = |
||

154 | fun call -> |
||

155 | match call with |
||

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

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

158 | pp_call call |
||

159 | (pp_path "_from_") p |
||

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

161 | pp_frontier f) |
||

162 | | Dcall -> (fun p -> |
||

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

164 | pp_call call |
||

165 | (pp_path "_from_") p) |
||

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

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

168 | pp_call call |
||

169 | (pp_path "_from_") p |
||

170 | pp_frontier f) |
||

171 | in |
||

172 | fun arg -> |
||

173 | pp_name call arg; |
||

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

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

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

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

178 | |||

179 | let mkact' action sin sout = |
||

180 | match action with |
||

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

182 | | Action.Quote a -> |
||

183 | let funname = "action_" ^ a.ident in |
||

184 | let args = vars_to_exprl ~prefix:sin Vars.state_vars in |
||

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

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

187 | | Action.Open p -> |
||

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

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

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

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

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

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

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

195 | { |
||

196 | statements = [ |
||

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

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

199 | ]; |
||

200 | assert_false = false |
||

201 | } |
||

202 | |||

203 | | Action.Close p -> |
||

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

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

206 | let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) 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.Nil -> |
||

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

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

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

223 | |||

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

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

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

227 | mkact' action sin sout )) |
||

228 | |||

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

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

231 | match condition with |
||

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

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

234 | | Condition.Event e -> |
||

235 | mkpredef_call "=" [ |
||

236 | Corelang.expr_of_vdecl event_var; |
||

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

238 | ] |
||

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

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

241 | mkcond' sin cond2] |
||

242 | | Condition.Quote c -> c (* TODO: shall we prefix with sin ? *) |
||

243 | |||

244 | let rec eval_cond condition ok ko sin sout = |
||

245 | let open LustreSpec in |
||

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

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

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

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

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

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

252 | (ActiveStates.Vars.empty, |
||

253 | { |
||

254 | statements = [ |
||

255 | Aut ( |
||

256 | { aut_id = aut; |
||

257 | aut_loc = loc; |
||

258 | aut_handlers = |
||

259 | [ |
||

260 | (* Default mode : CenterPoint *) |
||

261 | { hand_state = "CenterPoint_" ^ aut; |
||

262 | hand_unless = [ |
||

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

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

265 | ]; |
||

266 | hand_until = []; |
||

267 | hand_locals = []; |
||

268 | hand_stmts = tr0.statements; |
||

269 | hand_asserts = if tr0.assert_false then |
||

270 | [{assert_expr = expr_of_bool false; assert_loc = loc}] |
||

271 | else |
||

272 | []; |
||

273 | hand_annots = []; |
||

274 | hand_loc = loc; |
||

275 | }; |
||

276 | (* Cond mode *) |
||

277 | { hand_state = "Cond_" ^ aut; |
||

278 | hand_unless = []; |
||

279 | hand_until = [ |
||

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

281 | ]; |
||

282 | hand_locals = [vars1] (* TODO convert to valid type *); |
||

283 | hand_stmts = tr1.statements; |
||

284 | hand_asserts = if tr1.assert_false then |
||

285 | [{assert_expr = expr_of_bool false; assert_loc = loc}] |
||

286 | else |
||

287 | []; |
||

288 | hand_annots = []; |
||

289 | hand_loc = loc; |
||

290 | }; |
||

291 | (* NotCond mode *) |
||

292 | { hand_state = "NotCond_" ^ aut; |
||

293 | hand_unless = []; |
||

294 | hand_until = [ |
||

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

296 | ]; |
||

297 | hand_locals = [vars2] (* TODO convert to valid type *); |
||

298 | hand_stmts = tr2.statements; |
||

299 | hand_asserts = if tr2.assert_false then |
||

300 | [{assert_expr = expr_of_bool false; assert_loc = loc}] |
||

301 | else |
||

302 | []; |
||

303 | hand_annots = []; |
||

304 | hand_loc = loc; |
||

305 | }; |
||

306 | ] |
||

307 | } |
||

308 | ) |
||

309 | ]; |
||

310 | assert_false = false |
||

311 | } |
||

312 | ) |
||

313 | |||

314 | let pp_transformer fmt tr = |
||

315 | let (vars, tr) = tr "sin_" "sout_" |
||

316 | in tr fmt |
||

317 | |||

318 | let mkcomponent : |
||

319 | type c. c call_t -> c -> t -> prog = |
||

320 | fun fmt call -> match call with |
||

321 | | Ecall -> (fun (p, p', f) tr -> |
||

322 | reset_loc (); |
||

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

324 | Format.fprintf fmt "node theta%a%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@." |
||

325 | pp_call call |
||

326 | (pp_path "_from_") p |
||

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

328 | pp_frontier f |
||

329 | (pp_vars_decl "sin_") Vars.state_vars |
||

330 | (pp_vars_decl "sout_") Vars.state_vars |
||

331 | (fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.") |
||

332 | pp_locals vars' |
||

333 | tr') |
||

334 | | Dcall -> (fun p tr -> |
||

335 | reset_loc (); |
||

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

337 | Format.fprintf fmt "node theta%a%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@." |
||

338 | pp_call call |
||

339 | (pp_path "_from_") p |
||

340 | (pp_vars_decl "sin_") Vars.state_vars |
||

341 | (pp_vars_decl "sout_") Vars.state_vars |
||

342 | (fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.") |
||

343 | pp_locals vars' |
||

344 | tr') |
||

345 | | Xcall -> (fun (p, f) tr -> |
||

346 | reset_loc (); |
||

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

348 | Format.fprintf fmt "node theta%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@." |
||

349 | pp_call call |
||

350 | (pp_path "_from_") p |
||

351 | pp_frontier f |
||

352 | (pp_vars_decl "sin_") Vars.state_vars |
||

353 | (pp_vars_decl "sout_") Vars.state_vars |
||

354 | (fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.") |
||

355 | pp_locals vars' |
||

356 | tr') |
||

357 | |||

358 | let mk_main_loop () = |
||

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

360 | let node_principal = |
||

361 | Corelang.mktop ( |
||

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

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

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

365 | node_inputs = [event_var]; |
||

366 | node_outputs = state_vars_to_vdecl_list ~prefx:"sout_" Vars.state_vars; |
||

367 | node_locals = []; (* TODO: add global vars *) |
||

368 | node_gencalls = []; |
||

369 | node_checks = []; |
||

370 | node_asserts = []; |
||

371 | node_stmts = call_stmt; |
||

372 | node_dec_stateless = false; |
||

373 | node_stateless = None; |
||

374 | node_spec = None; |
||

375 | node_annot = []} |
||

376 | ) |
||

377 | in |
||

378 | |||

379 | let call_stmt = |
||

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

381 | let init = mkexpr loc |
||

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

383 | in |
||

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

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

386 | in |
||

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

388 | let pre_call_expr = mkexpr loc (Expr_pre (call_expr)) in |
||

389 | let rhs = mkexpr loc (Expr_arrow (init, pre_call_expr)) in |
||

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

391 | in |
||

392 | [ |
||

393 | event_type_decl; |
||

394 | node_principal |
||

395 | ] |
||

396 | |||

397 | let mkprincipal tr = |
||

398 | mk_main_loop () @ mkcomponent Dcall ["principal"] tr |
||

399 | |||

400 | end |