c
module main {

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

    init {
        coin = 0;
        dispensed_drinks = 0;
    }

    // Inserting a coin increments the number of coins
    procedure insert_coin()
        modifies coin;
    {
        coin = coin + 1;
    }

    // Dispensing a drink decrements the number of coins and increments the number of dispensed drinks
    procedure dispense_drink()
        requires coin > 0;
        modifies coin, dispensed_drinks;
    {
        coin = coin - 1;
        dispensed_drinks = dispensed_drinks + 1;
    }

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

    // Main control loop
    control {
        havoc coin; havoc dispensed_drinks;
        assume coin >= 0;
        assume dispensed_drinks >= 0;

        // Insert coins and dispense drinks
        insert_coin();
        dispense_drink();
    }
}
