ColorUniRing.prot

constant N := 3;

variable x[N] < 3;

process P[i < N]
{
  read: x[i-1];
  random write: x[i];

  (future & silent)
    (x[i-1]!=x[i]);
}