Revision 9c4cc944
Added by Corentin Lauverjat over 1 year ago
src/tools/stateflow/semantics/cPS_lustre_generator.ml  

14  14 
include TransformerStub 
15  15  
16  16 
type name_t = string 
17 
type t_base = { statements : Lustre_types.statement list; assert_false: bool } 

17 
type t_base = { statements : Lustrec.Lustre_types.statement list; assert_false: bool }


18  18 
type t = name_t > name_t > (ActiveStates.Vars.t * t_base) 
19  19  
20  20 

...  ...  
31  31 
let pp_path prefix fmt path = 
32  32 
Format.fprintf fmt "%s%t" 
33  33 
prefix 
34 
(fun fmt > Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path) 

34 
(fun fmt > Lustrec.Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)


35  35  
36  36 
let pp_typed_path sin fmt path = 
37  37 
Format.fprintf fmt "%a : bool" (pp_path sin) path 
38  38  
39  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)) 

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


41  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)) 

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


43  43 

44  44 
let var_to_ident prefix p = 
45  45 
pp_path prefix Format.str_formatter p; 
...  ...  
51  51 
) (ActiveStates.Vars.elements vars) 
52  52  
53  53 
let mkvar name typ = 
54 
let loc = Location.dummy_loc in 

55 
Corelang.mkvar_decl 

54 
let loc = Lustrec.Location.dummy_loc in


55 
Lustrec.Corelang.mkvar_decl


56  56 
loc 
57 
(name, typ, Corelang.mkclock loc Lustre_types.Ckdec_any, false, None, None (*"__no_parent__" *))


57 
(name, typ, Lustrec.Corelang.mkclock loc Lustrec.Lustre_types.Ckdec_any, false, None, None (*"__no_parent__" *))


58  58  
59  59 
let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
60  60 
let state_vars_to_vdecl_list ?(prefix="") vars = 
61 
let bool_type = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_bool in


61 
let bool_type = Lustrec.Corelang.mktyp Lustrec.Location.dummy_loc Lustrec.Lustre_types.Tydec_bool in


62  62 
List.map 
63  63 
(fun v > var_to_vdecl ~prefix:prefix v bool_type) 
64  64 
(ActiveStates.Vars.elements vars) 
...  ...  
69  69 
) locs [] 
70  70 
(* TODO: declare global vars *) 
71  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 (Lustre_types.Expr_const (Corelang.const_of_bool b))


72 
let mkeq = Lustrec.Corelang.mkeq Lustrec.Location.dummy_loc


73 
let mkexpr = Lustrec.Corelang.mkexpr Lustrec.Location.dummy_loc


74 
let mkpredef_call = Lustrec.Corelang.mkpredef_call Lustrec.Location.dummy_loc


75 
let expr_of_bool b = mkexpr (Lustrec.Lustre_types.Expr_const (Lustrec.Corelang.const_of_bool b))


