| 68 |
68 |
mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
|
| 69 |
69 |
|
| 70 |
70 |
let rec unless_read reads handler =
|
|
71 |
let res =
|
| 71 |
72 |
List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_unless
|
|
73 |
in
|
|
74 |
(
|
|
75 |
(*
|
|
76 |
Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
|
|
77 |
Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
|
|
78 |
*)
|
|
79 |
res
|
|
80 |
)
|
| 72 |
81 |
|
| 73 |
82 |
let rec until_read reads handler =
|
| 74 |
83 |
List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_until
|
| ... | ... | |
| 79 |
88 |
List.fold_left (fun read stmt ->
|
| 80 |
89 |
match stmt with
|
| 81 |
90 |
| Eq eq -> get_expr_vars read eq.eq_rhs
|
| 82 |
|
| Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts
|
| 83 |
|
in ISet.diff allvars locals
|
|
91 |
| Aut aut -> automata_read read aut) reads handler.hand_stmts
|
|
92 |
in let res = ISet.diff allvars locals
|
|
93 |
in
|
|
94 |
(
|
|
95 |
(*
|
|
96 |
Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements allvars);
|
|
97 |
Format.eprintf "handler_read %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
|
|
98 |
*)
|
|
99 |
res
|
|
100 |
)
|
|
101 |
|
|
102 |
and automata_read reads aut =
|
|
103 |
List.fold_left (fun read handler -> until_read (handler_read (unless_read read handler) handler) handler) reads aut.aut_handlers
|
| 84 |
104 |
|
| 85 |
105 |
let rec handler_write writes handler =
|
| 86 |
106 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
|
| ... | ... | |
| 117 |
137 |
[aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s]
|
| 118 |
138 |
|
| 119 |
139 |
let node_of_unless nused used node aut_id aut_state handler =
|
|
140 |
(*Format.eprintf "node_of_unless %s@." node.node_id;*)
|
| 120 |
141 |
let inputs = unless_read ISet.empty handler in
|
| 121 |
142 |
let var_inputs = aut_state.incoming_r :: aut_state.incoming_s :: (node_vars_of_idents node inputs) in
|
| 122 |
143 |
let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in
|
| ... | ... | |
| 160 |
181 |
(fun name -> try IMap.find name table with Not_found -> name)
|
| 161 |
182 |
|
| 162 |
183 |
let node_of_assign_until nused used node aut_id aut_state handler =
|
|
184 |
(*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
|
| 163 |
185 |
let writes = handler_write ISet.empty handler in
|
| 164 |
186 |
let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in
|
| 165 |
187 |
let frename = mk_frename used writes in
|
Bug solved in automaton part