examples/msg/mc/automaton2_PROMELA

   1 never { /* !G(p->Fq) */
   2 T0_init :    /* init */
   3         if
   4         :: (1) -> goto T0_init
   5         :: (!q && p) -> goto accept_S2
   6         fi;
   7 accept_S2 :    /* 1 */
   8         if
   9         :: (!q) -> goto accept_S2
  10         fi;
  11 }