
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 {
    // Insert coin
    coin' = coin + 1;

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

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

  invariant coins_geq_drinks : coin >= dispensed_drinks;
}

module main
{
  var vm : vending_machine;
  var sp : safety_property;

  init {
    vm.coin = 0;
    vm.dispensed_drinks = 0;
    sp.coin = vm.coin;
    sp.dispensed_drinks = vm.dispensed_drinks;
  }

  transition {
    next(vm);
    next(sp);
  }

  control {
    check(sp.coins_geq_drinks);
  }
}
