\documentclass[letterpaper,11pt]{article}
% Use the Z/EVES style file for Z notation
\usepackage{z-eves}
% Shrink margins to use more of the page.
\usepackage{fullpage}
\begin{document}
\title{Elevator Control System (Version 0.5)}
%\author{Mark J. Sebern}
\date{8 March 2003}
\maketitle
\section{Introduction}
The purpose of the elevator control system is to manage movement of an elevator in
response to user requests.
\subsection{Basic elements}
The elevator system has the following basic elements and parameters.
\subsubsection{Number of elevators}
Number of elevators in the system.
\begin{axdef}
numElevators : \nat_1
\end{axdef}
\subsubsection{Floors}
Floors serviced by the elevator system. Floors are numbered starting at one
even though in some circumstances they might be labeled differently.
(Have you noticed that many hotels and other buildings don't have a
floor that is labeled ``13'', for example?)
$Floors$ is modeled as a finite set, since we may need to
apply the cardinality operator, which does not work with infinite sets.
\begin{axdef}
nFloors : \nat \\
Floors : \finset \num
\where
\Label{grule TopFloorGE2}
nFloors \geq 2 \\
\Label{rule FloorsDef}
Floors = 1 \upto nFloors
\end{axdef}
\begin{quote}
Proof note:
The $TopFloorGE2$ label marks the $nFloors \geq 2$ predicate
as a theorem that the Z/EVES prover can assume to be true.
The $FloorsDef$ label marks the $Floors = 1 \upto nFloors$
equality predicate so it can be used as a substitution rule.
In other words, when the prover sees $Floors$, this rule means
that it can rewrite that part of the expression to be
$1 \upto nFloors$ instead.
These proof rules are needed for use in later proofs.
\end{quote}
\subsubsection{Elevator status}
An elevator may be in service or out of service.
\begin{zed}
ServiceStatus::= InSvc | OutSvc
\end{zed}
\begin{quote}
Proof note:
The following theorem is defined so that Z/EVES knows
that the service status is binary; an elevator is either
in service or out of service. This permits the theorem
prover to infer, for example, that if an elevator is not
in service it must be out of service.
The theorem might seem obvious from the type definition,
but Z/EVES doesn't automatically know this fact about
free types.
\begin{theorem}{frule ServiceStatusDef}
\forall s:ServiceStatus @ s = InSvc \lor s = OutSvc
\end{theorem}
\end{quote}
\subsubsection{Elevator direction}
An elevator may be stopped, or it may be moving up or down.
\begin{zed}
Direction::= DirUp | DirDown | DirHalt
\end{zed}
\begin{quote}
Proof note:
The following theorem is defined to specify the enumerated
directions, so the theorem prover can know that these are
the only possible direction values.
\begin{theorem}{frule DirectionDef}
\forall d:Direction @ d = DirUp \lor d = DirDown \lor d = DirHalt
\end{theorem}
\end{quote}
\subsection{Elevator}
An elevator has a current location (floor) and direction of movement.
It also has a set of floor requests that correspond to the
floor buttons currently selected inside the elevator.
A finite set is used to model $requests$.
\begin{schema}{Elevator}
curFloor : Floors \\
status : ServiceStatus \\
curDir : Direction \\
requests : \finset Floors \\
%\where
% No predicates needed at the current stage of the model.
\end{schema}
The following schema describes the initial state of an elevator.
\begin{schema}{InitElevator}
Elevator \\
\where
curFloor = 1 \\
status = InSvc \\
curDir = DirHalt \\
requests = \emptyset
\end{schema}
The following theorem asserts that an elevator can be
successfully initialized.
\begin{theorem}{InitElevatorOK}
\exists Elevator @ InitElevator
\end{theorem}
\begin{quote}
Proof note:
The following proof steps demonstrate how the
$InitElevatorOK$ theorem can
be proved. A faster alternative would be to
use a single step of \emph{prove by reduce},
which in effect combines all the steps into one operation.
\begin{zproof}
reduce;
invoke Elevator;
apply FloorsDef to expression Floors;
prove;
\end{zproof}
\end{quote}
\begin{quote}
Proof notes:
Create an initialized elevator instance for later use in proofs.
\begin{axdef}
elevator0 : Elevator
\where
\exists InitElevator' @ elevator0 = \theta Elevator'
\end{axdef}
Create a sequence of initialized elevator instances for later proofs.
The reason for this is that new ``objects'' cannot be created in
the middle of a proof script, but existing ones can be used.
\begin{axdef}
elevator0Seq : \seq Elevator
\where
\Label{Elev0SeqDef}
elevator0Seq = (\lambda j : 1 \upto numElevators @ elevator0)
\end{axdef}
Make a couple of assumptions about the sequence of initialized
elevators. These assumptons are used in later proofs.
Mark them \emph{disabled} so that they have to explicitly
referenced in proofs.
(These assumptions should themselves be proved,
but we'll defer that for now.)
\begin[disabled]{theorem}{grule Elev0SeqRangeIsElev0}
\ran elevator0Seq = \{ elevator0 \}
\end{theorem}
\begin[disabled]{theorem}{grule Elev0SeqCardinality}
\# elevator0Seq = numElevators
\end{theorem}
\end{quote}
\subsection{Elevator calls}
An elevator call is a summons from a specific floor,
which indicates that a user has signaled a desire to travel
in a specified direction (up or down) from that floor.
The requested direction uses the same type as that used for
an elevator's direction of travel, but the ``halt'' direction
is excluded.
\begin{zed}
CallDirection == \{ DirUp, DirDown \}
\end{zed}
\begin{quote}
Proof note:
The following theorem allows the Z/EVES prover to assume the correct type of
$CallDirection$; it is needed for later proofs.
\begin{theorem}{grule CallDirectionType}
CallDirection \in \power Direction
\end{theorem}
All that is necessary to prove this theorem is to expand
the definition of $CallDirection$.
\begin{zproof}
invoke CallDirection;
prove;
\end{zproof}
\end{quote}
A call is represented by a pair that contains the originating floor
and the desired direction of travel. The bottom floor has no
``down'' button and the top floor has no ``up'' button.
\begin{axdef}
ValidCalls : \power (Floors \cross CallDirection)
\where
ValidCalls = (Floors \cross CallDirection)
\setminus \{ (nFloors,DirUp), (1, DirDown) \}
\end{axdef}
\begin{quote}
Proof note:
The following theorem specifies the type of the domain of $ValidCalls$
so that the Z/EVES theorem prover can assume this fact.
\begin{theorem}{grule ValidCallsDomType}
\forall c : \finset ValidCalls @ \dom c \in \finset (1 \upto nFloors)
\end{theorem}
\end{quote}
A schema is used to model the set of pending elevator calls,
to make it easier to define operations.
A finite set is used to model $call$.
\begin{schema}{Calls}
calls : \finset ValidCalls
%\where
% No predicates needed at the current stage of the model.
\end{schema}
The following schema describes the initial state of the
elevator calls.
\begin{schema}{InitCalls}
Calls \\
\where
calls = \emptyset
\end{schema}
The following theorem asserts that the elevator calls
can be successfully initialized.
\begin{theorem}{InitCallsOK}
\exists Calls @ InitCalls
\end{theorem}
\begin{quote}
Proof note:
The following proof steps demonstrate how the
$InitCallsOK$ theorem can be proved.
A single step of \emph{prove by reduce} would
also work.
\begin{zproof}
reduce;
invoke Calls;
prove;
\end{zproof}
\end{quote}
\subsection{Complete elevator system}
The elevator system consists of the specified number
of elevators and the elevator calls.
\begin{schema}{ElevatorSystem}
Calls \\
elevators : \seq Elevator
\where
\# elevators = numElevators
\end{schema}
The following schema describes the initial state of the
elevator system.
\begin{schema}{InitElevatorSystem}
ElevatorSystem \\
InitCalls
\where
\ran elevators = \{ elevator0 \}
\end{schema}
\begin{quote}
Proof note:
The automatically generated domain check for
$InitElevatorSystem$ can be proved with a
single step of \emph{prove by reduce}.
\end{quote}
The following theorem asserts that the elevator system
can be successfully initialized.
\begin{theorem}{InitElevatorSystemOK}
\exists ElevatorSystem @ InitElevatorSystem
\end{theorem}
\begin{quote}
Proof note:
The following proof steps demonstrate how the
$InitElevatorSystemOK$ theorem can be proved.
\begin{zproof}
prove by reduce;
instantiate elevators == elevator0Seq;
use Elev0SeqRangeIsElev0;
use Elev0SeqCardinality;
prove by reduce;
\end{zproof}
\end{quote}
\section{Elevator system operations}
A number of operations are specified for the elevator system.
Some apply to a single elevator, with or without information
on elevator calls, and others apply to the elevator system
as a whole.
\subsection{Operation status}
Operations return a status code to indicate their success
or failure. The following set of status codes represents
the values defined so far.
\begin{zed}
OpStatusCode ::= StatusOK | \\
StatusOutOfService | \\
StatusInvalidMovement
\end{zed}
The following schema simply returns a success status.
It is used in composite operations so its declaration and
predicate don't need to be repeated.
\begin{schema}{Success}
opStatus! : OpStatusCode
\where
opStatus! = StatusOK
\end{schema}
\subsection{Elevator movement}
In this model, elevator movement is broken down into the following
components:
\begin{itemize}
\item
Movement up or down by one floor.
\item
Visiting a floor (opening doors, exchanging passengers,
closing doors, accepting requests from passengers).
\item
Choosing (calculating) an updated direction of movement,
taking into account the pending requests and calls.
\end{itemize}
Other operations (e.g., deciding whether to visit a floor when an
elevator moves past it or is halted there) still need to be defined.
These operation components are specified in the following sections.
\subsubsection{Single-floor movement}
An elevator may move up one floor or down one floor, depending on
its current direction. An elevator may not move if it is currently
halted, if it has reached the limit of travel in its current
direction, or if it is out of service.
The following operation moves an elevator up one floor.
\begin{schema}{MoveElevatorUp}
\Delta Elevator
\where
curDir = DirUp \\
curFloor < nFloors \\
status = InSvc \also
curFloor' = curFloor + 1 \also
curDir' = curDir \\
status' = status \\
requests' = requests
\end{schema}
The following operation moves an elevator down one floor.
\begin{schema}{MoveElevatorDown}
\Delta Elevator
\where
curDir = DirDown \\
curFloor > 1 \\
status = InSvc \also
curFloor' = curFloor - 1 \also
curDir' = curDir \\
status' = status \\
requests' = requests
\end{schema}
The following operation specifies that an elevator cannot move
if it is out of service.
\begin{schema}{MoveElevatorOutOfSvc}
\Xi Elevator \\
opStatus! : OpStatusCode
\where
status = OutSvc \also
opStatus! = StatusOutOfService
\end{schema}
The following operation handles the case where movement is not valid
because the elevator is halted or cannot move farther in the current
direction.
\begin{schema}{MoveElevatorInvalid}
\Xi Elevator \\
opStatus! : OpStatusCode
\where
status = InSvc \\
(curDir = DirHalt) \lor \\
(curDir = DirUp \land \lnot(curFloor < nFloors)) \lor \\
(curDir = DirDown \land \lnot(curFloor > 1)) \also
opStatus! = StatusInvalidMovement
\end{schema}
The above partial operations are now combined into a total operation.
\begin{zed}
MoveElevator \defs \\
(MoveElevatorUp \lor MoveElevatorDown) \land Success \lor \\
MoveElevatorOutOfSvc \lor \\
MoveElevatorInvalid
\end{zed}
The following theorem asserts that the total operation is in
fact total, meaning that it can correctly handle any elevator
state. Technically, the theorem asserts that the total operation
precondition is met in all cases.
\begin{theorem}{MoveElevatorIsTotal}
\forall Elevator @ \pre MoveElevator
\end{theorem}
\begin{quote}
Proof note:
To prove the theorem, it is necessary to identify all the cases,
so that the theorem prover can attempt each one separately.
Each of the ``split'' steps specifies one binary condition;
together, they partition the system states.
\begin{zproof}
split status = InSvc;
split (curDir = DirHalt) \lor
(curDir = DirUp \land \lnot curFloor < nFloors) \lor
(curDir = DirDown \land \lnot curFloor > 1);
split curDir = DirHalt;
split curDir = DirUp;
prove by reduce;
\end{zproof}
\end{quote}
\subsubsection{Visiting a floor}
When an elevator visits a floor, it opens its doors, permits entry and
exit of passengers, closes its doors, and accepts new floor requests.
The elevator's current floor and direction are not changed by this operation.
The normal case is handled first, followed by the case of the elevator
being out of service. These cases are then combined in the total operation.
\begin{schema}{VisitFloorOK}
\Delta Elevator \\
\Delta Calls \\
newRequests? : \finset Floors
\where
status = InSvc
\also
calls' = calls \setminus \{ curFloor \mapsto curDir \} \\
requests' = (requests \cup newRequests?) \setminus \{ curFloor \}
\also
status' = status \\
curDir' = curDir \\
curFloor' = curFloor
\end{schema}
\begin{schema}{VisitFloorOutOfSvc}
\Xi Elevator \\
\Xi Calls \\
newRequests? : \finset Floors \\
opStatus! : OpStatusCode
\where
status = OutSvc \also
opStatus! = StatusOutOfService
\end{schema}
\begin{zed}
VisitFloor \defs
(VisitFloorOK \land Success) \lor
VisitFloorOutOfSvc
\end{zed}
The following theorem asserts that the total operation covers all possible
cases of system state and input.
\begin{theorem}{VisitFloorIsTotal}
\forall Elevator; Calls; newRequests? : \finset Floors @ \pre VisitFloor
\end{theorem}
\begin{quote}
Proof note:
The proof separates the two cases corresponding to the operation schemas above.
\begin{zproof}
split status = InSvc;
prove by reduce;
\end{zproof}
\end{quote}
\subsubsection{Choosing a direction to travel}
When an elevator is at a floor, perhaps after visiting it, the system
must decide what direction (up, down, or halt) is appropriate for the
next movement. This decision depends on the current floor and direction,
as well as the pending requests and calls. The result is a new current
direction. The elevator's current floor, status, and requests are not
changed by this operation. The elevator calls are also not affected.
The first part of the operation identifies the floors above and below
the current floor for which there are pending requests or calls.
The output parameters ($above!$ and $below!$) are piped to the
schemas that actually implement the choice of direction.
The reason for defining this preliminary operation is to ``factor out''
the part of the specification that would otherwise be repeated in
several partial operations.
The $ChooseDirectionCommon$ schema also specifies that the elevator must be
in service. The ``out of service'' condition is handled as an exception.
\begin{schema}{ChooseDirectionCommon}
\Delta Elevator \\
\Xi Calls \\
above! : \finset Floors \\
below! : \finset Floors
\where
status = InSvc
\also
above! = (requests \cup \dom calls) \setminus (1 \upto curFloor ) \\
below! = (requests \cup \dom calls) \setminus (curFloor \upto nFloors)
\end{schema}
The following partial operation schema handles the situation where
the elevator direction is up or down (not halted) and there is still
a reason to proceed in the current direction. For example, an elevator
moving upward continues to do so if there are requests or calls on
higher floors.
\begin{schema}{ChooseDirectionSame}
\Xi Elevator \\
above? : \finset Floors \\
below? : \finset Floors
\where
(curDir = DirUp \land above? \neq \emptyset) \lor \\
(curDir = DirDown \land below? \neq \emptyset)
\end{schema}
The following partial operation handles the case where an elevator is
moving up or down, there is no reason to continue in the current
direction, and there is a reason to go in the opposite direction.
\begin{schema}{ChooseDirectionReverse}
\Delta Elevator \\
above? : \finset Floors \\
below? : \finset Floors
\where
(curDir = DirUp \land above? = \emptyset \land below? \neq \emptyset \land curDir' = DirDown) \lor \\
(curDir = DirDown \land below? = \emptyset \land above? \neq \emptyset \land curDir' = DirUp)
\also
status' = status \\
curFloor' = curFloor \\
requests' = requests
\end{schema}
The following partial operation handles the case in which a halted elevator now
has a reason to move up or down. If there are requests or calls in both directions,
an arbitrary choice is made to move upward.
\begin{schema}{ChooseDirectionRestart}
\Delta Elevator \\
above? : \finset Floors \\
below? : \finset Floors
\where
curDir = DirHalt \\
(above? \neq \emptyset \land curDir' = DirUp) \lor \\
(above? = \emptyset \land below? \neq \emptyset \land curDir' = DirDown)
\also
status' = status \\
curFloor' = curFloor \\
requests' = requests
\end{schema}
The following partial operation handles the situation where there is no reason
for movement, and the direction is set to halted.
(Note that there might be a reason to visit the current floor, because of a
call or request, but that is not part of choosing a direction of travel.)
\begin{schema}{ChooseDirectionHalt}
\Delta Elevator \\
above? : \finset Floors \\
below? : \finset Floors
\where
above? = \emptyset \\
below? = \emptyset
\also
curDir' = DirHalt
\also
status' = status \\
curFloor' = curFloor \\
requests' = requests
\end{schema}
The following partial operation handles the case of an elevator that is out of service.
No state change takes place, but an error status is returned.
\begin{schema}{ChooseDirectionOutSvc}
\Xi Elevator \\
\Xi Calls \\
opStatus! : OpStatusCode
\where
status = OutSvc
\also
opStatus! = StatusOutOfService
\end{schema}
The partial operations are combined in the following total operation. Note that the
common preparation schema pipes its output to the choice operations.
\begin{zed}
ChooseDirection \defs (ChooseDirectionCommon \pipe \\
(ChooseDirectionSame \lor ChooseDirectionReverse \lor ChooseDirectionHalt \lor ChooseDirectionRestart)) \\
\land Success \lor \\
ChooseDirectionOutSvc
\end{zed}
The following theorem asserts that the $ChooseDirection$ operation covers all possible
cases of system state and input.
\begin{theorem}{ChooseDirectionIsTotal}
\forall Elevator; Calls @ \pre ChooseDirection
\end{theorem}
\begin{quote}
Proof note:
The theorem is proved by splitting across cases handled by the various partial
operations.
\begin{zproof}
split (requests \cup \dom calls) \setminus (1 \upto curFloor) = \emptyset;
split (requests \cup \dom calls) \setminus (curFloor \upto nFloors) = \emptyset;
split curDir = DirUp;
split curDir = DirDown;
split status = InSvc;
prove by reduce;
\end{zproof}
\end{quote}
\section{Remaining work}
This specification is currently incomplete. At least the following issues need to be dealt with:
\begin{itemize}
\item
Deciding whether to visit a floor when an elevator has moved to it or is halted there.
\item
Handling new calls from waiting passengers.
\item
Implementing policies such as cancelling all pending requests when an elevator
reaches the top or bottom floors.
\item
Managing the overall elevator system by invoking operations on individual elevators.
This will likely involve promoting elevator-level operations to the aggregate
(sequence) of elevators.
\item
Taking elevators out of service and returning them to service.
\end{itemize}
\end{document}