examples/msg/mc/promela_bugged2_liveness

   1 never { /* !(GF((pready U produce) -> (cready U consume))) */
   2 T0_init :    /* init */
   3         if
   4         :: (1) -> goto T1_S1
   5         :: (produce && !consume) -> goto accept_S5
   6         :: (pready && !consume) -> goto T0_S5
   7         fi;
   8 T1_S1 :    /* 1 */
   9         if
  10         :: (1) -> goto T1_S1
  11         :: (produce && !consume) || (pready && !consume) -> goto accept_S5
  12         fi;
  13 accept_S5 :    /* 2 */
  14         if
  15         :: (pready && !consume) -> goto T0_S5
  16         :: (produce && !consume) -> goto accept_S5
  17         fi;
  18 T0_S5 :    /* 3 */
  19         if
  20         :: (pready && !consume) -> goto T0_S5
  21         :: (produce && !consume) -> goto accept_S5
  22         fi;
  23 }