TLA Exercises
Peterson's algorithm
Create a new project peterson.tla. Start with the code for Dekker's algorithm that we discussed during the lecture: threads.tla. Modify this to implement Peterson's algorithm. You will find it useful to have a thread-local variable other = CHOOSE t \in Threads : t /= self.
- Run and make sure the sanity checks (AtMostOneCritical, Deadlocks, NoLiveLocks) pass.
- Make sure you have kept the outer loop (P5: goto P1 in the original code). Termination checking should fail, but the other liveness condition should succeed.
- Anticipate what happens if you change the goto into
P5: goto P2. - Now, for the most important exercise, change the liveness condition so that
P5: goto P4fails, butP5: goto P1succeeds.
Ferryman
A classic problem in model checking is the ferryman problem... You have a ferryman, goat, cabbage, and wolf who want to cross the river. The ferryman can cross with at most one passenger. The following combination of items violate the invariant of things remaining uneaten:
- the goat and the cabbage on the same side without ferryman
- the goat and the wolf on the same side without ferryman
Can the ferryman transport get them all over to the other side? Or more precisely, can TLA find a way to transport them over?
Train crossing.
Let's try to model a train crossing... There's been enough crossings, I know, but now we have a train! It's a very simple model, but it's a bit tricky how to do this in TLA. We'll try that, but it's also a good exercise to practice our Yakindu skills. So create this model first in Yakindu!
- We have a train sensor that detects whether trains are either far, near or inside the crossing.
- When a train approaches (gets "near"), it sens a warning to the controller. The controller will then start lowering its bar. This takes 3 seconds.
- Then the train leaves from "inside" the sensors area, the sensor signals the controller that things are safe. The bar is then raised. This again takes 3 seconds.
Note: this is not safe since these 3 second delays are just arbitrary and not in any way related to how quickly the train can enter "inside". See if you can model this in TLA and express the invariant to show this simple flaw.
If we don't have time to do the Yakindu part ourselves, the solution is behind this paywall:
