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