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

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

    // Input actions
    input insert_coin : boolean;
    input request_drink : boolean;

    // Transition relation describing how the state variables change
    next {
        if (insert_coin) {
            coins' = coins + 1;
        }
        if (request_drink && coins > dispensed_drinks) {
            dispensed_drinks' = dispensed_drinks + 1;
        }
    }

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

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