Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / semantics / cPS_lustre_generator.ml @ 93119c3f

History | View | Annotate | Download (12.3 KB)

1 93119c3f ploc
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
  let new_loc, reset_loc =
20
    let cpt = ref 0 in
21
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
22
     (fun () -> cpt := 0))
23
24
  let new_aut, reset_aut =
25
    let cpt = ref 0 in
26
    ((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt),
27
     (fun () -> cpt := 0))
28
      
29
  let pp_path prefix fmt path =
30
    Format.fprintf fmt "%s%t"
31
      prefix
32
      (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
33
34
  let pp_typed_path sin fmt path =
35
    Format.fprintf fmt "%a : bool" (pp_path sin) path
36
37
  let pp_vars sin fmt vars =
38
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars))
39
  let pp_vars_decl sin fmt vars =
40
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))
41
42
  let pp_locals fmt locs =
43
    ActiveStates.Vars.iter (fun v -> Format.fprintf fmt "%a;@ " (pp_vars_decl (List.hd v)) Vars.state_vars) locs;
44
    () (* TODO: declare global vars *)
45
46
  let var_to_ident prefix p =
47
    pp_path prefix Format.str_formatter p;
48
    Format.flush_str_formatter ()
49
50
  let vars_to_ident_list ?(prefix="") vars =
51
    List.map (
52
      fun p -> var_to_ident prefix p
53
    ) (ActiveStates.Vars.elements vars)
54
55
  let mkvar name typ = 
56
    let loc = Location.dummy_loc in
57
    Corelang.mkvar_decl
58
      loc
59
      (name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None)
60
61
  let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
62
  let state_vars_to_vdecl_list ?(prefix="") vars =
63
    let bool_type = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_bool in
64
    List.map 
65
      (fun v -> var_to_vdecl ~prefix:prefix v bool_type)
66
      (ActiveStates.Vars.elements vars)
67
68
  let mkeq = Corelang.mkeq Location.dummy_loc
69
  let mkexpr = Corelang.mkexpr Location.dummy_loc
70
  let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc
71
  let expr_of_bool b = mkexpr (LustreSpec.Expr_const (Corelang.const_of_bool b))
72
  let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs =
73
    { statements = [
74
      LustreSpec.Eq (
75
	mkeq (
76
	  vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *)
77
	  rhs (* rhs *)
78
	)
79
      )
80
      ];
81
      assert_false = false
82
    }
83
    
84
  let var_to_expr ?(prefix="") p =
85
    let id = var_to_ident prefix p in
86
    Corelang.expr_of_ident id Location.dummy_loc
87
88
  let vars_to_exprl ?(prefix="") vars =
89
    List.map
90
      (fun p -> var_to_expr ~prefix:prefix p)
91
      (ActiveStates.Vars.elements vars)
92
93
94
  (* Events *)
95
  let event_type_decl =
96
    Corelang.mktop
97
      (
98
	LustreSpec.TypeDef {
99
	  LustreSpec.tydef_id = "event_type";
100
	  tydef_desc = LustreSpec.Tydec_int
101
	}
102
      )
103
    
104
  let event_type = {
105
    LustreSpec.ty_dec_desc = LustreSpec.Tydec_const "event_type";
106
    LustreSpec.ty_dec_loc = Location.dummy_loc;
107
  }
108
    
109
  let event_var = mkvar "event" event_type
110
111
112
  let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13
113
  let get_event_const e =
114
    try Hashtbl.find const_map e
115
    with Not_found -> (
116
      let nb = Hashtbl.length const_map in
117
      Hashtbl.add const_map e nb;
118
      nb	
119
    )
120
121
122
      
123
  let null sin sout =
124
    let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
125
    ActiveStates.Vars.empty,
126
    (
127
      (* Nothing happen here: out_vars = in_vars *)
128
      let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
129
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
130
    )
131
      
132
  let bot sin sout =
133
    let (vars, tr) = null sin sout in
134
    (
135
      ActiveStates.Vars.empty,
136
      { tr with assert_false = true }
137
    )
138
      
139
  let ( >> ) tr1 tr2 sin sout =
140
    let l = new_loc () in
141
    let (vars1, tr1) = tr1 sin l in
142
    let (vars2, tr2) = tr2 l sout in
143
    (ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2),
144
     {
145
       statements = tr1.statements @ tr2.statements;
146
       assert_false = tr1.assert_false || tr2.assert_false
147
     }
148
    )
149
       
150
  let mkcall' :
151
  type c. name_t -> name_t -> c call_t -> c -> t_base =
152
    fun sin sout call ->
