Add a 'trace' mode (must be enabled at build time) that saves the

[tatoo.git] / src / auto / eval.ml

diff --git a/src/auto/eval.ml b/src/auto/eval.ml
index 71adf56..3192773 100644 (file)
--- a/src/auto/eval.ml
+++ b/src/auto/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-14 11:12:24 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-14 19:13:55 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -27,6 +27,16 @@ module Make (T : Tree.Sig.S) :
   end
  = struct
 
+
+IFDEF HTMLTRACE
+  THEN
+DEFINE TRACE(e) = (e)
+  ELSE
+DEFINE TRACE(e) = ()
+END
+
+
+
   type cache = StateSet.t Cache.N1.t
   let get c t n = Cache.N1.find c (T.preorder t n)
 
@@ -128,6 +138,10 @@ module Make (T : Tree.Sig.S) :
               (auto.Ata.states.StateSet.id :> int) trs; trs)
           else trs
         in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a<br/>Pre Trans: %a<br/>"
+                  StateSet.print states0 Ata.TransList.print trans0)
+        in
         let ps = get cache tree parent in
         let fcs = get cache tree fc in
         let nss = get cache tree ns in
@@ -141,17 +155,26 @@ module Make (T : Tree.Sig.S) :
         let trans1, states1 =
           eval_trans trans_cache6 trans0 node_info fcs nss ps states0
         in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "TD States: %a<br/>TD Trans: %a<br/>" StateSet.print states1 Ata.TransList.print trans1)
+        in
         if states1 != states0 then set cache tree node states1;
         let () = loop fc in
         let fcs1 = get cache tree fc in
         let trans2, states2 =
           eval_trans trans_cache6 trans1 node_info fcs1 nss ps states1
         in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a<br/>Left BU Trans: %a<br/>" StateSet.print states2 Ata.TransList.print trans2)
+        in
         if states2 != states1 then set cache tree node states2;
         let () = loop ns in
-        let _, states3 =
+        let _trans3, states3 =
           eval_trans trans_cache6 trans2 node_info fcs1 (get cache tree ns) ps states2
         in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a<br/>Right BU Trans: %a<br/>" StateSet.print states3 Ata.TransList.print _trans3)
+        in
         if states3 != states2 then set cache tree node states3;
         if states0 != states3 && (not !redo) then redo := true
       end
@@ -174,7 +197,7 @@ module Make (T : Tree.Sig.S) :
     loop node []
 
   let eval auto tree node =
-    let cache = Cache.N1.create (T.size tree) StateSet.empty in
+    let cache = Cache.N1.create StateSet.empty in
     let redo = ref true in
     let iter = ref 0 in
     let dummy2 = Ata.TransList.cons
@@ -182,8 +205,8 @@ module Make (T : Tree.Sig.S) :
       Ata.TransList.nil
     in
     let dummy6 = (dummy2, StateSet.empty) in
-    let trans_cache6 = Cache.N6.create 17 dummy6 in
-    let trans_cache2 = Cache.N2.create 17 dummy2 in
+    let trans_cache6 = Cache.N6.create dummy6 in
+    let trans_cache2 = Cache.N2.create dummy2 in
     let () = at_exit (fun () ->
       let num_phi = ref 0 in
       let num_trans = ref 0 in
@@ -196,6 +219,8 @@ module Make (T : Tree.Sig.S) :
       redo := top_down_run auto tree node cache trans_cache2 trans_cache6 !iter;
       incr iter;
     done;
-    get_results auto tree node cache
+    let r = get_results auto tree node cache in
+    TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree));
+    r
 
 end