TLA Exercises (Continued)
We will do the exercises from last week we didn't finish. We will revisit the train crossing with more modern trains now that can listen to a signal safe:
- When the controller has this enabled, the trains will not enter the crossing.
- We also assume the train does not return too quickly, so the train can wait for the crossing to turn of its "unsafe" signal before coming back.
The question is now, as it always should be, what will happen if we have two trains?
The exercise from last time:
- We have a train sensor that detects whether trains are either far, near or inside the crossing.
- When a train approaches (gets "near"), it sends 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.