Rush Hour XTL
This case studies tackles encoding the 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 hardest puzzle Nr 40.
This is a Prolog XTL encoding of the 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. This file needs to be saved with a .P extension so that it can be loaded by ProB Tcl/Tk or probcli.
/* a Prolog XTL translation of the more elegant encoding of the Rush Hour puzzle */
/* Michael Leuschel, July 2014 */
/* ProB finds solution in about 1 second *using mixed DF/BF search */
/* Using BF search it takes 1.8 seconds */
/* 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 ) */
:- use_module(library(lists)).
sze([2,2,2,2,2, 2,2,2,2, 3,3,3, 2]). /* the sizes of the cars */
dir([v,v,v,v,v, h,h,h,h, v,v,h, h]). /* indicating whether the cars move vertically or horizontally */
red(Len) :- sze(S), length(S,Len). /* the last car is the red one */
dim(5). /* the grid goes from 0..dim */
free_initial([(0,3),(1,3), (0,5), (3,4),(4,0),(4,1),(5,5)]).
col_initial([(1),(2),(2),(3),(4), /* vertical 2-size cars */
(0),(1),(3),(4), /* horiz. 2-size cars */
(0),(5), /* vertical 3-size cars */
(0), /* horiz. 3-size cars */
(3)] /* red car */
).
row_initial([(1),(1),(4),(3),(0),
(5),(0),(5),(4),
(0),(1),
(3),
(2)]).
init(S) :- start(S).
start(rcf(Rows,Cols,SFree)) :- free_initial(Free),
sort(Free,SFree),
row_initial(Rows),
col_initial(Cols).
prop(rcf(_,_,Free),free(I,J)) :- member((I,J),Free).
prop(rcf(Rows,Cols,_),car(Car,Row,Col)) :- nth1(Car,Rows,Row),nth1(Car,Cols,Col).
/*
prop(rcf(_,_,Free),unsafe) :- member((N,M),Free), (N>5 ; N<0 ; M>5 ; M<0).
prop(rcf(Rows,_,_),unsafe) :- member(N,Rows), (N>5 ; N<0).
prop(rcf(_,Cols,_),unsafe) :- member(N,Cols), (N>5 ; N<0).
*/
prop(rcf(_Rows,Cols,_Free),unsafe) :- last(Cols,4). /* The target : move red car to the right */
% utility for updating lists of columns/rows:
replace([_|T],1,New,Res) :- !, Res=[New|T].
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)) :-
dir(Dir),
nth1(Car,Dir,v),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
sze(Sze),
nth1(Car,Sze,SC),
FR is RC+SC, F = (FR,CC),
% print(try_down(Car,F)),nl,
select(F,Free,Free0),
Free1 = [(RC,CC)|Free0], sort(Free1,SFree1),
RC1 is RC+1,
replace(Rows,Car,RC1,Rows1).
/*
mv_down(c,F) = PRE c:1..red & c |-> v : dir & F = row(c)+sze(c)|->col(c) &
F : free THEN
free := free - {F} \/ {row(c)|->col(c)} ||
row(c) := row(c)+1
END;
*/
trans(mv_up(Car,F),rcf(Rows,Cols,Free),rcf(Rows1,Cols,SFree1)) :-
dir(Dir),
nth1(Car,Dir,v),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
FR is RC-1, F = (FR,CC),
% print(try_up(Car,F)),nl,
select(F,Free,Free0),
sze(Sze),
nth1(Car,Sze,SC),
RSC1 is RC+SC-1,
Free1 = [(RSC1,CC)|Free0], sort(Free1,SFree1),
replace(Rows,Car,FR,Rows1).
/*
mv_up(c,F) = PRE c:1..red & c |-> v : dir & F = row(c)-1|->col(c) &
F : free THEN
free := free - {F} \/ {row(c)+sze(c)-1|->col(c)} ||
row(c) := row(c)-1
END; */
trans(mv_right(Car,F),rcf(Rows,Cols,Free),rcf(Rows,Cols1,SFree1)) :-
dir(Dir),
nth1(Car,Dir,h),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
sze(Sze),
nth1(Car,Sze,SC),
CCS is CC+SC, F = (RC,CCS),
% print(try_right(Car,RC,CC,SC,F)),nl,
select(F,Free,Free0),
Free1 = [(RC,CC)|Free0], sort(Free1,SFree1),
CC1 is CC+1,
replace(Cols,Car,CC1,Cols1).
/*
mv_right(c,F) = PRE c:1..red & c |-> h : dir & F = row(c)|->col(c)+sze(c) &
F : free THEN
free := free - {F} \/ {row(c)|->col(c)} ||
col(c) := col(c)+1
END; */
trans(mv_left(Car,F,RC,CC,SC,CCS),rcf(Rows,Cols,Free),rcf(Rows,Cols1,SFree1)) :-
dir(Dir),
nth1(Car,Dir,h),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
CC1 is CC-1, F = (RC,CC1),
%print(try_left(Car,F)),nl,
select(F,Free,Free0),
sze(Sze),
nth1(Car,Sze,SC),
CCS is CC1+SC,
Free1 = [(RC,CCS)|Free0], sort(Free1,SFree1),
replace(Cols,Car,CC1,Cols1).
/*
mv_left(c,F) = PRE c:1..red & c |-> h : dir & F = row(c)|->col(c)-1 &
F : free THEN
free := free - {F} \/ {row(c)|->col(c)+sze(c)-1} ||
col(c) := col(c)-1
END
END
*/
We can also add a simple graphical visualisation by including the following in the XTL file (using the animation_function_result predicate recognised by ProB as of version 1.4.0-rc3):
% Graphical Visualization Animation Function:
is_index(I,I).
is_index(I,Res) :- dim(N), I<N, I1 is I+1, is_index(I1,Res).
animation_function_result(State,Matrix) :-
findall(((RowNr,ColNr),Cell), (is_index(0,RowNr),is_index(0,ColNr),
cell_content(State,RowNr,ColNr,Cell)),Matrix).
cell_content(rcf(Rows,Cols,Free),Row,Col,'--') :- member((Row,Col),Free).
cell_content(rcf(Rows,Cols,Free),Row,Col,Car) :- nth1(Car,Rows,Row), nth1(Car,Cols,Col).
cell_content(rcf(Rows,Cols,Free),Row1,Col,Car) :- dir(Dir),
sze(Sze),
nth1(Car,Dir,v),
nth1(Car,Sze,SC),
nth1(Car,Rows,Row), nth1(Car,Cols,Col),
(Row1 is Row+1 ; SC>2, Row1 is Row+2).
cell_content(rcf(Rows,Cols,Free),Row,Col1,Car) :- dir(Dir),
sze(Sze),
nth1(Car,Dir,h),
nth1(Car,Sze,SC),
nth1(Car,Rows,Row), nth1(Car,Cols,Col),
(Col1 is Col+1 ; SC>2, Col1 is Col+2).
Here is a screenshot of ProB after finding the shortest solution using model checking.
You can see the (simple) graphical visualisation of the state of the model.
