OrientRingViaToken.prot

// Ring orientation
// Title: Uniform Self-Stabilizing Ring Orientation
// Author: Amos Israeli
// Author: Marc Jalfon
// Year: 1993

// Synthesis for this is MUCH TOO DIFFICULT at the moment
// due to the high number of candidate actions!

constant N := 3;

puppet variable c[N] < 3;
puppet variable tok[N] < 3;
direct variable way[(2*N)] < 2;

process P[i < N]
{
  symmetric (j, way_idx, adj_way_idx, adj_way_idx_far)
    <- {# (i-1, 2*i, 2*i-1, 2*i-2), (i+1, 2*i+1, 2*i+2, 2*i+3) #}
  {
    read: c[j];
    read: tok[j];
    read: way[adj_way_idx];
    read: way[adj_way_idx_far];
    write: way[way_idx];
  }
  write: c[i];
  write: tok[i];

  (assume & closed)
    (way[2*i] != way[2*i+1]);

  forbid: ( way[2*i-2]==way[2*i-1] --> );
  forbid: ( way[2*i+0]==way[2*i+1] --> );
  forbid: ( way[2*i+2]==way[2*i+3] --> );
}

// Eventually, all processes are pointing in the same direction.
((future & shadow) % puppet)
  (forall i < (2*N) : way[i] != way[i-1])
  ;