Die Hard Jugs Puzzle
This is the B model of a puzzle from the movie "Die Hard with a Vengeance". This shows Bruce Willis and Samuel Jackson having a go at the puzzle. A detailed explanation can be found here. At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs.
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
After opening the file in ProB, choose the Model Check command in the Verify menu and then check the "Find Define GOAL" check box. This instructs ProB to search for states satisfying the GOAL predicate (4:ran(level)) defined above.
Now press the model check button and you should now obtain the following message:
The main window of ProB now contains the following information:
You can see that the second jug contains exactly 4 gallons. The steps required to reach this state can be found in the history pane on the right (in reverse order).
Graphical Animation
This machine above is actually included in the ProB distribution (inside the examples/B/GraphicalAnimation/ directory). It also contains the following lines in the DEFINITIONS section, which defines a quick-and-dirty graphical visualisation of the state. The images can be found in the subfolder images along the file Jars.mch.
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
Here is a screenshot of ProB Tcl/Tk after loading the model and having found the goal:
Using probcli (command-line version)
To find the solution using probcli you just need to type:
probcli -model_check Jars.mch
The output will be as follows:
$ probcli -model_check Jars.mch
% found_enumeration_of_constants(30,40)
% backtrack(found_enumeration_of_constants(30,40))
ALL OPERATIONS COVERED
found_error(goal_found,10)
finding_trace_from_to(root)
.
Model Checking Time: 60 ms (60 ms walltime)
States analysed: 10
Transitions fired: 36
*** COUNTER EXAMPLE FOUND ***
goal_found
*** TRACE:
1: SETUP_CONSTANTS({(j3|->3),(j5|->5)}):
2: INITIALISATION({(j3|->0),(j5|->0)}):
3: FillJar(j5):
4: Transfer(j5,3,j3):
5: EmptyJar(j3):
6: Transfer(j5,2,j3):
7: FillJar(j5):
8: Transfer(j5,1,j3):
! *** error occurred ***
! goal_found
TLA+ Version
A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory). The specification was developed by Leslie Lamport in order to be validated by the TLC model checker. However, it possible to load TLA+ specifications with ProB as shown on the TLA wiki page.
------------------------------ MODULE DieHard -------------------------------
(***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
(* goal: to get TLC to solve the problem for us. *)
(* *)
(* First, we write a spec that describes all allowable behaviors of our *)
(* heros. *)
(***************************************************************************)
EXTENDS Naturals
(*************************************************************************)
(* This statement imports the definitions of the ordinary operators on *)
(* natural numbers, such as +. *)
(*************************************************************************)
(***************************************************************************)
(* We next declare the specification's variables. *)
(***************************************************************************)
VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
small \* The number of gallons of water in the 3 gallon jug.
(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set. A type *)
(* invariant like this is not part of the specification, but it's *)
(* generally a good idea to include it because it helps the reader *)
(* understand the spec. Moreover, having TLC check that it is an *)
(* invariant of the spec catches errors that, in a typed language, are *)
(* caught by type checking. *)
(* *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
(* or \/ denotes the conjunction or disjunction of those formulas. *)
(* Indentation of subitems is significant, allowing one to eliminate lots *)
(* of parentheses. This makes a large formula much easier to read. *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3
/\ big \in 0..5
(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. I like to name this predicate Init, but the *)
(* name doesn't matter. *)
(***************************************************************************)
Init == /\ big = 0
/\ small = 0
(***************************************************************************)
(* Now we define the actions that our hero can perform. There are three *)
(* things they can do: *)
(* *)
(* - Pour water from the faucet into a jug. *)
(* *)
(* - Pour water from a jug onto the ground. *)
(* *)
(* - Pour water from one jug into another *)
(* *)
(* We now consider the first two. Since the jugs are not calibrated, *)
(* partially filling or partially emptying a jug accomplishes nothing. *)
(* So, the first two possibilities yield the following four possible *)
(* actions. *)
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big
FillBigJug == /\ big' = 5
/\ small' = small
EmptySmallJug == /\ small' = 0
/\ big' = big
EmptyBigJug == /\ big' = 0
/\ small' = small
(***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *)
(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
(* makes sense only to either fill B or empty A. And there's no point in *)
(* emptying A if this will cause B to overflow, since that could be *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this *)
(* mathematically, we first define Min(m,n) to equal the minimum of the *)
(* numbers m and n. *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n
(***************************************************************************)
(* Now we define the last two pouring actions. From the observation *)
(* above, these definitions should be clear. *)
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)
BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small)
(***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *)
(* step is a step of one of the six actions defined above. Hence, Next is *)
(* the disjunction of those actions. *)
(***************************************************************************)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall
-----------------------------------------------------------------------------
(***************************************************************************)
(* Remember that our heros must measure out 4 gallons of water. *)
(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
(* solved their problem when they reach a state with big = 4. So, we *)
(* define NotSolved to be the predicate asserting that big # 4. *)
(***************************************************************************)
NotSolved == big # 4
(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant, *)
(* which will cause it to print out an "error trace" consisting of a *)
(* behavior ending in a states where NotSolved is false. Such a *)
(* behavior is the desired solution. (Because TLC uses a breadth-first *)
(* search, it will find the shortest solution.) *)
(***************************************************************************)
=============================================================================
Z Version
A Z version of the puzzle is also included with ProB (inside the examples/Z/GraphicalAnimation/ directory) and shown on the ProZ wiki page.
Here is how the animation of the Z specification should look like:
