Project

General

Profile

Revision 69c96b6c src/tools/stateflow/semantics/cPS_lustre_generator.ml

View differences:

src/tools/stateflow/semantics/cPS_lustre_generator.ml
16 16
  type t_base = { statements : LustreSpec.statement list; assert_false: bool }
17 17
  type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base)
18 18

  
19
	
19 20
  let new_loc, reset_loc =
20 21
    let cpt = ref 0 in
21 22
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
......
39 40
  let pp_vars_decl sin fmt vars =
40 41
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))
41 42

  
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 43
  let var_to_ident prefix p =
47 44
    pp_path prefix Format.str_formatter p;
48 45
    Format.flush_str_formatter ()
......
65 62
      (fun v -> var_to_vdecl ~prefix:prefix v bool_type)
66 63
      (ActiveStates.Vars.elements vars)
67 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

  
68 71
  let mkeq = Corelang.mkeq Location.dummy_loc
69 72
  let mkexpr = Corelang.mkexpr Location.dummy_loc
70 73
  let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc
......
80 83
      ];
81 84
      assert_false = false
82 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

  
83 92
    
84 93
  let var_to_expr ?(prefix="") p =
85 94
    let id = var_to_ident prefix p in
......
146 155
       assert_false = tr1.assert_false || tr2.assert_false
147 156
     }
148 157
    )
149
       
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

  
150 180
  let mkcall' :
151 181
  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

  
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
	
179 189
  let mkact' action sin sout =
180 190
    match action with
181 191
    | Action.Call (c, a) -> mkcall' sin sout c a
......
241 251
							  mkcond' sin cond2]
242 252
    | Condition.Quote c            -> c (* TODO: shall we prefix with sin ? *)
243 253

  
244
  let rec eval_cond condition ok ko sin sout =
254
  let rec eval_cond condition (ok:t) ko sin sout =
245 255
    let open LustreSpec in
246 256
    let loc = Location.dummy_loc in
247 257
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
......
266 276
		   hand_until = [];
267 277
		   hand_locals = [];
268 278
		   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
		       [];
279
		   hand_asserts = base_to_assert tr0;
273 280
		   hand_annots = [];
274 281
		   hand_loc = loc;
275 282
		 };
......
279 286
		   hand_until = [
280 287
		     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
281 288
		   ];
282
		   hand_locals = [vars1] (* TODO convert to valid type *);
289
		   hand_locals = mk_locals vars1;
283 290
		   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
		       [];
291
		   hand_asserts = base_to_assert tr1;
288 292
		   hand_annots = [];
289 293
		   hand_loc = loc;
290 294
		 };
......
294 298
		   hand_until = [
295 299
		     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
296 300
		   ];
297
		   hand_locals = [vars2] (* TODO convert to valid type *);
301
		   hand_locals = mk_locals vars2;
298 302
		   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_asserts = base_to_assert tr2;
303 304
		   hand_annots = [];
304 305
		   hand_loc = loc;
305 306
		 };
......
311 312
     }
312 313
    )
313 314
      
314
  let pp_transformer fmt tr =
315
  let mktransformer tr =
315 316
    let (vars, tr) = tr "sin_" "sout_"
316
    in tr fmt
317
    in tr 
317 318
    
318 319
  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

  
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
	  
358 347
  let mk_main_loop () =
359
    let loc = Location.dummy_loc in
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
360 363
    let node_principal =
361 364
      Corelang.mktop (	
362 365
	LustreSpec.Node {LustreSpec.node_id = "principal_loop";
363 366
			 node_type = Types.new_var ();
364 367
			 node_clock = Clocks.new_var true;
365 368
			 node_inputs = [event_var];
366
			 node_outputs = state_vars_to_vdecl_list ~prefx:"sout_" Vars.state_vars;
369
			 node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars;
367 370
			 node_locals = []; (* TODO: add global vars *)
368 371
			 node_gencalls = [];
369 372
			 node_checks = [];
370
			 node_asserts = []; 
371
			 node_stmts = call_stmt;
373
			 node_asserts = base_to_assert call_stmt; 
374
			 node_stmts = call_stmt.statements;
372 375
			 node_dec_stateless = false;
373 376
			 node_stateless = None;
374 377
			 node_spec = None;
375 378
			 node_annot = []}
376 379
      )  
377 380
    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 381
      node_principal
395
    ]
382
    
396 383

  
397 384
  let mkprincipal tr =
398
    mk_main_loop () @ mkcomponent Dcall ["principal"] tr
385
    event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()]
399 386

  
400 387
end

Also available in: Unified diff