SortRing.prot

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

variable x[N] < M;

// Assumed initial states.
// Exactly one x[i] is zero.
(assume & closed)
  (unique i < N : x[i]==0);

// Want to converge to a state where the values are sorted
// starting from the zero value.
(future & silent)
  (forall i < N :
   x[i] <= x[i+1]
   ||
   x[i+1]==0
  );


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

  // Only permit actions that swap x[i] and x[i+1] values.
  permit:
    ( true --> x[i]:=x[i+1]; x[i+1]:=x[i]; )
    ;

  puppet action:
    ( x[i+1]!=0 && x[i] > x[i+1] --> x[i]:=x[i+1]; x[i+1]:=x[i]; )
    ;
}