From a089738aa464521c0ae79944eb00fc147cc37ac9 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= <kn@lri.fr>
Date: Mon, 9 Dec 2013 10:57:59 +0100
Subject: [PATCH] Refactor the tracing code, store the whole tree structure in
 a javascript array and handle it from the javascript side.

---
 src/html_trace.ml    | 74 +++++++++++++++++++++++++++++++-------------
 src/pretty.ml        | 25 ++++++++++++---
 src/pretty.mli       | 12 +++++++
 src/run.ml           |  1 +
 src/trace_css.ml.str | 15 +++++++--
 src/trace_js.ml.str  | 70 +++++++++++++++++++++++------------------
 6 files changed, 139 insertions(+), 58 deletions(-)

diff --git a/src/html_trace.ml b/src/html_trace.ml
index 0d4890e..7ce3f39 100644
--- a/src/html_trace.ml
+++ b/src/html_trace.ml
@@ -83,10 +83,18 @@ let get_conf sel l i =
     accb || StateSet.intersect a.(i) sel,
     a.(i) :: accl) (false,[]) l
 
+let dup_rev_list l =
+  List.fold_left (fun acc e -> e::e::acc) [] l
+
 let gen_trace (type s) = fun auto sat_arrays t tree ->
+  let sat_arrays = dup_rev_list sat_arrays in
   let module T = (val (t) : Tree.S with type t = s) in
   let root = T.root tree in
   let sel = Ata.get_selecting_states auto in
+  let todos = Ata.get_states_by_rank auto in
+  let pr_sets = Pretty.print_list ~sep:", "
+    (fun fmt s -> fprintf fmt "'%a'" StateSet.print s)
+  in
   let rec loop output node parent prevsib x y =
     if node != T.nil then begin
       let node_id = T.preorder tree node in
@@ -97,9 +105,31 @@ let gen_trace (type s) = fun auto sat_arrays t tree ->
       let s_node = "node" ^ (string_of_int node_id) in
       let first = T.first_child tree node in
       let next = T.next_sibling tree node in
+      fprintf output "<script type='text/javascript'><![CDATA[ ";
+      let pass, max_active_pass, diff_list, full_list =
+        List.fold_left
+          (fun (pass, max_active_pass, diff_list, full_list) a ->
+            let todo = if pass >= Array.length todos then StateSet.empty
+              else todos.(pass)
+            in
+            let diff = StateSet.inter a.(node_id) todo in
+            let new_active_pass =
+              if diff == StateSet.empty then max_active_pass else pass
+            in
+            pass+1, new_active_pass, diff::diff_list, a.(node_id) :: full_list)
+          (0, -1, [], []) sat_arrays
+      in
+      fprintf output "tree['%s'] = { marked: %b, fc: 'node%i', ns: 'node%i', par: 'node%i', ps: 'node%i', max: %i, dlist: [%a], flist: [%a] };]]></script>\n"
+        s_node
+        marked
+        (T.preorder tree first) (T.preorder tree next)
+        (T.preorder tree parent) (T.preorder tree prevsib)
+        max_active_pass
+        pr_sets (List.rev diff_list)
+        pr_sets (List.rev full_list);
       fprintf output
         "<rect id=\"%s\" onclick=\"activate(\'%s\');\" x=\"%i\" y=\"%i\"\
- width=\"%i\" height=\"22\" style=\"fill:%s;stroke:rgb(0,0,0)%s\">%!"
+ width=\"%i\" height=\"22\" style=\"fill:%s;stroke:rgb(0,0,0)%s\"/>%!"
         s_node
         s_node
         x y
@@ -108,10 +138,6 @@ let gen_trace (type s) = fun auto sat_arrays t tree ->
         (if marked
          then ";stroke-width:4"
          else ";stroke-width:2;stroke-dasharray:2,2");
-      fprintf output "<metadata id='%s_fs'>node%i</metadata><metadata id='%s_ns'>node%i</metadata><metadata id='%s_par'>node%i</metadata><metadata id='%s_ps'>node%i</metadata></rect>\n%!"
-s_node (T.preorder tree first) s_node (T.preorder tree next)
-s_node (T.preorder tree parent) s_node (T.preorder tree prevsib)
-;
       fprintf output "<text x=\"%i\" y=\"%i\" style=\"fill:%s;font-size:17;\
 font-family:typewriter;\" onclick=\"activate(\'%s\');\" >%s</text>\n"
         (x+10)
@@ -148,29 +174,35 @@ style=\"stroke:rgb(0,0,0);stroke-width:2\"/>\n"
 <div id='automata' >%a</div>\n\
 <div id='data' > </div>\n\
 <script type='text/javascript'>\n\
