From: Kim Nguyễn Date: Fri, 6 Dec 2013 15:09:27 +0000 (+0100) Subject: Resurect the HTML trace. Now generates a single HTML file containing the SVG. X-Git-Tag: v0.1~13 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=129708eaa5983b9463f96b714c00468602339b0a Resurect the HTML trace. Now generates a single HTML file containing the SVG. --- diff --git a/src/html.ml b/src/html.ml index b35f17d..f5aa8b2 100644 --- a/src/html.ml +++ b/src/html.ml @@ -36,15 +36,21 @@ let finalize_node n r b = Hashtbl.replace final n (b,r) module K = struct - type t = int * StateSet.t * StateSet.t - let hash (a,b,c) = HASHINT3(a, (b.StateSet.id :> int), (c.StateSet.id :> int)) - let equal ((a1,b1,c1) as x) ((a2,b2,c2) as y) = - x == y || (a1 == a2 && b1 == b2 && c1 == c2) + type t = StateSet.t list + let hash l = + List.fold_left (fun acc set -> + HASHINT2(acc, (set.StateSet.id :> int))) 17 l + + let equal l1 l2 = + try + List.for_all2 (==) l1 l2 + with _ -> false end module CTable = Hashtbl.Make (K) let ctable = CTable.create 20 + let rgb x = let h = K.hash x in let r = h land 0xff @@ -52,7 +58,8 @@ let rgb x = and b = (h lsr 16) land 0xff in r, g, b -let color ((a,b,c) as x) = + +let color x = try CTable.find ctable x with @@ -64,41 +71,31 @@ let color ((a,b,c) as x) = in CTable.add ctable x s; s + let text_color x = let r,g,b = rgb x in let av = (r + g + b) / 3 in if av > 128 then "rgb(0,0,0)" else "rgb(255,255,255)" +let get_conf sel l i = + List.fold_left (fun (accb,accl) a -> + accb || StateSet.intersect a.(i) sel, + a.(i) :: accl) (false,[]) l -let gen_trace (type s) = fun auto t tree -> +let gen_trace (type s) = fun auto sat_arrays t tree -> let module T = (val (t) : Tree.S with type t = s) in let root = T.root tree in - let rec loop osvg ohtml node parent x y = + let sel = Ata.get_selecting_states auto in + let rec loop output node parent x y = if node != T.nil then begin - let m = - try - Hashtbl.find info (T.preorder tree node) - with Not_found -> M.empty - in let node_id = T.preorder tree node in - let marked, last_round = try Hashtbl.find final node_id with Not_found -> - Printf.eprintf ">>> %i\n%!" node_id; false, !max_round; - in - let scolor, tcolor = - let { sat ; todo; _ } = - match M.find last_round m with - [] -> { sat = StateSet.empty; todo= StateSet.empty; msg = "ERROR" } - | [ e ] -> e - | l -> List.hd (List.tl (List.rev l)) - in - let c = (last_round, StateSet.union sat todo, StateSet.empty) in - color c, text_color c - in + let marked, conf = get_conf sel sat_arrays node_id in + let scolor, tcolor = color conf, text_color conf in let tag = QName.to_string (T.tag tree node) in let lbox = (String.length tag + 2) * 10 in let s_node = "node" ^ (string_of_int node_id) in - fprintf osvg + fprintf output "\n%!" s_node @@ -109,75 +106,96 @@ let gen_trace (type s) = fun auto t tree -> (if marked then ";stroke-width:4" else ";stroke-width:2;stroke-dasharray:2,2"); - fprintf osvg "%s\n" (x+10) (y+15) tcolor s_node tag; - fprintf ohtml "data['%s'] = new Array();\n" s_node; - M.iter - (fun i l -> - let msg = String.concat "" (List.rev_map (fun x -> x.msg) l) in - fprintf ohtml "data['%s'][%i] = '%s';\n" s_node i msg) - m; let first = T.first_child tree node in - let maxw1, maxy1 = loop osvg ohtml first node x (y + 40) in + let maxw1, maxy1 = loop output first node x (y + 40) in let next = T.next_sibling tree node in let x_next = max (x+lbox) (maxw1+10) in if node != root then begin if node == T.first_child tree parent then - fprintf osvg "\n" (x + lbox / 2) (y-20) (x + lbox / 2) (y); if next != T.nil then - fprintf osvg "\n" (x + lbox) (y+10) x_next (y+10); end; - let maxw2, maxy2 = loop osvg ohtml next node x_next y in + let maxw2, maxy2 = loop output next node x_next y in maxw2, max maxy1 maxy2 end else x, y in ignore (Sys.command "mkdir -p tests/trace"); - let osvg_ = open_out "tests/trace/trace.svg" in let ohtml_ = open_out "tests/trace/trace.html" in - let osvg = formatter_of_out_channel osvg_ in let ohtml = formatter_of_out_channel ohtml_ in fprintf ohtml "\ -\ \ +\ \ \
%a
-
\ -\n
\n" + fprintf ohtml "\n
\n"; + let maxw, maxh = loop ohtml (T.root tree) T.nil 50 50 in + fprintf ohtml "\n\ +
\n%!" maxw maxh; - let fi = open_in "tests/trace/trace.svg" in - try - while true do - let s = input_line fi in - fprintf ohtml "%s\n" s; - done - with - End_of_file -> - fprintf ohtml "\n
\n%!"; - pp_print_flush ohtml (); - close_out ohtml_; - close_in fi + pp_print_flush ohtml (); + close_out ohtml_ diff --git a/src/html.mli b/src/html.mli index a6cd212..5e8d4c2 100644 --- a/src/html.mli +++ b/src/html.mli @@ -1,6 +1 @@ -val trace : ?msg:string -> int -> int -> StateSet.t -> StateSet.t -> unit -(** [trace nid round d t msg] records the message [msg] together - with the a node preorder [nid], the [round], the [d]one set and - the [t]odo set *) -val finalize_node : int -> int -> bool -> unit -val gen_trace : Ata.t -> (module Tree.S with type t = 'a) -> 'a -> unit +val gen_trace : Ata.t -> StateSet.t array list -> (module Tree.S with type t = 'a) -> 'a -> unit diff --git a/src/run.ml b/src/run.ml index 1824aeb..291faa4 100644 --- a/src/run.ml +++ b/src/run.ml @@ -80,12 +80,28 @@ module Make (T : Tree.S) = let dummy_set = StateSet.singleton State.dummy open Bigarray + +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 run = { tree : T.t ; (* 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 *) @@ -107,7 +123,8 @@ module Make (T : Tree.S) = { tree = tree; auto = auto; - sat = Array.create len StateSet.empty; + 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; @@ -201,7 +218,6 @@ module Make (T : Tree.S) = new_sat - let unsafe_get a i = if i < 0 then StateSet.empty else Array.unsafe_get a i let top_down run = let i = run.pass in @@ -214,7 +230,9 @@ module Make (T : Tree.S) = 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 @@ -243,19 +261,20 @@ module Make (T : Tree.S) = parent_sat status0 td_todo summary in - (* update the cache if the status of the node changed *) - if status1 != status0 then run.sat.(node_id) <- status1; + (* 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 + 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 *) - else + 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 fcs1 nss1 parent_sat status1 bu_todo summary in - if status2 != status1 then run.sat.(node_id) <- status2; + unsafe_set run.sat node_id status2 status0; status2 end in @@ -264,7 +283,7 @@ module Make (T : Tree.S) = 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 @@ -283,7 +302,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 @@ -320,10 +339,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 +355,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.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,()); run let full_eval auto tree nodes = diff --git a/src/tatoo.ml b/src/tatoo.ml index 6464cb4..57d5f1a 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -15,8 +15,6 @@ open Format - - let time f arg msg = let t1 = Unix.gettimeofday () in let r = f arg in @@ -55,6 +53,7 @@ let main () = let d = time Naive_tree.load_xml_file fd "parsing xml document" in close_fd (); d in + let () = Gc.compact () in let queries = time (fun l -> diff --git a/tests/trace/trace.css b/tests/trace/trace.css deleted file mode 100644 index effe42e..0000000 --- a/tests/trace/trace.css +++ /dev/null @@ -1,26 +0,0 @@ -div#data { - position: absolute; - top: 50%; - left: 0%; - width: 30%; - height: 50%; - overflow: auto; -} -div#svg { - position: absolute; - top: 0%; - left: 30%; - width: 70%; - height: 100%; - overflow: auto; -} - -div#automata { - white-space: pre; - overflow: auto; - position: absolute; - width: 30%; - top: 0%; - left: 0%; - height: 50%; -} \ No newline at end of file