X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=7677af1faef38b85b6842fdf7d5b1bc8fd9c3119;hp=2dd5ad5cecf051d8a47feea5184810327394c7c7;hb=22d98520210487a6ad8cd70c3fa711c382ffa6ca;hpb=78d247dc5e6d5e64a4ab848702c23ce81b6fc615 diff --git a/src/run.ml b/src/run.ml index 2dd5ad5..7677af1 100644 --- a/src/run.ml +++ b/src/run.ml @@ -14,6 +14,8 @@ (***********************************************************************) INCLUDE "utils.ml" +INCLUDE "debug.ml" + open Format open Misc @@ -130,8 +132,6 @@ module Make (T : Tree.S) = (* The automaton to be run *) status : NodeStatus.t array; (* A mapping from node preorders to NodeStatus *) - unstable : Bitvector.t; - (* A bitvector remembering whether a subtree is stable *) mutable redo : bool; (* A boolean indicating whether the run is incomplete *) mutable pass : int; @@ -155,7 +155,6 @@ module Make (T : Tree.S) = tree = tree; auto = auto; status = Array.create len dummy_status; - unstable = Bitvector.create ~init:true len; redo = true; pass = 0; cache2 = Cache.N2.create dummy_form; @@ -251,15 +250,15 @@ DEFINE AND_(t1,t2) = let open NodeSummary in match a.Atom.node with | Move (m, q) -> - let { NodeStatus.node = n_sum; _ } as sum = + let down, ({ NodeStatus.node = n_sum; _ } as sum) = match m with - `First_child -> fcs - | `Next_sibling -> nss - | `Parent | `Previous_sibling -> ps - | `Stay -> ss + `First_child -> true, fcs + | `Next_sibling -> true, nss + | `Parent | `Previous_sibling -> false, ps + | `Stay -> false, ss in if sum == dummy_status - || n_sum.rank < ss.NodeStatus.node.rank + || (down && n_sum.rank < ss.NodeStatus.node.rank) || StateSet.mem q n_sum.todo then Unknown else @@ -289,23 +288,12 @@ DEFINE AND_(t1,t2) = in let v = eval_form phi fcs nss ps old_status old_summary in -(* - Logger.msg `STATS "Evaluating for tag %a, state %a@\ncontext: %a@\nleft: %a@\nright: %a@\n\t formula %a yields %s" - QName.print tag - State.print q - NodeStatus.print old_status - NodeStatus.print fcs - NodeStatus.print nss - Ata.Formula.print phi - (match v with True -> "True" | False -> "False" | _ -> "Unknown"); -*) match v with True -> StateSet.add q a_sat, a_todo | False -> acc | Unknown -> a_sat, StateSet.add q a_todo ) old_todo (old_sat, StateSet.empty) in - (* Logger.msg `STATS ""; *) if old_sat != sat || old_todo != todo then NodeStatus.make { os_node with sat; todo } else old_status @@ -339,12 +327,15 @@ DEFINE AND_(t1,t2) = let status = run.status in let cache2 = run.cache2 in let cache5 = run.cache5 in - let unstable = run.unstable in let states_by_rank = Ata.get_states_by_rank auto in - let init_todo = states_by_rank.(i) in + let td_todo = states_by_rank.(i) in + let bu_todo = if i + 1 = Array.length states_by_rank then StateSet.empty + else + states_by_rank.(i+1) + in let rec loop node = let node_id = T.preorder tree node in - if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false else begin + if node != T.nil then begin let parent = T.parent tree node in let fc = T.first_child tree node in let fc_id = T.preorder tree fc in @@ -352,7 +343,6 @@ DEFINE AND_(t1,t2) = let ns_id = T.preorder tree ns in let tag = T.tag tree node in (* We enter the node from its parent *) - let status0 = let c = unsafe_get_status status node_id in if c.NodeStatus.node.rank < i then @@ -360,7 +350,7 @@ DEFINE AND_(t1,t2) = NodeStatus.make { rank = i; sat = c.NodeStatus.node.sat; - todo = init_todo; + todo = td_todo; summary = let summary = c.NodeStatus.node.summary in if summary != NodeSummary.dummy then summary @@ -374,77 +364,65 @@ DEFINE AND_(t1,t2) = } else c in - IFTRACE(html tree node _i status0 "Entering node"); - (* get the node_statuses for the first child, next sibling and parent *) let ps = unsafe_get_status status (T.preorder tree parent) in let fcs = unsafe_get_status status fc_id in let nss = unsafe_get_status status ns_id in (* evaluate the transitions with all this statuses *) - let status1 = if status0.NodeStatus.node.todo == StateSet.empty then status0 else begin - let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in - IFTRACE(html tree node _i status1 "Updating transitions"); + let status1 = + if status0.NodeStatus.node.todo == StateSet.empty then status0 + else begin + let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in (* update the cache if the status of the node changed *) - if status1 != status0 then status.(node_id) <- status1; - status1 - end + if status1 != status0 then status.(node_id) <- status1; + status1 + end in (* recursively traverse the first child *) - let unstable_left = loop fc in + let () = loop fc in (* here we re-enter the node from its first child, get the new status of the first child *) let fcs1 = unsafe_get_status status fc_id in (* update the status *) - let status2 = if status1.NodeStatus.node.todo == StateSet.empty then status1 else begin - let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in - IFTRACE(html tree node _i status2 "Updating transitions (after first-child)"); - if status2 != status1 then status.(node_id) <- status2; - status2 - end + let status1 = if status1.NodeStatus.node.rank < i then + NodeStatus.make { status1.NodeStatus.node with + rank = i; + todo = bu_todo } + else + status1 in - let unstable_right = loop ns in + let status2 = + if status1.NodeStatus.node.todo == StateSet.empty then status1 + else begin + let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in + if status2 != status1 then status.(node_id) <- status2; + status2 + end + in + let () = loop ns in let nss1 = unsafe_get_status status ns_id in - let status3 = if status2.NodeStatus.node.todo == StateSet.empty then status2 else begin + if status2.NodeStatus.node.todo != StateSet.empty then let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in - IFTRACE(html tree node _i status3 "Updating transitions (after next-sibling)"); - if status3 != status2 then status.(node_id) <- status3; - status3 - end - in - let unstable_self = - (* if either our left or right child is unstable or if we still have transitions - pending, the current node is unstable *) - unstable_left - || unstable_right - || StateSet.empty != status3.NodeStatus.node.todo - in - Bitvector.unsafe_set unstable node_id unstable_self; - IFTRACE((if not unstable_self then - Html.finalize_node - node_id - _i - Ata.(StateSet.intersect status3.NodeStatus.node.sat (get_selecting_states auto)))); - unstable_self + if status3 != status2 then status.(node_id) <- status3 end in - run.redo <- loop (T.root tree); - run.pass <- run.pass + 1 + loop (T.root tree) let get_results run = let cache = run.status in let auto = run.auto in let tree = run.tree in + let sel_states = Ata.get_selecting_states auto in let rec loop node acc = if node == T.nil then acc else let acc0 = loop (T.next_sibling tree node) acc in let acc1 = loop (T.first_child tree node) acc0 in - if Ata.( - StateSet.intersect - cache.(T.preorder tree node).NodeStatus.node.sat - (get_selecting_states auto)) then node::acc1 + if StateSet.intersect + cache.(T.preorder tree node).NodeStatus.node.sat + sel_states then node::acc1 else acc1 in loop (T.root tree) [] @@ -518,7 +496,8 @@ DEFINE AND_(t1,t2) = let run = make auto tree in prepare_run run nodes; for i = 0 to Ata.get_max_rank auto do - top_down run + top_down run; + run.pass <- run.pass + 1 done; pass := Ata.get_max_rank auto + 1; IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);