never { s0_init: if :: (p) -> goto accept_s1 :: !(p) -> goto s0_init fi; accept_s1: if :: (1) -> goto accept_s1 fi; }