specification VM [coffee,tea,dispence] : exit

  behaviour

    coffee; dispence; exit
    []
    tea; dispence; exit

endspec