c
module main {
    var nsoda : int;
    var nbeer : int;
    var sget : bool;
    var bget : bool;
    var refill : bool;
    var coin : bool;

    const max : int;

    init {
        nsoda = max;
        nbeer = max;
        sget = false;
        bget = false;
        refill = false;
        coin = false;
    }

    transition {
        start --(true:coin)-> select;
        start --(true:refill)-> start;

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

    action {
        coin := true;
        ret_coin := false;
        refill := false;

        if (sget) {
            nsoda := nsoda - 1;
            sget := false;
        }

        if (bget) {
            nbeer := nbeer - 1;
            bget := false;
        }

        if (refill) {
            nsoda := max;
            nbeer := max;
            refill := false;
        }
    }
}
