Write a spec for two independent counters x and y, each cycling through
0, 1, 2 and wrapping back to 0 — like two hour clocks running side by
side, never affecting each other.
Requirements:
x and y, both starting at 0.TypeOK: both x and y are always in 0..2.IncX: advances x by one, wrapping from 2 back to 0; leaves y
unchanged. (% is modulo — (x + 1) % 3 wraps 2 -> 0 automatically.)IncY: the mirror image for y.Next: IncX \/ IncY — at each step, exactly one counter advances.Spec: Init conjoined with [][Next]_vars, where vars == <<x, y>>.Fill in starter.tla where marked, then click Run Model Checker. TLC
should report no invariant violations.