Rush Hour XTL - Revision history

David Geleßus: Update Wikipedia link

2021-02-03T13:54:20Z

Update Wikipedia link

← Older revision		Revision as of 13:54, 3 February 2021
Line 1:		Line 1:
	This case studies tackles encoding the [~~http~~://en.wikipedia.org/wiki/Rush_Hour_(~~board_game~~) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].		This case studies tackles encoding the [https://en.wikipedia.org/wiki/Rush_Hour_(puzzle) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].

	This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second (on a Mac Book Air, 1.7 GHz i7), on the B version it takes ProB about 10 seconds (but the TLC backend is faster).		This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second (on a Mac Book Air, 1.7 GHz i7), on the B version it takes ProB about 10 seconds (but the TLC backend is faster).

Michael Leuschel at 10:39, 23 July 2014

2014-07-23T10:39:28Z

← Older revision		Revision as of 10:39, 23 July 2014
Line 1:		Line 1:
	This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle Nr 40].		This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle of the original game Nr. 40].

	This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second (on a Mac Book Air, 1.7 GHz i7), on the B version it takes ProB about 10 seconds (but the TLC backend is faster).		This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second (on a Mac Book Air, 1.7 GHz i7), on the B version it takes ProB about 10 seconds (but the TLC backend is faster).
	Part of the B models are shown in comments for reference below.		Part of the B models are shown in comments for reference below.
	This file needs to be saved with a <tt>.P</tt> extension so that it can be loaded by ProB Tcl/Tk or probcli.		This file needs to be saved with a <tt>.P</tt> extension so that it can be loaded by [[Installation\|ProB Tcl/Tk]] or [[Using_the_Command-Line_Version_of_ProB\|probcli]].

	Observe how we use sort and ord_add_element to avoid multiple versions of the same state.		Observe how we use sort and ord_add_element to avoid multiple versions of the same state.
Line 184:		Line 184:
	== Running using probcli ==		== Running using probcli ==

	Here is how you can find the solution using probcli (run on a Mac Book Air, 1.7 GHz i7):		Here is how you can find the solution using [[Using_the_Command-Line_Version_of_ProB\|probcli]] (run on a Mac Book Air, 1.7 GHz i7):

	<pre>		<pre>

Michael Leuschel at 10:25, 23 July 2014

2014-07-23T10:25:33Z

