X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=f9ab76ae642e5e652886c43084914e65b89020a3;hp=1824aebec8d311591cc88fe8a6c15f6908dfe900;hb=c6a89f390d6171f99d98f794427c1cce42fbf40c;hpb=f9b9f1ce524acda75c7f3583cd3751901ecd17a5 diff --git a/src/run.ml b/src/run.ml index 1824aeb..f9ab76a 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) = + 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,16 +228,17 @@ 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 @@ -235,47 +255,51 @@ 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 + 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 *) + if StateSet.intersect cache.(T.preorder tree node) sel_states then node::acc1 else acc1 in @@ -283,7 +307,7 @@ module Make (T : Tree.S) = 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 @@ -309,7 +333,7 @@ module Make (T : Tree.S) = if res != dummy then Cache.N1.add res_mapper (q :> int) (node::res) ) - cache.(T.preorder tree node)(* NodeStatus.node.sat *) + cache.(T.preorder tree node) in loop (T.root tree); (StateSet.fold_right @@ -320,10 +344,11 @@ 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 -> 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 @@ -335,11 +360,12 @@ module Make (T : Tree.S) = let rank = Ata.get_max_rank auto in while run.pass <= rank do top_down run; + 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; 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 =