module VendingMachine {
    // State variables
    var coins : int;
    var dispensed_drinks : int;

    // Inputs
    input insert_coin : boolean;
    input request_drink : boolean;

    // Initialize the state variables
    init {
        coins = 0;
        dispensed_drinks = 0;
    }

    // State transition
    next {
        if (insert_coin) {
            coins' = coins + 1;
        } else {
            coins' = coins;
        }

        if (request_drink && coins > dispensed_drinks) {
            dispensed_drinks' = dispensed_drinks + 1;
        } else {
            dispensed_drinks' = dispensed_drinks;
        }
    }

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

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