Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 9c654082

History | View | Annotate | Download (13.5 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 : GlobalVarDef.t list
11

    
12
  end) : TransformerType =
13
struct
14
  include TransformerStub
15

    
16
  type name_t = string
17
  type t_base = { statements : LustreSpec.statement list; assert_false: bool }
18
  type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base)
19

    
20
	
21
  let new_loc, reset_loc =
22
    let cpt = ref 0 in
23
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
24
     (fun () -> cpt := 0))
25

    
26
  let new_aut, reset_aut =
27
    let cpt = ref 0 in
28
    ((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt),
29
     (fun () -> cpt := 0))
30
      
31
  let pp_path prefix fmt path =
32
    Format.fprintf fmt "%s%t"
33
      prefix
34
      (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
35

    
36
  let pp_typed_path sin fmt path =
37
    Format.fprintf fmt "%a : bool" (pp_path sin) path
38

    
39
  let pp_vars sin fmt vars =
40
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars))
41
  let pp_vars_decl sin fmt vars =
42
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))
43
       
44
  let var_to_ident prefix p =
45
    pp_path prefix Format.str_formatter p;
46
    Format.flush_str_formatter ()
47

    
48
  let vars_to_ident_list ?(prefix="") vars =
49
    List.map (
50
      fun p -> var_to_ident prefix p
51
    ) (ActiveStates.Vars.elements vars)
52

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

    
59
  let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
60
  let state_vars_to_vdecl_list ?(prefix="") vars =
61
    let bool_type = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_bool in
62
    List.map 
63
      (fun v -> var_to_vdecl ~prefix:prefix v bool_type)
64
      (ActiveStates.Vars.elements vars)
65

    
66
  let mk_locals locs =
67
    ActiveStates.Vars.fold (fun v accu ->
68
      (state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars)@accu
69
    ) locs []
70
     (* TODO: declare global vars *)
71

    
72
  let mkeq = Corelang.mkeq Location.dummy_loc
73
  let mkexpr = Corelang.mkexpr Location.dummy_loc
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))
76
  let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs =
77
    { statements = [
78
      LustreSpec.Eq (
79
	mkeq (
80
	  vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *)
81
	  rhs (* rhs *)
82
	)
83
      )
84
      ];
85
      assert_false = false
86
    }
87
  let base_to_assert b =
88
    if b.assert_false then
89
      [{LustreSpec.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]
90
    else
91
      []
92

    
93
    
94
  let var_to_expr ?(prefix="") p =
95
    let id = var_to_ident prefix p in
96
    Corelang.expr_of_ident id Location.dummy_loc
97

    
98
  let vars_to_exprl ?(prefix="") vars =
99
    List.map
100
      (fun p -> var_to_expr ~prefix:prefix p)
101
      (ActiveStates.Vars.elements vars)
102

    
103

    
104
  (* Events *)
105
  let event_type_decl =
106
    Corelang.mktop
107
      (
108
	LustreSpec.TypeDef {
109
	  LustreSpec.tydef_id = "event_type";
110
	  tydef_desc = LustreSpec.Tydec_int
111
	}
112
      )
113
    
114
  let event_type = {
115
    LustreSpec.ty_dec_desc = LustreSpec.Tydec_const "event_type";
116
    LustreSpec.ty_dec_loc = Location.dummy_loc;
117
  }
118
    
119
  let event_var = mkvar "event" event_type 
120

    
121

    
122
  let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13
123
  let get_event_const e =
124
    try Hashtbl.find const_map e
125
    with Not_found -> (
126
      let nb = Hashtbl.length const_map in
127
      Hashtbl.add const_map e nb;
128
      nb	
129
    )
130

    
131

    
132
      
133
  let null sin sout =
134
    let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
135
    ActiveStates.Vars.empty,
136
    (
137
      (* Nothing happen here: out_vars = in_vars *)
138
      let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
139
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
140
    )
141
      
142
  let bot sin sout =
143
    let (vars, tr) = null sin sout in
144
    (
145
      ActiveStates.Vars.empty,
146
      { tr with assert_false = true }
147
    )
148
      
149
  let ( >> ) tr1 tr2 sin sout =
150
    let l = new_loc () in
151
    let (vars1, tr1) = tr1 sin l in
152
    let (vars2, tr2) = tr2 l sout in
153
    (ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2),
154
     {
155
       statements = tr1.statements @ tr2.statements;
156
       assert_false = tr1.assert_false || tr2.assert_false
157
     }
158
    )
