constant N := 4; constant M := 5; variable x[Nat % N] <- Nat % M; // Want to converge to a state where the array is sorted. (future & silent) (forall i <- Nat % (N-1) : x[i] <= x[i+1] ); process P[i <- Nat % (N-1)] { 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]; ) ; }