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 19bcf6f..3192773 100644 (file)
--- a/src/auto/eval.ml
+++ b/src/auto/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 19:02:13 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)
 
@@ -106,15 +116,8 @@ module Make (T : Tree.Sig.S) :
   in
   loop ltrs ss
 
-  let top_down_run auto tree node cache _i =
+  let top_down_run auto tree node cache trans_cache2 trans_cache6  _i =
     let redo = ref false in
-    let dummy2 = Ata.TransList.cons
-      (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_))
-      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 rec loop node =
       if node != T.nil then begin
         let parent = T.parent tree node in
@@ -127,7 +130,7 @@ module Make (T : Tree.Sig.S) :
             Cache.N2.find trans_cache2
               (tag.QName.id :> int) (auto.Ata.states.StateSet.id :> int)
           in
-          if trs == dummy2 then
+          if trs == Cache.N2.dummy trans_cache2 then
             let trs = Ata.get_trans auto auto.Ata.states tag in
             (Cache.N2.add
               trans_cache2
@@ -135,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
@@ -148,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
@@ -181,13 +197,30 @@ 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
+      (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_))
+      Ata.TransList.nil
+    in
+    let dummy6 = (dummy2, StateSet.empty) 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
+      Cache.N6.iteri (fun _ _ _ _ _ _ _ b  -> if not b then incr num_phi) trans_cache6;
+      Cache.N2.iteri (fun _ _ _ b -> if not b then incr num_trans) trans_cache2;
+      Format.eprintf "PROFILE:materialized %i transitions and %i configurations\n@." !num_trans !num_phi
+    )
+    in
     while !redo do
-      redo := top_down_run auto tree node cache !iter;
+      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