module main {
    type state_t = enum { pay, select, soda, beer };
    var state : state_t;

    init {
        state = pay;
    }

    input insert_coin : boolean;
    input get_soda : boolean;
    input get_beer : boolean;

    transition {
        if (state == pay && insert_coin) {
            state' = select;
        } else if (state == select && get_soda) {
            state' = soda;
        } else if (state == select && get_beer) {
            state' = beer;
        }
    }

    invariant property_deliver_after_coin : G(select -> X(soda ∨ beer));
}

control {
    check;
    print_results;
}
