c
module main
{
  var coin : int; // number of coins inserted
  var dispensed_drinks : int; // number of drinks dispensed

  init {
    coin = 0;
    dispensed_drinks = 0;
  }

  // Insert a coin and dispense a drink if enough coins are inserted
  procedure insert_coin_and_dispense_drink()
    modifies coin;
    modifies dispensed_drinks;
  {
    coin := coin + 1;
    if coin >= 2 {
      dispensed_drinks := dispensed_drinks + 1;
      coin := coin - 2;
    }
  }

  // Safety property: Number of inserted coins is always at least the number of dispensed drinks
  invariant safety_property {
    coin >= dispensed_drinks;
  }

  // Main control loop for vending machine
  control {
    havoc coin;
    havoc dispensed_drinks;
    insert_coin_and_dispense_drink();
  }
}
