X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=8eb58f9867c8f96445c6e005b7829ded57874822;hp=1824aebec8d311591cc88fe8a6c15f6908dfe900;hb=3406b26f1ea26a997d7f194c547439891c108ce6;hpb=f9b9f1ce524acda75c7f3583cd3751901ecd17a5 diff --git a/src/run.ml b/src/run.ml index 1824aeb..8eb58f9 100644 --- a/src/run.ml +++ b/src/run.ml @@ -18,6 +18,7 @@ INCLUDE "debug.ml" open Format open Misc +open Bigarray type stats = { run : int; tree_size : int; @@ -38,54 +39,70 @@ let reset_stat_counters () = eval_trans_cache_access := 0 -module Make (T : Tree.S) = - struct - - module NodeSummary = - struct +module NodeSummary = +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 = + 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 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) + 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 - open Bigarray - type run = { - tree : T.t ; + + + +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 *) - sat: StateSet.t array; + mutable sat: sat_array; (* A mapping from node preorders to states satisfied at that node *) mutable pass : int; (* Number of run we have performed *) @@ -99,23 +116,8 @@ module Make (T : Tree.S) = node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; } - let dummy_form = Ata.Formula.stay State.dummy - let make auto tree = - let len = T.size tree in - { - tree = tree; - auto = auto; - sat = Array.create len StateSet.empty; - 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 = let ba = Array1.create int16_unsigned c_layout len in - Array1.fill ba 0; ba - } - let get_form fetch_trans_cache auto tag q = let phi = incr fetch_trans_cache_access; @@ -166,10 +168,10 @@ module Make (T : Tree.S) = loop phi - let eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary = + let eval_trans_aux auto trans_cache tag summary fcs nss ps sat todo = StateSet.fold (fun q (a_sat) -> let phi = - get_form fetch_trans_cache auto tag q + get_form trans_cache auto tag q in if eval_form phi fcs nss ps a_sat summary then StateSet.add q a_sat @@ -177,15 +179,15 @@ module Make (T : Tree.S) = ) todo sat - let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps sat todo summary = + let rec eval_trans_fix auto trans_cache tag summary fcs nss ps sat todo = let new_sat = - eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary + eval_trans_aux auto trans_cache tag summary fcs nss ps sat todo in if new_sat == sat then sat else - eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_sat todo summary + eval_trans_fix auto trans_cache tag summary fcs nss ps new_sat todo - let eval_trans auto fetch_trans_cache eval_cache tag fcs nss ps ss todo summary = + let eval_trans auto fetch_trans_cache eval_cache tag summary fcs nss ps ss todo = let fcsid = (fcs.StateSet.id :> int) in let nssid = (nss.StateSet.id :> int) in let psid = (ps.StateSet.id :> int) in @@ -195,13 +197,30 @@ module Make (T : Tree.S) = incr eval_trans_cache_access; if res != dummy_set then begin incr eval_trans_cache_hit; res end else let new_sat = - eval_trans_fix auto fetch_trans_cache tag fcs nss ps ss todo summary + eval_trans_fix auto fetch_trans_cache tag summary fcs nss ps ss todo in Cache.N6.add eval_cache tagid summary ssid fcsid nssid psid new_sat; new_sat - let unsafe_get a i = if i < 0 then StateSet.empty else Array.unsafe_get a i +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 + { + 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 = let ba = Array1.create int16_unsigned c_layout len in + Array1.fill ba 0; ba + } + let top_down run = let i = run.pass in @@ -209,24 +228,25 @@ module Make (T : Tree.S) = let auto = run.auto 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 + let bu_todo = + if i == Array.length states_by_rank - 1 then StateSet.empty else states_by_rank.(i+1) in let rec loop_td_and_bu node parent parent_sat = - if node == T.nil then StateSet.empty else begin + if node == T.nil then StateSet.empty + else begin let node_id = T.preorder tree node in let fc = T.first_child tree node in let ns = T.next_sibling tree node in - let tag = T.tag 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 *) + (node_id == T.preorder tree (T.first_child tree parent)) (*is_left *) + (node_id == T.preorder tree (T.next_sibling tree parent))(*is_right *) (fc != T.nil) (* has_left *) (ns != T.nil) (* has_right *) (T.kind tree node) (* kind *) @@ -235,55 +255,61 @@ module Make (T : Tree.S) = in let status0 = unsafe_get run.sat node_id in (* get the node_statuses for the first child, next sibling and parent *) - let fcs = unsafe_get run.sat (T.preorder tree fc) in - let nss = unsafe_get run.sat (T.preorder tree ns) in (* evaluate the transitions with all this statuses *) + let tag = T.tag tree node in let status1 = - eval_trans auto run.fetch_trans_cache run.td_cache tag fcs nss + eval_trans + auto run.fetch_trans_cache 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 summary + status0 td_todo in - (* update the cache if the status of the node changed *) - if status1 != status0 then run.sat.(node_id) <- status1; - let fcs1 = loop_td_and_bu fc node status1 in - if bu_todo == StateSet.empty then - loop_td_and_bu ns node status1 (* tail call *) - else - let nss1 = loop_td_and_bu ns node status1 in - let status2 = - eval_trans auto run.fetch_trans_cache run.bu_cache tag fcs1 nss1 - parent_sat - status1 bu_todo summary - in - if status2 != status1 then run.sat.(node_id) <- status2; - status2 - end + + (* update the cache if the status of the node changed + unsafe_set run.sat node_id status1 status0;*) + let fcs1 = loop_td_and_bu fc node status1 in + if bu_todo == StateSet.empty then begin + unsafe_set run.sat node_id status1 status0; (* write the td_states *) + loop_td_and_bu ns node status1 (* tail call *) + end else + let nss1 = loop_td_and_bu ns node status1 in + let status2 = + eval_trans auto run.fetch_trans_cache run.bu_cache tag + summary fcs1 + nss1 + parent_sat + status1 bu_todo + in + unsafe_set run.sat node_id status2 status0; + status2 + end in - let _ = loop_td_and_bu (T.root tree) T.nil StateSet.empty in + let _ = loop_td_and_bu (T.root tree) T.nil dummy_set in run.pass <- run.pass + 2 let get_results run = - let cache = run.sat in + let cache = IFHTML((List.hd run.sat), run.sat) 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 StateSet.intersect - cache.(T.preorder tree node)(* NodeStatus.node.sat *) - sel_states then node::acc1 - else acc1 + let res = ref (L.create ()) in + let rec loop node = + if node != T.nil then begin + if StateSet.intersect sel_states cache.(T.preorder tree node) then + res := L.add node !res; + loop (T.first_child tree node); + loop (T.next_sibling tree node) + end in - loop (T.root tree) [] + loop (T.root tree); + !res let get_full_results run = - let cache = run.sat(*tatus*) in + let cache = IFHTML((List.hd run.sat), run.sat) in let auto = run.auto in let tree = run.tree in let res_mapper = Hashtbl.create MED_H_SIZE in @@ -292,24 +318,26 @@ module Make (T : Tree.S) = (fun q -> Hashtbl.add res_mapper q []) (Ata.get_selecting_states auto) in - let dummy = [ T.nil ] in + 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) []) + (fun q -> Cache.N1.add res_mapper (q :> int) (L.create())) (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 + if node != T.nil then begin StateSet.iter (fun q -> let res = Cache.N1.find res_mapper (q :> int) in if res != dummy then - Cache.N1.add res_mapper (q :> int) (node::res) + Cache.N1.add res_mapper (q :> int) (L.add node res) ) - cache.(T.preorder tree node)(* NodeStatus.node.sat *) + cache.(T.preorder tree node); + loop (T.first_child tree node); + loop (T.next_sibling tree node) + end in loop (T.root tree); (StateSet.fold_right @@ -320,13 +348,25 @@ module Make (T : Tree.S) = 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 - List.iter (fun node -> + L.iter (fun node -> let node_id = T.preorder tree node in - run.sat.(node_id) <- sat0) list + sat.(node_id) <- sat0) list let tree_size = ref 0 let pass = ref 0 + +let time f arg msg = + let t1 = Unix.gettimeofday () in + let r = f arg in + let t2 = Unix.gettimeofday () in + let time = (t2 -. t1) *. 1000. in + Printf.eprintf "%s: %fms%!" msg time; + r + + + let compute_run auto tree nodes = pass := 0; tree_size := T.size tree; @@ -334,12 +374,14 @@ module Make (T : Tree.S) = prepare_run run nodes; let rank = Ata.get_max_rank auto in while run.pass <= rank do - top_down run; + time top_down run ("Timing run number " ^ string_of_int run.pass ^ "/" ^ string_of_int (Ata.get_max_rank auto + 1)); + 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), ()); pass := Ata.get_max_rank auto + 1; - + IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,()); run let full_eval auto tree nodes = @@ -348,7 +390,8 @@ module Make (T : Tree.S) = let eval auto tree nodes = let r = compute_run auto tree nodes in - get_results r + let nl = get_results r in + nl let stats () = { tree_size = !tree_size;