constant N := 3; constant M := 2; shadow variable e[Nat % N] <- Nat % 2; puppet variable x[Nat % N] <- Nat % M; ((future & silent) % puppet) (forall i <- Nat % N : // No two adjacent edges can be selected. !(e[i]==1 && e[i+1]==1) && // At least one of every three consecutive edges must be selected. (e[i-1]==1 || e[i]==1 || e[i+1]==1) ); process P[i <- Nat % N] { read: x[i-1]; write: e[i]; // Left edge. write: x[i]; write: e[i+1]; // Right edge. read: x[i+1]; }