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

  init {
    coin = 0;
    dispensed_drinks = 0;
  }

  // Procedure to simulate inserting a coin
  procedure insert_coin()
    modifies coin;
  {
    coin = coin + 1;
  }

  // Procedure to simulate dispensing a drink
  procedure dispense_drink()
    modifies dispensed_drinks;
  {
    if (coin > dispensed_drinks) {
      dispensed_drinks = dispensed_drinks + 1;
    }
  }

  // Safety property: coins should always be >= dispensed drinks
  invariant safety_property: coin >= dispensed_drinks;

}

// Control block for model checking
control {
  v = unroll(5);
  check;
  print_results;
}
