No edit summary |
No edit summary |
||
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. | /* 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), | ||
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, | |||
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, | ||
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,Free)),nl, | |||
select(F,Free,Free0), | select(F,Free,Free0), | ||
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, | ||
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. | 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) | ||
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: | Model Checking Time: 1310 ms | ||
States analysed: 3026 | States analysed: 3026 | ||
Transitions fired: 19821 | Transitions fired: 19821 |
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 0.5 - 1 second *using mixed DF/BF search */ /* Using BF search it takes 1.3 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)). % 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 */ 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), ord_add_element(Free0,(RC,CC),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, ord_add_element(Free0,(RSC1,CC),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,Free)),nl, select(F,Free,Free0), ord_add_element(Free0,(RC,CC),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, ord_add_element(Free0,(RC,CCS),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.
Here is how you can find the solution using probcli.
$ 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) 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: 1310 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