Project

General

Profile

Revision 2822cf55 src/automata.ml

View differences:

src/automata.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open Utils
12 13
open LustreSpec
13 14
open Corelang
14 15

  
......
18 19
let mkident loc id =
19 20
 mkexpr loc (Expr_ident id)
20 21

  
21
let init (loc, restart, st) =
22
let init loc restart st =
22 23
 mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st])
23 24

  
24
let add_branch expr (loc, restart, st) cont =
25
 mkexpr loc (Expr_ite (expr, init (loc, restart, st), cont))
25
let add_branch (loc, expr, restart, st) cont =
26
 mkexpr loc (Expr_ite (expr, init loc restart st, cont))
26 27

  
27
let mkhandler loc st unless until locals eqs =
28
let mkhandler loc st unless until locals (eqs, asserts, annots) =
28 29
 {hand_state = st;
29 30
  hand_unless = unless;
30 31
  hand_until = until;
31 32
  hand_locals = locals;
32 33
  hand_eqs = eqs;
34
  hand_asserts = asserts;
35
  hand_annots = annots;
33 36
  hand_loc = loc}
34 37

  
35 38
let mkautomata loc id handlers =
......
37 40
   aut_handlers = handlers;
38 41
   aut_loc = loc}
39 42

  
43
let node_of_handler loc id inputs outputs handler =
44
 Node {
45
   node_id = id;
46
   node_type = Types.new_var ();
47
   node_clock = Clocks.new_var true;
48
   node_inputs = inputs;
49
   node_outputs = outputs;
50
   node_locals = handler.hand_locals;
51
   node_gencalls = [];
52
   node_checks = [];
53
   node_asserts = handler.hand_asserts; 
54
   node_eqs = handler.hand_eqs;
55
   node_dec_stateless = false;
56
   node_stateless = None;
57
   node_spec = None;
58
   node_annot = handler.hand_annots
59
 }
60

  
61
let handler_read handler =
62
 List.fold_left (fun read eq -> get_expr_vars read eq.eq_rhs) ISet.empty handler.hand_eqs
63

  
64
let handler_write handler =
65
 List.fold_left (fun write eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs) ISet.empty handler.hand_eqs
66

  
67
let expr_of_exit_conditions loc st conds =
68
 List.fold_right add_branch conds (init loc false st)
69

  
40 70
let pp_restart fmt restart =
41 71
  Format.fprintf fmt "%s" (if restart then "restart" else "resume")
42 72

  
43
let pp_unless fmt (expr, restart, st) =
73
let pp_unless fmt (_, expr, restart, st) =
44 74
  Format.fprintf fmt "unless %a %a %s"
45 75
    Printers.pp_expr expr
46 76
    pp_restart restart
47 77
    st
48 78

  
49
let pp_until fmt (expr, restart, st) =
79
let pp_until fmt (_, expr, restart, st) =
50 80
  Format.fprintf fmt "until %a %a %s"
51 81
    Printers.pp_expr expr
52 82
    pp_restart restart

Also available in: Unified diff