Revision 6a1a01d2 src/automata.ml
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