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 a5b30f1..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 13:52:04 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
@@ -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