Project

General

Profile

Revision 6a1a01d2 src/automata.ml

View differences:

src/automata.ml
22 22
let mkfby loc e1 e2 =
23 23
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
24 24

  
25
let init loc restart state =
25
let mkidentpair loc restart state =
26 26
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
27 27

  
28 28
let add_branch (loc, expr, restart, st) cont =
......
61 61
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
62 62
  in ISet.diff allvars locals
63 63

  
64
let node_of_handler nused node aut_id handler =
65
  let inputs = handler_read ISet.empty handler in
64
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
65

  
66
let rec rename_stmts_outputs frename stmts =
67
  match stmts with
68
  | []           -> []
69
  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
70
		      eq' :: rename_stmts_outputs frename q
71
  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in
72
                      let aut' = Aut { aut with aut_handlers = handlers' } in
73
		      aut' :: rename_stmts_outputs frename q
74

  
75
let mk_frename used outputs =
76
  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in
77
  (fun name -> try IMap.find name table with Not_found -> name)
78
  
79
let node_of_handler nused used node aut_id handler =
66 80
  let outputs = handler_write ISet.empty handler in
81
  let (new_locals, inputs) = ISet.partition (fun v -> ISet.mem v outputs) (handler_read ISet.empty handler) in
82
  let frename = mk_frename used outputs in
83
  let var_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs) in
84
  let new_var_locals = List.map (fun v -> get_node_var v node) (ISet.elements new_locals) in
85
  let var_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs) in
86
  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
87
  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
88
  var_outputs,
67 89
  {
68 90
    node_id = mk_new_name nused (Format.sprintf "%s_%s_handler" aut_id handler.hand_state);
69 91
    node_type = Types.new_var ();
70 92
    node_clock = Clocks.new_var true;
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);
73
    node_locals = handler.hand_locals;
93
    node_inputs = var_inputs;
94
    node_outputs = new_var_outputs;
95
    node_locals = new_var_locals @ handler.hand_locals;
74 96
    node_gencalls = [];
75 97
    node_checks = [];
76 98
    node_asserts = handler.hand_asserts; 
77
    node_stmts = handler.hand_stmts;
99
    node_stmts = new_output_eqs @ handler.hand_stmts;
78 100
    node_dec_stateless = false;
79 101
    node_stateless = None;
80 102
    node_spec = None;
......
82 104
  }
83 105

  
84 106
let expr_of_exit loc restart state conds tag =
85
  mkexpr loc (Expr_when (List.fold_right add_branch conds (init loc restart state), state, tag))
107
  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
86 108

  
87 109
let expr_of_handler loc restart state node tag =
88
  let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in
89
  mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag))
110
  let args = List.map (fun v -> mkexpr loc (Expr_when (mkident loc v.var_id, state, tag))) node.node_inputs in
111
  let arg = mkexpr loc (Expr_tuple args) in
112
  let reset = Some (mkident loc restart) in
113
  mkexpr loc (Expr_appl (node.node_id, arg, reset))
90 114

  
91 115
let assign_aut_handlers loc actual_r actual_s hnodes =
92
  let outputs = (snd (List.hd hnodes)).node_outputs in
93
  let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
116
  let outputs = fst (snd (List.hd hnodes)) in
117
  let assign_handlers = List.map (fun (hs, (_, n)) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
94 118
  let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in
95 119
  let assign_eq = mkeq loc (List.map (fun v -> v.var_id) outputs, assign_expr) in
96 120
  assign_eq
......
100 124
  { tydef_id = tname;
101 125
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
102 126
  }
127
(*
128
let expand_automata nused used owner typedef node aut =
129
  let initial = (List.hd aut.aut_handlers).hand_state in
130
  let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in
131
  let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in
132
  let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in
133
  let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in
134
  let next_incoming_r = mk_new_name used (aut.aut_id ^ "__next_restart_in") in
135
  let next_incoming_s = mk_new_name used (aut.aut_id ^ "__next_state_in") in
136
  (* merge on incoming_s gives actual_s by the unless equations *)
137
  let actual_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc incoming_r incoming_s h.hand_unless h.hand_state)) aut.aut_handlers in
138
  let actual_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in
139
  let actual_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
140
  (* next_incoming_s and initial conditions gives incoming_s *)
141
  let incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc next_incoming_r next_incoming_s) in
142
  let incoming_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], incoming_expr) in
143
  (* merge on actual_s gives handler assigned variables and next_incoming_s by the until equations *)
144
  let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in
145
  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
146
  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in
147
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
148
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in
149
  let outputs = fst (snd (List.hd hnodes)) in
150
  let next_incoming_and_assigned_vars = next_incoming_r :: next_incoming_s :: List.map (fun v -> v.var_id) outputs in
151
  let next_incoming_and_assigned_handlers =
152
    List.map (fun h -> ) aut.aut_handlers in
153
  let next_incoming_and_assigned_expr = mkexpr loc (Expr_merge (actual_s, next_incoming_and_assigned_handlers) in
154
  let next_incoming_and_assigned_eq = mkeq aut.aut_loc (next_incoming_and_assigned_vars, next_incoming_and_assigned_expr) in
155
  (* declaration of new local variables, equations and handler nodes *)
156
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
157
  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in
158
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
159
  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);
160
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
161
                 mkvar_decl aut.aut_loc (next_incoming_r  , tydec_bool, ckdec_any, false);
162
                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
163
                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false);
164
                 mkvar_decl aut.aut_loc (next_incoming_s, tydec_state typedef.tydef_id, ckdec_any, false)] in
165
  let eqs' = [Eq actual_eq; Eq next_incoming_and_assigned_eq; Eq incoming_eq] in
166
  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
167
  locals',
168
  eqs')
169
*)
103 170

  
104 171
let expand_automata nused used owner typedef node aut =
105 172
  let initial = (List.hd aut.aut_handlers).hand_state in
......
112 179
  let unless_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
113 180
  let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in
114 181
  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
115
  let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in
182
  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in
116 183
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
117
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused node aut.aut_id h)) aut.aut_handlers in
184
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in
118 185
  let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in
119 186
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
120
  let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in
187
  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in
121 188
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
122 189
  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);
123 190
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
124
                 mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);
125
                 mkvar_decl aut.aut_loc (actual_s  , tydec_const typedef.tydef_id, ckdec_any, false)] in
191
                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
192
                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false)] in
126 193
  let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
127
  (List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
194
  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
128 195
  locals',
129 196
  eqs')
130 197

  

Also available in: Unified diff