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.