lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 74ca6b61
History  View  Annotate  Download (11.7 KB)
1 
open Basetypes 

2 
open ActiveStates 
3 
open CPS_transformer 
4  
5 
let ff = Format.fprintf 
6 

7 
module LustrePrinter ( 
8 
Vars : sig 
9 
val state_vars : ActiveStates.Vars.t 
10 
val global_vars : LustreSpec.var_decl list 
11 
end) : TransformerType = 
12 
struct 
13 
include TransformerStub 
14  
15 
type name_t = string 
16 
type t_base = { statements : LustreSpec.statement list; assert_false: bool } 
17 
type t = name_t > name_t > (ActiveStates.Vars.t * t_base) 
18  
19 

20 
let new_loc, reset_loc = 
21 
let cpt = ref 0 in 
22 
((fun () > incr cpt; Format.sprintf "loc_%i" !cpt), 
23 
(fun () > cpt := 0)) 
24  
25 
let new_aut, reset_aut = 
26 
let cpt = ref 0 in 
27 
((fun () > incr cpt; Format.sprintf "aut_%i" !cpt), 
28 
(fun () > cpt := 0)) 
29 

30 
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) 
34  
35 
let pp_typed_path sin fmt path = 
36 
Format.fprintf fmt "%a : bool" (pp_path sin) path 
37  
38 
let pp_vars sin fmt vars = 
39 
Format.fprintf fmt "%t" (fun fmt > Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars)) 
40 
let pp_vars_decl sin fmt vars = 
41 
Format.fprintf fmt "%t" (fun fmt > Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars)) 
42 

