X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=31eb26c650486e188d493bbc956794b766bdb3f2;hp=f6812e4878ec61d6c79cd622095f02e5eaf6d576;hb=5f1d396f4a04c9a0c6bb3da4176fd47a4473d35d;hpb=cfef2deaf1a17df7bcb153c3b92e28e14edd912b

diff --git a/src/run.ml b/src/run.ml
index f6812e4..31eb26c 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -14,9 +14,30 @@
 (***********************************************************************)
 
 INCLUDE "utils.ml"
+INCLUDE "debug.ml"
+
 open Format
 open Misc
 
+type stats = { run : int;
+               tree_size : int;
+               cache2_access : int;
+               cache2_hit : int;
+               cache5_access : int;
+               cache5_hit : int;
+             }
+
+let cache2_hit = ref 0
+let cache2_access = ref 0
+let cache5_hit = ref 0
+let cache5_access = ref 0
+let reset_stat_counters () =
+  cache2_hit := 0;
+  cache2_access := 0;
+  cache5_hit := 0;
+  cache5_access := 0
+
+
 module Make (T : Tree.S) =
  struct
 
@@ -60,10 +81,11 @@ module Make (T : Tree.S) =
    end
 
    type node_status = {
+     rank : int;
      sat : StateSet.t;  (* States that are satisfied at the current node *)
      todo : StateSet.t; (* States that remain to be proven *)
-                        (* For every node_status and automaton a:
-                           a.states - (sat U todo) = unsat *)
+        (* For every node_status and automaton a,
+           a.states - (sat U todo) = unsat *)
      summary : NodeSummary.t; (* Summary of the shape of the node *)
    }
 (* Describe what is kept at each node for a run *)
@@ -74,28 +96,33 @@ module Make (T : Tree.S) =
          type t = node_status
          let equal c d =
            c == d ||
+             c.rank == d.rank &&
              c.sat == d.sat &&
              c.todo == d.todo &&
              c.summary == d.summary
 
          let hash c =
-           HASHINT3((c.sat.StateSet.id :> int),
+           HASHINT4(c.rank,
+                    (c.sat.StateSet.id :> int),
                     (c.todo.StateSet.id :> int),
                     c.summary)
        end
        )
        let print ppf s =
          fprintf ppf
-           "{ sat: %a; todo: %a; summary: _ }"
+           "{ rank: %i; sat: %a; todo: %a; summary: _ }"
+           s.node.rank
            StateSet.print s.node.sat
            StateSet.print s.node.todo
      end
 
    let dummy_status =
