\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.3 Skeleton)}
%\author{(Your team member names here)}
\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 markes 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}
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}
\subsubsection{Elevator direction}
An elevator may be stopped, or it may be moving up or down.
\begin{zed}
Direction::= DirUp | DirDown | DirHalt
\end{zed}
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}
\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}
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}
\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{theorem}{grule CallDirectionType}
CallDirection \in \power Direction
\end{theorem}
\begin{quote}
Proof note:
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
(nFloors,DirUp) \notin ValidCalls \\
(1, DirDown) \notin ValidCalls
\end{axdef}
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}
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.
\begin{schema}{MoveElevator}
\Delta Elevator \\
opStatus! : OpStatusCode
\where
(your~predicates~here)
\end{schema}
The following theorem asserts that the move elevator operation is
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 may be necessary to identify all the cases,
so that the theorem prover can attempt each one separately.
Each ``split'' step specifies one binary condition;
together, they partition the system states.
(your proof comments here)
\begin{zproof}
(your proof goes here)
\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.
\begin{schema}{VisitFloor}
\Delta Elevator \\
\Delta Calls \\
newRequests? : \finset Floors \\
opStatus! : OpStatusCode
\where
(your~predicates~here)
\end{schema}
The following theorem asserts that the 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:
(your proof comments here)
\begin{zproof}
(your proof steps go here)
\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.
\begin{schema}{ChooseDirection}
\Delta Elevator \\
\Xi Calls \\
opStatus! : OpStatusCode
\where
(your~predicates~here)
\end{schema}
The following theorem asserts that the operation covers all possible
cases of system state and input.
\begin{theorem}{ChooseDirectionIsTotal}
\forall Elevator; Calls @ \pre ChooseDirection
\end{theorem}
\begin{quote}
Proof note:
(your proof comments here)
\begin{zproof}
(your proof steps go here)
\end{zproof}
\end{quote}
\end{document}