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