never { s0_init: if :: (p) && !(q) -> goto s1 :: (p) && (q) -> goto s3 :: !(p) && (q) -> goto s3 :: (p) && !(q) -> goto s3 :: !(p) && !(q) -> goto s3 fi; s1: if :: (p) && !(q) -> goto s1 :: !(p) && !(q) -> goto accept_s2 fi; s3: if :: (p) && !(q) -> goto accept_s4 :: (p) && (q) -> goto s3 :: !(p) && (q) -> goto s3 :: (p) && !(q) -> goto s3 :: !(p) && !(q) -> goto s3 fi; accept_s2: if :: (p) && (q) -> goto accept_s2 :: !(p) && (q) -> goto accept_s2 :: (p) && !(q) -> goto accept_s2 :: !(p) && !(q) -> goto accept_s2 fi; accept_s4: if :: !(p) && !(q) -> goto accept_s2 :: (p) && !(q) -> goto s1 fi; }