[simiones]

Sure, that's a natural way of reading this requirement, but is it the right way? How would you specify the system such that it can produce:

[(x, y), (!x, y), (!x, !y), (x, !y), (!x, y), ...]

(that is, any interleaving of the two blinks that preserves the constraint that there is at least one blink in each "step")

[contravariant]

If you ask me requiring at least one blink in each step is a bit awkward as it is a global requirement as opposed to a local one.

But you can add the requirement Next(World) <> World if you really want to. Then you just get two sets:

- Next(World) <> World

- Next(World).x in (World.x, !World.x)

and

- Next(World) <> World

- Next(World).y in (World.y, !World.y)

and if you combine them you get

- Next(World) <> World

- Next(World).x in (World.x, !World.x)

- Next(World).y in (World.y, !World.y)

which seems to do what you want.

Adding global constraints seems like an easy way to shoot yourself in the foot though.