Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 69c96b6c

History | View | Annotate | Download (11.6 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