examples/msg/mc/automaton_PROMELA

   1 never {
   2 T0_init:
   3         if
   4         :: (!d) || (r) -> goto accept_S1
   5         :: (1) -> goto T1_S4
   6         :: (1) -> goto T0_S2
   7         :: (!e) -> goto accept_S3
   8         fi;
   9 T1_S4:
  10         if
  11         :: (1) -> goto T1_S4
  12         :: (r) -> goto accept_S1
  13         fi;
  14 accept_S1:
  15         if
  16         :: (!d) || (r) -> goto accept_S1
  17         :: (1) -> goto T1_S4
  18         fi;
  19 T0_S2:
  20         if
  21         :: (1) -> goto T0_S2
  22         :: (!e) -> goto accept_S3
  23         fi;
  24 accept_S3:
  25         if
  26         :: (!e) -> goto accept_S3
  27         fi;
  28 }