43 
let var_to_ident prefix p = 
44 
pp_path prefix Format.str_formatter p; 
45 
Format.flush_str_formatter () 
46  
47 
let vars_to_ident_list ?(prefix="") vars = 
48 
List.map ( 
49 
fun p > var_to_ident prefix p 
50 
) (ActiveStates.Vars.elements vars) 
51  
52 
let mkvar name typ = 
53 
let loc = Location.dummy_loc in 
54 
Corelang.mkvar_decl 
55 
loc 
56 
(name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None) 
57  
58 
let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
59 
let state_vars_to_vdecl_list ?(prefix="") vars = 
60 
let bool_type = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_bool in 
61 
List.map 
62 
(fun v > var_to_vdecl ~prefix:prefix v bool_type) 
63 
(ActiveStates.Vars.elements vars) 
64  
65 
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 *) 
70  
71 
let mkeq = Corelang.mkeq Location.dummy_loc 
72 
let mkexpr = Corelang.mkexpr Location.dummy_loc 
73 
let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc 
74 
let expr_of_bool b = mkexpr (LustreSpec.Expr_const (Corelang.const_of_bool b)) 
75 
let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs = 
76 
{ statements = [ 
77 
LustreSpec.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 base_to_assert b = 
87 
if b.assert_false then 
88 
[{LustreSpec.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}] 
89 
else 
90 
[] 
91  
92 

93 
let var_to_expr ?(prefix="") p = 
94 
let id = var_to_ident prefix p in 
95 
Corelang.expr_of_ident id Location.dummy_loc 
96  
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  
102  
103 
(* Events *) 
104 
let event_type_decl = 
105 
Corelang.mktop 
106 
( 
107 
LustreSpec.TypeDef { 
108 
LustreSpec.tydef_id = "event_type"; 
109 
tydef_desc = LustreSpec.Tydec_int 
110 
} 
111 
) 
112 

113 
let event_type = { 
114 
LustreSpec.ty_dec_desc = LustreSpec.Tydec_const "event_type"; 
115 
LustreSpec.ty_dec_loc = Location.dummy_loc; 
116 
} 
117 

118 
let event_var = mkvar "event" event_type 
119  
120  
121 
let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13 
122 
let get_event_const e = 
123 
try Hashtbl.find const_map e 
124 
with Not_found > ( 
125 
let nb = Hashtbl.length const_map in 
126 
Hashtbl.add const_map e nb; 
127 
nb 
128 
) 
129  
130  
131 

132 
let null sin sout = 
133 
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in 
134 
ActiveStates.Vars.empty, 
135 
( 
136 
(* Nothing happen here: out_vars = in_vars *) 
137 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
138 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
139 
) 
140 

141 
let bot sin sout = 
142 
let (vars, tr) = null sin sout in 
143 
( 
144 
ActiveStates.Vars.empty, 
145 
{ tr with assert_false = true } 
146 
) 
147 

148 
let ( >> ) tr1 tr2 sin sout = 
149 
let l = new_loc () in 
150 
let (vars1, tr1) = tr1 sin l in 
151 
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 

189 
let mkact' action sin sout = 
190 
match action with 
191 
 Action.Call (c, a) > mkcall' sin sout c a 
192 
 Action.Quote a > 
193 
let funname = "action_" ^ a.ident in 
194 
let args = vars_to_exprl ~prefix:sin Vars.state_vars in 
195 
let rhs = mkpredef_call funname args in 
196 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
197 
 Action.Open p > 
198 
let vars' = ActiveStates.Vars.remove p Vars.state_vars in 
199 
(* eq1: sout_p = true *) 
200 
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in 
201 
(* eq2: sout_xx = sin_xx *) 
202 
let expr_list = vars_to_exprl ~prefix:sin vars' in 
203 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
204 
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in 
205 
{ 
206 
statements = [ 
207 
LustreSpec.Eq (eq1); 
208 
LustreSpec.Eq (eq2); 
209 
]; 
210 
assert_false = false 
211 
} 
212 

213 
 Action.Close p > 
214 
let vars' = ActiveStates.Vars.remove p Vars.state_vars in 
215 
(* eq1: sout_p = false *) 
216 
let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in 
217 
(* eq2: sout_xx = sin_xx *) 
218 
let expr_list = vars_to_exprl ~prefix:sin vars' in 
219 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
220 
let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in 
221 
{ 
222 
statements = [ 
223 
LustreSpec.Eq (eq1); 
224 
LustreSpec.Eq (eq2); 
225 
]; 
226 
assert_false = false 
227 
} 
228  
229 
 Action.Nil > 
230 
let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in 
231 
let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
232 
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs 
233 

234 
let eval_act kenv (action : act_t) = 
235 
(*Format.printf " action = %a@." Action.pp_act action;*) 
236 
(fun sin sout > (ActiveStates.Vars.empty, 
237 
mkact' action sin sout )) 
238 

239 
let rec mkcond' sin condition = 
240 
(*Format.printf " cond = %a@." Condition.pp_cond condition;*) 
241 
match condition with 
242 
 Condition.True > expr_of_bool true 
243 
 Condition.Active p > var_to_expr ~prefix:sin p 
244 
 Condition.Event e > 
245 
mkpredef_call "=" [ 
246 
Corelang.expr_of_vdecl event_var; 
247 
mkexpr (LustreSpec.Expr_const (LustreSpec.Const_int (get_event_const e))) 
248 
] 
249 
 Condition.Neg cond > mkpredef_call "not" [mkcond' sin cond] 
250 
 Condition.And (cond1, cond2) > mkpredef_call "&&" [mkcond' sin cond1; 
251 
mkcond' sin cond2] 
252 
 Condition.Quote c > c (* TODO: shall we prefix with sin ? *) 
253  
254 
let rec eval_cond condition (ok:t) ko sin sout = 
255 
let open LustreSpec in 
256 
let loc = Location.dummy_loc in 
257 
(*Format.printf " cond = %a@." Condition.pp_cond condition;*) 
258 
let (vars1, tr1) = ok sin sout in 
259 
let (vars2, tr2) = ko sin sout in 
260 
let (vars0, tr0) = bot sin sout in 
261 
let aut = new_aut () in 
262 
(ActiveStates.Vars.empty, 
263 
{ 
264 
statements = [ 
265 
Aut ( 
266 
{ aut_id = aut; 
267 
aut_loc = loc; 
268 
aut_handlers = 
269 
[ 
270 
(* Default mode : CenterPoint *) 
271 
{ hand_state = "CenterPoint_" ^ aut; 
272 
hand_unless = [ 
273 
(loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut); 
274 
(loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut); 
275 
]; 
276 
hand_until = []; 
277 
hand_locals = []; 
278 
hand_stmts = tr0.statements; 
279 
hand_asserts = base_to_assert tr0; 
280 
hand_annots = []; 
281 
hand_loc = loc; 
282 
}; 
283 
(* Cond mode *) 
284 
{ hand_state = "Cond_" ^ aut; 
285 
hand_unless = []; 
286 
hand_until = [ 
287 
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); 
288 
]; 
289 
hand_locals = mk_locals vars1; 
290 
hand_stmts = tr1.statements; 
291 
hand_asserts = base_to_assert tr1; 
292 
hand_annots = []; 
293 
hand_loc = loc; 
294 
}; 
295 
(* NotCond mode *) 
296 
{ hand_state = "NotCond_" ^ aut; 
297 
hand_unless = []; 
298 
hand_until = [ 
299 
(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut); 
300 
]; 
301 
hand_locals = mk_locals vars2; 
302 
hand_stmts = tr2.statements; 
303 
hand_asserts = base_to_assert tr2; 
304 
hand_annots = []; 
305 
hand_loc = loc; 
306 
}; 
307 
] 
308 
} 
309 
) 
310 
]; 
311 
assert_false = false 
312 
} 
313 
) 
314 

315 
let mktransformer tr = 
316 
let (vars, tr) = tr "sin_" "sout_" 
317 
in tr 
318 

319 
let mkcomponent : 
320 
type c. c call_t > c > t > LustreSpec.program = 
321 
fun call args > 
322 
fun tr > 
323 
reset_loc (); 
324 
let (vars', tr') = tr "sin_" "sout_" in 
325 
pp_name call args; 
326 
let funname = Format.flush_str_formatter () in 
327 
let node = 
328 
Corelang.mktop ( 
329 
LustreSpec.Node {LustreSpec.node_id = funname; 
330 
node_type = Types.new_var (); 
331 
node_clock = Clocks.new_var true; 
332 
node_inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars; 
333 
node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars; 
334 
node_locals = mk_locals vars'; (* TODO: add global vars *) 
335 
node_gencalls = []; 
336 
node_checks = []; 
337 
node_stmts = tr'.statements; 
338 
node_asserts = base_to_assert tr'; 
339 
node_dec_stateless = false; 
340 
node_stateless = None; 
341 
node_spec = None; 
342 
node_annot = []} 
343 
) 
344 
in 
345 
[node] 
346 

347 
let mk_main_loop () = 
348 
(* let loc = Location.dummy_loc in *) 
349 

350 
let call_stmt = 
351 
(* (%t) > pre (thetaCallD_from_principal (event, %a)) *) 
352 
let init = mkexpr 
353 
(LustreSpec.Expr_tuple (vars_to_exprl ~prefix:"sout_" Vars.state_vars)) 
354 
in 
355 
let args = (Corelang.expr_of_vdecl event_var):: 
356 
(vars_to_exprl ~prefix:"sout_" Vars.state_vars) 
357 
in 
358 
let call_expr = mkpredef_call "thetaCallD_from_principal" args in 
359 
let pre_call_expr = mkexpr (LustreSpec.Expr_pre (call_expr)) in 
360 
let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in 
361 
mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs 
362 
in 
363 
let node_principal = 
364 
Corelang.mktop ( 
365 
LustreSpec.Node {LustreSpec.node_id = "principal_loop"; 
366 
node_type = Types.new_var (); 
367 
node_clock = Clocks.new_var true; 
368 
node_inputs = [event_var]; 
369 
node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars; 
370 
node_locals = []; (* TODO: add global vars *) 
371 
node_gencalls = []; 
372 
node_checks = []; 
373 
node_asserts = base_to_assert call_stmt; 
374 
node_stmts = call_stmt.statements; 
375 
node_dec_stateless = false; 
376 
node_stateless = None; 
377 
node_spec = None; 
378 
node_annot = []} 
379 
) 
380 
in 
381 
node_principal 
382 

383  
384 
let mkprincipal tr = 
385 
event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()] 
386  
387 
end 