never { accept_init: s0_init: if :: (p) -> goto s1 :: !(p) -> goto s2 fi; s1: if :: (p) -> goto s1 :: !(p) -> goto accept_s3 fi; s2: if :: (p) -> goto s1 :: !(p) -> goto s2 fi; accept_s3: if :: (1) -> goto accept_s3 fi; }