
module vending_machine
{
  var coin : int;
  var dispensed_drinks : int;

  init {
    coin = 0;
    dispensed_drinks = 0;
  }

  transition {
    coin' = coin + coin_in;
    dispensed_drinks' = (coin >= dispensed_drinks) ? dispensed_drinks + 1 : dispensed_drinks;
  }

  safety {
    coin >= dispensed_drinks;
  }
}
