MODULE main DEFINE N := 7;

VAR
  loc  : array 1..N of 0..2;
  c    : array 1..N of 0..1;

  for (k=1;k<N;k=k+1)
  {
    P[k] : process CM(k,loc[k],c[k],c[k+1]);
  }
  P[N] : process CM(N,loc[N],c[N],c[1]);

  Id   : Idle;

ASSIGN

  for (k=1;k<N;k=k+1)
  {
    init(c[k]) := 1;
  }


MODULE Idle

MODULE CM(i,loc,left,right)

ASSIGN
  init(loc)   := 0;

  next(loc) := case
                 loc = 0           : {0,1};
                 loc = 1 & left=1  : 2;
                 loc = 2           : 0;
                 1                 : loc;
               esac;

  next(left) := case
                  loc=0 & left  : 0;
                  1             : left;
                esac;
  next(right):= case
                  loc=0 & left  : 1;
                  1	        : right;
                esac;


JUSTICE
  !((loc = 0) & left),
  !((loc = 1) & left),
  loc != 2