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

  init {
    coin = 0;
    dispensed_drinks = 0;
  }

  transition {
    // Inserting a coin
    coin' = coin + 1;
    dispensed_drinks' = dispensed_drinks;

    // Dispensing a drink if enough coins are inserted
    if coin > 0 {
      coin' = coin - 1;
      dispensed_drinks' = dispensed_drinks + 1;
    }
  }
}

module main
{
  instance vm : vending_machine;

  invariant coins_geq_drinks : vm.coin >= vm.dispensed_drinks;

  control {
    v = unroll(10);
    check coins_geq_drinks;
    print_results;
  }
}
