X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=df9397b95949a175223967d1c7c6d007aa8ca6a9;hp=d7d5177a3275c5dc175a1b8beccdaaccaec5c499;hb=e9b4969905125718589b18ff6286e05688f7a929;hpb=be588f7af67f6b24aa423ff374c0f1c058e64951 diff --git a/src/run.ml b/src/run.ml index d7d5177..df9397b 100644 --- a/src/run.ml +++ b/src/run.ml @@ -221,6 +221,81 @@ END 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 = @@ -233,35 +308,9 @@ END 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 - 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) + let new_config = + eval_trans_aux cache4 fcs nss ps ss old_config 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 @@ -294,10 +343,11 @@ END 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 { sat = StateSet.empty; unsat = Ata.get_starting_states auto; - todo = get_trans cache2 auto tag (Ata.get_states auto); + todo = ltrs; summary = NodeSummary.make (node == T.first_child tree parent) (* is_left *) (node == T.next_sibling tree parent) (* is_right *) @@ -416,6 +466,35 @@ END in loop (T.root tree) [] + + 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 @@ -444,12 +523,24 @@ END status.(node_id) <- status0) list - - let eval auto tree nodes = + let eval full auto tree nodes = let run = make auto tree in prepare_run run nodes; while run.redo do - top_down run; + top_down run done; - get_results run + 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