From: Kim Nguyễn <kn@lri.fr>
Date: Sun, 8 Dec 2013 09:54:54 +0000 (+0100)
Subject: Refactor the run module, moving out of the Make functor everything that can be moved... 
X-Git-Tag: v0.1~12
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=fee64144491afab22d71f6e2de72a9f18f35cd55

Refactor the run module, moving out of the Make functor everything that can be moved. Slightly improve the cache module by avoiding one comparison during find on some cases and remove manual call to Gc.compact in main, since it does not seem to help.
---

diff --git a/src/cache.ml b/src/cache.ml
index 9ffb332..d0f7ac5 100644
--- a/src/cache.ml
+++ b/src/cache.ml
@@ -61,10 +61,12 @@ struct
 
   let find a i =
     let idx = i - a.offset in
-    let len = Array.length a.line in
-    if idx >= 0 && idx < len then
-      Array.unsafe_get a.line idx
-    else a.dummy
+    if idx < 0 then a.dummy
+    else
+      let len = Array.length a.line in
+      if idx < len then
+        Array.unsafe_get a.line idx
+      else a.dummy
 
   let dummy a = a.dummy
 
@@ -106,8 +108,8 @@ struct
 
   let find a i j =
     let v = N1.find a i in
-    if v == a.N1.dummy then v.N1.dummy
-    else N1.find v j
+    if v != a.N1.dummy then N1.find v j
+    else v.N1.dummy
 
 
   let dummy c = c.N1.dummy.N1.dummy
@@ -155,8 +157,8 @@ struct
 
   let find a i j k =
     let v = N1.find a i in
-    if v == a.N1.dummy then N2.dummy v
-    else N2.find v j k
+    if v != a.N1.dummy then N2.find v j k
+    else N2.dummy v
 
 
   let dummy a = N2.dummy a.N1.dummy
@@ -275,45 +277,32 @@ end
 
 module N6 =
 struct
-  type 'a t = 'a N5.t N1.t
+  type 'a t = 'a N3.t N3.t
 
-  let create_with_level level a =
-    let dummy5 = N5.create_with_level (level+1) a in
-    N1.create_with_level (level) dummy5
-
-  let create a = create_with_level 1 a
+  let create a =
+    let dummy3 = N3.create a in
+    N3.create dummy3
 
   let add a i j k l m n v =
-    let line = N1.find a i in
-    if line == N1.dummy a then
-      let nline = N5.create_with_level (a.N1.level+1) (N5.dummy line) in
-      N1.add a i nline;
-      N5.add nline j k l m n v
+    let line = N3.find a i j k in
+    if line == N3.dummy a then
+      let nline = N3.create (N3.dummy line) in
+      N3.add a i j k nline;
+      N3.add nline l m n v
     else
-      N5.add line j k l m n v
+      N3.add line l m n v
 
   let find a i j k l m n =
-    let v = N1.find a i in
-    if v == N1.dummy a then N5.dummy v
-    else N5.find v j k l m n
+    let v = N3.find a i j k in
+    if v == N3.dummy a then N3.dummy v
+    else N3.find v l m n
 
 
-  let dummy a = N5.dummy (N1.dummy a)
+  let dummy a = N3.dummy (N3.dummy a)
   let iteri f a =
