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