- 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 *)
- then redo := true
+ if config2 != config3 then set cache tree node (true, config3) _i;
+ let unstable =
+ unstable_left
+ || unstable_right
+ || Ata.(TransList.nil != config3.Config.node.todo)
+ in
+ if Ata.(config3.Config.node.unstable_subtree) && not unstable then
+ Ata.(config3.Config.node.unstable_subtree <- false);
+ unstable