-var data = new Array();\n\
+var tree = new Array();\n\
+var current_node = null;
+var nil_id = 'node%i';
+var last_id = %i;
 var rounds = %i;\n"
     Trace_css.content
     Ata.print auto
-    (List.length sat_arrays);
-    List.iteri (fun i _ ->
-      fprintf ohtml "data[%i] = new Array();\n" i) sat_arrays;
-    for node_id = 0 to (Array.length (List.hd sat_arrays)) - 1 do
-      let _,_ = List.fold_left (fun (pass, diff_set) a ->
-        let cur_set = a.(node_id) in
-        fprintf ohtml "data[%i]['node%i'] = \"new states %a<br/>full states = %a\";\n"
-        pass node_id StateSet.print (StateSet.diff cur_set diff_set) StateSet.print cur_set;
-        (pass+1, StateSet.union diff_set cur_set))
-        (0, StateSet.empty) (List.rev sat_arrays)
-      in ()
-    done;
+    (T.preorder tree T.nil)
+    (T.size tree)
+    (List.length sat_arrays - 1);
   fprintf ohtml "%s\n" Trace_js.content;
-  fprintf ohtml "%s"
+  fprintf ohtml
     "</script>\n\
+<div id='tree'>
+<div id='controls'><button onclick='activate_parent();'>↑</button>\n\
+<button onclick='activate_previous();'>←</button>\n\
+<button onclick='activate_first();'>↓</button>\n\
+<button onclick='activate_next();'>→</button>\n\
+<select id='relnodes' onchange='hide_nodes();'>\n\
+<option value='-1'>All nodes</option>\n\
+%a</select>\n\
+</div>
 <div id='svg'>\n
-   <svg id='svgimg' width='' height='' preserveAspectRatio='XMidYMid slice' xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n";
+   <svg id='svgimg' width='' height='' xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n"
+    (Pretty.print_range (fun fmt i ->
+      fprintf fmt "<option value='%i'>Relevant nodes on pass %i</option>\n" i i))
+    (0,(List.length sat_arrays - 1));
   let maxw, maxh = loop ohtml (T.root tree) T.nil T.nil 50 50 in
-  fprintf ohtml "</svg>\n</div><script type='text/javascript'>\n\
+  fprintf ohtml "</svg>\n</div></div><script type='text/javascript'>\n\
 window.onload = function () {\n\
     var svg = document.getElementById('svgimg');\n\
     svg.setAttribute('width', %i);\n\
diff --git a/src/pretty.ml b/src/pretty.ml
index 66a0225..b39375a 100644
--- a/src/pretty.ml
+++ b/src/pretty.ml
@@ -135,14 +135,29 @@ let pp_print_list ?(sep=dummy_printer) printer fmt l =
       fprintf fmt "%a" printer x) es
 
 
+let pp_print_range ?(sep=dummy_printer) printer fmt (first, last) =
+  for i = first to last - 1 do
+    printer fmt i;
+    sep fmt ();
+  done;
+  if first <= last then printer fmt last
+
 let pp_print_array ?(sep=dummy_printer) printer fmt a =
-  pp_print_list ~sep:sep printer fmt (Array.to_list a)
+  pp_print_range ~sep:sep (fun fmt i -> printer fmt a.(i)) fmt
+    (0, (Array.length a - 1))
 
-let print_list ?(sep=" ") printer fmt l =
+let with_printer (f : ?sep:('a) -> 'b) strsep pr fmt =
   let sep_printer fmt () =
-    pp_print_string fmt sep
+    pp_print_string fmt strsep
   in
-  pp_print_list ~sep:sep_printer printer fmt l
+  fun x -> f ~sep:sep_printer pr fmt x
+
+
+let print_list ?(sep=" ") printer fmt l =
+  with_printer pp_print_list sep printer fmt l
 
 let print_array ?(sep=" ") printer fmt a =
-  print_list ~sep:sep printer fmt (Array.to_list a)
+  with_printer pp_print_array sep printer fmt a
+
+let print_range ?(sep=" ") printer fmt r =
+  with_printer pp_print_range sep printer fmt r
diff --git a/src/pretty.mli b/src/pretty.mli
index 36fd430..cbdf196 100644
--- a/src/pretty.mli
+++ b/src/pretty.mli
@@ -49,10 +49,22 @@ val pp_superscript : Format.formatter -> int -> unit
 val pp_print_list :
   ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit)
   -> Format.formatter -> 'a list -> unit
+
 val pp_print_array :
   ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit)
   -> Format.formatter -> 'a array -> unit
