No edit summary |
No edit summary |
||
Line 51: | Line 51: | ||
The main window of ProB now contains the following information: | The main window of ProB now contains the following information: | ||
[[File:Jars_Panes.png| | [[File:Jars_Panes.png|700px|center]] | ||
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). | 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). |
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 /* This is the B model of a puzzle from the movie "Die Hard with a Vengeance": https://www.youtube.com/watch?v=BVtQNK_ZUJg http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm Input: one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons */ DEFINITIONS GOAL == (4:ran(level)); SETS Jars = {j3,j5} CONSTANTS maxf PROPERTIES maxf : Jars --> NAT & 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 GOAL" check box and press the model check button:
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).