module main {
    // Variables representing the state of the vending machine
    var coin : int;
    var dispensed_drinks : int;

    // Initialize the state of the vending machine
    init {
        coin = 0;
        dispensed_drinks = 0;
    }

    // Transition for inserting a coin
    procedure insert_coin()
    modifies coin;
    {
        coin = coin + 1;
    }

    // Transition for dispensing a drink
    procedure dispense_drink()
    modifies dispensed_drinks;
    {
        if (coin > dispensed_drinks) {
            dispensed_drinks = dispensed_drinks + 1;
        }
    }

    // Safety property: number of coins should always be at least the number of dispensed drinks
    invariant safety_property : coin >= dispensed_drinks;

    // Control block for model checking
    control {
        // Perform bounded model checking
        var v : verification;
        v = unroll(10);
        check;
        print_results;
    }
}
