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