c
module main {
    const max: int; // maximum capacity of bottle repositories
    var nsoda: int; // number of soda bottles
    var nbeer: int; // number of beer bottles
    var sget: bool; // action to get a soda bottle
    var bget: bool; // action to get a beer bottle
    var refill: bool; // action to refill the vending machine
    var coin: bool; // action to insert a coin
    var ret_coin: bool; // action to return the inserted coin

    location start;
    location select;

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

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

    init {
        nsoda = max;
        nbeer = max;
        sget = false;
        bget = false;
        refill = false;
        coin = false;
        ret_coin = false;
        start = true;
        select = false;
    }

    next {
        if (coin) {
            // Coin insertion leaves the number of bottles unchanged
            coin := false;
        }

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

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

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

        if (ret_coin) {
            // Coin return leaves the number of bottles unchanged
            ret_coin := false;
        }
    }
}
