// This is a solution for examplespec/TokenRingSuperpos.prot // using 4 states per process (M==2). // Though it is only stabilizing when 2 <= N <= 7. constant M := 2; constant N := 3; variable t[Nat % N] <- Nat % 2; puppet variable x[Nat % N] <- Nat % M; (future & shadow) (unique i <- Nat % N : i==0 && t[i-1]==t[i] || i!=0 && t[i-1]!=t[i]) ; process Bot[i <- Nat % 1] { read: t[i-1]; read: x[i-1]; write: t[i]; write: x[i]; shadow action: ( t[i-1]==t[i] --> t[i]:=1-t[i-1]; ) ; puppet action: ( x[i-1]==x[i] && t[i-1]!=t[i] --> x[i]:=1-x[i]; ) ( x[i-1]==x[i] && t[i-1]==t[i] --> x[i]:=1-x[i]; t[i]:=x[i-1]; ) ; } process P[j <- Nat % (N-1)] { let i := j+1; read: t[i-1]; read: x[i-1]; write: t[i]; write: x[i]; shadow action: ( t[i-1]!=t[i] --> t[i]:=t[i-1]; ) ; puppet action: ( x[i-1]!=x[i] && t[i-1]==t[i] --> x[i]:=1-x[i]; ) ( x[i-1]!=x[i] && t[i-1]!=t[i] --> x[i]:=1-x[i]; t[i]:=x[i-1]; ) ; }