X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Feval.ml;h=31927737d3375625bce86f92251d4b334884bf7f;hp=a5b30f18ee42ac497557a8753b15b9335b341faf;hb=ce09a30489dce8ac9e389c8c1525a34d1e02354e;hpb=3b653edd20248b66a005637c2b1e217042cef62b diff --git a/src/auto/eval.ml b/src/auto/eval.ml index a5b30f1..3192773 100644 --- a/src/auto/eval.ml +++ b/src/auto/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) 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
Pre Trans: %a
" + 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
TD Trans: %a
" 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
Left BU Trans: %a
" 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
Right BU Trans: %a
" 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