Project

General

Profile

Revision b08ffca7 src/automata.ml

View differences:

src/automata.ml
13 13
open LustreSpec
14 14
open Corelang
15 15

  
16
let pp_restart fmt restart =
17
  Format.fprintf fmt "%s" (if restart then "restart" else "resume")
18

  
19
let pp_unless fmt (_, expr, restart, st) =
20
  Format.fprintf fmt "unless %a %a %s"
21
    Printers.pp_expr expr
22
    pp_restart restart
23
    st
24

  
25
let pp_until fmt (_, expr, restart, st) =
26
  Format.fprintf fmt "until %a %a %s"
27
    Printers.pp_expr expr
28
    pp_restart restart
29
    st
30

  
31
let pp_handler fmt handler =
32
  Format.fprintf fmt "state %s -> %a %a let %a tel %a"
33
    handler.hand_state
34
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
35
    (fun fmt locals ->
36
      match locals with [] -> () | _ ->
37
	Format.fprintf fmt "@[<v 4>var %a@]@ " 
38
	  (Utils.fprintf_list ~sep:"@ " 
39
	     (fun fmt v -> Format.fprintf fmt "%a;" Printers.pp_node_var v))
40
	  locals)
41
    handler.hand_locals
42
    Printers.pp_node_eqs handler.hand_eqs
43
    (Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until
44

  
45
let pp_automata fmt aut =
46
  Format.fprintf fmt "automaton %s %a"
47
    aut.aut_id
48
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
49

  
50 16
let mkbool loc b =
51 17
 mkexpr loc (Expr_const (const_of_bool b))
52 18

  
......
62 28
let add_branch (loc, expr, restart, st) cont =
63 29
 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))
64 30

  
65
let mkhandler loc st unless until locals (eqs, asserts, annots) =
31
let mkhandler loc st unless until locals (stmts, asserts, annots) =
66 32
 {hand_state = st;
67 33
  hand_unless = unless;
68 34
  hand_until = until;
69 35
  hand_locals = locals;
70
  hand_eqs = eqs;
36
  hand_stmts = stmts;
71 37
  hand_asserts = asserts;
72 38
  hand_annots = annots;
73 39
  hand_loc = loc}
......
77 43
   aut_handlers = handlers;
78 44
   aut_loc = loc}
79 45

  
80
let handler_read handler =
81
 List.fold_left (fun read eq -> get_expr_vars read eq.eq_rhs) ISet.empty handler.hand_eqs
82

  
83
let handler_write handler =
84
 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
46
let rec handler_read reads handler =
47
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
48
  let allvars =
49
    List.fold_left (fun read stmt ->
50
      match stmt with
51
      | Eq eq -> get_expr_vars read eq.eq_rhs
52
      | Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts
53
  in ISet.diff allvars locals
54

  
55
let rec handler_write writes handler =
56
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
57
  let allvars =
58
    List.fold_left (fun write stmt ->
59
      match stmt with
60
      | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
61
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
62
  in ISet.diff allvars locals
85 63

  
86 64
let node_of_handler node aut_id handler =
87
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in 
88
  let inputs = handler_read handler in
89
  let outputs = handler_write handler in
65
  let inputs = handler_read ISet.empty handler in
66
  let outputs = handler_write ISet.empty handler in
90 67
  {
91 68
    node_id = Format.sprintf "%s_%s_handler" aut_id handler.hand_state;
92 69
    node_type = Types.new_var ();
93 70
    node_clock = Clocks.new_var true;
94
    node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff inputs locals));
95
    node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff outputs locals));
71
    node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs);
72
    node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs);
96 73
    node_locals = handler.hand_locals;
97 74
    node_gencalls = [];
98 75
    node_checks = [];
99 76
    node_asserts = handler.hand_asserts; 
100
    node_eqs = handler.hand_eqs;
77
    node_stmts = handler.hand_stmts;
101 78
    node_dec_stateless = false;
102 79
    node_stateless = None;
103 80
    node_spec = None;
......
111 88
  let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in
112 89
  mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag))
113 90

  
114
let assign_aut_handlers loc node actual_r actual_s hnodes =
91
let assign_aut_handlers loc actual_r actual_s hnodes =
115 92
  let outputs = (snd (List.hd hnodes)).node_outputs in
116 93
  let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
117 94
  let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in
......
123 100
  { tydef_id = tname;
124 101
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
125 102
  }
103
(*
104
let expand_automata_stmt (top_decls, locals, eqs) stmt =
105
  match stmt with
106
  | Eq eq -> (top_decls, locals, eq::eqs)
107
  | Aut aut ->
108

  
126 109

  
127 110
let expand_automata top_node aut =
128 111
  let node = node_of_top top_node in
......
141 124
  let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in
142 125
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
143 126
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler node aut.aut_id h)) aut.aut_handlers in
144
  let assign_eq = assign_aut_handlers aut.aut_loc node actual_r actual_s hnodes in
127
  let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in
145 128
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
146 129
  let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in
147 130
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
......
149 132
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
150 133
                 mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);
151 134
                 mkvar_decl aut.aut_loc (actual_s  , tydec_const typedef.tydef_id, ckdec_any, false)] in
152
  let eqs' = [unless_eq; assign_eq; until_eq] in
153
  let node' = { node with node_locals = locals'@node.node_locals; node_eqs = eqs'@node.node_eqs } in
135
  let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
136
  let node' = { node with node_locals = locals'@node.node_locals; node_stmts = eqs'@node.node_stmts } in
154 137
  (mktop_decl aut.aut_loc owner false (TypeDef typedef)) ::
155 138
  { top_node with top_decl_desc = Node node' } ::
156 139
  (List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes)
157

  
158
let node_extract_automata top_decl =
140
*)
141
let rec node_extract_automata top_decl =
159 142
  match top_decl.top_decl_desc with
160
  | Node nd -> [top_decl]
143
  | Node nd -> []
161 144
  | _ -> [top_decl]
162 145
(*
163 146
let extract_automata top_decls =

Also available in: Unified diff