MACHINE Cases
SETS DOOR; POSITION = {open, closed}
VARIABLES position
INVARIANT
    position : DOOR --> POSITION
INITIALISATION
    position := DOOR * {closed}
OPERATIONS
    opening(dd) =
        PRE dd : DOOR THEN position(dd) := open END;
    closedoor(dd) =
        PRE dd : DOOR THEN position(dd) := closed END
END


MACHINE LockCases
INCLUDES Cases
PROMOTES closedoor
SETS
    STATUS = {locked, unlocked}
VARIABLES
    status
INVARIANT
    status : DOOR --> STATUS &
    position~[{open}] <: status~[{unlocked}]
INITIALISATION
    status := DOOR * {locked}
OPERATIONS
    opendoor(dd) =
        PRE dd : DOOR & status(dd) = unlocked
        THEN opening(dd)
        END;
    unlockdoor(dd) =
        PRE dd : DOOR
        THEN status(dd) := unlocked
        END;
    lockdoor(dd) =
        PRE dd : DOOR & position(dd) = closed
        THEN status(dd) := locked
        END
END


MACHINE Keys
SETS KEY
VARIABLES keys 
INVARIANT keys <: KEY
INITIALISATION keys := {}
OPERATIONS
    insertkey(kk) =
        PRE kk : KEY THEN keys := keys \/ {kk} END;
    removekey(kk) =
        PRE kk : KEY THEN keys := keys - {kk} END
END


MACHINE Safes
INCLUDES LockCases; Keys
PROMOTES opendoor, closedoor
CONSTANTS unlocks
PROPERTIES unlocks : KEY >-> DOOR
INVARIANT status~[{unlocked}g] <: unlocks[keys]
OPERATIONS
    insert(kk, dd) 
    PRE kk : KEY & dd : DOOR & unlocks(kk) = dd & kk /: keys
    THEN insertkey(kk)
    END;
    
    extract(kk, dd) = 
    PRE kk : KEY & dd : DOOR & unlocks(kk) = dd & kk : keys & status(dd) = locked
    THEN removekey(kk)
    END;

    unlock(dd) =
    PRE dd : DOOR & unlocks~(dd) : keys
    THEN unlockdoor(dd)
    END;

    lock(dd) =
    PRE dd : DOOR & unlocks~(dd) : keys & position(dd) = closed
    THEN lockdoor(dd)
    END;

    quicklock(dd) =
    PRE dd : DOOR & unlocks~(dd) : keys & position(dd) = closed
    THEN lockdoor(dd) || removekey(unlocks~(dd))
    END
END