specification VM2[coin,accepted,reject,dispence] : noexit

  behaviour

    Basic [coin,accepted,reject,dispence]

  where

    process Basic [coin,accepted,reject,dispence] : noexit :=
       coin;
         (
          accepted; dispence; exit
          []
          reject; exit
         )
         >> Basic [coin,accepted,reject,dispence]
    endproc

endspec