module vending_machine {

    var coin : integer;
    var dispensed_drinks : integer;

    input request_drink : boolean;
    input coin_inserted : boolean;

    init {
        coin = 0;
        dispensed_drinks = 0;
    }

    next {
        if (coin_inserted) {
            coin' = coin + 1;
        }
        if (request_drink && coin > dispensed_drinks) {
            dispensed_drinks' = dispensed_drinks + 1;
        }
    }

    // Safety property.
    assert(coin >= dispensed_drinks);

    // No error.
}

control {
    // Check safety property with up to 5 unrollings.
    // If the safety property is violated, print a counterexample.
    check;
    v = print_cex(request_drink, coin_inserted, coin, dispensed_drinks);
}
