From a8f210b6229055c3c5101034d359c61476d8408a Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Sun, 18 Aug 2013 18:32:18 +0200 Subject: [PATCH] Refactor HTML tracing utility. Color the nodes that are in the same sat configuration in the same color. --- src/html.ml | 85 +++++++++++++++++++++++++++++++++++++++------------- src/html.mli | 4 ++- src/run.ml | 11 ++++--- 3 files changed, 73 insertions(+), 27 deletions(-) diff --git a/src/html.ml b/src/html.ml index 46d602c..f049195 100644 --- a/src/html.ml +++ b/src/html.ml @@ -1,34 +1,74 @@ +INCLUDE "utils.ml" + open Format module M = Map.Make(struct type t = int let compare = compare end) +type info = { sat : StateSet.t; + todo : StateSet.t; + msg : string; + } let info = Hashtbl.create 2017 let final = Hashtbl.create 2017 let max_round = ref 0 -let add_info (nodeid:int) (i:int) s = - if i > !max_round then max_round := i; - let m = try Hashtbl.find info nodeid with Not_found -> M.empty in - let old_s = try M.find i m with Not_found -> "" in - let s' = old_s ^ s in - let m' = M.add i s' m in - Hashtbl.replace info nodeid m' - let buff = Buffer.create 20 let fmt = formatter_of_buffer buff -let trace nodeid i = - let () = pp_print_flush fmt (); - Buffer.clear buff + +let trace ?(msg="") nid r t d = + if r > !max_round then max_round := r; + let m = try Hashtbl.find info nid with Not_found -> M.empty in + let () = pp_print_flush fmt () in + let _ = fprintf fmt + "node: %i
%s
todo: %a
sat: %a
_______________________
" + nid msg StateSet.print t StateSet.print d in - kfprintf (fun fmt -> - pp_print_flush fmt (); - let s = Buffer.contents buff in - add_info nodeid i s) fmt + let () = pp_print_flush fmt () in + let msg = Buffer.contents buff in + let () = Buffer.clear buff in + let old_inf = try M.find r m with Not_found -> [] in + let m' = M.add r ({ sat = d; todo = t; msg = msg }::old_inf) m in + Hashtbl.replace info nid m' 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) +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 + and g = (h lsr 8) land 0xff + and b = (h lsr 16) land 0xff + in + r, g, b +let color ((a,b,c) as x) = + try + CTable.find ctable x + with + Not_found -> + let r,g,b = rgb x in + let s = "rgb(" ^ (string_of_int r) ^ "," + ^ (string_of_int g) ^ "," + ^ (string_of_int b) ^ ")" + 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 gen_trace (type s) = fun auto t tree -> @@ -46,16 +86,21 @@ let gen_trace (type s) = fun auto t tree -> Printf.eprintf ">>> %i\n%!" node_id; false, !max_round; in let pc = if !max_round == 0 then 1. else float_of_int last_round /. float_of_int !max_round in - let color = int_of_float (255. *. (1. -. pc)) in + let scolor, tcolor = + let { sat ; todo; _ } = List.hd(M.find last_round m) in + let c = (last_round, sat, todo) in color c, text_color c + 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 "\n%!" - s_node s_node x y lbox color color (if marked then ";stroke-width:4" else ";stroke-width:2;stroke-dasharray:2,2"); - fprintf osvg "%s\n" (x+10) (y+15) s_node tag; + fprintf osvg "\n%!" + s_node s_node x y lbox scolor (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 s -> fprintf ohtml "data['%s'][%i] = '%s';\n" s_node i s) + (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 diff --git a/src/html.mli b/src/html.mli index 0772863..48551f7 100644 --- a/src/html.mli +++ b/src/html.mli @@ -1,3 +1,5 @@ -val trace : int -> int -> ('a, Format.formatter, unit, unit) format4 -> 'a +val trace : ?msg:string -> int -> int -> StateSet.t -> StateSet.t -> unit +(** [trace nid round d t msg] records a 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 diff --git a/src/run.ml b/src/run.ml index 7310e71..ca162a1 100644 --- a/src/run.ml +++ b/src/run.ml @@ -152,12 +152,11 @@ END let html tree node i config msg = let config = config.NodeStatus.node in - Html.trace (T.preorder tree node) i - "node: %i
%s
sat: %a
todo: %a
_______________________
" - (T.preorder tree node) - msg - StateSet.print config.sat - StateSet.print config.todo + Html.trace ~msg:msg + (T.preorder tree node) i + config.todo + config.sat + let debug msg tree node i config = -- 2.17.1