← Older revision		Revision as of 10:25, 23 July 2014
Line 1:		Line 1:
	This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle Nr 40].		This case studies tackles encoding the [http://en.wikipedia.org/wiki/Rush_Hour_(board_game) rush hour board game] in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit. In this particular instance we try to solve the [http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40 hardest puzzle Nr 40].

	This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second, on the B version it takes ProB about 10 seconds (but the TLC backend is faster).		This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second (on a Mac Book Air, 1.7 GHz i7), on the B version it takes ProB about 10 seconds (but the TLC backend is faster).
	Part of the B models are shown in comments for reference below.		Part of the B models are shown in comments for reference below.
	This file needs to be saved with a <tt>.P</tt> extension so that it can be loaded by ProB Tcl/Tk or probcli.		This file needs to be saved with a <tt>.P</tt> extension so that it can be loaded by ProB Tcl/Tk or probcli.
Line 184:		Line 184:
	== Running using probcli ==		== Running using probcli ==

	Here is how you can find the solution using probcli.		Here is how you can find the solution using probcli (run on a Mac Book Air, 1.7 GHz i7):

	<pre>		<pre>
Line 303:		Line 303:
	start_xtl_system:1		start_xtl_system:1
	UNCOVERED_OPERATIONS		UNCOVERED_OPERATIONS
			</pre>


			Complete model checking, without looking for goal states, takes 1.6 seconds (on a Mac Book Air, 1.7 GHz i7):
			<pre>
			$ probcli -mc 100000 RushHour_Prolog.P -noinv --coverage
			tcltk_open_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
			new_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
			% All open nodes visited
			Model Checking Time: 1610 ms
			States analysed: 4780
			Transitions fired: 29889
			No Counter Example found. ALL nodes visited.
			Coverage:

			[STATES,deadlocked:0,open:0,live:4781,total:4781,TOTAL_OPERATIONS,29889,COVERED_OPERATIONS,mv_down:8461,mv_left:6483,mv_right:6483,mv_up:8461,start_xtl_system:1,UNCOVERED_OPERATIONS]
	</pre>		</pre>

Michael Leuschel at 10:20, 23 July 2014

2014-07-23T10:20:14Z

@@ Line 284: / Line 284: @@
 ! *** error occurred ***
 ! xtl_error
 </pre>

Michael Leuschel at 10:14, 23 July 2014

2014-07-23T10:14:19Z

← Older revision		Revision as of 10:14, 23 July 2014
Line 4:		Line 4:
	Part of the B models are shown in comments for reference below.		Part of the B models are shown in comments for reference below.
	This file needs to be saved with a <tt>.P</tt> extension so that it can be loaded by ProB Tcl/Tk or probcli.		This file needs to be saved with a <tt>.P</tt> extension so that it can be loaded by ProB Tcl/Tk or probcli.

			Observe how we use sort and ord_add_element to avoid multiple versions of the same state.
			The important predicates that ProB uses are <tt>start/1</tt>, <tt>trans/3</tt> and <tt>prop/2</tt>.

	<pre>		<pre>

Michael Leuschel at 10:10, 23 July 2014

2014-07-23T10:10:58Z

← Older revision		Revision as of 10:10, 23 July 2014
Line 65:		Line 65:
	nth1(Car,Sze,SC),		nth1(Car,Sze,SC),
	FR is RC+SC, F = (FR,CC),		FR is RC+SC, F = (FR,CC),
	~~% print(try_down(Car,F)),nl,~~
	select(F,Free,Free0),		select(F,Free,Free0),
	ord_add_element(Free0,(RC,CC),SFree1),		ord_add_element(Free0,(RC,CC),SFree1),
Line 87:		Line 86:
	nth1(Car,Cols,CC),		nth1(Car,Cols,CC),
	FR is RC-1, F = (FR,CC),		FR is RC-1, F = (FR,CC),
	~~% print(try_up(Car,F)),nl,~~
	select(F,Free,Free0),		select(F,Free,Free0),
	sze(Sze),		sze(Sze),
Line 111:		Line 109:
	nth1(Car,Sze,SC),		nth1(Car,Sze,SC),
	CCS is CC+SC, F = (RC,CCS),		CCS is CC+SC, F = (RC,CCS),
	~~% print(try_right(Car,RC,CC,SC,F,Free)),nl,~~
	select(F,Free,Free0),		select(F,Free,Free0),
	ord_add_element(Free0,(RC,CC),SFree1),		ord_add_element(Free0,(RC,CC),SFree1),
Line 131:		Line 128:
	nth1(Car,Cols,CC),		nth1(Car,Cols,CC),
	CC1 is CC-1, F = (RC,CC1),		CC1 is CC-1, F = (RC,CC1),
	~~%print(try_left(Car,F)),nl,~~
	select(F,Free,Free0),		select(F,Free,Free0),
	sze(Sze),		sze(Sze),

Michael Leuschel at 10:10, 23 July 2014

2014-07-23T10:10:11Z

← Older revision		Revision as of 10:10, 23 July 2014
Line 8:		Line 8:
	/* a Prolog XTL translation of the more elegant encoding of the Rush Hour puzzle */		/* a Prolog XTL translation of the more elegant encoding of the Rush Hour puzzle */
	/* Michael Leuschel, July 2014 */		/* Michael Leuschel, July 2014 */
	/* ProB finds solution in about 1 second using mixed DF/BF search /		/* ProB finds solution in about 0.5 - 1 second using mixed DF/BF search /
	/* Using BF search it takes 1.8 seconds */		/* Using BF search it takes 1.3 seconds */
	/* This shows the potential of compiling the ProB B interpreter down to Prolog */		/* This shows the potential of compiling the ProB B interpreter down to Prolog */
	/* The Prolog could still be optimized further (e.g. run through a partial evaluator ) */		/* The Prolog could still be optimized further (e.g. run through a partial evaluator ) */


	:- use_module(library(lists)).		%:- use_module(library(lists)). % not needed when run from ProB
			%:- use_module(library(ordsets)). % not needed when run from ProB

	sze([2,2,2,2,2, 2,2,2,2, 3,3,3, 2]). /* the sizes of the cars */		sze([2,2,2,2,2, 2,2,2,2, 3,3,3, 2]). /* the sizes of the cars */
Line 54:		Line 55:
	replace([_\|T],1,New,Res) :- !, Res=[New\|T].		replace([_\|T],1,New,Res) :- !, Res=[New\|T].
	replace([H\|T],N,New,[H\|TR]) :- N1 is N-1, replace(T,N1,New,TR).		replace([H\|T],N,New,[H\|TR]) :- N1 is N-1, replace(T,N1,New,TR).


	trans(mv_down(Car,F),rcf(Rows,Cols,Free),rcf(Rows1,Cols,SFree1)) :-		trans(mv_down(Car,F),rcf(Rows,Cols,Free),rcf(Rows1,Cols,SFree1)) :-
Line 65:		Line 67:
	% print(try_down(Car,F)),nl,		% print(try_down(Car,F)),nl,
	select(F,Free,Free0),		select(F,Free,Free0),
	~~Free1 = [~~(RC,CC)~~\|Free0], sort(Free1~~,SFree1),		ord_add_element(Free0,(RC,CC),SFree1),
	RC1 is RC+1,		RC1 is RC+1,
	replace(Rows,Car,RC1,Rows1).		replace(Rows,Car,RC1,Rows1).
Line 85:		Line 87:
	nth1(Car,Cols,CC),		nth1(Car,Cols,CC),
	FR is RC-1, F = (FR,CC),		FR is RC-1, F = (FR,CC),
	% print(try_up(Car,F)),nl,		% print(try_up(Car,F)),nl,
	select(F,Free,Free0),		select(F,Free,Free0),
	sze(Sze),		sze(Sze),
	nth1(Car,Sze,SC),		nth1(Car,Sze,SC),
	RSC1 is RC+SC-1,		RSC1 is RC+SC-1,
	~~Free1 = [~~(RSC1,CC)~~\|Free0], sort(Free1~~,SFree1),		ord_add_element(Free0,(RSC1,CC),SFree1),
	replace(Rows,Car,FR,Rows1).		replace(Rows,Car,FR,Rows1).

Line 109:		Line 111:
	nth1(Car,Sze,SC),		nth1(Car,Sze,SC),
	CCS is CC+SC, F = (RC,CCS),		CCS is CC+SC, F = (RC,CCS),
	% print(try_right(Car,RC,CC,SC,F)),nl,		% print(try_right(Car,RC,CC,SC,F,Free)),nl,
	select(F,Free,Free0),		select(F,Free,Free0),
	~~Free1 = [~~(RC,CC)~~\|Free0], sort(Free1~~,SFree1),		ord_add_element(Free0,(RC,CC),SFree1),
	CC1 is CC+1,		CC1 is CC+1,
	replace(Cols,Car,CC1,Cols1).		replace(Cols,Car,CC1,Cols1).
Line 134:		Line 136:
	nth1(Car,Sze,SC),		nth1(Car,Sze,SC),
	CCS is CC1+SC,		CCS is CC1+SC,
	~~Free1 = [~~(RC,CCS)~~\|Free0], sort(Free1~~,SFree1),		ord_add_element(Free0,(RC,CCS),SFree1),
	replace(Cols,Car,CC1,Cols1).		replace(Cols,Car,CC1,Cols1).

Line 183:		Line 185:
	== Running using probcli ==		== Running using probcli ==

	Here is how you can find the solution using probcli. ~~Please ignore the use_module error messages or remove the use_module declarations from the .P code above if they bother you:~~		Here is how you can find the solution using probcli.

	<pre>		<pre>
	$ probcli -mc 100000 RushHour_Prolog.P -bf		$ probcli -mc 100000 RushHour_Prolog.P -bf
	tcltk_open_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)		tcltk_open_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
	~~! Existence error in argument 1 of use_module/1~~
	~~! file library(lists) does not exist~~
	~~! goal: use_module(xtl_interface:library(lists))~~
	~~! Existence error in argument 1 of use_module/1~~
	~~! file library(ordsets) does not exist~~
	~~! goal: use_module(xtl_interface:library(ordsets))~~
	new_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)		new_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
	found_error(xtl_error,3026)		found_error(xtl_error,3026)
	finding_trace_from_to(root)		finding_trace_from_to(root)
	....................		....................
	Model Checking Time: ~~1280~~ ms		Model Checking Time: 1310 ms
	States analysed: 3026		States analysed: 3026
	Transitions fired: 19821		Transitions fired: 19821

