module vending_machine {
    var nsoda: 0..max;
    var nbeer: 0..max;
    var coin: boolean;
    var refill: boolean;
    var sget: boolean;
    var bget: boolean;

    start:
        coin -> select;
        refill -> start;

    select:
        nsoda > 0: sget -> start;
        nbeer > 0: bget -> start;
        nsoda == 0 && nbeer == 0: ret_coin -> start;

    next {
        if (coin) {
            nsoda' = nsoda;
            nbeer' = nbeer;
        } else if (refill) {
            nsoda' = max;
            nbeer' = max;
        } else if (sget) {
            nsoda' = nsoda - 1;
            nbeer' = nbeer;
        } else if (bget) {
            nsoda' = nsoda;
            nbeer' = nbeer - 1;
        } else {
            nsoda' = nsoda;
            nbeer' = nbeer;
        }
    }

    init {
        nsoda = 0;
        nbeer = 0;
    }
}