+
+val pp_print_range :
+  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> int -> unit)
+  -> Format.formatter -> (int * int) -> unit
+
+
 val print_list : ?sep:string -> (Format.formatter -> 'a -> unit)
   -> Format.formatter -> 'a list -> unit
+
 val print_array : ?sep:string -> (Format.formatter -> 'a -> unit)
   -> Format.formatter -> 'a array -> unit
+
+val print_range :
+  ?sep:string -> (Format.formatter -> int -> unit)
+  -> Format.formatter -> (int * int) -> unit
diff --git a/src/run.ml b/src/run.ml
index f9ab76a..fb9f81d 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -364,6 +364,7 @@ module Make (T : Tree.S) =
       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
diff --git a/src/trace_css.ml.str b/src/trace_css.ml.str
index 00fc918..7d40718 100644
--- a/src/trace_css.ml.str
+++ b/src/trace_css.ml.str
@@ -1,4 +1,8 @@
 /* -*-CSS-*- */
+button {
+    border-radius: 5px;
+    border: none;
+}
 div#data {
     position: absolute;
     top: 0%;
@@ -7,15 +11,22 @@ div#data {
     height: 50%;
     overflow: auto;
 }
-div#svg {
+div#tree {
     position: absolute;
     top: 50%;
     left: 0%;
     width: 100%;
     height: 50%;
+    overflow: hidden;
+}
+div#svg {
+    position: absolute;
+    left:0%;
+    right:0%;
+    top:10%;
+    bottom:0%;
     overflow: auto;
 }
-
 div#automata {
     white-space: pre;
     overflow: auto;
diff --git a/src/trace_js.ml.str b/src/trace_js.ml.str
index 4d17382..53af07c 100644
--- a/src/trace_js.ml.str
+++ b/src/trace_js.ml.str
@@ -1,24 +1,47 @@
 // -*-Javascript-*-
-var old_timer = null;
-var old_node = null;
 
-var make_button = function (target, label)
-{
-    var msg  = '<button onclick="';
-    msg += 'activate(\'' + target + '\')"';
-    if (target == 'node-1') msg+= ' disabled="disabled" ';
-    msg+= '>' + label + '</button>';
-    return msg;
+var hide_nodes = function () {
+    var v = document.getElementById('relnodes').value;
+    for(i = 0; i < last_id; i++) {
+	var id = 'node' + i;
+	var rect = document.getElementById(id);
+
+	if ((v-0) <= tree[id].max)
+	    rect.style.fillOpacity = 1;
+	else
+	    rect.style.fillOpacity = 0.3;
+    }
 };
 
+var activate_parent = function () {
+    if (current_node) activate(tree[current_node].par);
+};
+var activate_previous = function () {
+    if (current_node) activate(tree[current_node].ps);
+};
+var activate_next = function () {
+    if (current_node) activate(tree[current_node].ns);
+};
+var activate_first = function () {
+    if (current_node) activate(tree[current_node].fc);
+};
+var buttons = document.getElementsByTagName("button");
 var activate = function (id)
 {
-    if (old_node) {
-        clearInterval(old_timer);
-        old_node.style.fillOpacity = 1.0;
-        old_node.style.stroke = 'black';
-        old_node.classList.remove('blink');
+    if (id == nil_id) return;
+    if (current_node) {
+	var rect = document.getElementById(current_node);
+        rect.style.fillOpacity = 1.0;
+        rect.style.stroke = 'black';
+        rect.classList.remove('blink');
     };
+    hide_nodes();
+    current_node = id;
+    buttons[0].disabled = tree[id].par == nil_id;
+    buttons[1].disabled = tree[id].ps == nil_id;
+    buttons[2].disabled = tree[id].fc == nil_id;
+    buttons[3].disabled = tree[id].ns == nil_id;
+
     var node = document.getElementById(id);
     var div = document.getElementById('svg');
     var node_dim = node.getBBox();
@@ -35,22 +58,9 @@ var activate = function (id)
 
     var d = document.getElementById('data');
     var msg = '';
-    for (i=0; i < rounds; i++)
-	msg += ('<p>round: ' + i + ':<br/>') + data[i][id] + '</p>\n';
-
-    var rect = document.getElementById(id);
-    var fce = rect.firstElementChild;
-    var nse = fce.nextElementSibling;
-    var pare = nse.nextElementSibling;
-    var pse = pare.nextElementSibling;
-    var fc = fce.textContent;
-    var ns = nse.textContent;
-    var par = pare.textContent;
-    var ps = pse.textContent;
-    msg += make_button(par, "↑");
-    msg += make_button(ps, "←");
-    msg += make_button(fc, "↓");
-    msg += make_button(ns,"→");
+    for (i=0; i <= rounds; i++)
+	msg += ('<p>round ' + i + ':<br/>new states:') + tree[id].dlist[i]
+    + '<br/>all states:' + tree[id].flist[i] + '</p>\n';
     d.innerHTML = msg;
     return;
 };
-- 
2.17.1