76  76 
let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs = 
77  77 
{ statements = [ 
78 
Lustre_types.Eq ( 

78 
Lustrec.Lustre_types.Eq (


79  79 
mkeq ( 
80  80 
vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *) 
81  81 
rhs (* rhs *) 
...  ...  
86  86 
} 
87  87 
let base_to_assert b = 
88  88 
if b.assert_false then 
89 
[{Lustre_types.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]


89 
[{Lustrec.Lustre_types.assert_expr = expr_of_bool false; assert_loc = Lustrec.Location.dummy_loc}]


90  90 
else 
91  91 
[] 
92  92  
93  93 

94  94 
let var_to_expr ?(prefix="") p = 
95  95 
let id = var_to_ident prefix p in 
96 
Corelang.expr_of_ident id Location.dummy_loc


96 
Lustrec.Corelang.expr_of_ident id Lustrec.Location.dummy_loc


97  97  
98  98 
let vars_to_exprl ?(prefix="") vars = 
99  99 
List.map 
...  ...  
103  103  
104  104 
(* Events *) 
105  105 
let event_type_decl = 
106 
Corelang.mktop 

106 
Lustrec.Corelang.mktop


107  107 
( 
108 
Lustre_types.TypeDef { 

109 
Lustre_types.tydef_id = "event_type"; 

110 
tydef_desc = Lustre_types.Tydec_int 

108 
Lustrec.Lustre_types.TypeDef {


109 
Lustrec.Lustre_types.tydef_id = "event_type";


110 
tydef_desc = Lustrec.Lustre_types.Tydec_int


111  111 
} 
112  112 
) 
113  113 

114  114 
let event_type = { 
115 
Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";


116 
Lustre_types.ty_dec_loc = Location.dummy_loc;


115 
Lustrec.Lustre_types.ty_dec_desc = Lustrec.Lustre_types.Tydec_const "event_type";


116 
Lustrec.Lustre_types.ty_dec_loc = Lustrec.Location.dummy_loc;


117  117 
} 
118  118 

119  119 
let event_var = mkvar "event" event_type 
...  ...  
135  135 
ActiveStates.Vars.empty, 
136  136 
( 
137  137 
(* Nothing happen here: out_vars = in_vars *) 
138 
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 

138 
let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in


139  139 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
140  140 
) 
141  141 

...  ...  
183  183 
fun sin sout call arg > 
184  184 
pp_name call arg; 
185  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 

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


187  187 
let rhs = mkpredef_call funname args in 
188  188 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
189  189 

...  ...  
207  207 
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in 
208  208 
(* eq2: sout_xx = sin_xx *) 
209  209 
let expr_list = vars_to_exprl ~prefix:sin vars' in 
210 
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 

210 
let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in


211  211 
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in 
212  212 
{ 
213  213 
statements = [ 
214 
Lustre_types.Eq (eq1); 

215 
Lustre_types.Eq (eq2); 

214 
Lustrec.Lustre_types.Eq (eq1);


215 
Lustrec.Lustre_types.Eq (eq2);


216  216 
]; 
217  217 
assert_false = false 
218  218 
} 
...  ...  
223  223 
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in 
224  224 
(* eq2: sout_xx = sin_xx *) 
225  225 
let expr_list = vars_to_exprl ~prefix:sin vars' in 
226 
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 

226 
let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in


227  227 
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in 
228  228 
{ 
229  229 
statements = [ 
230 
Lustre_types.Eq (eq1); 

231 
Lustre_types.Eq (eq2); 

230 
Lustrec.Lustre_types.Eq (eq1);


231 
Lustrec.Lustre_types.Eq (eq2);


232  232 
]; 
233  233 
assert_false = false 
234  234 
} 
235  235  
236  236 
 Action.Nil > 
237  237 
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in 
238 
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 

238 
let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in


239  239 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
240  240 

241  241 
let eval_act kenv (action : act_t) = 
...  ...  
250  250 
 Condition.Active p > var_to_expr ~prefix:sin p 
251  251 
 Condition.Event e > 
252  252 
mkpredef_call "=" [ 
253 
Corelang.expr_of_vdecl event_var; 

254 
mkexpr (Lustre_types.Expr_const (Lustre_types.Const_int (get_event_const e)))


253 
Lustrec.Corelang.expr_of_vdecl event_var;


254 
mkexpr (Lustrec.Lustre_types.Expr_const (Lustrec.Lustre_types.Const_int (get_event_const e)))


255  255 
] 
256  256 
 Condition.Neg cond > mkpredef_call "not" [mkcond' sin cond] 
257  257 
 Condition.And (cond1, cond2) > mkpredef_call "&&" [mkcond' sin cond1; 
...  ...  
259  259 
 Condition.Quote c > c.expr (* TODO: shall we prefix with sin ? *) 
260  260  
261  261 
let rec eval_cond condition (ok:t) ko sin sout = 
262 
let open Lustre_types in 

263 
let loc = Location.dummy_loc in 

262 
let open Lustrec.Lustre_types in


263 
let loc = Lustrec.Location.dummy_loc in


264  264 
(*Format.printf " cond = %a@." Condition.pp_cond condition;*) 
265  265 
let (vars1, tr1) = ok sin sout in 
266  266 
let (vars2, tr2) = ko sin sout in 
...  ...  
275  275 
(loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut); 
276  276 
] 
277  277 
in 
278 
Automata.mkhandler 

278 
Lustrec.Automata.mkhandler


279  279 
loc (* location *) 
280  280 
("CenterPoint_" ^ aut) (* state name *) 
281  281 
handler_default_mode_unless (* unless *) 
...  ...  
288  288 
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); 
289  289 
] 
290  290 
in 
291 
Automata.mkhandler 

291 
Lustrec.Automata.mkhandler


292  292 
loc (* location *) 
293  293 
("Cond_" ^ aut) (* state name *) 
294  294 
[] (* unless *) 
...  ...  
301  301 
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); 
302  302 
] 
303  303 
in 
304 
Automata.mkhandler 

304 
Lustrec.Automata.mkhandler


305  305 
loc (* location *) 
306  306 
("NotCond_" ^ aut) (* state name *) 
307  307 
[] (* unless *) 
...  ...  
310  310 
(tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *) 
311  311 
in 
312  312 
let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in 
313 
Aut (Automata.mkautomata loc aut handlers) 

313 
Aut (Lustrec.Automata.mkautomata loc aut handlers)


314  314 
]; 
315  315 
assert_false = false 
316  316 
} 
...  ...  
321  321 
in tr 
322  322 

