Revision 8446bf03 src/tools/stateflow/semantics/cPS_lustre_generator.ml
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 : LustreSpec.statement list; assert_false: bool }


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


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

...  ...  
54  54 
let loc = Location.dummy_loc in 
55  55 
Corelang.mkvar_decl 
56  56 
loc 
57 
(name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None, None (*"__no_parent__" *))


57 
(name, typ, Corelang.mkclock loc 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 LustreSpec.Tydec_bool in


61 
let bool_type = Corelang.mktyp Location.dummy_loc 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) 
...  ...  
72  72 
let mkeq = Corelang.mkeq Location.dummy_loc 
73  73 
let mkexpr = Corelang.mkexpr Location.dummy_loc 
74  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))


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


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


78 
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 
[{LustreSpec.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]


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


90  90 
else 
91  91 
[] 
92  92  
...  ...  
105  105 
let event_type_decl = 
106  106 
Corelang.mktop 
107  107 
( 
108 
LustreSpec.TypeDef {


109 
LustreSpec.tydef_id = "event_type";


110 
tydef_desc = LustreSpec.Tydec_int


108 
Lustre_types.TypeDef {


109 
Lustre_types.tydef_id = "event_type";


110 
tydef_desc = Lustre_types.Tydec_int


111  111 
} 
112  112 
) 
113  113 

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


116 
LustreSpec.ty_dec_loc = Location.dummy_loc;


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


116 
Lustre_types.ty_dec_loc = 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 (LustreSpec.Expr_tuple expr_list) in


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


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

...  ...  
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 (LustreSpec.Expr_tuple expr_list) in


210 
let rhs = mkexpr (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 
LustreSpec.Eq (eq1);


215 
LustreSpec.Eq (eq2);


214 
Lustre_types.Eq (eq1);


215 
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 (LustreSpec.Expr_tuple expr_list) in


226 
let rhs = mkexpr (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 
LustreSpec.Eq (eq1);


231 
LustreSpec.Eq (eq2);


230 
Lustre_types.Eq (eq1);


231 
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 (LustreSpec.Expr_tuple expr_list) in


238 
let rhs = mkexpr (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) = 
...  ...  
251  251 
 Condition.Event e > 
252  252 
mkpredef_call "=" [ 
253  253 
Corelang.expr_of_vdecl event_var; 
254 
mkexpr (LustreSpec.Expr_const (LustreSpec.Const_int (get_event_const e)))


254 
mkexpr (Lustre_types.Expr_const (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 LustreSpec in


262 
let open Lustre_types in


263  263 
let loc = Location.dummy_loc in 
264  264 
(*Format.printf " cond = %a@." Condition.pp_cond condition;*) 
265  265 
let (vars1, tr1) = ok sin sout in 
...  ...  
321  321 
in tr 
322  322 

323  323 
let mkcomponent : 
324 
type c. c call_t > c > t > LustreSpec.program =


324 
type c. c call_t > c > t > Lustre_types.program =


325  325 
fun call args > 
326  326 
fun tr > 
327  327 
reset_loc (); 
...  ...  
332  332 
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in 
333  333 
let node = 
334  334 
Corelang.mktop ( 
335 
LustreSpec.Node {LustreSpec.node_id = funname;


335 
Lustre_types.Node {Lustre_types.node_id = funname;


336  336 
node_type = Types.new_var (); 
337  337 
node_clock = Clocks.new_var true; 
338  338 
node_inputs = inputs; 
...  ...  
372  372 
List.map (fun _ > expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in 
373  373 
let init_globals = 
374  374 
List.map (fun v > v.GlobalVarDef.init_val) Vars.global_vars in 
375 
mkexpr (LustreSpec.Expr_tuple (init_state_false @ init_globals))


375 
mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))


376  376 
in 
377  377 
let args = (Corelang.expr_of_vdecl event_var):: 
378  378 
(vars_to_exprl ~prefix:"sout_" Vars.state_vars) 
379  379 
in 
380  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


381 
let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in


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


383  383 
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs 
384  384 
in 
385  385 
let inputs = List.map Corelang.copy_var_decl [event_var] in 
...  ...  
387  387 
(* TODO add the globals as sout_data_x entry values *) 
388  388 
let node_principal = 
389  389 
Corelang.mktop ( 
390 
LustreSpec.Node {LustreSpec.node_id = "principal_loop";


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


391  391 
node_type = Types.new_var (); 
392  392 
node_clock = Clocks.new_var true; 
393  393 
node_inputs = inputs; 
Also available in: Unified diff