MACHINE
    Reading
SETS
    READER; BOOK; COPY; RESPONSE = {yes, no}
CONSTANTS
    copy
PROPERTIES
    copy : COPY -->> BOOK
VARIABLES
    hasread, reading
INVARIANT
    hasread : READER <-> BOOK &
    reading : READER >+> COPY &
    (reading ; copy) /\ hasread = {}
INITIALISATION
    hasread := {} || reading := {}
OPERATIONS
    borrow(rd, cp) = 
    PRE
        rd : READER & cp : COPY & copy(cp) /: hasread[{rd}] &
        rd /: dom(reading) & cp /: ran(reading)
    THEN
        reading := reading \/ { rd |-> cp }
    END;
    
    return(rd, cp) =
    PRE
        rd : READER & cp : COPY & cp: ran(reading)
    THEN
        hasread := hasread \/ { rd |-> copy(cp) } ||
        reading := { rd } <<| reading
    END;
    
    res <-- isreading(rd) =
    PRE
        rd : READER
    THEN
        IF rd : dom(reading)
        THEN
            res := yes
        ELSE
            res := no
        END
    END;
    
    bk <-- curreading(rd) =
    PRE
        rd : READER & rd: dom(reading)
    THEN
        bk := copy(reading(rd))
    END;
    
    res <-- rdhasread(rd, bk) =
    PRE
        rd : READER & bk : BOOK
    THEN
        IF bk : hasread[{rd}]
        THEN
            res := yes
        ELSE
            res := no
        END
    END  
END