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

    init {
        coin = 0;
        dispensed_drinks = 0;
    }

    next {
        coin' = coin + 1;
        dispensed_drinks' = coin;
    }

    safety {
        coin >= dispensed_drinks;
    }
}