Michael Leuschel at 09:49, 23 July 2014

2014-07-23T09:49:07Z

← Older revision		Revision as of 09:49, 23 July 2014
Line 179:		Line 179:

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


			== Running using probcli ==

			Here is how you can find the solution using probcli. Please ignore the use_module error messages or remove the use_module declarations from the .P code above if they bother you:

			<pre>
			$ probcli -mc 100000 RushHour_Prolog.P -bf
			tcltk_open_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
			! Existence error in argument 1 of use_module/1
			! file library(lists) does not exist
			! goal: use_module(xtl_interface:library(lists))
			! Existence error in argument 1 of use_module/1
			! file library(ordsets) does not exist
			! goal: use_module(xtl_interface:library(ordsets))
			new_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
			found_error(xtl_error,3026)
			finding_trace_from_to(root)
			....................
			Model Checking Time: 1280 ms
			States analysed: 3026
			Transitions fired: 19821
			* COUNTER EXAMPLE FOUND *

			xtl_error
			*** TRACE:
			1: start_xtl_system:
			2: mv_right(8,(5,5)):
			3: mv_down(4,(5,3)):
			4: mv_up(11,(0,5)):
			5: mv_right(12,(3,3)):
			6: mv_down(10,(3,0)):
			7: mv_left(7,(0,0),0,1,2,2):
			8: mv_right(12,(3,4)):
			9: mv_up(2,(0,2)):
			10: mv_down(1,(3,1)):
			11: mv_down(10,(4,0)):
			12: mv_right(12,(3,5)):
			13: mv_left(13,(2,2),2,3,2,4):
			14: mv_down(1,(4,1)):
			15: mv_up(3,(3,2)):
			16: mv_right(6,(5,2)):
			17: mv_left(13,(2,1),2,2,2,3):
			18: mv_down(10,(5,0)):
			19: mv_left(13,(2,0),2,1,2,2):
			20: mv_down(2,(2,2)):
			21: mv_right(7,(0,2)):
			22: mv_down(5,(2,4)):
			23: mv_right(7,(0,3)):
			24: mv_right(7,(0,4)):
			25: mv_up(2,(0,2)):
			26: mv_right(13,(2,2)):
			27: mv_up(10,(2,0)):
			28: mv_left(6,(5,0),5,1,2,2):
			29: mv_down(3,(5,2)):
			30: mv_left(12,(3,2),3,3,3,5):
			31: mv_right(13,(2,3)):
			32: mv_up(1,(2,1)):
			33: mv_up(1,(1,1)):
			34: mv_left(12,(3,1),3,2,3,4):
			35: mv_up(10,(1,0)):
			36: mv_up(10,(0,0)):
			37: mv_up(1,(0,1)):
			38: mv_left(12,(3,0),3,1,3,3):
			39: mv_up(4,(3,3)):
			40: mv_left(13,(2,1),2,2,2,3):
			41: mv_up(4,(2,3)):
			42: mv_up(4,(1,3)):
			43: mv_right(12,(3,3)):
			44: mv_down(10,(3,0)):
			45: mv_down(11,(3,5)):
			46: mv_right(7,(0,5)):
			47: mv_up(4,(0,3)):
			48: mv_right(13,(2,3)):
			49: mv_right(12,(3,4)):
			50: mv_down(1,(2,1)):
			51: mv_down(1,(3,1)):
			52: mv_down(1,(4,1)):
			53: mv_left(13,(2,1),2,2,2,3):
			54: mv_down(4,(2,3)):
			55: mv_left(7,(0,3),0,4,2,5):
			56: mv_up(11,(0,5)):
			57: mv_right(12,(3,5)):
			58: mv_up(3,(3,2)):
			59: mv_right(6,(5,2)):
			60: mv_down(10,(4,0)):
			61: mv_down(10,(5,0)):
			62: mv_left(13,(2,0),2,1,2,2):
			63: mv_down(2,(2,2)):
			64: mv_left(7,(0,2),0,3,2,4):
			65: mv_left(7,(0,1),0,2,2,3):
			66: mv_left(7,(0,0),0,1,2,2):
			67: mv_up(2,(0,2)):
			68: mv_right(13,(2,2)):
			69: mv_left(9,(4,3),4,4,2,5):
			70: mv_up(10,(2,0)):
			71: mv_left(6,(5,0),5,1,2,2):
			72: mv_up(4,(0,3)):
			73: mv_right(13,(2,3)):
			74: mv_left(8,(5,3),5,4,2,5):
			75: mv_down(3,(5,2)):
			76: mv_left(12,(3,2),3,3,3,5):
			77: mv_down(11,(3,5)):
			78: mv_down(11,(4,5)):
			79: mv_up(5,(0,4)):
			80: mv_right(13,(2,4)):
			81: mv_down(11,(5,5)):
			82: mv_right(13,(2,5)):
			! * error occurred *
			! xtl_error
			</pre>

