Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/stateflow/semantics/cPS_lustre_generator.ml | ||
---|---|---|
1 | 1 |
open Basetypes |
2 | 2 |
open CPS_transformer |
3 | 3 |
|
4 |
let ff = Format.fprintf |
|
5 |
|
|
6 |
module LustrePrinter ( |
|
7 |
Vars : sig |
|
8 |
val state_vars : ActiveStates.Vars.t |
|
9 |
val global_vars : GlobalVarDef.t list |
|
10 |
|
|
11 |
end) : TransformerType = |
|
12 |
struct |
|
4 |
let ff = Format.fprintf |
|
5 |
|
|
6 |
module LustrePrinter (Vars : sig |
|
7 |
val state_vars : ActiveStates.Vars.t |
|
8 |
|
|
9 |
val global_vars : GlobalVarDef.t list |
|
10 |
end) : TransformerType = struct |
|
13 | 11 |
include TransformerStub |
14 | 12 |
|
15 | 13 |
type name_t = string |
16 |
type t_base = { statements : Lustre_types.statement list; assert_false: bool } |
|
17 |
type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base) |
|
18 | 14 |
|
19 |
|
|
15 |
type t_base = { |
|
16 |
statements : Lustre_types.statement list; |
|
17 |
assert_false : bool; |
|
18 |
} |
|
19 |
|
|
20 |
type t = name_t -> name_t -> ActiveStates.Vars.t * t_base |
|
21 |
|
|
20 | 22 |
let new_loc, reset_loc = |
21 | 23 |
let cpt = ref 0 in |
22 |
((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt), |
|
23 |
(fun () -> cpt := 0)) |
|
24 |
( (fun () -> |
|
25 |
incr cpt; |
|
26 |
Format.sprintf "loc_%i" !cpt), |
|
27 |
fun () -> cpt := 0 ) |
|
24 | 28 |
|
25 | 29 |
let new_aut, _reset_aut = |
26 | 30 |
let cpt = ref 0 in |
27 |
((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt), |
|
28 |
(fun () -> cpt := 0)) |
|
29 |
|
|
31 |
( (fun () -> |
|
32 |
incr cpt; |
|
33 |
Format.sprintf "aut_%i" !cpt), |
|
34 |
fun () -> cpt := 0 ) |
|
35 |
|
|
30 | 36 |
let pp_path prefix fmt path = |
31 |
Format.fprintf fmt "%s%t" |
|
32 |
prefix |
|
33 |
(fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path) |
|
37 |
Format.fprintf fmt "%s%t" prefix (fun fmt -> |
|
38 |
Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path) |
|
34 | 39 |
|
35 | 40 |
(* let pp_typed_path sin fmt path = |
36 | 41 |
* Format.fprintf fmt "%a : bool" (pp_path sin) path *) |
... | ... | |
39 | 44 |
* Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars)) *) |
40 | 45 |
(* let pp_vars_decl sin fmt vars = |
41 | 46 |
* Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars)) *) |
42 |
|
|
47 |
|
|
43 | 48 |
let var_to_ident prefix p = |
44 | 49 |
pp_path prefix Format.str_formatter p; |
45 | 50 |
Format.flush_str_formatter () |
46 | 51 |
|
47 |
let vars_to_ident_list ?(prefix="") vars = |
|
48 |
List.map ( |
|
49 |
fun p -> var_to_ident prefix p |
|
50 |
) (ActiveStates.Vars.elements vars) |
|
52 |
let vars_to_ident_list ?(prefix = "") vars = |
|
53 |
List.map (fun p -> var_to_ident prefix p) (ActiveStates.Vars.elements vars) |
|
51 | 54 |
|
52 |
let mkvar name typ =
|
|
55 |
let mkvar name typ = |
|
53 | 56 |
let loc = Location.dummy_loc in |
54 |
Corelang.mkvar_decl |
|
55 |
loc |
|
56 |
(name, typ, Corelang.mkclock loc Lustre_types.Ckdec_any, false, None, None (*"__no_parent__" *)) |
|
57 |
Corelang.mkvar_decl loc |
|
58 |
( name, |
|
59 |
typ, |
|
60 |
Corelang.mkclock loc Lustre_types.Ckdec_any, |
|
61 |
false, |
|
62 |
None, |
|
63 |
None (*"__no_parent__" *) ) |
|
64 |
|
|
65 |
let var_to_vdecl ?(prefix = "") var typ = mkvar (var_to_ident prefix var) typ |
|
57 | 66 |
|
58 |
let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ |
|
59 |
let state_vars_to_vdecl_list ?(prefix="") vars = |
|
67 |
let state_vars_to_vdecl_list ?(prefix = "") vars = |
|
60 | 68 |
let bool_type = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_bool in |
61 |
List.map
|
|
62 |
(fun v -> var_to_vdecl ~prefix:prefix v bool_type)
|
|
69 |
List.map |
|
70 |
(fun v -> var_to_vdecl ~prefix v bool_type) |
|
63 | 71 |
(ActiveStates.Vars.elements vars) |
64 | 72 |
|
65 | 73 |
let mk_locals locs = |
66 |
ActiveStates.Vars.fold (fun v accu -> |
|
67 |
(state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars)@accu |
|
68 |
) locs [] |
|
69 |
(* TODO: declare global vars *) |
|
74 |
ActiveStates.Vars.fold |
|
75 |
(fun v accu -> |
|
76 |
state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars @ accu) |
|
77 |
locs [] |
|
78 |
(* TODO: declare global vars *) |
|
70 | 79 |
|
71 | 80 |
let mkeq = Corelang.mkeq Location.dummy_loc |
81 |
|
|
72 | 82 |
let mkexpr = Corelang.mkexpr Location.dummy_loc |
83 |
|
|
73 | 84 |
let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc |
74 |
let expr_of_bool b = mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b)) |
|
75 |
let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs = |
|
76 |
{ statements = [ |
|
77 |
Lustre_types.Eq ( |
|
78 |
mkeq ( |
|
79 |
vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *) |
|
80 |
rhs (* rhs *) |
|
81 |
) |
|
82 |
) |
|
83 |
]; |
|
84 |
assert_false = false |
|
85 |
|
|
86 |
let expr_of_bool b = |
|
87 |
mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b)) |
|
88 |
|
|
89 |
let mkstmt_eq lhs_vars ?(prefix_lhs = "") rhs = |
|
90 |
{ |
|
91 |
statements = |
|
92 |
[ |
|
93 |
Lustre_types.Eq |
|
94 |
(mkeq |
|
95 |
( vars_to_ident_list ~prefix:prefix_lhs lhs_vars, |
|
96 |
(* lhs *) |
|
97 |
rhs (* rhs *) )); |
|
98 |
]; |
|
99 |
assert_false = false; |
|
85 | 100 |
} |
101 |
|
|
86 | 102 |
let base_to_assert b = |
87 | 103 |
if b.assert_false then |
88 |
[{Lustre_types.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}] |
|
89 |
else |
|
90 |
[] |
|
104 |
[ |
|
105 |
{ |
|
106 |
Lustre_types.assert_expr = expr_of_bool false; |
|
107 |
assert_loc = Location.dummy_loc; |
|
108 |
}; |
|
109 |
] |
|
110 |
else [] |
|
91 | 111 |
|
92 |
|
|
93 |
let var_to_expr ?(prefix="") p = |
|
112 |
let var_to_expr ?(prefix = "") p = |
|
94 | 113 |
let id = var_to_ident prefix p in |
95 | 114 |
Corelang.expr_of_ident id Location.dummy_loc |
96 | 115 |
|
97 |
let vars_to_exprl ?(prefix="") vars = |
|
98 |
List.map |
|
99 |
(fun p -> var_to_expr ~prefix:prefix p) |
|
100 |
(ActiveStates.Vars.elements vars) |
|
101 |
|
|
116 |
let vars_to_exprl ?(prefix = "") vars = |
|
117 |
List.map (fun p -> var_to_expr ~prefix p) (ActiveStates.Vars.elements vars) |
|
102 | 118 |
|
103 | 119 |
(* Events *) |
104 | 120 |
let event_type_decl = |
105 | 121 |
Corelang.mktop |
106 |
( |
|
107 |
Lustre_types.TypeDef { |
|
108 |
Lustre_types.tydef_id = "event_type"; |
|
109 |
tydef_desc = Lustre_types.Tydec_int |
|
110 |
} |
|
111 |
) |
|
112 |
|
|
113 |
let event_type = { |
|
114 |
Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type"; |
|
115 |
Lustre_types.ty_dec_loc = Location.dummy_loc; |
|
116 |
} |
|
117 |
|
|
118 |
let event_var = mkvar "event" event_type |
|
122 |
(Lustre_types.TypeDef |
|
123 |
{ |
|
124 |
Lustre_types.tydef_id = "event_type"; |
|
125 |
tydef_desc = Lustre_types.Tydec_int; |
|
126 |
}) |
|
119 | 127 |
|
128 |
let event_type = |
|
129 |
{ |
|
130 |
Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type"; |
|
131 |
Lustre_types.ty_dec_loc = Location.dummy_loc; |
|
132 |
} |
|
133 |
|
|
134 |
let event_var = mkvar "event" event_type |
|
120 | 135 |
|
121 | 136 |
let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13 |
137 |
|
|
122 | 138 |
let get_event_const e = |
123 | 139 |
try Hashtbl.find const_map e |
124 |
with Not_found -> (
|
|
140 |
with Not_found -> |
|
125 | 141 |
let nb = Hashtbl.length const_map in |
126 | 142 |
Hashtbl.add const_map e nb; |
127 |
nb |
|
128 |
) |
|
143 |
nb |
|
129 | 144 |
|
130 |
|
|
131 |
|
|
132 | 145 |
let null sin sout = |
133 | 146 |
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in |
134 |
ActiveStates.Vars.empty, |
|
135 |
( |
|
147 |
( ActiveStates.Vars.empty, |
|
136 | 148 |
(* Nothing happen here: out_vars = in_vars *) |
137 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
138 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
|
139 |
) |
|
140 |
|
|
149 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
150 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs ) |
|
151 |
|
|
141 | 152 |
let bot sin sout = |
142 | 153 |
let _, tr = null sin sout in |
143 |
( |
|
144 |
ActiveStates.Vars.empty, |
|
145 |
{ tr with assert_false = true } |
|
146 |
) |
|
147 |
|
|
154 |
ActiveStates.Vars.empty, { tr with assert_false = true } |
|
155 |
|
|
148 | 156 |
let ( >> ) tr1 tr2 sin sout = |
149 | 157 |
let l = new_loc () in |
150 | 158 |
let vars1, tr1 = tr1 sin l in |
151 | 159 |
let vars2, tr2 = tr2 l sout in |
152 |
(ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2), |
|
153 |
{ |
|
154 |
statements = tr1.statements @ tr2.statements; |
|
155 |
assert_false = tr1.assert_false || tr2.assert_false |
|
156 |
} |
|
157 |
) |
|
158 |
|
|
159 |
let pp_name : |
|
160 |
type c. c call_t -> c -> unit = |
|
161 |
fun call -> |
|
162 |
match call with |
|
163 |
| Ecall -> (fun (p, p', f) -> |
|
164 |
Format.fprintf Format.str_formatter "theta%a%a%a_%a" |
|
165 |
pp_call call |
|
166 |
(pp_path "_from_") p |
|
167 |
(pp_path "_to_") p' |
|
168 |
pp_frontier f) |
|
169 |
| Dcall -> (fun p -> |
|
170 |
Format.fprintf Format.str_formatter "theta%a%a" |
|
171 |
pp_call call |
|
172 |
(pp_path "_from_") p) |
|
173 |
| Xcall -> (fun (p, f) -> |
|
174 |
Format.fprintf Format.str_formatter "theta%a%a_%a" |
|
175 |
pp_call call |
|
176 |
(pp_path "_from_") p |
|
177 |
pp_frontier f) |
|
178 |
|
|
179 |
|
|
180 |
let mkcall' : |
|
181 |
type c. name_t -> name_t -> c call_t -> c -> t_base = |
|
182 |
fun sin sout call arg -> |
|
183 |
pp_name call arg; |
|
184 |
let funname = Format.flush_str_formatter () in |
|
185 |
let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in |
|
186 |
let rhs = mkpredef_call funname args in |
|
187 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
|
188 |
|
|
160 |
( ActiveStates.Vars.add [ l ] (ActiveStates.Vars.union vars1 vars2), |
|
161 |
{ |
|
162 |
statements = tr1.statements @ tr2.statements; |
|
163 |
assert_false = tr1.assert_false || tr2.assert_false; |
|
164 |
} ) |
|
165 |
|
|
166 |
let pp_name : type c. c call_t -> c -> unit = |
|
167 |
fun call -> |
|
168 |
match call with |
|
169 |
| Ecall -> |
|
170 |
fun (p, p', f) -> |
|
171 |
Format.fprintf Format.str_formatter "theta%a%a%a_%a" pp_call call |
|
172 |
(pp_path "_from_") p (pp_path "_to_") p' pp_frontier f |
|
173 |
| Dcall -> |
|
174 |
fun p -> |
|
175 |
Format.fprintf Format.str_formatter "theta%a%a" pp_call call |
|
176 |
(pp_path "_from_") p |
|
177 |
| Xcall -> |
|
178 |
fun (p, f) -> |
|
179 |
Format.fprintf Format.str_formatter "theta%a%a_%a" pp_call call |
|
180 |
(pp_path "_from_") p pp_frontier f |
|
181 |
|
|
182 |
let mkcall' : type c. name_t -> name_t -> c call_t -> c -> t_base = |
|
183 |
fun sin sout call arg -> |
|
184 |
pp_name call arg; |
|
185 |
let funname = Format.flush_str_formatter () in |
|
186 |
let args = |
|
187 |
Corelang.expr_of_vdecl event_var |
|
188 |
:: vars_to_exprl ~prefix:sin Vars.state_vars |
|
189 |
in |
|
190 |
let rhs = mkpredef_call funname args in |
|
191 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
|
192 |
|
|
189 | 193 |
let mkact' action sin sout = |
190 | 194 |
match action with |
191 |
| Action.Call (c, a) -> mkcall' sin sout c a |
|
192 |
| Action.Quote a -> |
|
193 |
(* TODO: check. This seems to be innappropriate *) |
|
194 |
(* let funname = "action_" ^ a.ident in |
|
195 |
let args = vars_to_exprl ~prefix:sin Vars.state_vars in |
|
196 |
let rhs = mkpredef_call funname args in |
|
197 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
|
198 |
*) |
|
199 |
{ |
|
200 |
statements = a.defs; |
|
201 |
assert_false = false |
|
202 |
} |
|
203 |
| Action.Open p -> |
|
204 |
let vars' = ActiveStates.Vars.remove p Vars.state_vars in |
|
205 |
(* eq1: sout_p = true *) |
|
206 |
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in |
|
207 |
(* eq2: sout_xx = sin_xx *) |
|
208 |
let expr_list = vars_to_exprl ~prefix:sin vars' in |
|
209 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
210 |
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in |
|
211 |
{ |
|
212 |
statements = [ |
|
213 |
Lustre_types.Eq (eq1); |
|
214 |
Lustre_types.Eq (eq2); |
|
215 |
]; |
|
216 |
assert_false = false |
|
217 |
} |
|
218 |
|
|
219 |
| Action.Close p -> |
|
220 |
let vars' = ActiveStates.Vars.remove p Vars.state_vars in |
|
221 |
(* eq1: sout_p = false *) |
|
222 |
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in |
|
223 |
(* eq2: sout_xx = sin_xx *) |
|
224 |
let expr_list = vars_to_exprl ~prefix:sin vars' in |
|
225 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
226 |
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in |
|
227 |
{ |
|
228 |
statements = [ |
|
229 |
Lustre_types.Eq (eq1); |
|
230 |
Lustre_types.Eq (eq2); |
|
231 |
]; |
|
232 |
assert_false = false |
|
233 |
} |
|
234 |
|
|
235 |
| Action.Nil -> |
|
236 |
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in |
|
237 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
238 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
|
239 |
|
|
240 |
let eval_act _kenv (action : act_t) = |
|
241 |
(*Format.printf "----- action = %a@." Action.pp_act action;*) |
|
242 |
(fun sin sout -> (ActiveStates.Vars.empty, |
|
243 |
mkact' action sin sout )) |
|
195 |
| Action.Call (c, a) -> |
|
196 |
mkcall' sin sout c a |
|
197 |
| Action.Quote a -> |
|
198 |
(* TODO: check. This seems to be innappropriate *) |
|
199 |
(* let funname = "action_" ^ a.ident in let args = vars_to_exprl |
|
200 |
~prefix:sin Vars.state_vars in let rhs = mkpredef_call funname args in |
|
201 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs *) |
|
202 |
{ statements = a.defs; assert_false = false } |
|
203 |
| Action.Open p -> |
|
204 |
let vars' = ActiveStates.Vars.remove p Vars.state_vars in |
|
205 |
(* eq1: sout_p = true *) |
|
206 |
let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool true) in |
|
207 |
(* eq2: sout_xx = sin_xx *) |
|
208 |
let expr_list = vars_to_exprl ~prefix:sin vars' in |
|
209 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
210 |
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in |
|
211 |
{ |
|
212 |
statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ]; |
|
213 |
assert_false = false; |
|
214 |
} |
|
215 |
| Action.Close p -> |
|
216 |
let vars' = ActiveStates.Vars.remove p Vars.state_vars in |
|
217 |
(* eq1: sout_p = false *) |
|
218 |
let eq1 = mkeq ([ var_to_ident sout p ], expr_of_bool false) in |
|
219 |
(* eq2: sout_xx = sin_xx *) |
|
220 |
let expr_list = vars_to_exprl ~prefix:sin vars' in |
|
221 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
222 |
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in |
|
223 |
{ |
|
224 |
statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ]; |
|
225 |
assert_false = false; |
|
226 |
} |
|
227 |
| Action.Nil -> |
|
228 |
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in |
|
229 |
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in |
|
230 |
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs |
|
231 |
|
|
232 |
let eval_act _kenv (action : act_t) |
|
233 |
(*Format.printf "----- action = %a@." Action.pp_act action;*) |
|
234 |
sin sout = |
|
235 |
ActiveStates.Vars.empty, mkact' action sin sout |
|
244 | 236 |
|
245 | 237 |
let rec mkcond' sin condition = |
246 | 238 |
(*Format.printf "----- cond = %a@." Condition.pp_cond condition;*) |
247 | 239 |
match condition with |
248 |
| Condition.True -> expr_of_bool true |
|
249 |
| Condition.Active p -> var_to_expr ~prefix:sin p |
|
250 |
| Condition.Event e -> |
|
251 |
mkpredef_call "=" [ |
|
252 |
Corelang.expr_of_vdecl event_var; |
|
253 |
mkexpr (Lustre_types.Expr_const (Lustre_types.Const_int (get_event_const e))) |
|
254 |
] |
|
255 |
| Condition.Neg cond -> mkpredef_call "not" [mkcond' sin cond] |
|
256 |
| Condition.And (cond1, cond2) -> mkpredef_call "&&" [mkcond' sin cond1; |
|
257 |
mkcond' sin cond2] |
|
258 |
| Condition.Quote c -> c.expr (* TODO: shall we prefix with sin ? *) |
|
259 |
|
|
260 |
let eval_cond condition (ok:t) ko sin sout = |
|
240 |
| Condition.True -> |
|
241 |
expr_of_bool true |
|
242 |
| Condition.Active p -> |
|
243 |
var_to_expr ~prefix:sin p |
|
244 |
| Condition.Event e -> |
|
245 |
mkpredef_call "=" |
|
246 |
[ |
|
247 |
Corelang.expr_of_vdecl event_var; |
|
248 |
mkexpr |
|
249 |
(Lustre_types.Expr_const |
|
250 |
(Lustre_types.Const_int (get_event_const e))); |
|
251 |
] |
|
252 |
| Condition.Neg cond -> |
|
253 |
mkpredef_call "not" [ mkcond' sin cond ] |
|
254 |
| Condition.And (cond1, cond2) -> |
|
255 |
mkpredef_call "&&" [ mkcond' sin cond1; mkcond' sin cond2 ] |
|
256 |
| Condition.Quote c -> |
|
257 |
c.expr |
|
258 |
(* TODO: shall we prefix with sin ? *) |
|
259 |
|
|
260 |
let eval_cond condition (ok : t) ko sin sout = |
|
261 | 261 |
let open Lustre_types in |
262 | 262 |
let loc = Location.dummy_loc in |
263 | 263 |
(*Format.printf "----- cond = %a@." Condition.pp_cond condition;*) |
... | ... | |
265 | 265 |
let vars2, tr2 = ko sin sout in |
266 | 266 |
let _, tr0 = bot sin sout in |
267 | 267 |
let aut = new_aut () in |
268 |
(ActiveStates.Vars.empty, |
|
269 |
{ |
|
270 |
statements = [ |
|
271 |
let handler_default_mode = (* Default mode : CenterPoint *) |
|
272 |
let handler_default_mode_unless = [ |
|
273 |
(loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut); |
|
274 |
(loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut); |
|
275 |
] |
|
276 |
in |
|
277 |
Automata.mkhandler |
|
278 |
loc (* location *) |
|
279 |
("CenterPoint_" ^ aut) (* state name *) |
|
280 |
handler_default_mode_unless (* unless *) |
|
281 |
[] (* until *) |
|
282 |
[] (* locals *) |
|
283 |
(tr0.statements, base_to_assert tr0, []) (* stmts, asserts, annots *) |
|
284 |
in |
|
285 |
let handler_cond_mode = (* Cond mode *) |
|
286 |
let handler_cond_mode_until = [ |
|
287 |
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); |
|
288 |
] |
|
289 |
in |
|
290 |
Automata.mkhandler |
|
291 |
loc (* location *) |
|
292 |
("Cond_" ^ aut) (* state name *) |
|
293 |
[] (* unless *) |
|
294 |
handler_cond_mode_until (* until *) |
|
295 |
(mk_locals vars1) (* locals *) |
|
296 |
(tr1.statements, base_to_assert tr1, []) (* stmts, asserts, annots *) |
|
297 |
in |
|
298 |
let handler_notcond_mode = (* NotCond mode *) |
|
299 |
let handler_notcond_mode_until = [ |
|
300 |
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); |
|
301 |
] |
|
302 |
in |
|
303 |
Automata.mkhandler |
|
304 |
loc (* location *) |
|
305 |
("NotCond_" ^ aut) (* state name *) |
|
306 |
[] (* unless *) |
|
307 |
handler_notcond_mode_until (* until *) |
|
308 |
(mk_locals vars2) (* locals *) |
|
309 |
(tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *) |
|
310 |
in |
|
311 |
let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in |
|
312 |
Aut (Automata.mkautomata loc aut handlers) |
|
313 |
]; |
|
314 |
assert_false = false |
|
315 |
} |
|
316 |
) |
|
317 |
|
|
268 |
( ActiveStates.Vars.empty, |
|
269 |
{ |
|
270 |
statements = |
|
271 |
[ |
|
272 |
(let handler_default_mode = |
|
273 |
(* Default mode : CenterPoint *) |
|
274 |
let handler_default_mode_unless = |
|
275 |
[ |
|
276 |
loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut; |
|
277 |
( loc, |
|
278 |
mkcond' sin (Condition.Neg condition), |
|
279 |
true (* restart *), |
|
280 |
"NotCond_" ^ aut ); |
|
281 |
] |
|
282 |
in |
|
283 |
Automata.mkhandler loc |
|
284 |
(* location *) |
|
285 |
("CenterPoint_" ^ aut) |
|
286 |
(* state name *) |
|
287 |
handler_default_mode_unless (* unless *) [] (* until *) [] |
|
288 |
(* locals *) |
|
289 |
(tr0.statements, base_to_assert tr0, []) |
|
290 |
(* stmts, asserts, annots *) |
|
291 |
in |
|
292 |
let handler_cond_mode = |
|
293 |
(* Cond mode *) |
|
294 |
let handler_cond_mode_until = |
|
295 |
[ |
|
296 |
( loc, |
|
297 |
expr_of_bool true, |
|
298 |
true (* restart *), |
|
299 |
"CenterPoint_" ^ aut ); |
|
300 |
] |
|
301 |
in |
|
302 |
Automata.mkhandler loc |
|
303 |
(* location *) |
|
304 |
("Cond_" ^ aut) |
|
305 |
(* state name *) |
|
306 |
[] (* unless *) handler_cond_mode_until |
|
307 |
(* until *) |
|
308 |
(mk_locals vars1) |
|
309 |
(* locals *) |
|
310 |
(tr1.statements, base_to_assert tr1, []) |
|
311 |
(* stmts, asserts, annots *) |
|
312 |
in |
|
313 |
let handler_notcond_mode = |
|
314 |
(* NotCond mode *) |
|
315 |
let handler_notcond_mode_until = |
|
316 |
[ |
|
317 |
( loc, |
|
318 |
expr_of_bool true, |
|
319 |
true (* restart *), |
|
320 |
"CenterPoint_" ^ aut ); |
|
321 |
] |
|
322 |
in |
|
323 |
Automata.mkhandler loc |
|
324 |
(* location *) |
|
325 |
("NotCond_" ^ aut) |
|
326 |
(* state name *) |
|
327 |
[] (* unless *) handler_notcond_mode_until |
|
328 |
(* until *) |
|
329 |
(mk_locals vars2) |
|
330 |
(* locals *) |
|
331 |
(tr2.statements, base_to_assert tr2, []) |
|
332 |
(* stmts, asserts, annots *) |
|
333 |
in |
|
334 |
let handlers = |
|
335 |
[ handler_default_mode; handler_cond_mode; handler_notcond_mode ] |
|
336 |
in |
|
337 |
Aut (Automata.mkautomata loc aut handlers)); |
|
338 |
]; |
|
339 |
assert_false = false; |
|
340 |
} ) |
|
341 |
|
|
318 | 342 |
(* let mktransformer tr = |
319 | 343 |
* let _, tr = tr "sin_" "sout_" |
320 |
* in tr *) |
|
321 |
|
|
322 |
let mkcomponent : |
|
323 |
type c. c call_t -> c -> t -> Lustre_types.program_t = |
|
324 |
fun call args -> |
|
325 |
fun tr -> |
|
326 |
reset_loc (); |
|
327 |
let (vars', tr') = tr "sin_" "sout_" in |
|
328 |
pp_name call args; |
|
329 |
let funname = Format.flush_str_formatter () in |
|
330 |
let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in |
|
331 |
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in |
|
332 |
let node = |
|
333 |
Corelang.mktop ( |
|
334 |
Lustre_types.Node {Lustre_types.node_id = funname; |
|
335 |
node_type = Types.new_var (); |
|
336 |
node_clock = Clocks.new_var true; |
|
337 |
node_inputs = inputs; |
|
338 |
node_outputs = outputs; |
|
339 |
node_locals = mk_locals vars'; (* TODO: add global vars *) |
|
340 |
node_gencalls = []; |
|
341 |
node_checks = []; |
|
342 |
node_stmts = tr'.statements; |
|
343 |
node_asserts = base_to_assert tr'; |
|
344 |
node_dec_stateless = false; |
|
345 |
node_stateless = None; |
|
346 |
node_spec = None; |
|
347 |
node_annot = []; |
|
348 |
node_iscontract = false} |
|
349 |
) |
|
350 |
in |
|
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 |
|
|
364 |
|
|
344 |
* in tr *) |
|
345 |
|
|
346 |
let mkcomponent : type c. c call_t -> c -> t -> Lustre_types.program_t = |
|
347 |
fun call args tr -> |
|
348 |
reset_loc (); |
|
349 |
let vars', tr' = tr "sin_" "sout_" in |
|
350 |
pp_name call args; |
|
351 |
let funname = Format.flush_str_formatter () in |
|
352 |
let inputs = |
|
353 |
event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars |
|
354 |
in |
|
355 |
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in |
|
356 |
let node = |
|
357 |
Corelang.mktop |
|
358 |
(Lustre_types.Node |
|
359 |
{ |
|
360 |
Lustre_types.node_id = funname; |
|
361 |
node_type = Types.new_var (); |
|
362 |
node_clock = Clocks.new_var true; |
|
363 |
node_inputs = inputs; |
|
364 |
node_outputs = outputs; |
|
365 |
node_locals = mk_locals vars'; |
|
366 |
(* TODO: add global vars *) |
|
367 |
node_gencalls = []; |
|
368 |
node_checks = []; |
|
369 |
node_stmts = tr'.statements; |
|
370 |
node_asserts = base_to_assert tr'; |
|
371 |
node_dec_stateless = false; |
|
372 |
node_stateless = None; |
|
373 |
node_spec = None; |
|
374 |
node_annot = []; |
|
375 |
node_iscontract = false; |
|
376 |
}) |
|
377 |
in |
|
378 |
[ node ] |
|
379 |
|
|
380 |
(* TODO C'est pas evident. Il faut faire les choses suivantes: - rajouter dans |
|
381 |
un ensemble les variables manipulées localement - on doit comprendre |
|
382 |
comment les variables globales sont injectées dans le modele final: - le |
|
383 |
node principal doit uniquement les afficher. Il peut les initialiser avec |
|
384 |
les valeurs init définies. Puis appeller la fcn thetacallD_from_principal. |
|
385 |
- elles peuvent/doivent etre dans input et output de ce node thetacallD *) |
|
386 |
|
|
365 | 387 |
let mk_main_loop () = |
366 | 388 |
(* let loc = Location.dummy_loc in *) |
367 |
|
|
368 | 389 |
let call_stmt = |
369 | 390 |
(* (%t) -> pre (thetaCallD_from_principal (event, %a)) *) |
370 | 391 |
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 (Lustre_types.Expr_tuple (init_state_false @ init_globals)) |
|
392 |
let init_state_false = |
|
393 |
List.map |
|
394 |
(fun _ -> expr_of_bool false) |
|
395 |
(ActiveStates.Vars.elements Vars.state_vars) |
|
396 |
in |
|
397 |
let init_globals = |
|
398 |
List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars |
|
399 |
in |
|
400 |
mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals)) |
|
376 | 401 |
in |
377 |
let args = (Corelang.expr_of_vdecl event_var):: |
|
378 |
(vars_to_exprl ~prefix:"sout_" Vars.state_vars) |
|
402 |
let args = |
|
403 |
Corelang.expr_of_vdecl event_var |
|
404 |
:: vars_to_exprl ~prefix:"sout_" Vars.state_vars |
|
379 | 405 |
in |
380 | 406 |
let call_expr = mkpredef_call "thetaCallD_from_principal" args in |
381 |
let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in
|
|
407 |
let pre_call_expr = mkexpr (Lustre_types.Expr_pre call_expr) in
|
|
382 | 408 |
let rhs = mkexpr (Lustre_types.Expr_arrow (init, pre_call_expr)) in |
383 | 409 |
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs |
384 | 410 |
in |
385 |
let inputs = List.map Corelang.copy_var_decl [event_var] in
|
|
411 |
let inputs = List.map Corelang.copy_var_decl [ event_var ] in
|
|
386 | 412 |
let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in |
387 | 413 |
(* TODO add the globals as sout_data_x entry values *) |
388 | 414 |
let node_principal = |
389 |
Corelang.mktop ( |
|
390 |
Lustre_types.Node {Lustre_types.node_id = "principal_loop"; |
|
391 |
node_type = Types.new_var (); |
|
392 |
node_clock = Clocks.new_var true; |
|
393 |
node_inputs = inputs; |
|
394 |
node_outputs = outputs; |
|
395 |
node_locals = []; (* TODO: add global vars *) |
|
396 |
node_gencalls = []; |
|
397 |
node_checks = []; |
|
398 |
node_asserts = base_to_assert call_stmt; |
|
399 |
node_stmts = call_stmt.statements; |
|
400 |
node_dec_stateless = false; |
|
401 |
node_stateless = None; |
|
402 |
node_spec = None; |
|
403 |
node_annot = []; |
|
404 |
node_iscontract = false;} |
|
405 |
) |
|
415 |
Corelang.mktop |
|
416 |
(Lustre_types.Node |
|
417 |
{ |
|
418 |
Lustre_types.node_id = "principal_loop"; |
|
419 |
node_type = Types.new_var (); |
|
420 |
node_clock = Clocks.new_var true; |
|
421 |
node_inputs = inputs; |
|
422 |
node_outputs = outputs; |
|
423 |
node_locals = []; |
|
424 |
(* TODO: add global vars *) |
|
425 |
node_gencalls = []; |
|
426 |
node_checks = []; |
|
427 |
node_asserts = base_to_assert call_stmt; |
|
428 |
node_stmts = call_stmt.statements; |
|
429 |
node_dec_stateless = false; |
|
430 |
node_stateless = None; |
|
431 |
node_spec = None; |
|
432 |
node_annot = []; |
|
433 |
node_iscontract = false; |
|
434 |
}) |
|
406 | 435 |
in |
407 | 436 |
node_principal |
408 |
|
|
409 | 437 |
|
410 | 438 |
let mkprincipal tr = |
411 |
event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()]
|
|
412 |
|
|
439 |
event_type_decl :: mkcomponent Dcall [ "principal" ] tr
|
|
440 |
@ [ mk_main_loop () ] |
|
413 | 441 |
end |
414 | 442 |
|
415 | 443 |
(* Local Variables: *) |
Also available in: Unified diff
reformatting