lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 9c654082
History  View  Annotate  Download (13.5 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 : GlobalVarDef.t list 
11  
12 
end) : TransformerType = 
13 
struct 
14 
include TransformerStub 
15  
16 
type name_t = string 
17 
type t_base = { statements : LustreSpec.statement list; assert_false: bool } 
18 
type t = name_t > name_t > (ActiveStates.Vars.t * t_base) 
19  
20 

21 
let new_loc, reset_loc = 
22 
let cpt = ref 0 in 
23 
((fun () > incr cpt; Format.sprintf "loc_%i" !cpt), 
24 
(fun () > cpt := 0)) 
25  
26 
let new_aut, reset_aut = 
27 
let cpt = ref 0 in 
28 
((fun () > incr cpt; Format.sprintf "aut_%i" !cpt), 
29 
(fun () > cpt := 0)) 
30 

31 
let pp_path prefix fmt path = 
32 
Format.fprintf fmt "%s%t" 
33 
prefix 
34 
(fun fmt > Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path) 
35  
36 
let pp_typed_path sin fmt path = 
37 
Format.fprintf fmt "%a : bool" (pp_path sin) path 
38  
39 
let pp_vars sin fmt vars = 
40 
Format.fprintf fmt "%t" (fun fmt > Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars)) 
41 
let pp_vars_decl sin fmt vars = 
42 
Format.fprintf fmt "%t" (fun fmt > Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars)) 
43 

44 
let var_to_ident prefix p = 
45 
pp_path prefix Format.str_formatter p; 
46 
Format.flush_str_formatter () 
47  
48 
let vars_to_ident_list ?(prefix="") vars = 
49 
List.map ( 
50 
fun p > var_to_ident prefix p 
51 
) (ActiveStates.Vars.elements vars) 
52  
53 
let mkvar name typ = 
54 
let loc = Location.dummy_loc in 
55 
Corelang.mkvar_decl 
56 
loc 
57 
(name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None, None (*"__no_parent__" *)) 
58  
59 
let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
60 
let state_vars_to_vdecl_list ?(prefix="") vars = 
61 
let bool_type = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_bool in 
62 
List.map 
63 
(fun v > var_to_vdecl ~prefix:prefix v bool_type) 
64 
(ActiveStates.Vars.elements vars) 
65  
66 
let mk_locals locs = 
67 
ActiveStates.Vars.fold (fun v accu > 
68 
(state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars)@accu 
69 
) locs [] 
70 
(* TODO: declare global vars *) 
71  
72 
let mkeq = Corelang.mkeq Location.dummy_loc 
73 
let mkexpr = Corelang.mkexpr Location.dummy_loc 
74 
let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc 
75 
let expr_of_bool b = mkexpr (LustreSpec.Expr_const (Corelang.const_of_bool b)) 
76 
let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs = 
77 
{ statements = [ 
78 
LustreSpec.Eq ( 
79 
mkeq ( 
80 
vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *) 
81 
rhs (* rhs *) 
82 
) 
83 
) 
84 
]; 
85 
assert_false = false 
86 
} 
87 
let base_to_assert b = 
88 
if b.assert_false then 
89 
[{LustreSpec.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}] 
90 
else 
91 
[] 
92  
93 

94 
let var_to_expr ?(prefix="") p = 
95 
let id = var_to_ident prefix p in 
96 
Corelang.expr_of_ident id Location.dummy_loc 
97  
98 
let vars_to_exprl ?(prefix="") vars = 
99 
List.map 
100 
(fun p > var_to_expr ~prefix:prefix p) 
101 
(ActiveStates.Vars.elements vars) 
102  
103  
104 
(* Events *) 
105 
let event_type_decl = 
106 
Corelang.mktop 
107 
( 
108 
LustreSpec.TypeDef { 
109 
LustreSpec.tydef_id = "event_type"; 
110 
tydef_desc = LustreSpec.Tydec_int 
111 
} 
112 
) 
113 

114 
let event_type = { 
115 
LustreSpec.ty_dec_desc = LustreSpec.Tydec_const "event_type"; 
116 
LustreSpec.ty_dec_loc = Location.dummy_loc; 
117 
} 
118 

119 
let event_var = mkvar "event" event_type 
120  
121  
122 
let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13 
123 
let get_event_const e = 
124 
try Hashtbl.find const_map e 
125 
with Not_found > ( 
126 
let nb = Hashtbl.length const_map in 
127 
Hashtbl.add const_map e nb; 
128 
nb 
129 
) 
130  
131  
132 

133 
let null sin sout = 
134 
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in 
135 
ActiveStates.Vars.empty, 
136 
( 
137 
(* Nothing happen here: out_vars = in_vars *) 
138 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
139 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
140 
) 
141 

142 
let bot sin sout = 
143 
let (vars, tr) = null sin sout in 
144 
( 
145 
ActiveStates.Vars.empty, 
146 
{ tr with assert_false = true } 
147 
) 
148 

