- 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 config3 _i;
+ let unstable =
+ unstable_left
+ || unstable_right
+ || (config0 != config3 && 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);
+ unstable