X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Feval.ml;h=f3b81cbde3561a322cebac445238689437f326a8;hp=4647b84feec81f7c04c9545ba1ce60b12143656d;hb=249bd234500a64919cf00f4a59ab4927a068d689;hpb=8026ca9faaa968ced3c2e75ca1d6b55f7270ca50

diff --git a/src/auto/eval.ml b/src/auto/eval.ml
index 4647b84..f3b81cb 100644
--- a/src/auto/eval.ml
+++ b/src/auto/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-05 16:24:35 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-05 18:35:19 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -33,6 +33,7 @@ module Make (T : Tree.Sig.S) = struct
 
   let eval_trans l ctx acc =
     List.fold_left (fun (acct, accs) ((q, phi) as trs) ->
+      if StateSet.mem q accs then (acct, accs) else
       if Ata.SFormula.eval ctx phi then
         (acct, StateSet.add q accs)
       else
@@ -49,18 +50,19 @@ module Make (T : Tree.Sig.S) = struct
         let states0 = get cache tree node in
         let tag = T.tag tree node in
         let trans0 = Ata.get_trans auto auto.Ata.states tag in
-        let parent_states = if parent == T.nil then auto.Ata.top_states else get cache tree parent in
-        let fc_states = if fc == T.nil then auto.Ata.bottom_states else get cache tree fc in
-        let ns_states = if ns == T.nil then auto.Ata.bottom_states else get cache tree ns in
+        let parent_states = (*if parent == T.nil then auto.Ata.top_states else*) get cache tree parent in
+        let fc_states = (*if fc == T.nil then auto.Ata.bottom_states else*) get cache tree fc in
+        let ns_states = (*if ns == T.nil then auto.Ata.bottom_states else*) get cache tree ns in
+        let is_root = parent == T.nil in
         let ctx0 =
           if is_left then
-            Ata.make_ctx fc_states ns_states parent_states  StateSet.empty states0
+            Ata.make_ctx fc_states ns_states parent_states  StateSet.empty states0 is_left is_root
           else
-            Ata.make_ctx fc_states ns_states StateSet.empty parent_states states0
+            Ata.make_ctx fc_states ns_states StateSet.empty parent_states states0 is_left is_root
         in
-        eprintf "[Iteration % 4d] node: %a, context: %a\n%!"
+        eprintf "-- [Iteration % 4d] --\n node: %a\n context: %a\n%!"
           i T.print_node node Ata.print_ctx ctx0;
-        List.iter (fun (q, phi) -> eprintf "%a -> %a\n" State.print q Ata.SFormula.print phi) trans0;
+        List.iter (fun (q, phi) -> eprintf " %a -> %a\n" State.print q Ata.SFormula.print phi) trans0;
         eprintf "----------------------\n%!";
         let trans1, states1 = eval_trans trans0 ctx0 StateSet.empty in
         if states1 != states0 then set cache tree node states1;