ColorRing.prot

// 3-coloring protocol
// We want no two adjacent colors to be the same.

constant N := 3;

variable x[N] < 3;

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

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