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 of the original game Nr. 40.
Inspired by discussions with Neng-Fa Zhou at ICLP'14 in Vienna, we now have a new version of the B model for this puzzle.
The old version can still be found below. There is also a Prolog XTL encoding of the same problem available, where ProB finds the example in one second or less. Explanations and comparison with the Picat solution will follow soon.
As we show below, the shortest solution can be found very quickly using our new feature to use TLC for model checking B specifications (about 1 second model checking time; rest of time needed to replay counter example).
First, here is the B model of the Rush Hour puzzle:
MACHINE RushHour /* 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 by adding the c:1..red guards: 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
To find a solution you need to run the ProB "Model Check" command in the "Verify" menu. Be sure to enable the "Find GOAL (from DEFINITIONS)" checkbox, as above we have specified the target state col(red) = 4 inside the GOAL definition.
Here is a screenshot of ProB after finding the shortest solution using model checking. As you can see there is also a (simple) graphical visualisation of the state of the model. We have also opened the "Evaluation View".
You can inspect or export the solution trace found by ProB in various ways:
Note: you can also find the solution from the command line using probcli: probcli -mc 10000 RushHour.mch. The command line version probcli will output the trace on the console, but also provides various commands to save the history to file.
If you want to find the shortest solution with ProB you should set the "Search Strategy" in the ProB "Model Check" command to "Breadth First". 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).
You can also use ou It was found in 3 seconds (about 1 second model checking time) using our TLC model checking backend on a Mac Book Air 1.7 GHz i7:
Note; without invariant checking the overall TLC runtime goes down to 2 seconds. Note that we had to add the predicates c:1..red to the guards, as otherwise TLC cannot reduce the domain c to a finite domain. ProB itself has no issue with this, but ProB is slower (about 10 seconds to find a solution trace).
Here is the solution as obtained when saving 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))
The full state space has 4782 states (including the root node and the set-up-constants node) and 29890 transitions, as indicated by ProB's coverage info (after doing full model checking without looking for states satisfying the GOAL predicate):
STATES deadlocked:0 invariant_violated:0 invariant_not_checked:0 open:0 live:4782 total:4782 TOTAL_OPERATIONS 29890 COVERED_OPERATIONS INITIALISATION:1 SETUP_CONSTANTS:1 mv_down:8461 mv_left:6483 mv_right:6483 mv_up:8461 UNCOVERED_OPERATIONS
For reference, here are the statistics as output by TLC (when not looking for states satisfying the goal predicate):
TLC2 Version 2.05 of 23 July 2013 Running in Model-Checking mode. Parsing file /Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour_v2_TLC.tla ... Semantic processing of module RushHour_v2_TLC Starting... (2014-07-23 12:28:17) Computing initial states... Finished computing initial states: 1 distinct state generated. Model checking completed. No error has been found. Estimates of the probability that TLC did not check all reachable states because two distinct states had the same fingerprint: calculated (optimistic): val = 6.5E-12 based on the actual fingerprints: val = 8.0E-13 29889 states generated, 4780 distinct states found, 0 states left on queue. The depth of the complete state graph search is 123. Finished. (2014-07-23 12:28:21) -------------------------------- Parsing time: 644 ms Translation time: 107 ms Model checking time: 3 sec States analysed: 4780 Transitions fired: 29889 Result: NoError
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