temp commit.

[tatoo.git] / src / eval.ml

diff --git a/src/eval.ml b/src/eval.ml
index 5eb7e29..358a7a7 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-04-24 18:41:35 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-24 21:54:43 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -38,11 +38,11 @@ END
      let config = config.Ata.Config.node in
      let oldi = config.Ata.round in
      Html.trace (T.preorder tree node) i oldi
-       "%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
+       "%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>unstable_subtree: %b<br/>"
        msg
        StateSet.print config.Ata.sat
        StateSet.print config.Ata.unsat
-       (Ata.TransList.print ~sep:"<br/>") config.Ata.todo oldi
+       (Ata.TransList.print ~sep:"<br/>") config.Ata.todo oldi config.Ata.unstable_subtree
 
 
   type cache = StateSet.t Cache.N1.t
@@ -86,15 +86,20 @@ END
         TRACE(html tree node _i config1 "Updating transitions");
 
         if config0 != config1 then set cache tree node config1 _i;
-        let unstable_left = loop fc in
+        if not Ata.(fcs.Config.node.unstable_subtree) then
+          Printf.eprintf "Could skip left subtree!%!";
+        let unstable_left = Ata.(fcs.Config.node.unstable_subtree) && loop fc in
         let fcs1 = get cache tree fc in
         let config2 = Ata.eval_trans auto fcs1 nss ps config1 in
 
         TRACE(html tree node _i config2 "Updating transitions (after first-child)");
 
         if config1 != config2 then set cache tree node config2 _i;
-        let unstable_right = loop ns in
-        let config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in
+        if not Ata.(nss.Config.node.unstable_subtree) then
+          Printf.eprintf "Could skip right subtree!%!";
+        let unstable_right = Ata.(nss.Config.node.unstable_subtree) && loop ns in
+        let nss1 = get cache tree ns in
+        let config3 = Ata.eval_trans auto fcs1 nss1 ps config2 in
 
         TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
 
@@ -102,10 +107,10 @@ END
         let unstable =
           unstable_left
           || unstable_right
-          || (config0 != config3 && Ata.(TransList.nil != config3.Config.node.todo))
+          || Ata.(TransList.nil != config3.Config.node.todo)
         in
         if Ata.(unstable && not config3.Config.node.unstable_subtree) then
-          Ata.(config3.Config.node.unstable_subtree <- unstable);
+          Ata.(config3.Config.node.unstable_subtree <- true);
         unstable
       end
     in