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