Michael Leuschel at 08:26, 23 July 2014

2014-07-23T08:26:13Z

← Older revision		Revision as of 08:26, 23 July 2014
Line 147:		Line 147:
	</pre>		</pre>

	We can also add a simple [[Graphical_Visualization\|graphical visualisation]] by including the following in the XTL file (recognised by ProB as of version 1.4.0-rc3):		We can also add a simple [[Graphical_Visualization\|graphical visualisation]] by including the following in the XTL file (using the <tt>animation_function_result</tt> predicate recognised by ProB as of version 1.4.0-rc3):

	<pre>		<pre>

Michael Leuschel at 08:22, 23 July 2014

2014-07-23T08:22:29Z

← Older revision		Revision as of 08:22, 23 July 2014
Line 3:		Line 3:
	This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second, on the B version it takes ProB about 10 seconds (but the TLC backend is faster).		This is a [[Other_languages\|Prolog XTL encoding]] of the [[Rush_Hour_Puzzle\|B solution which is also available]]. On the Prolog XTL encoding presented here ProB finds the example in one second, on the B version it takes ProB about 10 seconds (but the TLC backend is faster).
	Part of the B models are shown in comments for reference below.		Part of the B models are shown in comments for reference below.
	This file needs to be saved with a <~~pre~~>.P</~~pre~~> extension so that it can be loaded by ProB Tcl/Tk or probcli.		This file needs to be saved with a <tt>.P</tt> extension so that it can be loaded by ProB Tcl/Tk or probcli.

	<pre>		<pre>
Line 147:		Line 147:
	</pre>		</pre>

	We can also add a simple graphical visualisation (as of ~~ProB~~ 1.4.0-rc3):		We can also add a simple [[Graphical_Visualization\|graphical visualisation]] by including the following in the XTL file (recognised by ProB as of version 1.4.0-rc3):

	<pre>		<pre>
Line 173:		Line 173:
	(Col1 is Col+1 ; SC>2, Col1 is Col+2).		(Col1 is Col+1 ; SC>2, Col1 is Col+2).
	</pre>		</pre>


			Here is a screenshot of ProB after finding the shortest solution using model checking.
			You can see the (simple) [[Graphical_Visualization\|graphical visualisation]] of the state of the model.

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