MACHINE Elevator SETS /* Possible states of the cab door. */ DSTATE = {closed, open} CONSTANTS /* Floors range from flmin to flmax. */ flmin, flmax, floors PROPERTIES flmin : INT & flmax : INT & flmin < flmax & floors = (flmin..flmax) CONCRETE_VARIABLES /* Cab's current floor. */ cab, /* State of the cab door. */ door ABSTRACT_VARIABLES /* Pending requests. */ req INVARIANT cab : floors & req <: floors & door : DSTATE & (door = open => cab : req) INITIALISATION cab := flmin || req := {} || door := closed OPERATIONS /* * Add a request for the given floor. Requests * may either originate from inside the cab, or * from a floor: they are processed identically. */ request (fl) = PRE fl : floors THEN req := req \/ {fl} END ; /* * Move the cab to a floor that belongs to req. * The current floor must not be in req, and the * door must be closed. */ move = PRE req /= {} & cab /: req & door = closed THEN cab :: req END ; /* * Switch the state of the cab door: open it if * it is closed, and close it otherwise. In the * latter case, remove the request from req. * The door must be toggled only if the current * floor is a pending request. */ toggle = PRE cab : req THEN IF door = closed THEN door := open ELSE req := req - {cab} || door := closed END END END