module Module {
  next {
    ??;

  }
}
module VendingMachine {
  var coins: integer;
  var dispensed_drinks: integer;
  var insert_coin: integer;
  var enough_coins_for_drinks: bv1;

  input request_drink: bv1;

  output safety_status: bv2;

  init {
    coins = 0;
    dispensed_drinks = 0;
    enough_coins_for_drinks = 1bv1;

  }
  next {
    if (request_drink == 1bv1) {
      if (coins > 0) {
        dispensed_drinks' = (dispensed_drinks + 1);
        coins' = (coins - 1);
        enough_coins_for_drinks' = 1bv1;
      } else {
        enough_coins_for_drinks' = 0bv1;
      }
    }
    coins' = (coins + insert_coin);

  }
  invariant spec: (coins >= dispensed_drinks);

}
