- if states3 != states2 then set cache tree node states3;
- if states0 != states3 && (not !redo) then redo := true
+ if config2 != config3 then set cache tree node config3;
+ (* We do set the redo flat if : *)
+ if not (
+ !redo (* already set *)
+ || (Ata.TransList.nil == config3.Ata.Config.node.Ata.todo) (* no more transition to check *)
+ || (config0 == config3) (* did not gain any new information *)
+ )
+ then redo := true