examples/msg/mc/promela2_bugged2_liveness

   1 never { /* !(G((pready U produce) -> F(cready U consume))) */
   2 T1_init :    /* init */
   3         if
   4         :: (1) -> goto T1_init
   5         :: (pready && !consume) -> goto T0_S2
   6         :: (produce && !consume) -> goto accept_S3
   7         fi;
   8 T0_S2 :    /* 1 */
   9         if
  10         :: (pready && !consume) -> goto T0_S2
  11         :: (produce && !consume) -> goto accept_S3
  12         fi;
  13 accept_S3 :    /* 2 */
  14         if
  15         :: (!consume) -> goto accept_S3
  16         fi;
  17 }