-     NodeStatus.make { sat = StateSet.empty;
-                       todo = StateSet.empty;
-                       summary = NodeSummary.dummy;
-                     }
+     NodeStatus.make {
+       rank = -1;
+       sat = StateSet.empty;
+       todo = StateSet.empty;
+       summary = NodeSummary.dummy;
+     }
 
 
    type run = {
@@ -145,20 +172,18 @@ module Make (T : Tree.S) =
 
 IFDEF HTMLTRACE
   THEN
-DEFINE TRACE(e) = (e)
+DEFINE IFTRACE(e) = (e)
   ELSE
-DEFINE TRACE(e) = ()
+DEFINE IFTRACE(e) = ()
 END
 
    let html tree node i config msg =
      let config = config.NodeStatus.node in
-     Html.trace (T.preorder tree node) i
-       "node: %i<br/>%s<br/>sat: %a<br/>todo: %a<br/>round: %i<br/>"
-       (T.preorder tree node)
-       msg
-       StateSet.print config.sat
-       StateSet.print config.todo
-       i
+     Html.trace ~msg:msg
+       (T.preorder tree node) i
+       config.todo
+       config.sat
+
 
 
    let debug msg tree node i config =
@@ -173,6 +198,7 @@ END
 
    let get_form cache2 auto tag q =
      let phi =
+       incr cache2_access;
        Cache.N2.find cache2 (tag.QName.id :> int) (q :> int)
      in
      if phi == dummy_form then
@@ -183,7 +209,10 @@ END
            (tag.QName.id :> int)
            (q :> int) phi
        in phi
-     else phi
+     else begin
+       incr cache2_hit;
+       phi
+     end
 
    type trivalent = False | True | Unknown
    let of_bool = function false -> False | true -> True
@@ -201,14 +230,12 @@ END
 
  (* Define as macros to get lazyness *)
 DEFINE OR_(t1,t2) =
-     let __t1 = (t1) in
      match t1 with
        False -> (t2)
      | True -> True
      | Unknown -> if (t2) == True then True else Unknown
 
 DEFINE AND_(t1,t2) =
-     let __t1 = (t1) in
      match t1 with
        False -> False
      | True -> (t2)
@@ -226,14 +253,16 @@ DEFINE AND_(t1,t2) =
                  let open NodeSummary in
                      match a.Atom.node with
                      | Move (m, q) ->
-                         let { NodeStatus.node = n_sum; _ } as sum =
+                         let down, ({ NodeStatus.node = n_sum; _ } as sum) =
                            match m with
-                             `First_child -> fcs
-                           | `Next_sibling -> nss
-                           | `Parent | `Previous_sibling -> ps
-                           | `Stay -> ss
+                             `First_child -> true, fcs
+                           | `Next_sibling -> true, nss
+                           | `Parent | `Previous_sibling -> false, ps
+                           | `Stay -> false, ss
                          in
-                         if sum == dummy_status || StateSet.mem q n_sum.todo then
+                         if sum == dummy_status
+                           || (down && n_sum.rank < ss.NodeStatus.node.rank)
+                           || StateSet.mem q n_sum.todo then
                            Unknown
                          else
                            of_bool (b == StateSet.mem q n_sum.sat)
@@ -260,6 +289,7 @@ DEFINE AND_(t1,t2) =
          let phi =
            get_form cache2 auto tag q
          in
+
          let v = eval_form phi fcs nss ps old_status old_summary in
          match v with
            True -> StateSet.add q a_sat, a_todo
@@ -285,7 +315,8 @@ DEFINE AND_(t1,t2) =
      let ssid = (ss.NodeStatus.id :> int) in
      let tagid = (tag.QName.id :> int) in
      let res = Cache.N5.find cache5 tagid ssid fcsid nssid psid in
-     if res != dummy_status then res
+     incr cache5_access;
+     if res != dummy_status then begin incr cache5_hit; res end
      else let new_status = loop ss in
           Cache.N5.add cache5 tagid ssid fcsid nssid psid new_status;
           new_status
@@ -293,15 +324,23 @@ DEFINE AND_(t1,t2) =
 
 
   let top_down run =
+    let i = run.pass in
     let tree = run.tree in
     let auto = run.auto in
     let status = run.status in
     let cache2 = run.cache2 in
     let cache5 = run.cache5 in
     let unstable = run.unstable 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
+      else
+        states_by_rank.(i+1)
+    in
     let rec loop node =
       let node_id = T.preorder tree node in
-      if node == T.nil || not (Bitvector.get unstable node_id) then false else begin
+      if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false
+      else begin
         let parent = T.parent tree node in
         let fc = T.first_child tree node in
         let fc_id = T.preorder tree fc in
@@ -312,110 +351,97 @@ DEFINE AND_(t1,t2) =
 
         let status0 =
           let c = unsafe_get_status status node_id in
-          if c == dummy_status then
-            (* first time we visit the node *)
+          if c.NodeStatus.node.rank < i then
+            (* first time we visit the node during this run *)
             NodeStatus.make
-              { sat = StateSet.empty;
-                todo = StateSet.diff
-                  (Ata.get_states auto)
-                  (Ata.get_starting_states auto);
-                summary = NodeSummary.make
-                  (node == T.first_child tree parent) (* is_left *)
-                  (node == T.next_sibling tree parent) (* is_right *)
-                  (fc != T.nil) (* has_left *)
-                  (ns != T.nil) (* has_right *)
-                  (T.kind tree node) (* kind *)
+              { rank = i;
+                sat = c.NodeStatus.node.sat;
+                todo = td_todo;
+                summary = let summary = c.NodeStatus.node.summary
+                          in
+                          if summary != NodeSummary.dummy then summary
+                          else
+                            NodeSummary.make
+                              (node == T.first_child tree parent) (* is_left *)
+                              (node == T.next_sibling tree parent) (* is_right *)
+                              (fc != T.nil) (* has_left *)
+                              (ns != T.nil) (* has_right *)
+                              (T.kind tree node) (* kind *)
               }
           else c
         in
-        TRACE(html tree node _i config0 "Entering node");
-
+        IFTRACE(html tree node _i status0 "Entering node");
         (* get the node_statuses for the first child, next sibling and parent *)
         let ps = unsafe_get_status status (T.preorder tree parent) in
         let fcs = unsafe_get_status status fc_id in
         let nss = unsafe_get_status status ns_id in
         (* evaluate the transitions with all this statuses *)
-        let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in
-        TRACE(html tree node _i config1 "Updating transitions");
-
-        (* update the cache if the status of the node changed *)
-
-        if status1 != status0 then status.(node_id) <- status1;
+        let status1 =
+          if status0.NodeStatus.node.todo == StateSet.empty then status0
+          else begin
+            let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in
+            IFTRACE(html tree node _i status1 "Updating transitions");
+          (* update the cache if the status of the node changed *)
+            if status1 != status0 then status.(node_id) <- status1;
+            status1
+          end
+        in
         (* recursively traverse the first child *)
         let unstable_left = loop fc in
         (* here we re-enter the node from its first child,
            get the new status of the first child *)
         let fcs1 = unsafe_get_status status fc_id in
         (* update the status *)
-        let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in
-
-        TRACE(html tree node _i config2 "Updating transitions (after first-child)");
-
-        if status2 != status1 then status.(node_id) <- status2;
+        let status1 = if status1.NodeStatus.node.rank < i then
+            NodeStatus.make { status1.NodeStatus.node with
+              rank = i;
+              todo = bu_todo }
+          else
+            status1
+        in
+        let status2 =
+          if status1.NodeStatus.node.todo == StateSet.empty then status1
+          else begin
+            let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in
+            IFTRACE(html tree node _i status2
+                      "Updating transitions (after first-child)");
+            if status2 != status1 then status.(node_id) <- status2;
+            status2
+          end
+        in
         let unstable_right = loop ns in
         let nss1 = unsafe_get_status status ns_id in
-        let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
-
-        TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
-
-        if status3 != status2 then status.(node_id) <- status3;
-
+        let status3 =
+          if status2.NodeStatus.node.todo == StateSet.empty then status2
+          else begin
+            let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
+            IFTRACE(html tree node _i status3
+                      "Updating transitions (after next-sibling)");
+          if status3 != status2 then status.(node_id) <- status3;
+          status3
+        end
+        in
         let unstable_self =
-          (* if either our left or right child is unstable or if we still have transitions
-             pending, the current node is unstable *)
+          (* if either our left or right child is unstable or if we
+             still have transitions pending, the current node is
+             unstable *)
           unstable_left
           || unstable_right
           || StateSet.empty != status3.NodeStatus.node.todo
         in
         Bitvector.unsafe_set unstable node_id unstable_self;
-        TRACE((if not unstable_self then
+        IFTRACE((if not unstable_self then
             Html.finalize_node
               node_id
               _i
-              Ata.(StateSet.intersect config3.Config.node.sat auto.selection_states)));
+              Ata.(StateSet.intersect status3.NodeStatus.node.sat
+                     (get_selecting_states auto))));
         unstable_self
       end
     in
     run.redo <- loop (T.root tree);
     run.pass <- run.pass + 1
 
-(*
-  let stats run =
-    let count = ref 0 in
-    let len = Bitvector.length run.unstable in
-    for i = 0 to len - 1 do
-      if not (Bitvector.unsafe_get run.unstable i) then
-        incr count
-    done;
-    Logger.msg `STATS
-      "%i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b"
-      !count len run.pass (100. *. (float !count /. float len))
-      run.redo
-
-
-  let eval auto tree node =
-    let len = T.size tree in
-    let run = { config = Array.create len Ata.dummy_config;
-                unstable = Bitvector.create ~init:true len;
-                redo = true;
-                pass = 0
-              }
-    in
-    while run.redo do
-      run.redo <- false;
-      Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *)
-      run.redo <- top_down_run auto tree node run;
-      stats run;
-      run.pass <- run.pass + 1;
-    done;
-    at_exit (fun () -> Logger.msg `STATS "%i iterations" run.pass);
-    at_exit (fun () -> stats run);
-    let r = get_results auto tree node run.config in
-
-    TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree));
-
-    r
-*)
 
   let get_results run =
     let cache = run.status in
