From: Kim Nguyễn Date: Wed, 14 May 2014 23:08:04 +0000 (+0200) Subject: Implement a new automaton run (non optimized) with cleaner semantics w.r.t. ranked... X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=3b9dbcd9318dba41999dc6cc43093edbe5bc4c5d Implement a new automaton run (non optimized) with cleaner semantics w.r.t. ranked states. Paves the way for a "real" bottom-up run. --- diff --git a/src/ata.ml b/src/ata.ml index 9ad2b12..939586f 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -212,6 +212,9 @@ struct Formula.print f sep) l end +type rank = { td : StateSet.t; + bu : StateSet.t; + exit : StateSet.t } type t = { @@ -220,7 +223,7 @@ type t = { mutable starting_states : StateSet.t; mutable selecting_states: StateSet.t; transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t; - mutable ranked_states : (StateSet.t*StateSet.t) array + mutable ranked_states : rank array } let uid t = t.id @@ -252,8 +255,10 @@ let print fmt a = (StateSet.cardinal a.states) StateSet.print a.starting_states StateSet.print a.selecting_states - (let r = ref 0 in Pretty.print_array ~sep:", " (fun ppf (s1,s2) -> - fprintf ppf "(%i:%a,%a)" !r StateSet.print s1 StateSet.print s2; incr r)) a.ranked_states; + (let r = ref 0 in Pretty.print_array ~sep:", " (fun ppf s -> + fprintf ppf "(%i:{td=%a,bu=%a,exit=%a)" !r + StateSet.print s.td StateSet.print s.bu StateSet.print s.exit; + incr r)) a.ranked_states; let trs = Hashtbl.fold (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t) @@ -453,6 +458,7 @@ let state_prerequisites dir auto q = StateSet.union prereq acc) StateSet.empty trans + let compute_rank auto = let dependencies = compute_dependencies auto in let upward = [ `Stay ; `Parent ; `Previous_sibling ] in @@ -503,24 +509,37 @@ let compute_rank auto = let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list; let rank = Hashtbl.length by_rank in - auto.ranked_states <- - Array.init rank - (fun i -> - let set = try Hashtbl.find by_rank i with Not_found -> StateSet.empty in - let source = - if i + 1 == rank then auto.selecting_states else - let post_set = Hashtbl.find by_rank (i+1) in - let source = if i + 1 == rank then post_set else - StateSet.fold (fun q acc -> - List.fold_left (fun acc m -> - StateSet.union acc (state_prerequisites m auto q )) - acc [`First_child; `Next_sibling; `Parent; `Previous_sibling; `Stay] - ) post_set StateSet.empty - in - StateSet.inter set source - in - (source, set) - ) + if rank mod 2 == 1 then Hashtbl.replace by_rank rank StateSet.empty; + let rank = Hashtbl.length by_rank in + assert (rank mod 2 == 0); + let rank_array = + Array.init (rank / 2) + (fun i -> + let td_set = Hashtbl.find by_rank (2 * i) in + let bu_set = Hashtbl.find by_rank (2 * i + 1) in + { td = td_set; bu = bu_set ; exit = StateSet.empty } + ) + in + let max_rank = Array.length rank_array - 1 in + for i = 0 to max_rank do + let this_rank = rank_array.(i) in + let exit = if i == max_rank then auto.selecting_states else + let next = rank_array.(i+1) in + let res = + StateSet.fold (fun q acc -> + List.fold_left (fun acc m -> + StateSet.union acc (state_prerequisites m auto q )) + acc [`First_child; `Next_sibling; `Parent; `Previous_sibling; `Stay] + ) (StateSet.union next.td next.bu) StateSet.empty + in + + StateSet.( + union auto.selecting_states ( inter res (union this_rank.td this_rank.bu))) + + in + rank_array.(i) <- {this_rank with exit = exit }; + done; + auto.ranked_states <- rank_array module Builder = @@ -608,7 +627,11 @@ let rename_states mapper a = (fun l -> (List.map (fun (labels, form) -> (labels, map_form rename form)) l)) a.transitions; - ranked_states = Array.map (fun (a,b) -> map_set rename a, map_set rename b) a.ranked_states + ranked_states = Array.map (fun s -> + { td = map_set rename s.td; + bu = map_set rename s.bu; + exit = map_set rename s.exit; + }) a.ranked_states } let copy a = diff --git a/src/ata.mli b/src/ata.mli index 815e20a..89593cc 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -122,7 +122,11 @@ val get_starting_states : t -> StateSet.t val get_selecting_states : t -> StateSet.t (** return the set of selecting states of the automaton *) -val get_states_by_rank : t -> (StateSet.t*StateSet.t) array +type rank = { td : StateSet.t; + bu : StateSet.t; + exit : StateSet.t } + +val get_states_by_rank : t -> rank array (** return an array of states (sources, states) ordered by ranks. *) diff --git a/src/naive_node_list.ml b/src/naive_node_list.ml deleted file mode 100644 index 1b32c47..0000000 --- a/src/naive_node_list.ml +++ /dev/null @@ -1,110 +0,0 @@ -(***********************************************************************) -(* *) -(* TAToo *) -(* *) -(* Kim Nguyen, LRI UMR8623 *) -(* Université Paris-Sud & CNRS *) -(* *) -(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) -(* Recherche Scientifique. All rights reserved. This file is *) -(* distributed under the terms of the GNU Lesser General Public *) -(* License, with the special exception on linking described in file *) -(* ../LICENSE. *) -(* *) -(***********************************************************************) - - -type node = Naive_tree.node -type cell = { node : node; - mutable next : cell } - -type iterator = cell - -type t = { mutable length : int; - mutable head : cell; - mutable last : cell; } - -let rec nil = { node = Naive_tree.nil; - next = nil } - -let create () = { length = 0; - head = nil; - last = nil } - -let iter f l = - let rec loop c = - if c != nil then begin - f c.node; - loop c.next - end - in - loop l.head - - - - -let length l = l.length -let is_empty l = l.head == nil - -let pop l = - if is_empty l then failwith "pop" - else - let v = l.head.node in - let nhead = l.head.next in - l.head <- nhead; - if nhead == nil then l.last <- nil; - v - - - -let add n l = - let ncell = { node = n; - next = nil } - in - if l.head == nil then begin - l.head <- ncell; - l.last <- ncell; - l.length <- 1 - end else begin - l.last.next <- ncell; - l.last <- ncell; - l.length <- l.length + 1 - end - -let push_back n l = add n l -let push_front n l = - let ncell = { node = n; - next = l.head } - in - if l.head == nil then begin - l.head <- ncell; - l.last <- ncell; - l.length <- 1; - end else begin - l.head <- ncell; - l.length <- l.length + 1; - end - -let append l1 l2 = - let len2 = l2.length in - if len2 != 0 then begin - l1.length <- l1.length + len2; - l1.last.next <- l2.head; - l1.last <- l2.last; - end; - l1 - -let head l = l.head -let last l = l.last -let next i = i.next -let value i = i.node -let finished i = i == nil - -let copy l = - let rec loop l2 i = - if finished i then l2 else begin - add (value i) l2; - loop l2 (next i) - end - in - loop (create ()) (head l) diff --git a/src/naive_node_list.mli b/src/naive_node_list.mli deleted file mode 100644 index e1fde9c..0000000 --- a/src/naive_node_list.mli +++ /dev/null @@ -1,17 +0,0 @@ -(***********************************************************************) -(* *) -(* TAToo *) -(* *) -(* Kim Nguyen, LRI UMR8623 *) -(* Université Paris-Sud & CNRS *) -(* *) -(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) -(* Recherche Scientifique. All rights reserved. This file is *) -(* distributed under the terms of the GNU Lesser General Public *) -(* License, with the special exception on linking described in file *) -(* ../LICENSE. *) -(* *) -(***********************************************************************) - - -include Node_list.S with type node = Naive_tree.node diff --git a/src/node_list.ml b/src/node_list.ml deleted file mode 100644 index 1856bb8..0000000 --- a/src/node_list.ml +++ /dev/null @@ -1,37 +0,0 @@ -(***********************************************************************) -(* *) -(* TAToo *) -(* *) -(* Kim Nguyen, LRI UMR8623 *) -(* Université Paris-Sud & CNRS *) -(* *) -(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) -(* Recherche Scientifique. All rights reserved. This file is *) -(* distributed under the terms of the GNU Lesser General Public *) -(* License, with the special exception on linking described in file *) -(* ../LICENSE. *) -(* *) -(***********************************************************************) - -module type S = - sig - type node - type t - type iterator - - val create : unit -> t - val add : node -> t -> unit - val push_front : node -> t -> unit - val push_back : node -> t -> unit - val pop : t -> node - val append : t -> t -> t - val iter : (node -> unit) -> t -> unit - val length : t -> int - val is_empty : t -> bool - val head : t -> iterator - val last : t -> iterator - val next : iterator -> iterator - val value : iterator -> node - val finished : iterator -> bool - val copy : t -> t - end diff --git a/src/run.ml b/src/run.ml index 167e0af..a39d8b4 100644 --- a/src/run.ml +++ b/src/run.ml @@ -16,378 +16,198 @@ INCLUDE "utils.ml" INCLUDE "debug.ml" -open Format -open Misc -open Bigarray -type stats = { mutable pass : int; - tree_size : int; - mutable fetch_trans_cache_access : int; - mutable fetch_trans_cache_hit : int; - mutable eval_trans_cache_access : int; - mutable eval_trans_cache_hit : int; - mutable nodes_per_run : int list; - } - -module NodeSummary = +module Make (T : Tree.S) = struct - (* Pack into an integer the result of the is_* and has_ predicates - for a given node *) - type t = int - let dummy = -1 - (* - ...44443210 - ...4444 -> kind - 3 -> has_right - 2 -> has_left - 1 -> is_right - 0 -> is_left - *) - let is_left (s : t) : bool = - s land 1 != 0 - - let is_right (s : t) : bool = - s land 0b10 != 0 - - let has_left (s : t) : bool = - s land 0b100 != 0 - - let has_right (s : t) : bool = - s land 0b1000 != 0 - - let kind (s : t) : Tree.NodeKind.t = - Obj.magic (s lsr 4) - - let make is_left is_right has_left has_right kind = - (int_of_bool is_left) lor - ((int_of_bool is_right) lsl 1) lor - ((int_of_bool has_left) lsl 2) lor - ((int_of_bool has_right) lsl 3) lor - ((Obj.magic kind) lsl 4) -end - -let dummy_set = StateSet.singleton State.dummy - - - - IFDEF HTMLTRACE - THEN -type sat_array = StateSet.t array list - DEFINE IFHTML(a,b) = (a) - ELSE -type sat_array = StateSet.t array - DEFINE IFHTML(a,b) = (b) - END - -let unsafe_get a i = - if i < 0 then StateSet.empty else - Array.unsafe_get (IFHTML(List.hd a, a)) i - -let unsafe_set a i v old_v = - if v != old_v then - Array.unsafe_set (IFHTML(List.hd a, a)) i v - -type 'a run = { - tree : 'a ; - (* The argument of the run *) - auto : Ata.t; - (* The automaton to be run *) - mutable sat: sat_array; - (* A mapping from node preorders to states satisfied at that node *) - mutable pass : int; - (* Number of run we have performed *) - mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t; - (* A cache from states * label to list of transitions *) - mutable td_cache : StateSet.t Cache.N6.t; - mutable bu_cache : StateSet.t Cache.N6.t; - (* Two 6-way caches used during the top-down and bottom-up phase - label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set - *) - node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; - stats : stats; -} -let dummy_form = Ata.Formula.stay State.dummy - -let get_form run tag q = - let auto = run.auto in - let fetch_trans_cache = run.fetch_trans_cache in - let stats = run.stats in - let phi = - stats.fetch_trans_cache_access <- stats.fetch_trans_cache_access + 1; - 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 - fetch_trans_cache - (tag.QName.id :> int) - (q :> int) phi - in phi - else begin - stats.fetch_trans_cache_hit <- stats.fetch_trans_cache_hit + 1; - phi - end - - -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 + let eval_form phi tree node fcs nss pars selfs = + let rec loop phi = + let open Boolean in + match Ata.Formula.expr phi with + False -> false + | True -> true + | Or (phi1, phi2) -> loop phi1 || loop phi2 + | And (phi1, phi2) -> loop phi1 && loop phi2 + | Atom (a, b) -> b == Ata.( + match Atom.node a with + Is_first_child -> let par = T.parent tree node in + (T.first_child tree par) == node + | Is_next_sibling -> let par = T.parent tree node in + (T.next_sibling tree par) == node + | Is k -> k == T.kind tree node + | Has_first_child -> T.nil != T.first_child tree node + | Has_next_sibling -> T.nil != T.next_sibling tree node | Move (m, q) -> - b && StateSet.mem q ( + let set = match m with `First_child -> fcs | `Next_sibling -> nss - | `Parent | `Previous_sibling -> ps - | `Stay -> ss - ) - | Is_first_child -> b == is_left summary - | Is_next_sibling -> b == is_right summary - | Is k -> b == (k == kind summary) - | Has_first_child -> b == has_left summary - | Has_next_sibling -> b == has_right summary - end - | Boolean.And(phi1, phi2) -> loop phi1 && loop phi2 - | Boolean.Or (phi1, phi2) -> loop phi1 || loop phi2 - end - in - loop phi - - -let eval_trans_aux run tag summary fcs nss ps sat todo = - StateSet.fold (fun q (a_sat) -> - let phi = - get_form run tag q + | `Parent + | `Previous_sibling -> pars + | `Stay -> selfs + in + StateSet.mem q set + ) in - if eval_form phi fcs nss ps a_sat summary then - StateSet.add q a_sat - else a_sat - ) todo sat - - -let rec eval_trans_fix run tag summary fcs nss ps sat todo = - let new_sat = - eval_trans_aux run tag summary fcs nss ps sat todo - in - if new_sat == sat then sat else - eval_trans_fix run tag summary fcs nss ps new_sat todo - - -let eval_trans run trans_cache tag summary fcs nss ps ss todo = - let stats = run.stats in - let fcsid = (fcs.StateSet.id :> int) in - let nssid = (nss.StateSet.id :> int) in - let psid = (ps.StateSet.id :> int) in - let ssid = (ss.StateSet.id :> int) in - let tagid = (tag.QName.id :> int) in - - let res = Cache.N6.find trans_cache tagid summary ssid fcsid nssid psid in - stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access; - if res != dummy_set then begin - stats.eval_trans_cache_hit <- 1 + stats.eval_trans_cache_hit; - res - end else let new_sat = - eval_trans_fix run tag summary fcs nss ps ss todo - in - Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat; - new_sat - - -module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = -struct - - let make auto tree = - let len = T.size tree in - let ba = Array1.create int16_unsigned c_layout len in - Array1.fill ba 0; - { - tree = tree; - auto = auto; - sat = (let a = Array.create len StateSet.empty in - IFHTML([a], a)); - pass = 0; - fetch_trans_cache = Cache.N2.create dummy_form; - td_cache = Cache.N6.create dummy_set; - bu_cache = Cache.N6.create dummy_set; - node_summaries = ba; - stats = { - pass = 0; - tree_size = len; - fetch_trans_cache_access = 0; - fetch_trans_cache_hit = 0; - eval_trans_cache_access = 0; - eval_trans_cache_hit = 0; - nodes_per_run = []; - } - } - - - let top_down run update_res = - let num_visited = ref 0 in - let i = run.pass in - let tree = run.tree in - let auto = run.auto in - let states_by_rank = Ata.get_states_by_rank auto in - let td_todo = snd states_by_rank.(i) in - let bu_todo = - if i == Array.length states_by_rank - 1 then StateSet.empty + loop phi + + + let eval_trans_aux trans tree node fcs nss pars selfs = + let open Ata in + TransList.fold (fun trs acc -> + let q, _ , phi = Transition.node trs in + let res = eval_form phi tree node fcs nss pars selfs in + if false then begin + Format.eprintf "Formula %a evaluates to %b with context: (fcs=%a, nss=%a, pars=%a, olds=%a) @\n@." + Formula.print phi res + StateSet.print fcs + StateSet.print nss + StateSet.print pars + StateSet.print selfs + end; + if res then + StateSet.add q acc else - snd (states_by_rank.(i+1)) + acc) trans selfs + + let eval_trans trans tree node fcs nss pars sstates = + let rec loop olds = + + let news = eval_trans_aux trans tree node fcs nss pars olds in + if false then begin + Format.eprintf "Saturating formula: olds=%a, news=%a@\n@." + StateSet.print olds + StateSet.print news + end; + if news == olds then olds else + loop news in - let last_run = i >= Array.length states_by_rank - 2 in - let rec loop_td_and_bu node parent parent_sat = - if node == T.nil then StateSet.empty - else begin - incr num_visited; - let tag = T.tag tree node in - let node_id = T.preorder tree node in - let fc = T.first_child tree node in - let ns = T.next_sibling tree node in - (* We enter the node from its parent *) - let summary = - let s = Array1.unsafe_get run.node_summaries node_id in - if s != 0 then s else - let s = - 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 - run.node_summaries.{node_id} <- s; s - in - let status0 = unsafe_get run.sat node_id in - (* get the node_statuses for the first child, next sibling and parent *) - (* evaluate the transitions with all this statuses *) - let status1 = - eval_trans run - run.td_cache tag - summary - (unsafe_get run.sat (T.preorder tree fc)) - (unsafe_get run.sat (T.preorder tree ns)) - parent_sat - status0 td_todo + let r = loop sstates in + if false then begin + Format.eprintf "Evaluating transitions (fcs=%a, nss=%a, pars=%a, olds=%a):@\n\t%a@." + StateSet.print fcs + StateSet.print nss + StateSet.print pars + StateSet.print sstates + (Ata.TransList.print ~sep:"\n\t") trans; + Format.eprintf "Got %a@\n@." StateSet.print r; + end; + r + + + let auto_run auto tree prev_nodes td_states bu_states exit_states _i = + if false then + Format.eprintf "Doing a td (with states: %a) and a bu (with states: %a), exit states are: %a @\n@." + StateSet.print td_states + StateSet.print bu_states + StateSet.print exit_states; + let rec loop res node parset = + if node == T.nil then StateSet.empty else begin + let set,lset,rset = + if Sequence.is_empty prev_nodes then + StateSet.(empty,empty,empty) + else + let set,lset,rset, node' = Sequence.peek prev_nodes in + if node == node' then begin + ignore (Sequence.pop prev_nodes); + set,lset,rset + end + else + StateSet.(empty,empty,empty) in - (* update the cache if the status of the node changed - unsafe_set run.sat node_id status1 status0;*) - if bu_todo == StateSet.empty then begin - unsafe_set run.sat node_id status1 status0; (* write the td_states *) - update_res false status1 node; - let _ = loop_td_and_bu fc node status1 in - loop_td_and_bu ns node status1 (* tail call *) - end else - let fcs1, nss1 = - if last_run then - let nss1 = loop_td_and_bu ns node status1 in - let fcs1 = loop_td_and_bu fc node status1 in - fcs1, nss1 - else - let fcs1 = loop_td_and_bu fc node status1 in - let nss1 = loop_td_and_bu ns node status1 in - fcs1, nss1 - in - let status2 = - eval_trans run run.bu_cache tag - summary fcs1 - nss1 - parent_sat - status1 bu_todo - in - unsafe_set run.sat node_id status2 status0; - if last_run && status2 != StateSet.empty then update_res true status2 node; - status2 + let tag = T.tag tree node in + let td_trans = Ata.get_trans auto tag td_states in + let status1 = eval_trans td_trans tree node lset rset parset set in + let fcs = loop res (T.first_child tree node) status1 in + let rres = Sequence.create () in + let nss = loop rres (T.next_sibling tree node) status1 in + let bu_trans = Ata.get_trans auto tag bu_states in + let status2 = eval_trans bu_trans tree node fcs nss parset status1 in + let mstates = StateSet.inter status2 exit_states in + if false then begin + Format.eprintf "On node %i (tag : %a) status0 = %a, status1 = %a, fcs = %a, nss = %a, par = %a, status2 = %a, mstates = %a@\n@." + (T.preorder tree node) + QName.print tag + StateSet.print set + StateSet.print status1 + StateSet.print fcs + StateSet.print nss + StateSet.print parset + StateSet.print status2 + StateSet.print mstates; + end; + if mstates != StateSet.empty then + Sequence.push_front (mstates, + StateSet.inter exit_states fcs, + StateSet.inter exit_states nss, node) res; + Sequence.append res rres; + status2 end in - let _ = loop_td_and_bu (T.root tree) T.nil dummy_set in - run.pass <- run.pass + 2; - run.stats.pass <- run.stats.pass + 1; - run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run - - + let res = Sequence.create () in + ignore (loop res (T.root tree) StateSet.empty); + if false then Format.eprintf "Finished pass: %i @\n-----------------------@\n@." _i; + res - let mk_update_result auto = - let sel_states = Ata.get_selecting_states auto in - let res = L.create () in - (fun prepend sat node -> - if StateSet.intersect sel_states sat then begin - if prepend then L.push_front node res else - L.push_back node res - end), - (fun () -> res) - let mk_update_full_result auto = - let dummy = L.create () in - let res_mapper = Cache.N1.create dummy in - let () = - StateSet.iter - (fun q -> Cache.N1.add res_mapper (q :> int) (L.create())) - (Ata.get_selecting_states auto) - in - (fun prepend sat node -> - StateSet.iter - (fun q -> - let res = Cache.N1.find res_mapper (q :> int) in - if res != dummy then begin - if prepend then L.push_front node res - else L.push_back node res - end - ) sat), - (fun () -> - StateSet.fold_right - (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc) - (Ata.get_selecting_states auto) []) + let prepare_run auto l = + let res = Sequence.create () in + let start = Ata.get_starting_states auto in + Sequence.iter (fun n -> Sequence.push_back (start, StateSet.empty, StateSet.empty, n) res) l; + res - let prepare_run run list = - let tree = run.tree in - let auto = run.auto in - let sat = IFHTML((List.hd run.sat), run.sat) in - let sat0 = Ata.get_starting_states auto in - L.iter (fun node -> - let node_id = T.preorder tree node in - sat.(node_id) <- sat0) list + let main_eval auto tree nodes = + let s_nodes = prepare_run auto nodes in + + let ranked_states = Ata.get_states_by_rank auto in + let acc = ref s_nodes in + let max_rank = Ata.get_max_rank auto in + for i = 0 to max_rank do + let open Ata in + let { td; bu; exit } = ranked_states.(i) in + acc := auto_run auto tree !acc td bu exit i; + if false then begin + Format.eprintf "Intermediate result is: @\n"; + Sequence.iter (fun (s,_,_, n) -> + Format.eprintf "{%a, %i (%a)} " + StateSet.print s + (T.preorder tree n) + QName.print (T.tag tree n)) !acc; + Format.eprintf "@\n@."; + end - let compute_run auto tree nodes update_res = - let run = make auto tree in - prepare_run run nodes; - let rank = Ata.get_max_rank auto in - while run.pass <= rank do - top_down run update_res; - IFHTML((run.sat <- (Array.copy (List.hd run.sat)) :: run.sat), ()); - run.td_cache <- Cache.N6.create dummy_set; - run.bu_cache <- Cache.N6.create dummy_set; done; - IFHTML((run.sat <- List.tl run.sat), ()); - IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,()); - run - - - let last_stats = ref None - - let full_eval auto tree nodes = - let update_full,get_full = mk_update_full_result auto in - let run = compute_run auto tree nodes update_full in - last_stats := Some run.stats; - get_full () + !acc let eval auto tree nodes = - let update_res,get_res = mk_update_result auto in - let run = compute_run auto tree nodes update_res in - last_stats := Some run.stats; - get_res () + let res = main_eval auto tree nodes in + let r = Sequence.create () in + Sequence.iter (fun (_,_,_, n) -> Sequence.push_back n r) res; + r - let stats () = match !last_stats with - Some s -> s.nodes_per_run <- List.rev s.nodes_per_run;s - | None -> failwith "Missing stats" + let full_eval auto tree nodes = + let res = main_eval auto tree nodes in + let dummy = Sequence.create () in + let cache = Cache.N1.create dummy in + Sequence.iter (fun (set, _, _, n) -> + StateSet.iter (fun q -> + let qres = Cache.N1.find cache q in + let qres = + if qres == dummy then begin + let s = Sequence.create () in + Cache.N1.add cache q s; + s + end + else qres + in + Sequence.push_back n qres) set ) + res; + let l = StateSet.fold (fun q acc -> + let res = Cache.N1.find cache q in + (q, res) :: acc) (Ata.get_selecting_states auto) [] + in + List.rev l end diff --git a/src/run.mli b/src/run.mli index c942277..7704494 100644 --- a/src/run.mli +++ b/src/run.mli @@ -14,18 +14,8 @@ (***********************************************************************) -type stats = private { mutable pass : int; - tree_size : int; - mutable fetch_trans_cache_access : int; - mutable fetch_trans_cache_hit : int; - mutable eval_trans_cache_access : int; - mutable eval_trans_cache_hit : int; - mutable nodes_per_run : int list; - } - -module Make (T : Tree.S) (L : Node_list.S with type node = T.node) : +module Make (T : Tree.S) : sig - val eval : Ata.t -> T.t -> L.t -> L.t - val full_eval : Ata.t -> T.t -> L.t -> (State.t * L.t) list - val stats : unit -> stats + val eval : Ata.t -> T.t -> T.node Sequence.t -> T.node Sequence.t + val full_eval : Ata.t -> T.t -> T.node Sequence.t -> (State.t * T.node Sequence.t) list end diff --git a/src/tatoo.ml b/src/tatoo.ml index e0f29ee..eac804a 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -104,10 +104,10 @@ let main () = Logger.msg `STATS "@[Automaton: @\n%a@]" Ata.print auto) auto_list; end; - let module Naive = Run.Make(Naive_tree)(Naive_node_list) in + let module Naive = Run.Make(Naive_tree) in let result_list = - let root = Naive_node_list.create () in - let () = Naive_node_list.add (Naive_tree.root doc) root in + let root = Sequence.create () in + let () = Sequence.add (Naive_tree.root doc) root in let f, msg = match !Options.parallel, !Options.compose with true, true -> @@ -121,16 +121,6 @@ let main () = in time f () ("evaluating query in " ^ msg ^ " mode") in - let s = Naive.stats () in - Run.( - Logger.msg `STATS - "@[tree size: %d@\ntraversals: %d@\ntransition fetch cache hit ratio: %f@\ntransition eval cache hit ratio: %f@\nNumber of visited nodes per pass: %a@]" - s.tree_size s.pass - (float s.fetch_trans_cache_hit /. float s.fetch_trans_cache_access) - (float s.eval_trans_cache_hit /. float s.eval_trans_cache_access) - (let i = ref 0 in - Pretty.print_list ~sep:"," (fun fmt n -> Format.fprintf fmt "%i: %i" !i n;incr i)) - s.nodes_per_run); time (fun () -> let count = ref 1 in List.iter (fun results -> @@ -138,10 +128,10 @@ let main () = output_string output (string_of_int !count); output_string output "\" >\n"; if !Options.count then begin - output_string output (string_of_int (Naive_node_list.length results)); + output_string output (string_of_int (Sequence.length results)); output_char output '\n'; end else - Naive_node_list.iter (fun n -> + Sequence.iter (fun n -> Naive_tree.print_xml output doc n; output_char output '\n' ) results;