+ let eval_trans_aux cache4 fcs nss ps ss old_config =
+ let { sat = old_sat;
+ unsat = old_unsat;
+ todo = old_todo;
+ summary = old_summary } = old_config.NodeStatus.node
+ in
+ let sat, unsat, removed, kept, todo =
+ Ata.TransList.fold
+ (fun trs acc ->
+ let q, lab, phi = Ata.Transition.node trs in
+ let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in
+ if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else
+ let new_phi =
+ eval_form phi fcs nss ps old_config old_summary
+ in
+ if Ata.Formula.is_true new_phi then
+ StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
+ else if Ata.Formula.is_false new_phi then
+ a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
+ else
+ let new_tr = Ata.Transition.make (q, lab, new_phi) in
+ (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo))
+ ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
+ in
+ (* States that have been removed from the todo list and not kept are now
+ unsatisfiable *)
+ let unsat = StateSet.union unsat (StateSet.diff removed kept) in
+ (* States that were found once to be satisfiable remain so *)
+ let unsat = StateSet.diff unsat sat in
+ let new_config = NodeStatus.make { old_config.NodeStatus.node with sat; unsat; todo; } in
+ new_config
+