TLA exercise (Exam 1)
Consider the following TLA specification given in the printout. It can also be downloaded from http://bit.ly/2CVSIbp
We are modelling an elevator controller. We track the following variables: loc (the location of each elevator), dir (the direction the elevator is moving), idle (the set of elevators without a destination) and req (the set of requested floors; that is, people can press buttons on the floors or within the elevator, we just consider the set of active requests).
We have three processes. The requesting process simply adds requests non-deterministically. Requests can happen at any time with the only exception is that we don’t add requests while the elevator is on the same floor. Dealing with this would make the task more complicated; typically, elevators opens the door again, but we’re not going to simulate this.
The second process is the elevator that just follows the instructions of the controller. Upon reaching a floor, it checks if this is a requested floor and removes the request and sets itself to idle and waits for instructions: as soon as the controller makes it not idle, it will move in whatever direction the controller indicates.
The controller handles all the logic. It waits until there are some requests and elevators ready to move. It then just picks an elevator and sends it to a floor very arbitrarily:
- if some request exists below, the elevator will be sent down
- else if some request exists above, the elevator moves up.
- Otherwise we keep moving in the same direction!
(We could have just had a simple if request exist above, move up, else move down, but we’re going to modify the strategy later and I want that change to be minimal.)
Task 5 [8 points]. Analyse this system for defects and you may use TLA+ as an assistant. The there are two important things that I will grade here: first, precision and correctness of the temporal logic property, and second, the clarity of your explanation of the counter example trace. It's critical to narrate the situation that goes wrong; you don’t have to include every single step of the trace.
- First let’s explore if the system is safe: the controller will not send the elevators outside the given range. Specify a safety property NoCrash that states all elevators are located between floors 1 and NumFloors. [only graded at exam].
- Create a model with a single elevator (set of model values {e1}) and just two floors (ordinary assignment 2). This should work, but add a second elevator to the set and you should see an invariant violation. Explain the trace! [2 points].
- Now specify the following liveness property that should say that all floors are eventually served. More precisely, specify the property AllServed to say that all floors are always eventually removed from the set of requests. [only graded at exam]
- Go back to a model with a single elevator. This should work for two floors, but try a single elevator and set NumFloors to 3. You should get a temporal property violation. Explain the trace! [2 points]
- Can you think of a way to fix the problem? The code is written is such a way to really minimize the needed fix. We can make a small change in the controller, so elevators switch direction when all requests are below or above the current location. Can you clarify what needs to be changed? [1 point]