No edit summary |
No edit summary |
||
Line 76: | Line 76: | ||
</pre> | </pre> | ||
[[File:ProB_RushHour_v2_Screenshot.png|600px|center]] | |||
The shortest solution has 81 moves (if one allows a car to move multiple spaces in one move then the shortest solution has 51 moves). | |||
It was found in 3 seconds (about 1 second model checking time): | |||
[[File:ProB_RushHour_v2_TLC_Dialog.png|600px|center]] | |||
Here is the solution when save the trace to a B file (Save History to B File... command in the Verify -> Trace Checking submenu): | |||
<pre> | |||
/* Constants | |||
sze = [2,2,2,2,2,2,2,2,2,3,3,3,2] | |||
& dir = [v,v,v,v,v,h,h,h,h,v,v,h,h] | |||
& red = 13 | |||
& dim = 5 | |||
& free_initial = {(0|->3),(0|->5),(1|->3),(3|->4),(4|->0),(4|->1),(5|->5)} | |||
*/ | |||
/* Initialisation */ | |||
/* Variables | |||
free = {(0|->3),(0|->5),(1|->3),(3|->4),(4|->0),(4|->1),(5|->5)} | |||
& col = [1,2,2,3,4,0,1,3,4,0,5,0,3] | |||
& row = [1,1,4,3,0,5,0,5,4,0,1,3,2] | |||
*/ | |||
mv_up(11,(0|->5)); | |||
mv_right(8,(5|->5)); | |||
mv_down(4,(5|->3)); | |||
mv_right(12,(3|->3)); | |||
mv_down(10,(3|->0)); | |||
mv_down(10,(4|->0)); | |||
mv_right(12,(3|->4)); | |||
mv_down(1,(3|->1)); | |||
mv_down(1,(4|->1)); | |||
mv_right(12,(3|->5)); | |||
mv_up(3,(3|->2)); | |||
mv_right(6,(5|->2)); | |||
mv_down(10,(5|->0)); | |||
mv_left(7,(0|->0)); | |||
mv_up(2,(0|->2)); | |||
mv_left(13,(2|->2)); | |||
mv_left(13,(2|->1)); | |||
mv_left(13,(2|->0)); | |||
mv_down(2,(2|->2)); | |||
mv_right(7,(0|->2)); | |||
mv_right(7,(0|->3)); | |||
mv_down(5,(2|->4)); | |||
mv_right(7,(0|->4)); | |||
mv_up(2,(0|->2)); | |||
mv_right(13,(2|->2)); | |||
mv_up(10,(2|->0)); | |||
mv_up(10,(1|->0)); | |||
mv_up(10,(0|->0)); | |||
mv_right(13,(2|->3)); | |||
mv_up(1,(2|->1)); | |||
mv_up(1,(1|->1)); | |||
mv_up(1,(0|->1)); | |||
mv_left(13,(2|->1)); | |||
mv_left(6,(5|->0)); | |||
mv_down(3,(5|->2)); | |||
mv_left(12,(3|->2)); | |||
mv_down(11,(3|->5)); | |||
mv_right(7,(0|->5)); | |||
mv_left(12,(3|->1)); | |||
mv_left(12,(3|->0)); | |||
mv_up(4,(3|->3)); | |||
mv_up(4,(2|->3)); | |||
mv_up(4,(1|->3)); | |||
mv_up(4,(0|->3)); | |||
mv_right(13,(2|->3)); | |||
mv_down(1,(2|->1)); | |||
mv_right(12,(3|->3)); | |||
mv_down(10,(3|->0)); | |||
mv_right(12,(3|->4)); | |||
mv_down(1,(3|->1)); | |||
mv_down(10,(4|->0)); | |||
mv_left(9,(4|->3)); | |||
mv_down(1,(4|->1)); | |||
mv_left(13,(2|->1)); | |||
mv_down(4,(2|->3)); | |||
mv_left(7,(0|->3)); | |||
mv_left(8,(5|->3)); | |||
mv_up(11,(0|->5)); | |||
mv_right(12,(3|->5)); | |||
mv_up(3,(3|->2)); | |||
mv_right(6,(5|->2)); | |||
mv_down(10,(5|->0)); | |||
mv_left(13,(2|->0)); | |||
mv_down(2,(2|->2)); | |||
mv_left(7,(0|->2)); | |||
mv_up(5,(0|->4)); | |||
mv_left(7,(0|->1)); | |||
mv_up(4,(0|->3)); | |||
mv_left(7,(0|->0)); | |||
mv_up(2,(0|->2)); | |||
mv_right(13,(2|->2)); | |||
mv_up(10,(2|->0)); | |||
mv_right(13,(2|->3)); | |||
mv_right(13,(2|->4)); | |||
mv_left(6,(5|->0)); | |||
mv_down(3,(5|->2)); | |||
mv_left(12,(3|->2)); | |||
mv_down(11,(3|->5)); | |||
mv_down(11,(4|->5)); | |||
mv_down(11,(5|->5)); | |||
mv_right(13,(2|->5)) | |||
</pre> | |||
== Old Solution == | == Old Solution == | ||
This is my old solution to the Rush hour puzzle. | |||
It is not very elegant, but does work. | |||
It has a more sophisticated animation function for visualisation. | |||
<pre> | <pre> |
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.
Inspired by discussions with Neng-Fa Zhou, we now have a new version of the model.
The old version can still be found below. Explanations and comparison with Picat will follow soon.
The shortest solution can be found using our new TLC translation very quickly (about 1 second model checking time; rest of time needed to replay counter example).
MACHINE RushHour_v2_TLC /* a more elegant encoding of the Rush Hour puzzle */ /* Michael Leuschel, July 2014 */ /* ProB finds solution in about 10.5 secs (turning invariant checking off) */ /* This version has been slightly adapted for TLC: it finds a solution in 3 seconds (most of this time is spent replaying the counter ; the model checking seems less than a second) */ SETS DIR = {h,v} CONSTANTS sze, dir, red, dim, free_initial PROPERTIES 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 = size(sze) & /* 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)} DEFINITIONS GOAL == (col(red) = 4); /* The target : move red car to the right */ ANIMATION_STR_JUSTIFY_RIGHT == TRUE; ANIMATION_FUNCTION_DEFAULT == (0..dim)*(0..dim)*{-1}; ANIMATION_FUNCTION == {r,c,i| i:1..red & dir(i)=h & row(i)=r & c:col(i)..col(i)+sze(i)-1} \/ {r,c,i| i:1..red & dir(i)=v & col(i)=c & r:row(i)..row(i)+sze(i)-1} \/ free * {0} VARIABLES free, row, col INVARIANT free <: (0..dim)*(0..dim) & /* the currently free blocks */ card(free) = card(free_initial) & row : 1..red --> 0..dim & /* the row of each car */ col : 1..red --> 0..dim /* the column for each car */ INITIALISATION free := free_initial || col := [(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 := [(1),(1),(4),(3),(0), (5),(0),(5),(4), (0),(1), (3), (2)] /* red car */ OPERATIONS 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; 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; 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; 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
The shortest solution has 81 moves (if one allows a car to move multiple spaces in one move then the shortest solution has 51 moves).
It was found in 3 seconds (about 1 second model checking time):
Here is the solution when save the trace to a B file (Save History to B File... command in the Verify -> Trace Checking submenu):
/* Constants sze = [2,2,2,2,2,2,2,2,2,3,3,3,2] & dir = [v,v,v,v,v,h,h,h,h,v,v,h,h] & red = 13 & dim = 5 & free_initial = {(0|->3),(0|->5),(1|->3),(3|->4),(4|->0),(4|->1),(5|->5)} */ /* Initialisation */ /* Variables free = {(0|->3),(0|->5),(1|->3),(3|->4),(4|->0),(4|->1),(5|->5)} & col = [1,2,2,3,4,0,1,3,4,0,5,0,3] & row = [1,1,4,3,0,5,0,5,4,0,1,3,2] */ mv_up(11,(0|->5)); mv_right(8,(5|->5)); mv_down(4,(5|->3)); mv_right(12,(3|->3)); mv_down(10,(3|->0)); mv_down(10,(4|->0)); mv_right(12,(3|->4)); mv_down(1,(3|->1)); mv_down(1,(4|->1)); mv_right(12,(3|->5)); mv_up(3,(3|->2)); mv_right(6,(5|->2)); mv_down(10,(5|->0)); mv_left(7,(0|->0)); mv_up(2,(0|->2)); mv_left(13,(2|->2)); mv_left(13,(2|->1)); mv_left(13,(2|->0)); mv_down(2,(2|->2)); mv_right(7,(0|->2)); mv_right(7,(0|->3)); mv_down(5,(2|->4)); mv_right(7,(0|->4)); mv_up(2,(0|->2)); mv_right(13,(2|->2)); mv_up(10,(2|->0)); mv_up(10,(1|->0)); mv_up(10,(0|->0)); mv_right(13,(2|->3)); mv_up(1,(2|->1)); mv_up(1,(1|->1)); mv_up(1,(0|->1)); mv_left(13,(2|->1)); mv_left(6,(5|->0)); mv_down(3,(5|->2)); mv_left(12,(3|->2)); mv_down(11,(3|->5)); mv_right(7,(0|->5)); mv_left(12,(3|->1)); mv_left(12,(3|->0)); mv_up(4,(3|->3)); mv_up(4,(2|->3)); mv_up(4,(1|->3)); mv_up(4,(0|->3)); mv_right(13,(2|->3)); mv_down(1,(2|->1)); mv_right(12,(3|->3)); mv_down(10,(3|->0)); mv_right(12,(3|->4)); mv_down(1,(3|->1)); mv_down(10,(4|->0)); mv_left(9,(4|->3)); mv_down(1,(4|->1)); mv_left(13,(2|->1)); mv_down(4,(2|->3)); mv_left(7,(0|->3)); mv_left(8,(5|->3)); mv_up(11,(0|->5)); mv_right(12,(3|->5)); mv_up(3,(3|->2)); mv_right(6,(5|->2)); mv_down(10,(5|->0)); mv_left(13,(2|->0)); mv_down(2,(2|->2)); mv_left(7,(0|->2)); mv_up(5,(0|->4)); mv_left(7,(0|->1)); mv_up(4,(0|->3)); mv_left(7,(0|->0)); mv_up(2,(0|->2)); mv_right(13,(2|->2)); mv_up(10,(2|->0)); mv_right(13,(2|->3)); mv_right(13,(2|->4)); mv_left(6,(5|->0)); mv_down(3,(5|->2)); mv_left(12,(3|->2)); mv_down(11,(3|->5)); mv_down(11,(4|->5)); mv_down(11,(5|->5)); mv_right(13,(2|->5))
This is my old solution to the Rush hour puzzle. It is not very elegant, but does work. It has a more sophisticated animation function for visualisation.
MACHINE RushHour /* not a very elegant model; but it seems to work */ /* ProB finds a solution for the hardest puzzle (no. 40) */ DEFINITIONS SET_PREF_MAXINT == 8; /*"RushHour/Puzzle10.def"; */ "RushHour/Puzzle40.def"; INDEX == (1..dim); GOAL == (pos_hcar(red_hcar) >= dim-size_hcar(red_hcar)+1); HEURISTIC_FUNCTION == dim-size_hcar(red_hcar) - pos_hcar(red_hcar) ; /* not a very interesting heuristic function; as red_car can only be moved at very last step */ ANIMATION_IMG0 == "images/sm_empty_box.gif"; ANIMATION_IMG1 == "images/sm_vcar.gif"; ANIMATION_IMG2 == "images/sm_vcar_front.gif"; ANIMATION_IMG3 == "images/sm_hcar.gif"; ANIMATION_IMG4 == "images/sm_red_hcar.gif"; ANIMATION_FUNCTION == ( {r,c,i|r:1..dim & c:1..dim & i=0} <+ {r,c,i|r:1..dim & c:1..dim & i=1 & #j.(j:dom(col_vcar) & c=col_vcar(j) & r>pos_vcar(j) & r<pos_vcar(j)+size_vcar(j)) } <+ {r,c,i|r:1..dim & c:1..dim & i=2 & #j.(j:dom(col_vcar) & c=col_vcar(j) & r=pos_vcar(j)) } <+ {r,c,i|r:1..dim & c:1..dim & i:3..4 & #j.(j:dom(row_hcar) & r=row_hcar(j) & c>=pos_hcar(j) & c<pos_hcar(j)+size_hcar(j) & ((j=red_hcar & i=4) or (j/=red_hcar & i=3)) ) } ); POSs_VCAR(vc) == {c,r|c=col_vcar(vc) & r>=pos_vcar(vc) & r<pos_vcar(vc)+size_vcar(vc)}; POSs_HCAR(hc) == {c,r|r=row_hcar(hc) & c>=pos_hcar(hc) & c<pos_hcar(hc)+size_hcar(hc)} CONSTANTS vcars,hcars,dim, col_vcar, row_hcar, size_vcar, size_hcar, red_hcar PROPERTIES /* The particular puzzle */ STATIC_PROPS & dim = 6 & vcars : NATURAL1 & hcars: NATURAL1 & col_vcar: 1..vcars --> INDEX & row_hcar: 1..hcars --> INDEX & size_vcar: 1..vcars --> INDEX & size_hcar: 1..hcars --> INDEX & red_hcar : 1..hcars & /* vcars are in ascending in row order */ !r.(r:1..(vcars-1) => col_vcar(r)<=col_vcar(r+1)) & /* hcars are in ascending in col order */ !c.(c:1..(hcars-1) => row_hcar(c)<=row_hcar(c+1)) VARIABLES pos_vcar, pos_hcar INVARIANT pos_vcar: 1..vcars --> INDEX & pos_hcar: 1..hcars --> INDEX ASSERTIONS !(vc,hc).(vc:1..vcars & hc:1..hcars => POSs_VCAR(vc) /\ POSs_HCAR(hc) = {}); !(vc1,vc2).(vc1:1..(vcars-1) & vc2:2..vcars & vc1<vc2 => POSs_VCAR(vc1) /\ POSs_VCAR(vc2) = {}); !(hc1,hc2).(hc1:1..(hcars-1) & hc2:2..hcars & hc1<hc2 => POSs_HCAR(hc1) /\ POSs_HCAR(hc2) = {}) INITIALISATION pos_vcar := INIT_VCAR || pos_hcar := INIT_HCAR OPERATIONS move_hcar_right(car) = PRE car:1..hcars & pos_hcar(car)<=dim - size_hcar(car) & /* car not at extreme right */ (car<hcars => (row_hcar(car) /= row_hcar(car+1) or pos_hcar(car+1) > pos_hcar(car)+size_hcar(car))) & !cv.(cv:1..vcars & col_vcar(cv)=pos_hcar(car)+size_hcar(car) => row_hcar(car) /: pos_vcar(cv)..pos_vcar(cv)+size_vcar(cv)-1) THEN pos_hcar(car) := pos_hcar(car)+1 END; move_hcar_left(car) = PRE car:1..hcars & pos_hcar(car)> 1 & /* car not at extreme left */ (car>1 => (row_hcar(car) /= row_hcar(car-1) or pos_hcar(car-1)+size_hcar(car-1) <= pos_hcar(car)-1))& !cv.(cv:1..vcars & col_vcar(cv)=pos_hcar(car)-1 => row_hcar(car) /: pos_vcar(cv)..pos_vcar(cv)+size_vcar(cv)-1) THEN pos_hcar(car) := pos_hcar(car)-1 END; move_vcar_down(car) = PRE car:1..vcars & pos_vcar(car)<=dim - size_vcar(car) & /* car not at extreme bottom */ (car<vcars => (col_vcar(car) /= col_vcar(car+1) or pos_vcar(car+1) > pos_vcar(car)+size_vcar(car))) & !cv.(cv:1..hcars & row_hcar(cv)=pos_vcar(car)+size_vcar(car) => col_vcar(car) /: pos_hcar(cv)..pos_hcar(cv)+size_hcar(cv)-1) THEN pos_vcar(car) := pos_vcar(car)+1 END; move_vcar_up(car) = PRE car:1..vcars & pos_vcar(car)> 1 & /* car not at extreme top */ (car>1 => (col_vcar(car) /= col_vcar(car-1) or pos_vcar(car-1)+size_vcar(car-1) <= pos_vcar(car)-1)) & !cv.(cv:1..hcars & row_hcar(cv)=pos_vcar(car)-1 => col_vcar(car) /: pos_hcar(cv)..pos_hcar(cv)+size_hcar(cv)-1) THEN pos_vcar(car) := pos_vcar(car)-1 END END
The encoding of hardest puzzle Nr 40 in the file RushHour/Puzzle40.def is as follows:
DEFINITIONS /* The particular puzzle (nr. 40) */ STATIC_PROPS == (vcars=7 & hcars = 6 & col_vcar = {1|->1, 2|->2, 3|->3, 4|->3, 5|->4, 6|->5, 7|->6} & size_vcar = {1|->3, 2|->2, 3|->2, 4|->2, 5|->2, 6|->2, 7|->3} & row_hcar = {1|->1, 2|->3, 3|->4, 4|->5, 5|->6, 6|->6} & size_hcar = {1|->2, 2|->2, 3|->3, 4|->2, 5|->2, 6|->2} & red_hcar = 2); /* red hcar */ INIT_VCAR == {1|->1, 2|->2, 3|->2, 4|->5, 5|->4, 6|->1, 7|->2 }; INIT_HCAR == {1|->2, 2|->4, 3|->1, 4|->5, 5|->1, 6|->4}
ProB 1.3.7 took about 26 seconds to solve this puzzle (on my Mac Book Air 1.8 GHz i7; runtimes may vary as ProB uses a randomized depth-first/breadth-first search):
The solution found has 125 steps:
SETUP_CONSTANTS(6,7,6,[1,2,3,3,4,5,6],[1,3,4,5,6,6],[3,2,2,2,2,2,3],[2,2,3,2,2,2],2) INITIALISATION([1,2,2,5,4,1,2],[2,4,1,5,1,4]) move_hcar_right(6) move_vcar_down(5) move_hcar_right(3) move_vcar_down(1) move_vcar_up(7) move_hcar_left(1) move_vcar_down(1) move_hcar_right(3) move_vcar_down(2) move_hcar_right(3) move_vcar_down(2) move_vcar_up(4) move_vcar_up(3) move_hcar_right(5) move_vcar_down(1) move_hcar_left(2) move_vcar_down(6) move_hcar_left(2) move_hcar_left(2) move_vcar_down(3) move_hcar_right(1) move_hcar_right(1) move_hcar_right(1) move_vcar_up(3) move_hcar_right(2) move_vcar_up(1) move_vcar_up(1) move_vcar_up(1) move_hcar_right(2) move_vcar_up(2) move_vcar_up(2) move_hcar_left(5) move_vcar_down(4) move_vcar_up(2) move_hcar_left(3) move_hcar_left(3) move_hcar_left(3) move_hcar_left(2) move_vcar_up(5) move_vcar_up(5) move_vcar_up(5) move_vcar_down(7) move_hcar_right(1) move_hcar_right(3) move_vcar_up(5) move_hcar_right(2) move_vcar_down(1) move_vcar_down(2) move_hcar_right(3) move_vcar_down(2) move_vcar_down(2) move_hcar_left(2) move_vcar_down(5) move_vcar_down(1) move_hcar_left(1) move_vcar_up(7) move_hcar_right(3) move_vcar_up(4) move_hcar_right(5) move_vcar_down(1) move_hcar_left(2) move_vcar_down(3) move_hcar_left(1) move_hcar_left(1) move_hcar_left(1) move_vcar_up(3) move_hcar_right(2) move_vcar_up(1) move_hcar_left(5) move_hcar_left(4) move_vcar_up(5) move_vcar_down(4) move_hcar_right(2) move_vcar_up(2) move_vcar_up(6) move_hcar_right(2) move_vcar_up(1) move_vcar_up(4) move_vcar_up(4) move_vcar_down(2) move_vcar_down(1) move_vcar_down(4) move_vcar_down(3) move_vcar_up(2) move_vcar_up(2) move_hcar_left(6) move_hcar_right(1) move_vcar_up(1) move_vcar_up(1) move_vcar_down(4) move_vcar_down(3) move_vcar_down(2) move_vcar_down(2) move_vcar_up(3) move_vcar_up(4) move_vcar_down(1) move_vcar_down(1) move_vcar_down(4) move_vcar_up(2) move_vcar_up(1) move_hcar_left(3) move_vcar_up(2) move_vcar_down(7) move_vcar_up(1) move_vcar_down(7) move_vcar_down(7) move_vcar_down(2) move_vcar_down(2) move_vcar_up(7) move_vcar_up(7) move_hcar_right(6) move_vcar_up(7) move_vcar_up(2) move_vcar_up(2) move_hcar_left(3) move_vcar_down(7) move_vcar_down(7) move_vcar_down(1) move_vcar_down(1) move_hcar_left(6) move_vcar_down(7) move_vcar_up(1) move_hcar_right(2)
Using our translator to TLA+ we can solve an adapted version of the above model in 11 seconds plus the time for the translation and starting up the translator and TLC (a few seconds). (The model has to be rewritten slightly for TLC, as it's enumeration and constraint solving capabilities are more limited.)
Here is the slightly rewritten version which works with TLC (in addition to ProB):
MACHINE RushHour_TLC /* not a very elegant model; but it seems to work */ /* ProB finds a solution for the hardest puzzle (no. 40) */ DEFINITIONS SET_PREF_MAXINT == 8; /*"RushHour/Puzzle40.def"; */ STATIC_PROPS == (vcars=7 & hcars = 6 & col_vcar = {1|->1, 2|->2, 3|->3, 4|->3, 5|->4, 6|->5, 7|->6} & size_vcar = {1|->3, 2|->2, 3|->2, 4|->2, 5|->2, 6|->2, 7|->3} & row_hcar = {1|->1, 2|->3, 3|->4, 4|->5, 5|->6, 6|->6} & size_hcar = {1|->2, 2|->2, 3|->3, 4|->2, 5|->2, 6|->2} & red_hcar = 2); /* red hcar */ INIT_VCAR == {1|->1, 2|->2, 3|->2, 4|->5, 5|->4, 6|->1, 7|->2 }; INIT_HCAR == {1|->2, 2|->4, 3|->1, 4|->5, 5|->1, 6|->4}; INDEX == (1..dim); GOAL == (pos_hcar(red_hcar) >= dim-size_hcar(red_hcar)+1); HEURISTIC_FUNCTION == dim-size_hcar(red_hcar) - pos_hcar(red_hcar) ; /* not a very interesting heuristic function; as red_car can only be moved at very last step */ ANIMATION_IMG0 == "images/sm_empty_box.gif"; ANIMATION_IMG1 == "images/sm_vcar.gif"; ANIMATION_IMG2 == "images/sm_vcar_front.gif"; ANIMATION_IMG3 == "images/sm_hcar.gif"; ANIMATION_IMG4 == "images/sm_red_hcar.gif"; ANIMATION_FUNCTION == ( {r,c,i|r:1..dim & c:1..dim & i=0} <+ {r,c,i|r:1..dim & c:1..dim & i=1 & #j.(j:dom(col_vcar) & c=col_vcar(j) & r>pos_vcar(j) & r<pos_vcar(j)+size_vcar(j)) } <+ {r,c,i|r:1..dim & c:1..dim & i=2 & #j.(j:dom(col_vcar) & c=col_vcar(j) & r=pos_vcar(j)) } <+ {r,c,i|r:1..dim & c:1..dim & i:3..4 & #j.(j:dom(row_hcar) & r=row_hcar(j) & c>=pos_hcar(j) & c<pos_hcar(j)+size_hcar(j) & ((j=red_hcar & i=4) or (j/=red_hcar & i=3)) ) } ); POSs_VCAR(vc) == {c,r|c=col_vcar(vc) & r : pos_vcar(vc)..(pos_vcar(vc)+size_vcar(vc))-1}; /* r>=pos_vcar(vc) & r<pos_vcar(vc)+size_vcar(vc) */ POSs_HCAR(hc) == {c,r|r=row_hcar(hc) & c : pos_hcar(hc) ..(pos_hcar(hc)+size_hcar(hc))-1} /* c>=pos_hcar(hc) & c<pos_hcar(hc)+size_hcar(hc) */ CONSTANTS vcars,hcars,dim, col_vcar, row_hcar, size_vcar, size_hcar, red_hcar PROPERTIES /* The particular puzzle */ STATIC_PROPS & dim = 6 & vcars : NATURAL1 & hcars: NATURAL1 & col_vcar: 1..vcars --> INDEX & row_hcar: 1..hcars --> INDEX & size_vcar: 1..vcars --> INDEX & size_hcar: 1..hcars --> INDEX & red_hcar : 1..hcars & /* vcars are in ascending in row order */ !r.(r:1..(vcars-1) => col_vcar(r)<=col_vcar(r+1)) & /* hcars are in ascending in col order */ !c.(c:1..(hcars-1) => row_hcar(c)<=row_hcar(c+1)) VARIABLES pos_vcar, pos_hcar INVARIANT pos_vcar: 1..vcars --> INDEX & pos_hcar: 1..hcars --> INDEX ASSERTIONS !(vc,hc).(vc:1..vcars & hc:1..hcars => POSs_VCAR(vc) /\ POSs_HCAR(hc) = {}); !(vc1,vc2).(vc1:1..(vcars-1) & vc2:2..vcars & vc1<vc2 => POSs_VCAR(vc1) /\ POSs_VCAR(vc2) = {}); !(hc1,hc2).(hc1:1..(hcars-1) & hc2:2..hcars & hc1<hc2 => POSs_HCAR(hc1) /\ POSs_HCAR(hc2) = {}) INITIALISATION pos_vcar := INIT_VCAR || pos_hcar := INIT_HCAR OPERATIONS move_hcar_right(car) = PRE car:1..hcars & pos_hcar(car)<=dim - size_hcar(car) & /* car not at extreme right */ (car<hcars => (row_hcar(car) /= row_hcar(car+1) or pos_hcar(car+1) > pos_hcar(car)+size_hcar(car))) & !cv.(cv:1..vcars & col_vcar(cv)=pos_hcar(car)+size_hcar(car) => row_hcar(car) /: pos_vcar(cv)..pos_vcar(cv)+size_vcar(cv)-1) THEN pos_hcar(car) := pos_hcar(car)+1 END; move_hcar_left(car) = PRE car:1..hcars & pos_hcar(car)> 1 & /* car not at extreme left */ (car>1 => (row_hcar(car) /= row_hcar(car-1) or pos_hcar(car-1)+size_hcar(car-1) <= pos_hcar(car)-1))& !cv.(cv:1..vcars & col_vcar(cv)=pos_hcar(car)-1 => row_hcar(car) /: pos_vcar(cv)..pos_vcar(cv)+size_vcar(cv)-1) THEN pos_hcar(car) := pos_hcar(car)-1 END; move_vcar_down(car) = PRE car:1..vcars & pos_vcar(car)<=dim - size_vcar(car) & /* car not at extreme bottom */ (car<vcars => (col_vcar(car) /= col_vcar(car+1) or pos_vcar(car+1) > pos_vcar(car)+size_vcar(car))) & !cv.(cv:1..hcars & row_hcar(cv)=pos_vcar(car)+size_vcar(car) => col_vcar(car) /: pos_hcar(cv)..pos_hcar(cv)+size_hcar(cv)-1) THEN pos_vcar(car) := pos_vcar(car)+1 END; move_vcar_up(car) = PRE car:1..vcars & pos_vcar(car)> 1 & /* car not at extreme top */ (car>1 => (col_vcar(car) /= col_vcar(car-1) or pos_vcar(car-1)+size_vcar(car-1) <= pos_vcar(car)-1)) & !cv.(cv:1..hcars & row_hcar(cv)=pos_vcar(car)-1 => col_vcar(car) /: pos_hcar(cv)..pos_hcar(cv)+size_hcar(cv)-1) THEN pos_vcar(car) := pos_vcar(car)-1 END END