323  323 
let mkcomponent : 
324 
type c. c call_t > c > t > Lustre_types.program_t = 

324 
type c. c call_t > c > t > Lustrec.Lustre_types.program_t =


325  325 
fun call args > 
326  326 
fun tr > 
327  327 
reset_loc (); 
...  ...  
331  331 
let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in 
332  332 
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in 
333  333 
let node = 
334 
Corelang.mktop ( 

335 
Lustre_types.Node {Lustre_types.node_id = funname;


336 
node_type = Types.new_var (); 

337 
node_clock = Clocks.new_var true; 

334 
Lustrec.Corelang.mktop (


335 
Lustrec.Lustre_types.Node {Lustrec.Lustre_types.node_id = funname;


336 
node_type = Lustrec.Types.new_var ();


337 
node_clock = Lustrec.Clocks.new_var true;


338  338 
node_inputs = inputs; 
339  339 
node_outputs = outputs; 
340  340 
node_locals = mk_locals vars'; (* TODO: add global vars *) 
...  ...  
364  364  
365  365 

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

367 
(* let loc = Lustrec.Location.dummy_loc in *)


368  368 

369  369 
let call_stmt = 
370  370 
(* (%t) > pre (thetaCallD_from_principal (event, %a)) *) 
...  ...  
373  373 
List.map (fun _ > expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in 
374  374 
let init_globals = 
375  375 
List.map (fun v > v.GlobalVarDef.init_val) Vars.global_vars in 
376 
mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals)) 

376 
mkexpr (Lustrec.Lustre_types.Expr_tuple (init_state_false @ init_globals))


377  377 
in 
378 
let args = (Corelang.expr_of_vdecl event_var):: 

378 
let args = (Lustrec.Corelang.expr_of_vdecl event_var)::


379  379 
(vars_to_exprl ~prefix:"sout_" Vars.state_vars) 
380  380 
in 
381  381 
let call_expr = mkpredef_call "thetaCallD_from_principal" args in 
382 
let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in 

383 
let rhs = mkexpr (Lustre_types.Expr_arrow (init, pre_call_expr)) in 

382 
let pre_call_expr = mkexpr (Lustrec.Lustre_types.Expr_pre (call_expr)) in


383 
let rhs = mkexpr (Lustrec.Lustre_types.Expr_arrow (init, pre_call_expr)) in


384  384 
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs 
385  385 
in 
386 
let inputs = List.map Corelang.copy_var_decl [event_var] in 

386 
let inputs = List.map Lustrec.Corelang.copy_var_decl [event_var] in


387  387 
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in 
388  388 
(* TODO add the globals as sout_data_x entry values *) 
389  389 
let node_principal = 
390 
Corelang.mktop ( 

391 
Lustre_types.Node {Lustre_types.node_id = "principal_loop";


392 
node_type = Types.new_var (); 

393 
node_clock = Clocks.new_var true; 

390 
Lustrec.Corelang.mktop (


391 
Lustrec.Lustre_types.Node {Lustrec.Lustre_types.node_id = "principal_loop";


392 
node_type = Lustrec.Types.new_var ();


393 
node_clock = Lustrec.Clocks.new_var true;


394  394 
node_inputs = inputs; 
395  395 
node_outputs = outputs; 
396  396 
node_locals = []; (* TODO: add global vars *) 
Also available in: Unified diff
Transition to dune build system
Improvement of opam integration
Dockerfile based on Alpine
Dockerfile based on Ubuntu
Update the README.md