Revision 9c654082
Added by Pierre-Loï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