Die Hard Jugs Puzzle - Revision history

Dominik Hansen: /* TLA+ Version */

2016-02-03T12:34:42Z

TLA+ Version

← Older revision		Revision as of 12:34, 3 February 2016
Line 110:		Line 110:
	== TLA+ Version ==		== TLA+ Version ==
	A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory).		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~~ is possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.		The specification was developed by Leslie Lamport. It is possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.
	<pre>		<pre>
	------------------------------ MODULE DieHard -------------------------------		------------------------------ MODULE DieHard -------------------------------

2016-02-03T11:11:40Z

← Older revision		Revision as of 11:11, 3 February 2016
Line 1:		Line 1:
	This is the B model of a puzzle from the movie "Die Hard with a Vengeance".		This is the B model of a puzzle from the movie "Die Hard with a Vengeance".
	This [https://www.youtube.com/watch?v=BVtQNK_ZUJg clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].		This [https://www.youtube.com/watch?v=BVtQNK_ZUJg clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].
	A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm\|more detailed explanation can be found here].		A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm more 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.		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.

2016-02-03T11:11:09Z

← Older revision		Revision as of 11:11, 3 February 2016
Line 1:		Line 1:
	This is the B model of a puzzle from the movie "Die Hard with a Vengeance".		This is the B model of a puzzle from the movie "Die Hard with a Vengeance".
	This [https://www.youtube.com/watch?v=BVtQNK_ZUJg\|clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].		This [https://www.youtube.com/watch?v=BVtQNK_ZUJg clip shows Bruce Willis and Samuel Jackson having a go at the puzzle].
	A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm\|more detailed explanation can be found here].		A [http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm\|more 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.		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.

2016-02-03T11:03:47Z

TLA+ Version

← Older revision		Revision as of 11:03, 3 February 2016
Line 110:		Line 110:
	== TLA+ Version ==		== TLA+ Version ==
	A TLA+ version of the puzzle is also included with ProB (inside the examples/TLA+/ directory).		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.		The specification was developed by Leslie Lamport in order to be validated by the TLC model checker. However, it is possible to load TLA+ specifications with ProB as shown on the [[TLA]] wiki page.
	<pre>		<pre>
	------------------------------ MODULE DieHard -------------------------------		------------------------------ MODULE DieHard -------------------------------

2016-02-03T09:18:25Z

2016-02-03T08:53:52Z

2016-02-02T07:32:27Z

← Older revision		Revision as of 07:32, 2 February 2016
Line 52:		Line 52:
	== Graphical Animation ==		== Graphical Animation ==

	This machine above is actually included in the ProB distribution.		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_Visualization\|graphical visualisation]] of the state.		It also contains the following lines in the DEFINITIONS section, which defines a quick-and-dirty [[Graphical_Visualization\|graphical visualisation]] of the state.
	The images can be found in the subfolder images along the file Jars.mch.		The images can be found in the subfolder images along the file Jars.mch.
Line 107:		Line 107:
	! goal_found		! goal_found
	</pre>		</pre>

			== 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:

			[[File:ProZ_jars.png\|600px\|center]]

2016-02-02T07:18:29Z

← Older revision		Revision as of 07:18, 2 February 2016
Line 7:		Line 7:
	<pre>		<pre>
	MACHINE Jars		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		DEFINITIONS
	GOAL == (4:ran(level));		GOAL == (4:ran(level));

2016-02-02T07:16:46Z

← Older revision		Revision as of 07:16, 2 February 2016
Line 76:		Line 76:

	[[File:ProB_DieHard_Screenshot.png\|600px\|center]]		[[File:ProB_DieHard_Screenshot.png\|600px\|center]]

			== 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:

			<pre>
			$ 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
			</pre>

2016-02-02T07:15:24Z

← Older revision		Revision as of 07:15, 2 February 2016
Line 17:		Line 17:
	SETS Jars = {j3,j5}		SETS Jars = {j3,j5}
	CONSTANTS maxf		CONSTANTS maxf
	PROPERTIES maxf : Jars --> ~~NAT~~ &		PROPERTIES maxf : Jars --> NATURAL &
	maxf = {j3 \|-> 3, j5 \|-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */		maxf = {j3 \|-> 3, j5 \|-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
	VARIABLES level		VARIABLES level