(Ata.TransList.print ~sep:"<br/>") config.todo i
+ let debug msg tree node i config =
+ let config = config.NodeStatus.node in
+ eprintf
+ "DEBUG:%s node: %i\nsat: %a\nunsat: %a\ntodo: %around: %i\n"
+ msg
+ (T.preorder tree node)
+ StateSet.print config.sat
+ StateSet.print config.unsat
+ (Ata.TransList.print ~sep:"\n") config.todo i
+
let get_trans cache2 auto tag states =
let trs =
in
loop phi
+ 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
let eval_trans cache4 fcs nss ps ss =
let res = Cache.N4.find cache4 oid fcsid nssid psid in
if res != dummy_status then res
else
- let { sat = old_sat;
- unsat = old_unsat;
- todo = old_todo;
- summary = old_summary } = old_config.NodeStatus.node
+ let new_config =
+ eval_trans_aux cache4 fcs nss ps ss old_config
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
Cache.N4.add cache4 oid fcsid nssid psid new_config;
new_config
in
- let top_down node run =
+ let top_down run =
let tree = run.tree in
let auto = run.auto in
let status = run.status in
let c = unsafe_get_status status node_id in
if c == dummy_status then
(* first time we visit the node *)
+ let ltrs = get_trans cache2 auto tag (Ata.get_states auto) in
NodeStatus.make
- { c.NodeStatus.node with
- todo = get_trans cache2 auto tag (Ata.get_states auto);
+ { sat = StateSet.empty;
+ unsat = Ata.get_starting_states auto;
+ todo = ltrs;
summary = NodeSummary.make
(node == T.first_child tree parent) (* is_left *)
(node == T.next_sibling tree parent) (* is_right *)
unstable_self
end
in
- run.redo <- loop node;
+ run.redo <- loop (T.root tree);
run.pass <- run.pass + 1
(*
loop (T.root tree) []
- let eval auto tree node =
+ let get_full_results run =
+ let cache = run.status in
+ let auto = run.auto in
+ let tree = run.tree in
+ let res_mapper = Hashtbl.create MED_H_SIZE in
+ let () =
+ StateSet.iter
+ (fun q -> Hashtbl.add res_mapper q [])
+ (Ata.get_selecting_states auto)
+ in
+ let rec loop node =
+ if node != T.nil then
+ let () = loop (T.next_sibling tree node) in
+ let () = loop (T.first_child tree node) in
+ StateSet.iter
+ (fun q ->
+ try
+ let acc = Hashtbl.find res_mapper q in
+ Hashtbl.replace res_mapper q (node::acc)
+ with
+ Not_found -> ())
+ cache.(T.preorder tree node).NodeStatus.node.sat
+ in
+ loop (T.root tree);
+ StateSet.fold
+ (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
+ (Ata.get_selecting_states auto) []
+
+ let prepare_run run list =
+ let tree = run.tree in
+ let auto = run.auto in
+ let status = run.status in
+ let cache2 = run.cache2 in
+ List.iter (fun node ->
+ let parent = T.parent tree node in
+ let fc = T.first_child tree node in
+ let ns = T.next_sibling tree node in
+ let tag = T.tag tree node in
+
+ let status0 =
+ NodeStatus.make
+ { sat = Ata.get_starting_states auto;
+ unsat = StateSet.empty;
+ todo = get_trans cache2 auto tag (Ata.get_states auto);
+ summary = NodeSummary.make
+ (node == T.first_child tree parent) (* is_left *)
+ (node == T.next_sibling tree parent) (* is_right *)
+ (fc != T.nil) (* has_left *)
+ (ns != T.nil) (* has_right *)
+ (T.kind tree node) (* kind *)
+ }
+ in
+ let node_id = T.preorder tree node in
+ status.(node_id) <- status0) list
+
+
+ let eval full auto tree nodes =
let run = make auto tree in
- while run.redo do top_down node run done;
- get_results run
+ prepare_run run nodes;
+ while run.redo do
+ top_down run
+ done;
+ if full then `Full (get_full_results run)
+ else `Normal (get_results run)
+
+
+ let full_eval auto tree nodes =
+ match eval true auto tree nodes with
+ `Full l -> l
+ | _ -> assert false
+
+ let eval auto tree nodes =
+ match eval false auto tree nodes with
+ `Normal l -> l
+ | _ -> assert false
+
end
projects / tatoo.git / blobdiff