159
      
160
  let pp_name :
161
  type c. c call_t  -> c -> unit =
162
    fun call -> 
163
      match call with
164
      | Ecall -> (fun (p, p', f) ->
165
	Format.fprintf Format.str_formatter "theta%a%a%a_%a"
166
	  pp_call call
167
	  (pp_path "_from_") p
168
	  (pp_path "_to_") p'
169
	  pp_frontier f)
170
      | Dcall -> (fun p          ->
171
	Format.fprintf Format.str_formatter "theta%a%a"
172
	  pp_call call
173
	  (pp_path "_from_") p)
174
      | Xcall -> (fun (p, f)     ->
175
	Format.fprintf Format.str_formatter "theta%a%a_%a"
176
	  pp_call call
177
	  (pp_path "_from_") p
178
	  pp_frontier f)
179
	     
180

    
181
  let mkcall' :
182
  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 = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
187
      let rhs = mkpredef_call funname args in
188
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
189
	
190
  let mkact' action sin sout =
191
    match action with
192
    | Action.Call (c, a) -> mkcall' sin sout c a
193
    | Action.Quote a     ->
194
        (* TODO: check. This seems to be innappropriate *)
195
        (* let funname = "action_" ^ a.ident in
196
	let args = vars_to_exprl ~prefix:sin Vars.state_vars in
197
	let rhs = mkpredef_call funname args in
198
	mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
199
	*)
200
       {
201
	 statements = a.defs;
202
	 assert_false = false
203
       }
204
    | Action.Open p      ->
205
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
206
       (* eq1: sout_p = true *)
207
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in
208
       (* eq2: sout_xx = sin_xx *)
209
       let expr_list = vars_to_exprl ~prefix:sin vars' in
210
       let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
211
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
212
	 {
213
	   statements = [
214
	     LustreSpec.Eq (eq1);
215
	     LustreSpec.Eq (eq2);
216
	   ];
217
	   assert_false = false
218
	 }
219
	 
220
    | Action.Close p     ->
221
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
222
       (* eq1: sout_p = false *)
223
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in
224
       (* eq2: sout_xx = sin_xx *)
225
       let expr_list = vars_to_exprl ~prefix:sin vars' in
226
       let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
227
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
228
	 {
229
	   statements = [
230
	     LustreSpec.Eq (eq1);
231
	     LustreSpec.Eq (eq2);
232
	   ];
233
	   assert_false = false
234
	 }
235

    
236
    | Action.Nil         ->
237
       let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
238
       let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
239
       mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
240
	 
241
  let eval_act kenv (action : act_t) =
242
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
243
    (fun sin sout -> (ActiveStates.Vars.empty,
244
		      mkact' action sin sout   ))
245
       
246
  let rec mkcond' sin condition =
247
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
248
    match condition with
249
    | Condition.True               -> expr_of_bool true
250
    | Condition.Active p           -> var_to_expr ~prefix:sin p
251
    | Condition.Event e            ->
252
       mkpredef_call "=" [
253
	 Corelang.expr_of_vdecl event_var;
254
	 mkexpr (LustreSpec.Expr_const (LustreSpec.Const_int (get_event_const e)))
255
       ]
256
    | Condition.Neg cond           -> mkpredef_call "not" [mkcond' sin cond]
257
    | Condition.And (cond1, cond2) -> mkpredef_call "&&" [mkcond' sin cond1;
258
							  mkcond' sin cond2]
259
    | Condition.Quote c            -> c.expr (* TODO: shall we prefix with sin ? *)
260

    
261
  let rec eval_cond condition (ok:t) ko sin sout =
262
    let open LustreSpec in
263
    let loc = Location.dummy_loc in
264
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
265
    let (vars1, tr1) = ok sin sout in
266
    let (vars2, tr2) = ko sin sout in
267
    let (vars0, tr0) = bot sin sout in
268
    let aut = new_aut () in
269
    (ActiveStates.Vars.empty,
270
     {
271
       statements = [
272
	 let handler_default_mode =          	      (* Default mode : CenterPoint *)
273
	   let handler_default_mode_unless = [
274
	     (loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut);
275
	     (loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut);
276
	   ]
277
	   in
278
	   Automata.mkhandler
279
	     loc                                      (* location *)
280
	     ("CenterPoint_" ^ aut)                   (* state name *)
281
	     handler_default_mode_unless              (* unless *)
282
	     []                                       (* until *)
283
	     []                                       (* locals *)
284
	     (tr0.statements, base_to_assert tr0, []) (* stmts, asserts, annots *)
285
	 in
286
	 let handler_cond_mode =                       	 (* Cond mode *)
287
       	   let handler_cond_mode_until = [
288
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
289
       	   ]
290
	   in
291
	   Automata.mkhandler
292
	     loc                                      (* location *)
293
	     ("Cond_" ^ aut)                          (* state name *)
294
	     []                                       (* unless *)
295
	     handler_cond_mode_until                  (* until *)
296
	     (mk_locals vars1)                        (* locals *)
297
	     (tr1.statements, base_to_assert tr1, []) (* stmts, asserts, annots *)
298
	 in
299
	 let handler_notcond_mode =                       	 (* NotCond mode *)
300
       	   let handler_notcond_mode_until = [
301
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
302
       	   ]
303
	   in
304
	   Automata.mkhandler
305
	     loc                                      (* location *)
306
	     ("NotCond_" ^ aut)                       (* state name *)
307
	     []                                       (* unless *)
308
	     handler_notcond_mode_until               (* until *)
309
	     (mk_locals vars2)                        (* locals *)
310
	     (tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *)
311
	 in
312
	 let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in
313
	 Aut (Automata.mkautomata loc aut handlers)
314
       ];
315
       assert_false = false
316
     }
317
    )
318
      
319
  let mktransformer tr =
320
    let (vars, tr) = tr "sin_" "sout_"
321
    in tr 
322
    
323
  let mkcomponent :
324
  type c. c call_t -> c -> t -> LustreSpec.program =
325
    fun call args ->
326
      fun tr ->
327
	reset_loc ();
328
	let (vars', tr') = tr "sin_" "sout_" in
329
	pp_name call args;
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
333
	let node =
334
	  Corelang.mktop (	
335
	    LustreSpec.Node {LustreSpec.node_id = funname;
336
			   node_type = Types.new_var ();
337
			   node_clock = Clocks.new_var true;
338
			   node_inputs = inputs;
339
			   node_outputs = outputs;
340
			   node_locals = mk_locals vars'; (* TODO: add global vars *)
341
			   node_gencalls = [];
342
			   node_checks = [];
343
			   node_stmts = tr'.statements;
344
			   node_asserts = base_to_assert tr';
345
			   node_dec_stateless = false;
346
			   node_stateless = None;
347
			   node_spec = None;
348
			   node_annot = []}
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
	  
365
  let mk_main_loop () =
366
    (* let loc = Location.dummy_loc in *)
367
    
368
    let call_stmt =
369
      (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
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))
376
      in
377
      let args = (Corelang.expr_of_vdecl event_var)::
378
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
379
      in
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
383
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
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 *)
388
    let node_principal =
389
      Corelang.mktop (	
390
	LustreSpec.Node {LustreSpec.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
      )  
405
    in
406
    node_principal
407
    
408

    
409
  let mkprincipal tr =
410
    event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()]
411

    
412
end