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