# Formal design of lift controller

We consider a lift in a building with N > 0 floors. For simplicity, we
consider N = 4. The floors are numbered 0 to N - 1 (i.e. 0 to 3). Each floor
has a door, a call button and a light that signals whether the lift has been
called or not at that floor. The lift cabin has N buttons and N lights (one
per floor) to indicate the next stops of the cabin.

The goal is to formalize the following requirements in the LTL logic and
then, to build a PlusCal model of the lift that satisfies the

requirements.

1. The doors are safe: a floor door is never open if the cabin is not
present at that floor.

2. Each time a cabin or floor button is pressed, a floor service request is
issued and is pending until the cabin stops at that floor (if ever)

3. The lift only stops at requested floors and does not move if there is no
request.

4. All requests are eventually satisfied.

The PlusCal model is built incrementally by adding the requirements one
after the other. We start from the most abstract and most simple model
where each component is a process that can repeatedly and
non-deterministically choose an action to perfom. This model is refined in
order to meet the first requirement. Then, the model is refined again to
satisfy the second requirement, and so on. Each refinement should be as
simple as possible and it should not restrict the behaviors of the system
unnecessarily. In the end, we obtain a model that satifies all the
requirements and that is as permissive as possible.

## Starting PlusCal model (lift0.tla)

EXTENDS Naturals, TLC
CONSTANT N (* Number of floors *)
(*
--algorithm Lift {
variables
cabin_floor = 0; (* Cabin floor *)
locked = [ i \in 0..N-1 |-> TRUE ]; (* Door lock *)
closed = [ i \in 0..N-1 |-> TRUE ]; (* Door status: closed/opened *)
process (Cabin = 1)
{
c00: while (TRUE) {
with (f \in 0..N-1)
cabin_floor := f;
}
}
process (Controller \in 2..2+N-1)
variable
my_floor = self - 2; (* Controller's floor *)
{
l00: while (TRUE) {
with (l \in {FALSE,TRUE})
locked[my_floor] := l;
}
}
process (Door \in 2+N..2+N+N-1)
variable
my_floor = self - (2+N); (* Door's floor *)
{
d00: while (TRUE) {
with (c \in {FALSE,TRUE})
closed[my_floor] := c;
}
}
}
*)
\* BEGIN TRANSLATION
\* END TRANSLATION

## Formalizing the requirements

Formalize the requirements above as LTL formulas. First specify the
atomic propositions that are used, in particular, which state of the
system is observed by each atomic proposition.

## Incremental modeling

Starting from the PlusCal model above, introduce requirements one by
one, and update the model in order to satisfy each new requirement, while
keeping the model as permissive as possible.