1 never { /* !(G((pready U produce) -> F(cready U consume))) */
5 :: (pready && !consume) -> goto T0_S2
6 :: (produce && !consume) -> goto accept_S3
10 :: (pready && !consume) -> goto T0_S2
11 :: (produce && !consume) -> goto accept_S3
15 :: (!consume) -> goto accept_S3