module VendingMachine {
  var drinks_to_dispense: integer;
  var coin: integer;
  var dispensed_drinks: integer;

  init {
    coin = 0;
    dispensed_drinks = 0;

  }
  procedure step()
    modifies coin;
    modifies drinks_to_dispense;
    modifies dispensed_drinks;
  {
    coin = (coin + drinks_to_dispense);
    drinks_to_dispense = coin;
    if (drinks_to_dispense > 0) {
      coin = (coin - drinks_to_dispense);
      dispensed_drinks = (dispensed_drinks + drinks_to_dispense);
    }
  }

  next {
    call step();
  }
  invariant spec: (coin >= dispensed_drinks);

}
