TokenRingDijkstra.prot

// This is a clever way to specify the problem of synthesizing
// Dijkstra's token ring without shadow/puppet variables.
// Usually we are not so clever and would use the
// approach given in examplespec/TokenRing.prot.

constant N := 5;
constant M := N;

variable x[N] < M;

// Eventually one token will exist and the protocol will remain live.
// A token here is deviates from Dijkstra's definition in that
// a P[i] process only has a token when (x[i-1]==(x[i]+1)%M)
// rather than the more relaxed version (x[i-1]!=x[i]).
(future & active shadow)
  (exists j < N :
   forall i < N : false
   || i==0 && i==j && x[i-1]==x[i]
   || i==0 && i!=j && x[i-1]!=x[i]
   || i!=0 && i==j && x[i-1]==(x[i]+1)%M
   || i!=0 && i!=j && x[i-1]==x[i]
  );


process Bot[i < 1]
{
  read:  x[i-1];
  write: x[i];

  // Actions in the legitimate states:
  shadow action: ( x[i-1] == x[i] --> x[i] := x[i] + 1; );
}

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

  // Actions in the legitimate states:
  shadow action: ( x[i-1] == (x[i] + 1) % M --> x[i] := x[i] + 1; );
}