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