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