REFINEMENT Elevator_r1 REFINES Elevator ABSTRACT_VARIABLES /* Pending requests, with timestamps. */ treq INVARIANT treq : floors >+> NATURAL & req = dom(treq) INITIALISATION cab := flmin || treq := {} || door := closed OPERATIONS /* * Move the cab to the floor that has the least * timestamp. */ move = PRE treq /= {} & cab /: dom(treq) & door = closed THEN ANY dest WHERE dest : dom(treq) & treq(dest) = min(ran(treq)) THEN cab := dest END END ; toggle = PRE cab : dom(treq) THEN IF door = closed THEN door := open ELSE treq := {cab} <<| treq || door := closed END END ; /* * If there is no pending request for the given * floor, add it to treq with a timestamp that * is strictly larger than the timestamp of all * other pending requests. */ request (fl) = PRE fl : floors THEN IF fl /: dom(treq) THEN ANY ti WHERE ti : NATURAL & ((treq /= {}) => (ti > max(ran(treq)))) THEN treq(fl) := ti END END END END