- if states1 != states0 then set cache tree node states1;
- let () = loop fc in
- let fcs1 = get cache tree fc in
- let trans2, states2 =
- Ata.eval_trans auto trans1
- fcs1 nss ps states1
- is_left is_right has_left has_right kind
- 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 ~sep:"<br/>") trans2)
- in
- if states2 != states1 then set cache tree node states2;
- let () = loop ns in
- let _trans3, states3 =
- Ata.eval_trans auto trans2
- fcs1 (get cache tree ns) ps states2
- is_left is_right has_left has_right kind
- 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 ~sep:"<br/>") _trans3)
+
+ TRACE(html tree node _i config0 "Entering node");
+
+ let ps = cache.(T.preorder tree parent) in
+ let fcs = cache.(fc_id) in
+ let nss = cache.(ns_id) in
+ let config1 = Ata.eval_trans auto fcs nss ps config0 in
+
+ TRACE(html tree node _i config1 "Updating transitions");
+
+ if config0 != config1 then cache.(node_id) <- config1;
+ let unstable_left = loop fc in
+ let fcs1 = cache.(fc_id) 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 cache.(node_id) <- config2;
+ let unstable_right = loop ns in
+ let nss1 = cache.(ns_id) in
+ let config3 = Ata.eval_trans auto fcs1 nss1 ps config2 in
+
+ TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
+
+ if config2 != config3 then cache.(node_id) <- config3;
+ let unstable_self =
+ unstable_left
+ || unstable_right
+ || Ata.(TransList.nil != config3.Config.node.todo)