// Ring orientation // Title: Uniform Self-Stabilizing Ring Orientation // Author: Amos Israeli // Author: Marc Jalfon // Year: 1993 constant N := 3; direct variable c[Nat % N] <- Nat % 3; puppet variable tok[Nat % N] <- Nat % 3; // R S I direct variable way[Nat % (2*N)] <- Nat % 2; process P[i <- Nat % 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]; } read: c[i]; write: tok[i]; (assume & closed) (c[i] != c[i-1]); (assume & closed) (way[2*i] != way[2*i+1]); predicate depsat := way[2*i-2]!=way[2*i-1] && way[2*i+0]!=way[2*i+1] && way[2*i+2]!=way[2*i+3] && c[i-1]!=c[i] && c[i]!=c[i+1] ; puppet action: // 1 ( depsat && tok[i-1]==1 && way[2*i-1]==1 && tok[i]==2 --> tok[i]:=0; way[2*i+0]:=0; way[2*i+1]:=1; ) ( depsat && tok[i+1]==1 && way[2*i+2]==1 && tok[i]==2 --> tok[i]:=0; way[2*i+1]:=0; way[2*i+0]:=1; ) // 2 ( depsat && tok[i-1]==0 && way[2*i-1]==0 && tok[i]==1 && way[2*i+0]==1 && way[2*i+1]==0 --> tok[i]:=2; ) ( depsat && tok[i+1]==0 && way[2*i+2]==0 && tok[i]==1 && way[2*i+1]==1 && way[2*i+0]==0 --> tok[i]:=2; ) // 3 ( depsat && !(tok[i-1]==1 && way[2*i-1]==1) && tok[i]==0 && way[2*i+0]==0 --> tok[i]:=1; ) ( depsat && !(tok[i+1]==1 && way[2*i+2]==1) && tok[i]==0 && way[2*i+1]==0 --> tok[i]:=1; ) // 4 ( depsat && tok[i-1]==1 && way[2*i-1]==1 && tok[i]==1 && way[2*i+0]==1 && c[i-1]==(c[i]+1)%3 --> tok[i]:=0; way[2*i+0]:=0; way[2*i+1]:=1; ) ( depsat && tok[i+1]==1 && way[2*i+2]==1 && tok[i]==1 && way[2*i+1]==1 && c[i+1]==(c[i]+1)%3 --> tok[i]:=0; way[2*i+1]:=0; way[2*i+0]:=1; ) // 5 ( depsat && tok[i-1]==2 && way[2*i-1]==1 && tok[i]==2 && way[2*i+0]==1 && c[i-1]==(c[i]+1)%3 --> tok[i]:=1; ) ( depsat && tok[i+1]==2 && way[2*i+2]==1 && tok[i]==2 && way[2*i+1]==1 && c[i+1]==(c[i]+1)%3 --> tok[i]:=1; ) ; } ((future & shadow) % puppet) (forall i <- Nat % N : way[2*i-1] == way[2*i+1]);