constant N := 4; constant M := 5; variable x[Nat % N] <- Nat % M; // Assumed initial states. // Exactly one x[i] is zero. (assume & closed) (unique i <- Nat % N : x[i]==0); // Want to converge to a state where the values are sorted // starting from the zero value. (future & silent) (forall i <- Nat % N : x[i] <= x[i+1] || x[i+1]==0 ); process P[i <- Nat % N] { write: x[i]; write: x[i+1]; // Only permit actions which 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]; ) ; }