lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 9ae027f8
History | View | Annotate | Download (12.7 KB)
1 |
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 |
|
20 |
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 |
|
43 |
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 |
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 |
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 |
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 |
|
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 |
|
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 |
let mkcall' : |
181 |
type c. name_t -> name_t -> c call_t -> c -> t_base = |
182 |
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 |
let mkact' action sin sout = |
190 |
match action with |
191 |
| Action.Call (c, a) -> mkcall' sin sout c a |
192 |
| Action.Quote a -> |
193 |
(* TODO: check. This seems to be innappropriate *) |
194 |
(* let funname = "action_" ^ a.ident in |
195 |
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 |
*) |
199 |
{ |
200 |
statements = a.defs; |
201 |
assert_false = false |
202 |
} |
203 |
| 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 |
| Condition.Quote c -> c.expr (* TODO: shall we prefix with sin ? *) |
259 |
|
260 |
let rec eval_cond condition (ok:t) ko sin sout = |
261 |
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 |
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 |
]; |
314 |
assert_false = false |
315 |
} |
316 |
) |
317 |
|
318 |
let mktransformer tr = |
319 |
let (vars, tr) = tr "sin_" "sout_" |
320 |
in tr |
321 |
|
322 |
let mkcomponent : |
323 |
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 |
let mk_main_loop () = |
351 |
(* let loc = Location.dummy_loc in *) |
352 |
|
353 |
let call_stmt = |
354 |
(* (%t) -> pre (thetaCallD_from_principal (event, %a)) *) |
355 |
let init = mkexpr |
356 |
(LustreSpec.Expr_tuple (List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars))) |
357 |
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 |
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 |
node_inputs = List.map Corelang.copy_var_decl [event_var]; |
372 |
node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars; |
373 |
node_locals = []; (* TODO: add global vars *) |
374 |
node_gencalls = []; |
375 |
node_checks = []; |
376 |
node_asserts = base_to_assert call_stmt; |
377 |
node_stmts = call_stmt.statements; |
378 |
node_dec_stateless = false; |
379 |
node_stateless = None; |
380 |
node_spec = None; |
381 |
node_annot = []} |
382 |
) |
383 |
in |
384 |
node_principal |
385 |
|
386 |
|
387 |
let mkprincipal tr = |
388 |
event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()] |
389 |
|
390 |
end |