@@ -446,23 +472,30 @@ DEFINE AND_(t1,t2) =
         (fun q -> Hashtbl.add res_mapper q [])
         (Ata.get_selecting_states auto)
     in
+    let dummy = [ T.nil ] in
+    let res_mapper = Cache.N1.create dummy in
+    let () =
+      StateSet.iter
+        (fun q -> Cache.N1.add res_mapper (q :> int) [])
+        (Ata.get_selecting_states auto)
+    in
     let rec loop node =
       if node != T.nil then
         let () = loop (T.next_sibling tree node) in
         let () = loop (T.first_child tree node) in
         StateSet.iter
           (fun q ->
-            try
-              let acc = Hashtbl.find res_mapper q in
-              Hashtbl.replace res_mapper q (node::acc)
-            with
-              Not_found -> ())
+            let res = Cache.N1.find res_mapper (q :> int) in
+            if res != dummy then
+              Cache.N1.add res_mapper (q :> int) (node::res)
+          )
           cache.(T.preorder tree node).NodeStatus.node.sat
     in
     loop (T.root tree);
-    StateSet.fold
-      (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
-      (Ata.get_selecting_states auto) []
+    (StateSet.fold_right
+       (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
+       (Ata.get_selecting_states auto) [])
+
 
   let prepare_run run list =
     let tree = run.tree in
@@ -474,7 +507,8 @@ DEFINE AND_(t1,t2) =
       let ns = T.next_sibling tree node in
       let status0 =
         NodeStatus.make
-          { sat = Ata.get_starting_states auto;
+          { rank = 0;
+            sat = Ata.get_starting_states auto;
             todo =
               StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto);
             summary = NodeSummary.make
@@ -488,25 +522,36 @@ DEFINE AND_(t1,t2) =
       let node_id = T.preorder tree node in
       status.(node_id) <- status0) list
 
-
-  let eval full auto tree nodes =
+  let tree_size = ref 0
+  let pass = ref 0
+  let compute_run auto tree nodes =
+    pass := 0;
+    tree_size := T.size tree;
     let run = make auto tree in
     prepare_run run nodes;
-    while run.redo do
+    for i = 0 to Ata.get_max_rank auto do
       top_down run
     done;
-    if full then `Full (get_full_results run)
-    else `Normal (get_results run)
+    pass := Ata.get_max_rank auto + 1;
+    IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);
 
+    run
 
   let full_eval auto tree nodes =
-    match eval true auto tree nodes with
-      `Full l -> l
-    | _ -> assert false
+    let r = compute_run auto tree nodes in
+    get_full_results r
 
   let eval auto tree nodes =
-    match eval false auto tree nodes with
-      `Normal l -> l
-    | _ -> assert false
+    let r = compute_run auto tree nodes in
+    get_results r
+
+  let stats () = {
+    tree_size = !tree_size;
+    run = !pass;
+    cache2_access = !cache2_access;
+    cache2_hit = !cache2_hit;
+    cache5_access = !cache5_access;
+    cache5_hit = !cache5_hit;
+  }
 
 end