153
      let pp_name : type c. c call_t  -> c -> unit =
154
	fun call -> 
155
	  match call with
156
	  | Ecall -> (fun (p, p', f) ->
157
	    Format.fprintf Format.str_formatter "theta%a%a%a_%a"
158
	      pp_call call
159
	      (pp_path "_from_") p
160
	      (pp_path "_to_") p'
161
	      pp_frontier f)
162
	  | Dcall -> (fun p          ->
163
	    Format.fprintf Format.str_formatter "theta%a%a"
164
	      pp_call call
165
	      (pp_path "_from_") p)
166
	  | Xcall -> (fun (p, f)     ->
167
	    Format.fprintf Format.str_formatter "theta%a%a_%a"
168
	      pp_call call
169
	      (pp_path "_from_") p
170
	      pp_frontier f)
171
      in
172
      fun arg ->
173
	pp_name call arg;
174
	let funname = Format.flush_str_formatter () in
175
	let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
176
	let rhs = mkpredef_call funname args in
177
	mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
178
179
  let mkact' action sin sout =
180
    match action with
181
    | Action.Call (c, a) -> mkcall' sin sout c a
182
    | Action.Quote a     ->
183
	let funname = "action_" ^ a.ident in
184
	let args = vars_to_exprl ~prefix:sin Vars.state_vars in
185
	let rhs = mkpredef_call funname args in
186
	mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
187
    | Action.Open p      ->
188
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
189
       (* eq1: sout_p = true *)
190
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in
191
       (* eq2: sout_xx = sin_xx *)
192
       let expr_list = vars_to_exprl ~prefix:sin vars' in
193
       let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
194
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
195
	 {
196
	   statements = [
197
	     LustreSpec.Eq (eq1);
198
	     LustreSpec.Eq (eq2);
199
	   ];
200
	   assert_false = false
201
	 }
202
	 
203
    | Action.Close p     ->
204
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
205
       (* eq1: sout_p = false *)
206
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in
207
       (* eq2: sout_xx = sin_xx *)
208
       let expr_list = vars_to_exprl ~prefix:sin vars' in
209
       let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
210
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
211
	 {
212
	   statements = [
213
	     LustreSpec.Eq (eq1);
214
	     LustreSpec.Eq (eq2);
215
	   ];
216
	   assert_false = false
217
	 }
218
219
    | Action.Nil         ->
220
       let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
221
       let rhs = mkexpr (LustreSpec.Expr_tuple expr_list) in 
222
       mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
223
	 
224
  let eval_act kenv (action : act_t) =
225
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
226
    (fun sin sout -> (ActiveStates.Vars.empty,
227
		      mkact' action sin sout   ))
228
       
229
  let rec mkcond' sin condition =
230
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
231
    match condition with
232
    | Condition.True               -> expr_of_bool true
233
    | Condition.Active p           -> var_to_expr ~prefix:sin p
234
    | Condition.Event e            ->
235
       mkpredef_call "=" [
236
	 Corelang.expr_of_vdecl event_var;
237
	 mkexpr (LustreSpec.Expr_const (LustreSpec.Const_int (get_event_const e)))
238
       ]
239
    | Condition.Neg cond           -> mkpredef_call "not" [mkcond' sin cond]
240
    | Condition.And (cond1, cond2) -> mkpredef_call "&&" [mkcond' sin cond1;
241
							  mkcond' sin cond2]
242
    | Condition.Quote c            -> c (* TODO: shall we prefix with sin ? *)
243
244
  let rec eval_cond condition ok ko sin sout =
245
    let open LustreSpec in
246
    let loc = Location.dummy_loc in
247
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
248
    let (vars1, tr1) = ok sin sout in
249
    let (vars2, tr2) = ko sin sout in
250
    let (vars0, tr0) = bot sin sout in
251
    let aut = new_aut () in
252
    (ActiveStates.Vars.empty,
253
     {
254
       statements = [
255
	 Aut (
256
	   { aut_id = aut;
257
	     aut_loc = loc;
258
	     aut_handlers =
259
	       [
260
		 (* Default mode : CenterPoint *)
261
		 { hand_state = "CenterPoint_" ^ aut;
262
		   hand_unless = [
263
		     (loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut);
264
		     (loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut);
265
		   ];
266
		   hand_until = [];
267
		   hand_locals = [];
268
		   hand_stmts = tr0.statements;
269
		   hand_asserts = if tr0.assert_false then
270
		       [{assert_expr = expr_of_bool false; assert_loc = loc}]
271
		     else
272
		       [];
273
		   hand_annots = [];
274
		   hand_loc = loc;
275
		 };
276
		 (* Cond mode *)
277
		 { hand_state = "Cond_" ^ aut;
278
		   hand_unless = [];
279
		   hand_until = [
280
		     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
281
		   ];
282
		   hand_locals = [vars1] (* TODO convert to valid type *);
283
		   hand_stmts = tr1.statements;
284
		   hand_asserts = if tr1.assert_false then
285
		       [{assert_expr = expr_of_bool false; assert_loc = loc}]
286
		     else
287
		       [];
288
		   hand_annots = [];
289
		   hand_loc = loc;
290
		 };
291
		 (* NotCond mode *)
292
		 { hand_state = "NotCond_" ^ aut;
293
		   hand_unless = [];
294
		   hand_until = [
295
		     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
296
		   ];
297
		   hand_locals = [vars2] (* TODO convert to valid type *);
298
		   hand_stmts = tr2.statements;
299
		   hand_asserts = if tr2.assert_false then
300
		       [{assert_expr = expr_of_bool false; assert_loc = loc}]
301
		     else
302
		       [];
303
		   hand_annots = [];
304
		   hand_loc = loc;
305
		 };
306
	       ]
307
	   }
308
	 )
309
       ];
310
       assert_false = false
311
     }
312
    )
313
      
314
  let pp_transformer fmt tr =
315
    let (vars, tr) = tr "sin_" "sout_"
316
    in tr fmt
317
    
318
  let mkcomponent :
319
  type c. c call_t -> c -> t -> prog =
320
    fun fmt call -> match call with
321
    | Ecall -> (fun (p, p', f) tr ->
322
      reset_loc ();
323
      let (vars', tr') = tr "sin_" "sout_" in
324
      Format.fprintf fmt "node theta%a%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
325
	pp_call call
326
	(pp_path "_from_") p
327
	(pp_path "_to_") p'
328
	pp_frontier f
329
	(pp_vars_decl "sin_") Vars.state_vars
330
	(pp_vars_decl "sout_") Vars.state_vars
331
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
332
	pp_locals vars'
333
	tr')
334
    | Dcall -> (fun p tr ->
335
      reset_loc ();
336
      let (vars', tr') = tr "sin_" "sout_" in
337
      Format.fprintf fmt "node theta%a%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
338
	pp_call call
339
	(pp_path "_from_") p
340
	(pp_vars_decl "sin_") Vars.state_vars
341
	(pp_vars_decl "sout_") Vars.state_vars
342
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
343
	pp_locals vars'
344
	tr')
345
    | Xcall -> (fun (p, f) tr ->
346
      reset_loc ();
347
      let (vars', tr') = tr "sin_" "sout_" in
348
      Format.fprintf fmt "node theta%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
349
	pp_call call
350
	(pp_path "_from_") p
351
	pp_frontier f
352
	(pp_vars_decl "sin_") Vars.state_vars
353
	(pp_vars_decl "sout_") Vars.state_vars
354
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
355
	pp_locals vars'
356
	tr')
357
358
  let mk_main_loop () =
359
    let loc = Location.dummy_loc in
360
    let node_principal =
361
      Corelang.mktop (	
362
	LustreSpec.Node {LustreSpec.node_id = "principal_loop";
363
			 node_type = Types.new_var ();
364
			 node_clock = Clocks.new_var true;
365
			 node_inputs = [event_var];
366
			 node_outputs = state_vars_to_vdecl_list ~prefx:"sout_" Vars.state_vars;
367
			 node_locals = []; (* TODO: add global vars *)
368
			 node_gencalls = [];
369
			 node_checks = [];
370
			 node_asserts = []; 
371
			 node_stmts = call_stmt;
372
			 node_dec_stateless = false;
373
			 node_stateless = None;
374
			 node_spec = None;
375
			 node_annot = []}
376
      )  
377
    in
378
    
379
    let call_stmt =
380
      (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
381
      let init = mkexpr loc
382
	(Expr_tuple (vars_to_exprl ~prefix:"sout_" Vars.state_vars))
383
      in
384
      let args = (Corelang.expr_of_vdecl event_var)::
385
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
386
      in
387
      let call_expr = mkpredef_call "thetaCallD_from_principal" args in
388
      let pre_call_expr = mkexpr loc (Expr_pre (call_expr)) in
389
      let rhs = mkexpr loc (Expr_arrow (init, pre_call_expr)) in
390
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
391
    in
392
    [
393
      event_type_decl;
394
      node_principal
395
    ]
396
397
  let mkprincipal tr =
398
    mk_main_loop () @ mkcomponent Dcall ["principal"] tr
399
400
end