never { accept_init: s0_init: if :: (p) && !(q) -> goto s2 :: !(p) && !(q) -> goto s3 :: (q) -> goto accept_s1 fi; s2: if :: !(p) && !(q) -> goto s6 :: (p) && !(q) -> goto accept_s14 :: (q) -> goto accept_s1 fi; s3: if :: (p) && !(q) -> goto s5 :: !(p) && !(q) -> goto s6 :: (q) -> goto s4 fi; s4: if :: (1) -> goto s8 fi; s5: if :: (p) && !(q) -> goto s9 :: !(p) && !(q) -> goto s10 :: (q) -> goto s8 fi; s6: if :: !(q) -> goto s6 :: (q) -> goto s7 fi; s7: if :: (1) -> goto s7 fi; s8: if :: (1) -> goto s4 fi; s9: if :: (q) -> goto s4 :: !(p) && !(q) -> goto s12 :: (p) && !(q) -> goto s5 fi; s10: if :: (q) -> goto s11 :: !(q) -> goto s12 fi; s11: if :: (1) -> goto s13 fi; s12: if :: !(q) -> goto s10 :: (q) -> goto s13 fi; s13: if :: (1) -> goto s11 fi; accept_s1: if :: (1) -> goto accept_s1 fi; accept_s14: if :: !(p) && !(q) -> goto s6 :: (p) && !(q) -> goto accept_s14 :: (q) -> goto accept_s1 fi; }