X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=31eb26c650486e188d493bbc956794b766bdb3f2;hp=2dd5ad5cecf051d8a47feea5184810327394c7c7;hb=5f1d396f4a04c9a0c6bb3da4176fd47a4473d35d;hpb=78d247dc5e6d5e64a4ab848702c23ce81b6fc615 diff --git a/src/run.ml b/src/run.ml index 2dd5ad5..31eb26c 100644 --- a/src/run.ml +++ b/src/run.ml @@ -14,6 +14,8 @@ (***********************************************************************) INCLUDE "utils.ml" +INCLUDE "debug.ml" + open Format open Misc @@ -251,15 +253,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 +291,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 @@ -341,10 +332,15 @@ DEFINE AND_(t1,t2) = 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 (*|| not (Bitvector.get unstable node_id)*) then false + else begin let parent = T.parent tree node in let fc = T.first_child tree node in let fc_id = T.preorder tree fc in @@ -360,7 +356,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 @@ -375,19 +371,20 @@ 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 + IFTRACE(html tree node _i status1 "Updating transitions"); (* 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 @@ -395,25 +392,39 @@ DEFINE AND_(t1,t2) = 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 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 in let unstable_right = 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 - let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in - IFTRACE(html tree node _i status3 "Updating transitions (after next-sibling)"); + let status3 = + if status2.NodeStatus.node.todo == StateSet.empty then status2 + else begin + 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 *) + (* 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 @@ -423,7 +434,8 @@ DEFINE AND_(t1,t2) = Html.finalize_node node_id _i - Ata.(StateSet.intersect status3.NodeStatus.node.sat (get_selecting_states auto)))); + Ata.(StateSet.intersect status3.NodeStatus.node.sat + (get_selecting_states auto)))); unstable_self end in