From 9c65408284d9dc252cbc9aacbbd34430ce9eca7d Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Tue, 13 Feb 2018 17:42:39 +0100
Subject: [PATCH] [lustresf] work in progress. Added global env with initial
values
---
src/tools/stateflow/common/basetypes.ml | 9 +++-
src/tools/stateflow/common/datatype.ml | 4 +-
.../json-parser/main_parse_json_file.ml | 22 ++++++----
src/tools/stateflow/models/model_simple.ml | 8 +++-
src/tools/stateflow/models/model_stopwatch.ml | 16 +++++--
src/tools/stateflow/semantics/cPS.ml | 4 +-
.../semantics/cPS_lustre_generator.ml | 42 ++++++++++++++-----
src/tools/stateflow/sf_sem.ml | 4 +-
8 files changed, 79 insertions(+), 30 deletions(-)
diff --git a/src/tools/stateflow/common/basetypes.ml b/src/tools/stateflow/common/basetypes.ml
index b8781b20..8b19769e 100644
--- a/src/tools/stateflow/common/basetypes.ml
+++ b/src/tools/stateflow/common/basetypes.ml
@@ -122,8 +122,8 @@ sig
val pp_cond : Format.formatter -> t -> unit
end
-
- module Condition =
+
+module Condition =
struct
type t =
| Quote of base_condition_t
@@ -155,3 +155,8 @@ struct
end
let _ = (module Condition : ConditionType)
+
+module GlobalVarDef =
+struct
+ type t = {variable: LustreSpec.var_decl; init_val: LustreSpec.expr}
+end
diff --git a/src/tools/stateflow/common/datatype.ml b/src/tools/stateflow/common/datatype.ml
index 9d3c17a2..0b2eab44 100644
--- a/src/tools/stateflow/common/datatype.ml
+++ b/src/tools/stateflow/common/datatype.ml
@@ -39,7 +39,7 @@ type 'prog_t src_components_t =
| Junction of junction_name_t * transitions_t
| SFFunction of 'prog_t
-type prog_t = Program of state_name_t * prog_t src_components_t list * LustreSpec.var_decl list
+type prog_t = Program of state_name_t * prog_t src_components_t list * (LustreSpec.var_decl * LustreSpec.expr) list
type scope_t = Constant | Input | Local | Output | Parameter
@@ -159,7 +159,7 @@ struct
Format.fprintf fmt "Main node name: %s@ %a@ %a@"
name
(pp_src pp_sffunction) component_list
- pp_vars vars
+ pp_vars (List.map fst vars)
let pp_scope fmt src =
Format.fprintf fmt (match src with
diff --git a/src/tools/stateflow/json-parser/main_parse_json_file.ml b/src/tools/stateflow/json-parser/main_parse_json_file.ml
index a9c5a9c2..f0dd09c3 100644
--- a/src/tools/stateflow/json-parser/main_parse_json_file.ml
+++ b/src/tools/stateflow/json-parser/main_parse_json_file.ml
@@ -129,25 +129,31 @@ let json_parse _ file pp =
end) in
let module Sem = CPS.Semantics (T) (Model) in
let prog = Sem.code_gen modularmode in
+ let header = List.map Corelang.mktop [
+ (LustreSpec.Open (false,"lustrec_math"));
+ (LustreSpec.Open (false,"conv"));
+ (LustreSpec.Open (true,"locallib"));
+ ]
+ in
+ let prog =header@prog in
Options.print_dec_types := true;
- Format.printf "%a@." Printers.pp_prog prog;
+ (* Format.printf "%a@." Printers.pp_prog prog; *)
let auto_file = "sf_gen_test_auto.lus" in (* Could be changed *)
let auto_out = open_out auto_file in
let auto_fmt = Format.formatter_of_out_channel auto_out in
Format.fprintf auto_fmt "%a@." Printers.pp_prog prog;
-
- let prog = (LustreSpec.Open ("math",false))::prog
+ Format.eprintf "Print initial lustre model with automaton in sf_gen_test_auto.lus@.";
+
let prog, deps = Compiler_stages.stage1 prog "" "" in
- Format.printf "%a@." Printers.pp_prog prog;
+ (* Format.printf "%a@." Printers.pp_prog prog; *)
let noauto_file = "sf_gen_test_noauto.lus" in (* Could be changed *)
let noauto_out = open_out noauto_file in
let noauto_fmt = Format.formatter_of_out_channel noauto_out in
- Format.fprintf noauto_fmt "%a@." Printers.pp_prog prog
-
-
-
+ Format.fprintf noauto_fmt "%a@." Printers.pp_prog prog;
+ Format.eprintf "Print expanded lustre model in sf_gen_test_noauto.lus@.";
+ ()
with Parse.Error (l, err) -> Format.eprintf "Parse error at loc %a : %a@.@?" Location.pp_loc l Parse.pp_error err
diff --git a/src/tools/stateflow/models/model_simple.ml b/src/tools/stateflow/models/model_simple.ml
index 05c042ab..d89b8464 100644
--- a/src/tools/stateflow/models/model_simple.ml
+++ b/src/tools/stateflow/models/model_simple.ml
@@ -3,7 +3,13 @@ open SF
let name = "simple"
- let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
+let condition x = condition {
+ expr = Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true));
+ cinputs = [];
+ coutputs = [];
+ cvariables = [];
+}
+
let action _ = no_action
let model : prog_t =
diff --git a/src/tools/stateflow/models/model_stopwatch.ml b/src/tools/stateflow/models/model_stopwatch.ml
index 2abca849..b4ed5f22 100644
--- a/src/tools/stateflow/models/model_stopwatch.ml
+++ b/src/tools/stateflow/models/model_stopwatch.ml
@@ -5,8 +5,12 @@ open SF
let verbose = false
let actionv x = no_action (*TODO if verbose then action x else no_action*)
let action x = no_action (* TODO *)
-let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
-
+let condition x = condition {
+ expr = Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true));
+ cinputs = [];
+ coutputs = [];
+ cvariables = [];
+}
let name = "stopwatch"
let model =
@@ -250,8 +254,12 @@ let model =
int_typ, (* type *)
Corelang.dummy_clock_dec, (* clock *)
false, (* not a constant *)
- None (* no default value *)
- )
+ None, (* no default value *)
+ None (* no parent known *)
+ ),
+ (* Default value is zero *)
+ Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (LustreSpec.Const_int 0))
+
)
["cent";
"sec";
diff --git a/src/tools/stateflow/semantics/cPS.ml b/src/tools/stateflow/semantics/cPS.ml
index 795feb94..b73c2507 100644
--- a/src/tools/stateflow/semantics/cPS.ml
+++ b/src/tools/stateflow/semantics/cPS.ml
@@ -8,10 +8,10 @@ struct
module Prog =
struct
- let init, defs, state_vars =
+ let init, defs, state_vars, globals =
let Program (init, defs, globals) = M.model in
let state_vars = SF.states M.model in
- init, defs, state_vars
+ init, defs, state_vars, globals
(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; () *)
end
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.ml b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
index 481da149..06088873 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
@@ -7,7 +7,8 @@ let ff = Format.fprintf
module LustrePrinter (
Vars : sig
val state_vars : ActiveStates.Vars.t
- val global_vars : LustreSpec.var_decl list
+ val global_vars : GlobalVarDef.t list
+
end) : TransformerType =
struct
include TransformerStub
@@ -53,7 +54,7 @@ struct
let loc = Location.dummy_loc in
Corelang.mkvar_decl
loc
- (name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None)
+ (name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None, None (*"__no_parent__" *))
let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ
let state_vars_to_vdecl_list ?(prefix="") vars =
@@ -115,7 +116,7 @@ struct
LustreSpec.ty_dec_loc = Location.dummy_loc;
}
- let event_var = mkvar "event" event_type
+ let event_var = mkvar "event" event_type
let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13
@@ -327,13 +328,15 @@ struct
let (vars', tr') = tr "sin_" "sout_" in
pp_name call args;
let funname = Format.flush_str_formatter () in
+ let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in
+ let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
let node =
Corelang.mktop (
LustreSpec.Node {LustreSpec.node_id = funname;
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
- node_inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars;
- node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars;
+ node_inputs = inputs;
+ node_outputs = outputs;
node_locals = mk_locals vars'; (* TODO: add global vars *)
node_gencalls = [];
node_checks = [];
@@ -346,14 +349,30 @@ struct
)
in
[node]
+
+
+
+ (* TODO
+ C'est pas evident.
+Il faut faire les choses suivantes:
+- rajouter dans un ensemble les variables manipulées localement
+- on doit comprendre comment les variables globales sont injectées dans le modele final:
+ - le node principal doit uniquement les afficher. Il peut les initialiser avec les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.
+ - elles peuvent/doivent etre dans input et output de ce node thetacallD
+ *)
+
let mk_main_loop () =
(* let loc = Location.dummy_loc in *)
let call_stmt =
(* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
- let init = mkexpr
- (LustreSpec.Expr_tuple (List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars)))
+ let init =
+ let init_state_false =
+ List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in
+ let init_globals =
+ List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars in
+ mkexpr (LustreSpec.Expr_tuple (init_state_false @ init_globals))
in
let args = (Corelang.expr_of_vdecl event_var)::
(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
@@ -363,13 +382,16 @@ struct
let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
in
+ let inputs = List.map Corelang.copy_var_decl [event_var] in
+ let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
+ (* TODO add the globals as sout_data_x entry values *)
let node_principal =
Corelang.mktop (
LustreSpec.Node {LustreSpec.node_id = "principal_loop";
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
- node_inputs = List.map Corelang.copy_var_decl [event_var];
- node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars;
+ node_inputs = inputs;
+ node_outputs = outputs;
node_locals = []; (* TODO: add global vars *)
node_gencalls = [];
node_checks = [];
@@ -381,7 +403,7 @@ struct
node_annot = []}
)
in
- node_principal
+ node_principal
let mkprincipal tr =
diff --git a/src/tools/stateflow/sf_sem.ml b/src/tools/stateflow/sf_sem.ml
index 7ca676c0..0f7bd182 100644
--- a/src/tools/stateflow/sf_sem.ml
+++ b/src/tools/stateflow/sf_sem.ml
@@ -63,7 +63,9 @@ let _ =
| GenLus ->
let module Model = (val model) in
let state_vars = Datatype.SF.states Model.model in
- let global_vars = Datatype.SF.global_vars Model.model in
+ let global_vars =
+ List.map (fun (v,e) -> {Basetypes.GlobalVarDef.variable = v; init_val = e;})
+ (Datatype.SF.global_vars Model.model) in
let module T = CPS_lustre_generator.LustrePrinter (struct
let state_vars = state_vars
--
GitLab