- 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)
- in
- if states3 != states2 then set cache tree node states3;
- (*if states0 != states3 && (not !redo) then redo := true *)
- if (not !redo)
- && not (Ata.TransList.nil == _trans3)
- && (states1 != states3)
- && not (StateSet.intersect states3 auto.Ata.selection_states)
+ let config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in
+
+ TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
+
+ if config2 != config3 then set cache tree node config3;
+ (* We do set the redo flat if : *)
+ if not (
+ config0 == config3 (* did not gain any new information *)
+ || !redo (* already set *)
+ || Ata.TransList.nil == config3.Ata.Config.node.Ata.todo ) (* no more transition to check *)