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