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

    // Initialization
    init {
        coin = 0;
        dispensed_drinks = 0;
    }

    // Input handling procedures
    input insert_coin;
    input request_drink;

    // Procedures for handling inputs
    procedure insert_coin() {
        coin = coin + 1;
    }

    procedure request_drink() {
        if (coin > dispensed_drinks) {
            dispensed_drinks = dispensed_drinks + 1;
        }
    }

    // Transition relation describing how the state evolves
    next {
        if (insert_coin) {
            call insert_coin();
        } else if (request_drink) {
            call request_drink();
        }
    }

    // Safety property to ensure the number of drinks never exceeds the number of coins
    invariant coins_always_greater_or_equal_drinks : coin >= dispensed_drinks;

    // Control block for testing and verification
    control {
        v = unroll(10);
        check;
        print_results;
    }
}
