X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=1f59ef891969261c1b9b63f9bddf2521460145db;hp=31eb26c650486e188d493bbc956794b766bdb3f2;hb=e56b9fbeaed04c1f2fb7019de34f7d8e87d6db73;hpb=5f1d396f4a04c9a0c6bb3da4176fd47a4473d35d diff --git a/src/run.ml b/src/run.ml index 31eb26c..1f59ef8 100644 --- a/src/run.ml +++ b/src/run.ml @@ -21,21 +21,21 @@ open Misc type stats = { run : int; tree_size : int; - cache2_access : int; - cache2_hit : int; - cache5_access : int; - cache5_hit : int; + fetch_trans_cache_access : int; + fetch_trans_cache_hit : int; + eval_trans_cache_access : int; + eval_trans_cache_hit : int; } -let cache2_hit = ref 0 -let cache2_access = ref 0 -let cache5_hit = ref 0 -let cache5_access = ref 0 +let fetch_trans_cache_hit = ref 0 +let fetch_trans_cache_access = ref 0 +let eval_trans_cache_hit = ref 0 +let eval_trans_cache_access = ref 0 let reset_stat_counters () = - cache2_hit := 0; - cache2_access := 0; - cache5_hit := 0; - cache5_access := 0 + fetch_trans_cache_hit := 0; + fetch_trans_cache_access := 0; + eval_trans_cache_hit := 0; + eval_trans_cache_access := 0 module Make (T : Tree.S) = @@ -48,44 +48,40 @@ module Make (T : Tree.S) = type t = int let dummy = -1 (* - 4444444444443210 - 4 -> kind - 3 -> is_left - 2 -> is_right + 333333333333333210 + 3333 -> kind + 2 -> has_right 1 -> has_left - 0 -> has_right + 0 -> is_left/is_right *) + let is_left (s : t) : bool = + s land 1 == 1 - let has_right (s : t) : bool = - Obj.magic (s land 1) + let is_right (s : t) : bool = + s land 1 == 0 let has_left (s : t) : bool = - Obj.magic ((s lsr 1) land 1) + (s lsr 1) land 1 == 1 - let is_right (s : t) : bool = - Obj.magic ((s lsr 2) land 1) - - let is_left (s : t) : bool = - Obj.magic ((s lsr 3) land 1) + let has_right (s : t) : bool = + (s lsr 2) land 1 == 1 let kind (s : t) : Tree.NodeKind.t = - Obj.magic (s lsr 4) + Obj.magic (s lsr 3) - let make is_left is_right has_left has_right kind = - ((Obj.magic kind) lsl 4) lor - ((int_of_bool is_left) lsl 3) lor - ((int_of_bool is_right) lsl 2) lor + let make is_left has_left has_right kind = + (int_of_bool is_left) lor ((int_of_bool has_left) lsl 1) lor - (int_of_bool has_right) - + ((int_of_bool has_right) lsl 2) lor + ((Obj.magic kind) lsl 3) end type node_status = { rank : int; sat : StateSet.t; (* States that are satisfied at the current node *) todo : StateSet.t; (* States that remain to be proven *) - (* For every node_status and automaton a, - a.states - (sat U todo) = unsat *) + (* For every node_status and automaton a, + a.states - (sat U todo) = unsat *) summary : NodeSummary.t; (* Summary of the shape of the node *) } (* Describe what is kept at each node for a run *) @@ -132,21 +128,13 @@ 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; - (* The number of times this run was updated *) - mutable cache2 : Ata.Formula.t Cache.N2.t; + mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t; (* A cache from states * label to list of transitions *) - mutable cache5 : NodeStatus.t Cache.N5.t; + mutable td_cache : NodeStatus.t Cache.N5.t; + mutable bu_cache : NodeStatus.t Cache.N5.t; } - let pass r = r.pass - let stable r = not r.redo - let auto r = r.auto - let tree r = r.tree let dummy_form = Ata.Formula.stay State.dummy @@ -157,11 +145,10 @@ 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; - cache5 = Cache.N5.create dummy_status; + fetch_trans_cache = Cache.N2.create dummy_form; + td_cache = Cache.N5.create dummy_status; + bu_cache = Cache.N5.create dummy_status; } let get_status a i = @@ -196,21 +183,21 @@ END StateSet.print config.todo i - let get_form cache2 auto tag q = + let get_form fetch_trans_cache auto tag q = let phi = - incr cache2_access; - Cache.N2.find cache2 (tag.QName.id :> int) (q :> int) + incr fetch_trans_cache_access; + Cache.N2.find fetch_trans_cache (tag.QName.id :> int) (q :> int) in if phi == dummy_form then let phi = Ata.get_form auto tag q in let () = Cache.N2.add - cache2 + fetch_trans_cache (tag.QName.id :> int) (q :> int) phi in phi else begin - incr cache2_hit; + incr fetch_trans_cache_hit; phi end @@ -279,7 +266,7 @@ DEFINE AND_(t1,t2) = loop phi - let eval_trans_aux auto cache2 tag fcs nss ps old_status = + let eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status = let { sat = old_sat; todo = old_todo; summary = old_summary } as os_node = old_status.NodeStatus.node @@ -287,7 +274,7 @@ DEFINE AND_(t1,t2) = let sat, todo = StateSet.fold (fun q ((a_sat, a_todo) as acc) -> let phi = - get_form cache2 auto tag q + get_form fetch_trans_cache auto tag q in let v = eval_form phi fcs nss ps old_status old_summary in @@ -302,45 +289,44 @@ DEFINE AND_(t1,t2) = else old_status - let eval_trans auto cache2 cache5 tag fcs nss ps ss = - let rec loop old_status = - let new_status = - eval_trans_aux auto cache2 tag fcs nss ps old_status - in - if new_status == old_status then old_status else loop new_status + let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps old_status = + let new_status = + eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status in + if new_status == old_status then old_status else + eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_status + + + let eval_trans auto fetch_trans_cache td_cache tag fcs nss ps ss = let fcsid = (fcs.NodeStatus.id :> int) in let nssid = (nss.NodeStatus.id :> int) in let psid = (ps.NodeStatus.id :> int) in let ssid = (ss.NodeStatus.id :> int) in let tagid = (tag.QName.id :> int) in - let res = Cache.N5.find cache5 tagid ssid fcsid nssid psid in - incr cache5_access; - if res != dummy_status then begin incr cache5_hit; res end - else let new_status = loop ss in - Cache.N5.add cache5 tagid ssid fcsid nssid psid new_status; + let res = Cache.N5.find td_cache tagid ssid fcsid nssid psid in + incr eval_trans_cache_access; + if res != dummy_status then begin incr eval_trans_cache_hit; res end + else let new_status = eval_trans_fix auto fetch_trans_cache tag fcs nss ps ss in + Cache.N5.add td_cache tagid ssid fcsid nssid psid new_status; new_status - - let top_down run = let i = run.pass in let tree = run.tree in let auto = run.auto in let status = run.status in - let cache2 = run.cache2 in - let cache5 = run.cache5 in - let unstable = run.unstable in + let fetch_trans_cache = run.fetch_trans_cache in + let td_cache = run.td_cache in + let bu_cache = run.bu_cache in let states_by_rank = Ata.get_states_by_rank auto 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 + let rec loop_td_and_bu node = + if node == T.nil then () else begin + let node_id = T.preorder tree node in let parent = T.parent tree node in let fc = T.first_child tree node in let fc_id = T.preorder tree fc in @@ -348,7 +334,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 @@ -357,20 +342,18 @@ DEFINE AND_(t1,t2) = { rank = i; sat = c.NodeStatus.node.sat; todo = td_todo; - summary = let summary = c.NodeStatus.node.summary - in - if summary != NodeSummary.dummy then summary - else - 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 *) + summary = + let summary = c.NodeStatus.node.summary in + if summary != NodeSummary.dummy then summary + else + NodeSummary.make + (node != T.next_sibling tree parent) + (fc != T.nil) (* has_left *) + (ns != T.nil) (* has_right *) + (T.kind tree node) (* kind *) } 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 @@ -379,15 +362,14 @@ DEFINE AND_(t1,t2) = 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 = eval_trans auto fetch_trans_cache td_cache 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 in (* recursively traverse the first child *) - let unstable_left = loop fc in + let () = loop_td_and_bu 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 @@ -402,61 +384,80 @@ DEFINE AND_(t1,t2) = 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)"); + let status2 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss ps status1 in if status2 != status1 then status.(node_id) <- status2; status2 end in - let unstable_right = loop ns in + let () = loop_td_and_bu 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)"); - 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 + if status2.NodeStatus.node.todo != StateSet.empty then + let status3 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss1 ps status2 in + if status3 != status2 then status.(node_id) <- status3 + end + and loop_td_only node = + if node == T.nil then () else begin + let node_id = T.preorder tree node in + let parent = T.parent tree node in + let fc = T.first_child tree node in + let fc_id = T.preorder tree fc in + let ns = T.next_sibling tree node in + 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 + (* first time we visit the node during this run *) + NodeStatus.make + { rank = i; + sat = c.NodeStatus.node.sat; + todo = td_todo; + summary = + let summary = c.NodeStatus.node.summary in + if summary != NodeSummary.dummy then summary + else + NodeSummary.make + (node != T.next_sibling tree parent) + (fc != T.nil) (* has_left *) + (ns != T.nil) (* has_right *) + (T.kind tree node) (* kind *) + } + else c 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 + (* 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 *) + if status0.NodeStatus.node.todo != StateSet.empty then begin + let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in + (* update the cache if the status of the node changed *) + if status1 != status0 then status.(node_id) <- status1; + end; + (* recursively traverse the first child *) + loop_td_only fc; + loop_td_only ns end in - run.redo <- loop (T.root tree); - run.pass <- run.pass + 1 + if bu_todo == StateSet.empty then loop_td_only (T.root tree) + else loop_td_and_bu (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) [] @@ -512,8 +513,7 @@ DEFINE AND_(t1,t2) = todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto); summary = NodeSummary.make - (node == T.first_child tree parent) (* is_left *) - (node == T.next_sibling tree parent) (* is_right *) + (node != T.next_sibling tree parent) (* is_left *) (fc != T.nil) (* has_left *) (ns != T.nil) (* has_right *) (T.kind tree node) (* kind *) @@ -530,7 +530,10 @@ 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; + run.td_cache <- Cache.N5.create dummy_status; + run.bu_cache <- Cache.N5.create dummy_status; done; pass := Ata.get_max_rank auto + 1; IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree); @@ -548,10 +551,10 @@ DEFINE AND_(t1,t2) = let stats () = { tree_size = !tree_size; run = !pass; - cache2_access = !cache2_access; - cache2_hit = !cache2_hit; - cache5_access = !cache5_access; - cache5_hit = !cache5_hit; + fetch_trans_cache_access = !fetch_trans_cache_access; + fetch_trans_cache_hit = !fetch_trans_cache_hit; + eval_trans_cache_access = !eval_trans_cache_access; + eval_trans_cache_hit = !eval_trans_cache_hit; } end