- 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)
+ if not (Ata.eq_config 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.todo) (* no more transition to check *)
+ || (Ata.eq_config config0 config3) (* did not gain any new information *)
+ )