/* Vending
 * Author: hiche
 * Creation date: 5/4/2024
 */
MACHINE
    Vending
SETS
    PRODUCT ;
    STATE = {on, off}
CONSTANTS
    price,
    max_credit
PROPERTIES
    price : PRODUCT --> NAT1 &
    max_credit : NAT1
VARIABLES
    available,
    credit,
    state
INVARIANT
    available <: PRODUCT &
    credit : 0..max_credit &
    state : STATE &
    ((state = off) => (credit = 0))
INITIALISATION
    available :: POW(PRODUCT) ||
    credit := 0 ||
    state := off
OPERATIONS
    switch_on =
        PRE
            state = off
        THEN
            state := on
        END
    ;

    switch_off =
        PRE
            state = on
        THEN
            state := off ||
            credit := 0
        END
    ;

    insert_credit (cr) =
        PRE
            state = on &
            cr : NAT1 &
            credit + cr <= max_credit
        THEN
            credit := credit + cr
        END
    ;

    cr <-- return_credit =
        PRE
            state = on
        THEN
            cr := credit ||
            credit := 0
        END
    ;

    status <-- dispense (item) =
        PRE
            state = on &
            item : PRODUCT
        THEN
            IF
                item : available &
                credit >= price(item)
            THEN
                status := TRUE ||
                credit := credit - price(item) ||
                CHOICE
                    skip
                OR
                    available := available - {item}
                END
            ELSE
                status := FALSE
            END
        END
    ;

    restock =
        PRE
            state = off
        THEN
            ANY
                av
            WHERE
                av <: PRODUCT &
                available <: av
            THEN
                available := av
            END
        END
END