Lecture Exercises
Fairness: Traffic Light
Begin with this code:
------------------------------ MODULE traffic ------------------------------
NextColor(c) == CASE c = "red" -> "green"
[] c = "green" -> "red"
(*--algorithm traffic
variables
at_light = TRUE,
light = "red";
process light = "light"
begin Cycle:
while at_light do
light := NextColor(light);
end while;
end process;
process car = "car"
begin Drive:
when light = "green";
at_light := FALSE;
end process;
end algorithm;*)
=============================================================================
- Create a model and add/check "Termination" under Model Overview > What to Check? > Properties.
- Make both processes fair.
- Make the car process strongly fair.
Dekker's algorithm
Copy/Download the starting point: threads.tla.
- Write a safety condition that "only one thread should enter the critical section at a time."
- Run the model checker with and without the await-condition.
- Apply the this fix. Check if this works!
- Now liveness: State that both threads will be able to access critial section! Final Version.
Hillel Wayne's eSpark example
https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f