Die Hard 3 water jug problem — Pluscal solution.
In TLA+ video tutorials, Leslie Lamport provides a spec for Die Hard 3 water jug problem. You can read about the problem here, or watch it here. The spec is written in TLA+, but usually, when beginners start learning TLA+ they learn Pluscal — a language built on top of TLA+ which looks more similar to modern programming languages we use today. Below, you can the TLA+ spec for the problem.
If we write the same specification in Pluscal(without adding processes and other stuff), which looks like this - will not give you the answer- it will not find a case where the invariant big /= 4 is violated. A little surprise! TLC will find 7 distinct states and no invariant violation. Why is that?
The answer is the new code goes through labels only once - but to reach the solution we definitely need some iterations, that is why it cannot find the solution - invariant big /= 4 violation case. The one-to-one “translation” I did initially, from the TLA+ code to Pluscal does not work as expected. To make it work we must write in the Pluscal “understands”. The key here is to understand that TLA+ usually used for modeling concurrent and multi or single process algorithms/specifications. We should make our algorithm iterate over and over again until it does not find an invariant violation case. Thus, we add a while loop that iterates “infinitely”, and inside it, we write labels under either/or construction - this way TLC will choose “arbitrarily” which label to run next.
When we translate the Pluscal code and check it, the TLC model checker finds the big /= 4 invariant violation steps. If you agree or not, this code looks like to be written more from a programming perspective - quite close to how we could write in any other modern programming language. There is another way that is more mathematical-like and corresponds more to how we should model the problem.
This code also has the same cyclic behavior as the previous one with a while loop. Instead of a while loop, I am using a goto construct- once one of the or statements finishes executing with a goto statement I am returning the control to the beginning of the process. Both while loop and goto have the provide us with the same cyclic behavior we need. Running the spec with the process also find the big /= 4 violation steps just like the previous one.
To sum up, while writing specs in Pluscal it is important to keep in my that the systems we model are usually concurrent/parallel and usually execution of the system is non-terminating, especially for concurrent systems(we avoid deadlock or any other terminating cases). So, while modeling some problem/system we should remember about cyclic behavior and how we will implement it in Pluscal.