-    N1.iteri (fun i v _  ->
-      N5.iteri (fun j k l m n v2 b -> f i j k l m n v2 b) v
+    N3.iteri (fun i j k v _  ->
+      N3.iteri (fun l m n v2 b -> f i j k l m n v2 b) v
     ) a
 
-  let stats a =
-    let d = a.N1.dummy in
-    let len, used =
-      Array.fold_left (fun ((alen,aused) as acc) i ->
-        if i != d then
-          let l, u = N5.stats i in
-          (alen+l, aused+u)
-        else
-          acc) (0, 0) a.N1.line
-    in
-    len, used
-
+  let stats a = assert false
 end
diff --git a/src/html_trace.ml b/src/html_trace.ml
new file mode 100644
index 0000000..f5aa8b2
--- /dev/null
+++ b/src/html_trace.ml
@@ -0,0 +1,201 @@
+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 buff = Buffer.create 20
+let fmt = formatter_of_buffer 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<br/>%s<br/>todo: %a<br/>sat: %a<br/>_______________________<br/>"
+    nid msg  StateSet.print t StateSet.print d
+  in
+  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 = 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
+  and g = (h lsr 8) land 0xff
+  and b = (h lsr 16) land 0xff
+  in
+  r, g, b
+
+let color 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 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 sat_arrays t tree ->
+  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 rec loop output node parent x y =
+    if node != T.nil then begin
+      let node_id = T.preorder tree node 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 output
+        "<rect id=\"%s\" onclick=\"activate(\'%s\');\" x=\"%i\" y=\"%i\"\
+ width=\"%i\" height=\"20\" style=\"fill:%s;stroke:rgb(0,0,0)%s\"/>\n%!"
+        s_node
+        s_node
+        x y
+        lbox
+        scolor
+        (if marked
+         then ";stroke-width:4"
+         else ";stroke-width:2;stroke-dasharray:2,2");
+      fprintf output "<text x=\"%i\" y=\"%i\" style=\"fill:%s;font-size:17;\
+font-family:typewriter;\" onclick=\"activate(\'%s\');\" >%s</text>\n"
+        (x+10)
+        (y+15)
+        tcolor s_node tag;
+      let first = T.first_child tree node 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 output  "<line x1=\"%i\" y1=\"%i\" x2=\"%i\" y2=\"%i\"\
+style=\"stroke:rgb(0,0,0);stroke-width:2\"/>\n"
+            (x + lbox / 2) (y-20) (x + lbox / 2) (y);
+        if next != T.nil then
+          fprintf output "<line x1=\"%i\" y1=\"%i\" x2=\"%i\" y2=\"%i\"\
+style=\"stroke:rgb(0,0,0);stroke-width:2\"/>\n"
+            (x + lbox) (y+10) x_next (y+10);
+      end;
+      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 ohtml_ = open_out "tests/trace/trace.html" in
+  let ohtml = formatter_of_out_channel ohtml_ in
+  fprintf ohtml "<html>\
+<head><title></title>
+<meta http-equiv='content-type' content='text/html;charset=utf-8'/>\
+<style>\
+div#data {\
+    position: absolute;\
+    top: 0%%;\
+    left: 50%%;\
+    width: 50%%;\
+    height: 50%%;\
+    overflow: auto;\
+}\
+div#svg {\
+    position: absolute;\
+    top: 50%%;\
+    left: 0%%;\
+    width: 100%%;\
+    height: 50%%;\
+    overflow: auto;\
+}\
+\
+div#automata {\
+    white-space: pre;\
+    overflow: auto;\
+    position: absolute;\
+    width: 50%%;\
+    top: 0%%;\
+    left: 0%%;\
+    height: 50%%;\
+}\
+</style>\
+</head>\
+<body>\
+<div id='automata' >%a
+</div>
+<div id='data' > </div>\n\
+<script type='text/javascript'>\n\
+var data = new Array();\n\
+var rounds = %i;\n"
+    Ata.print auto
+    (List.length sat_arrays);
+  List.iteri (fun i a ->
+    fprintf ohtml "data[%i] = new Array();\n" i;
+    Array.iteri (fun id set ->
+      fprintf ohtml "data[%i]['node%i'] = \"%a\";\n"
+      i id StateSet.print set) a) (List.rev sat_arrays);
+  fprintf ohtml "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';
+  d.innerHTML = msg;
+  return;
+  };\n";
+  fprintf ohtml "</script>\n<div id='svg'><svg id='svgimg' width='' height='' xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n";
+  let maxw, maxh = loop ohtml (T.root tree) T.nil 50 50 in
+  fprintf ohtml "</svg>\n<script type=\"text/javascript\">window.onload = function () {\
+  var svg = document.getElementById('svgimg');
+  svg.setAttribute('width', %i);
+  svg.setAttribute('height', %i);
+};\
+</script>\
+</div></body></html>\n%!"
+    maxw maxh;
+  pp_print_flush ohtml ();
+  close_out ohtml_
diff --git a/src/html_trace.mli b/src/html_trace.mli
new file mode 100644
index 0000000..5e8d4c2
--- /dev/null
+++ b/src/html_trace.mli
@@ -0,0 +1 @@
+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 291faa4..c021dc2 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,48 +39,46 @@ 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
+
+
 
 IFDEF HTMLTRACE
 THEN
@@ -89,15 +88,17 @@ 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 ;
+   type 'a run = {
+     tree : 'a ;
      (* The argument of the run *)
      auto : Ata.t;
      (* The automaton to be run *)
@@ -115,24 +116,8 @@ END
      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 = (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 get_form fetch_trans_cache auto tag q =
      let phi =
        incr fetch_trans_cache_access;
@@ -183,10 +168,10 @@ END
          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
@@ -194,15 +179,15 @@ END
      ) 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
@@ -212,12 +197,30 @@ END
      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
 
 
+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
@@ -225,18 +228,17 @@ END
     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
+      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
@@ -253,32 +255,37 @@ END
         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
-        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 fcs1 nss1
-              parent_sat
-              status1 bu_todo summary
-          in
-          unsafe_set run.sat node_id status2 status0;
-          status2
-      end
+           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
 
 
@@ -288,13 +295,11 @@ END
     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
@@ -328,7 +333,7 @@ END
             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
diff --git a/src/tatoo.ml b/src/tatoo.ml
index 57d5f1a..9fb7045 100644
--- a/src/tatoo.ml
+++ b/src/tatoo.ml
@@ -53,7 +53,6 @@ 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 ->