+ type trivalent = False | True | Unknown
+
+ let or_ t1 t2 = match t1 with
+ False -> t2
+ | True -> True
+ | Unknown -> if t2 == True then True else Unknown
+
+ let and_ t1 t2 = match t1 with
+ False -> False
+ | True -> t2
+ | Unknown -> if t2 == False then False else Unknown
+ let of_bool = function false -> False | true -> True
+
+ let eval_form phi fcs nss ps ss summary =
+ let open Ata in
+ let rec loop phi =
+ begin match Formula.expr phi with
+ | Boolean.False -> False
+ | Boolean.True -> True
+ | Boolean.Atom (a, b) ->
+ begin
+ let open NodeSummary in
+ match a.Atom.node with
+ | Move (m, q) ->
+ let sum = match m with
+ `First_child -> fcs
+ | `Next_sibling -> nss
+ | `Parent | `Previous_sibling -> ps
+ | `Stay -> ss
+ in
+ if StateSet.mem q sum.NodeStatus.node.sat then of_bool b
+ else if StateSet.mem q sum.NodeStatus.node.unsat then of_bool (not b)
+ else Unknown
+ | Is_first_child -> of_bool (b == is_left summary)
+ | Is_next_sibling -> of_bool (b == is_right summary)
+ | Is k -> of_bool (b == (k == kind summary))
+ | Has_first_child -> of_bool (b == has_left summary)
+ | Has_next_sibling -> of_bool (b == has_right summary)
+ end
+ | Boolean.And(phi1, phi2) -> and_ (loop phi1) (loop phi2)
+ | Boolean.Or (phi1, phi2) -> or_ (loop phi1) (loop phi2)
+ end
+ in
+ loop phi
+
+
+ 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 phi_val =
+ eval_form phi fcs nss ps old_config old_summary
+ in
+ match phi_val with
+ | False -> a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
+ | True -> StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
+ | Unknown ->
+ (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons trs 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