1 never { /* !(GF((pready U produce) -> (cready U consume))) */
5 :: (produce && !consume) -> goto accept_S5
6 :: (pready && !consume) -> goto T0_S5
11 :: (produce && !consume) || (pready && !consume) -> goto accept_S5
15 :: (pready && !consume) -> goto T0_S5
16 :: (produce && !consume) -> goto accept_S5
20 :: (pready && !consume) -> goto T0_S5
21 :: (produce && !consume) -> goto accept_S5