Revision 9c654082
Added by PierreLoïc Garoche over 6 years ago
src/tools/stateflow/semantics/cPS_lustre_generator.ml  

7  7 
module LustrePrinter ( 
8  8 
Vars : sig 
9  9 
val state_vars : ActiveStates.Vars.t 
10 
val global_vars : LustreSpec.var_decl list 

10 
val global_vars : GlobalVarDef.t list 

11  
11  12 
end) : TransformerType = 
12  13 
struct 
13  14 
include TransformerStub 
...  ...  
53  54 
let loc = Location.dummy_loc in 
54  55 
Corelang.mkvar_decl 
55  56 
loc 
56 
(name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None) 

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


57  58  
58  59 
let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
59  60 
let state_vars_to_vdecl_list ?(prefix="") vars = 
...  ...  
115  116 
LustreSpec.ty_dec_loc = Location.dummy_loc; 
116  117 
} 
117  118 

118 
let event_var = mkvar "event" event_type 

119 
let event_var = mkvar "event" event_type


119  120  
120  121  
121  122 
let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13 
...  ...  
327  328 
let (vars', tr') = tr "sin_" "sout_" in 
328  329 
pp_name call args; 
329  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 

330  333 
let node = 
331  334 
Corelang.mktop ( 
332  335 
LustreSpec.Node {LustreSpec.node_id = funname; 
333  336 
node_type = Types.new_var (); 
334  337 
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;


338 
node_inputs = inputs;


339 
node_outputs = outputs;


337  340 
node_locals = mk_locals vars'; (* TODO: add global vars *) 
338  341 
node_gencalls = []; 
339  342 
node_checks = []; 
...  ...  
346  349 
) 
347  350 
in 
348  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  
349  364 

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

353  368 
let call_stmt = 
354  369 
(* (%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))) 

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

357  376 
in 
358  377 
let args = (Corelang.expr_of_vdecl event_var):: 
359  378 
(vars_to_exprl ~prefix:"sout_" Vars.state_vars) 
...  ...  
363  382 
let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in 
364  383 
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs 
365  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 *) 

366  388 
let node_principal = 
367  389 
Corelang.mktop ( 
368  390 
LustreSpec.Node {LustreSpec.node_id = "principal_loop"; 
369  391 
node_type = Types.new_var (); 
370  392 
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;


393 
node_inputs = inputs;


394 
node_outputs = outputs;


373  395 
node_locals = []; (* TODO: add global vars *) 
374  396 
node_gencalls = []; 
375  397 
node_checks = []; 
...  ...  
381  403 
node_annot = []} 
382  404 
) 
383  405 
in 
384 
node_principal


406 
node_principal 

385  407 

386  408  
387  409 
let mkprincipal tr = 
Also available in: Unified diff
[lustresf] work in progress. Added global env with initial values