149 
let ( >> ) tr1 tr2 sin sout = 
150 
let l = new_loc () in 
151 
let (vars1, tr1) = tr1 sin l in 
152 
let (vars2, tr2) = tr2 l sout in 
153 
(ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2), 
154 
{ 
155 
statements = tr1.statements @ tr2.statements; 
156 
assert_false = tr1.assert_false  tr2.assert_false 
157 
} 
158 
) 
159 

160 
let pp_name : 
161 
type c. c call_t > c > unit = 
162 
fun call > 
163 
match call with 
164 
 Ecall > (fun (p, p', f) > 
165 
Format.fprintf Format.str_formatter "theta%a%a%a_%a" 
166 
pp_call call 
167 
(pp_path "_from_") p 
168 
(pp_path "_to_") p' 
169 
pp_frontier f) 
170 
 Dcall > (fun p > 
171 
Format.fprintf Format.str_formatter "theta%a%a" 
172 
pp_call call 
173 
(pp_path "_from_") p) 
174 
 Xcall > (fun (p, f) > 
175 
Format.fprintf Format.str_formatter "theta%a%a_%a" 
176 
pp_call call 
177 
(pp_path "_from_") p 
178 
pp_frontier f) 
179 

180  
181 
let mkcall' : 
182 
type c. name_t > name_t > c call_t > c > t_base = 
183 
fun sin sout call arg > 
184 
pp_name call arg; 
185 
let funname = Format.flush_str_formatter () in 
186 
let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in 
187 
let rhs = mkpredef_call funname args in 
188 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
189 

190 
let mkact' action sin sout = 
191 
match action with 
192 
 Action.Call (c, a) > mkcall' sin sout c a 
193 
 Action.Quote a > 
194 
(* TODO: check. This seems to be innappropriate *) 
195 
(* let funname = "action_" ^ a.ident in 
196 
let args = vars_to_exprl ~prefix:sin Vars.state_vars in 
197 
let rhs = mkpredef_call funname args in 
198 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
199 
*) 
200 
{ 
201 
statements = a.defs; 
202 
assert_false = false 
203 
} 
204 
 Action.Open p > 
205 
let vars' = ActiveStates.Vars.remove p Vars.state_vars in 
206 
(* eq1: sout_p = true *) 
207 
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in 
208 
(* eq2: sout_xx = sin_xx *) 
209 
let expr_list = vars_to_exprl ~prefix:sin vars' in 
210 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
211 
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in 
212 
{ 
213 
statements = [ 
214 
LustreSpec.Eq (eq1); 
215 
LustreSpec.Eq (eq2); 
216 
]; 
217 
assert_false = false 
218 
} 
219 

220 
 Action.Close p > 
221 
let vars' = ActiveStates.Vars.remove p Vars.state_vars in 
222 
(* eq1: sout_p = false *) 
223 
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in 
224 
(* eq2: sout_xx = sin_xx *) 
225 
let expr_list = vars_to_exprl ~prefix:sin vars' in 
226 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
227 
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in 
228 
{ 
229 
statements = [ 
230 
LustreSpec.Eq (eq1); 
231 
LustreSpec.Eq (eq2); 
232 
]; 
233 
assert_false = false 
234 
} 
235  
236 
 Action.Nil > 
237 
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in 
238 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
239 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
240 

241 
let eval_act kenv (action : act_t) = 
242 
(*Format.printf " action = %a@." Action.pp_act action;*) 
243 
(fun sin sout > (ActiveStates.Vars.empty, 
244 
mkact' action sin sout )) 
245 

246 
let rec mkcond' sin condition = 
247 
(*Format.printf " cond = %a@." Condition.pp_cond condition;*) 
248 
match condition with 
249 
 Condition.True > expr_of_bool true 
250 
 Condition.Active p > var_to_expr ~prefix:sin p 
251 
 Condition.Event e > 
252 
mkpredef_call "=" [ 
253 
Corelang.expr_of_vdecl event_var; 
254 
mkexpr (LustreSpec.Expr_const (LustreSpec.Const_int (get_event_const e))) 
255 
] 
256 
 Condition.Neg cond > mkpredef_call "not" [mkcond' sin cond] 
257 
 Condition.And (cond1, cond2) > mkpredef_call "&&" [mkcond' sin cond1; 
258 
mkcond' sin cond2] 
259 
 Condition.Quote c > c.expr (* TODO: shall we prefix with sin ? *) 
260  
261 
let rec eval_cond condition (ok:t) ko sin sout = 
262 
let open LustreSpec in 
263 
let loc = Location.dummy_loc in 
264 
(*Format.printf " cond = %a@." Condition.pp_cond condition;*) 
265 
let (vars1, tr1) = ok sin sout in 
266 
let (vars2, tr2) = ko sin sout in 
267 
let (vars0, tr0) = bot sin sout in 
268 
let aut = new_aut () in 
269 
(ActiveStates.Vars.empty, 
270 
{ 
271 
statements = [ 
272 
let handler_default_mode = (* Default mode : CenterPoint *) 
273 
let handler_default_mode_unless = [ 
274 
(loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut); 
275 
(loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut); 
276 
] 
277 
in 
278 
Automata.mkhandler 
279 
loc (* location *) 
280 
("CenterPoint_" ^ aut) (* state name *) 
281 
handler_default_mode_unless (* unless *) 
282 
[] (* until *) 
283 
[] (* locals *) 
284 
(tr0.statements, base_to_assert tr0, []) (* stmts, asserts, annots *) 
285 
in 
286 
let handler_cond_mode = (* Cond mode *) 
287 
let handler_cond_mode_until = [ 
288 
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); 
289 
] 
290 
in 
291 
Automata.mkhandler 
292 
loc (* location *) 
293 
("Cond_" ^ aut) (* state name *) 
294 
[] (* unless *) 
295 
handler_cond_mode_until (* until *) 
296 
(mk_locals vars1) (* locals *) 
297 
(tr1.statements, base_to_assert tr1, []) (* stmts, asserts, annots *) 
298 
in 
299 
let handler_notcond_mode = (* NotCond mode *) 
300 
let handler_notcond_mode_until = [ 
301 
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); 
302 
] 
303 
in 
304 
Automata.mkhandler 
305 
loc (* location *) 
306 
("NotCond_" ^ aut) (* state name *) 
307 
[] (* unless *) 
308 
handler_notcond_mode_until (* until *) 
309 
(mk_locals vars2) (* locals *) 
310 
(tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *) 
311 
in 
312 
let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in 
313 
Aut (Automata.mkautomata loc aut handlers) 
314 
]; 
315 
assert_false = false 
316 
} 
317 
) 
318 

319 
let mktransformer tr = 
320 
let (vars, tr) = tr "sin_" "sout_" 
321 
in tr 
322 

323 
let mkcomponent : 
324 
type c. c call_t > c > t > LustreSpec.program = 
325 
fun call args > 
326 
fun tr > 
327 
reset_loc (); 
328 
let (vars', tr') = tr "sin_" "sout_" in 
329 
pp_name call args; 
330 
let funname = Format.flush_str_formatter () in 
331 
let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in 
332 
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in 
333 
let node = 
334 
Corelang.mktop ( 
335 
LustreSpec.Node {LustreSpec.node_id = funname; 
336 
node_type = Types.new_var (); 
337 
node_clock = Clocks.new_var true; 
338 
node_inputs = inputs; 
339 
node_outputs = outputs; 
340 
node_locals = mk_locals vars'; (* TODO: add global vars *) 
341 
node_gencalls = []; 
342 
node_checks = []; 
343 
node_stmts = tr'.statements; 
344 
node_asserts = base_to_assert tr'; 
345 
node_dec_stateless = false; 
346 
node_stateless = None; 
347 
node_spec = None; 
348 
node_annot = []} 
349 
) 
350 
in 
351 
[node] 
352  
353  
354  
355 
(* TODO 
356 
C'est pas evident. 
357 
Il faut faire les choses suivantes: 
358 
 rajouter dans un ensemble les variables manipulées localement 
359 
 on doit comprendre comment les variables globales sont injectées dans le modele final: 
360 
 le node principal doit uniquement les afficher. Il peut les initialiser avec les valeurs init définies. Puis appeller la fcn thetacallD_from_principal. 
361 
 elles peuvent/doivent etre dans input et output de ce node thetacallD 
362 
*) 
363  
364 

365 
let mk_main_loop () = 
366 
(* let loc = Location.dummy_loc in *) 
367 

368 
let call_stmt = 
369 
(* (%t) > pre (thetaCallD_from_principal (event, %a)) *) 
370 
let init = 
371 
let init_state_false = 
372 
List.map (fun _ > expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in 
373 
let init_globals = 
374 
List.map (fun v > v.GlobalVarDef.init_val) Vars.global_vars in 
375 
mkexpr (LustreSpec.Expr_tuple (init_state_false @ init_globals)) 
376 
in 
377 
let args = (Corelang.expr_of_vdecl event_var):: 
378 
(vars_to_exprl ~prefix:"sout_" Vars.state_vars) 
379 
in 
380 
let call_expr = mkpredef_call "thetaCallD_from_principal" args in 
381 
let pre_call_expr = mkexpr (LustreSpec.Expr_pre (call_expr)) in 
382 
let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in 
383 
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs 
384 
in 
385 
let inputs = List.map Corelang.copy_var_decl [event_var] in 
386 
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in 
387 
(* TODO add the globals as sout_data_x entry values *) 
388 
let node_principal = 
389 
Corelang.mktop ( 
390 
LustreSpec.Node {LustreSpec.node_id = "principal_loop"; 
391 
node_type = Types.new_var (); 
392 
node_clock = Clocks.new_var true; 
393 
node_inputs = inputs; 
394 
node_outputs = outputs; 
395 
node_locals = []; (* TODO: add global vars *) 
396 
node_gencalls = []; 
397 
node_checks = []; 
398 
node_asserts = base_to_assert call_stmt; 
399 
node_stmts = call_stmt.statements; 
400 
node_dec_stateless = false; 
401 
node_stateless = None; 
402 
node_spec = None; 
403 
node_annot = []} 
404 
) 
405 
in 
406 
node_principal 
407 

408  
409 
let mkprincipal tr = 
410 
event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()] 
411  
412 
end 