specification VM2 [coin,candy,toffee,dispence] : noexit

  behaviour

    VM2_BODY[coin,candy,toffee,dispence]

  where

    process VM2_BODY [coin,item1,item2,dispence] : noexit :=

      (
       coin;
          (
           item1; exit
           []
           item2; exit
          )
      )
      >> ( dispence; VM2_BODY[coin,item1,item2,dispence] )

    endproc

endspec