what does the never claim verify in this promela model

Question

bool p = true;

active proctype q() {
  do
    :: p=false; p=true; p=false
  od
}

never {
do
  :: !p -> goto acceptRun
  :: else -> skip; skip
od;
acceptRun : skip

}

In this promela model, the never claim verifies that initially and then at every second time step p holds. Why? Thanks!

Answer 1

A never claim takes one step with every step of the model. So if !p the next step will be the accept state (never claim fails). But if p then the never claim will need two addition steps before it returns to checking on p again.

While the claim is not 'looking for p', you can 'sneak in' some other value for p.