Help

Rush Hour Puzzle

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 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. Explanations and comparison with the Picat solution will follow soon.

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). 

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

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".

ProB RushHour v2 Screenshot.png


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) using our TLC model checking backend on a Mac Book Air 1.7 GHz i7:

ProB RushHour v2 TLC Dialog.png

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 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))

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. 

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):


ProB RushHour Screenshot.png

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)


Adapted version for TLC

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.)


ProB-TLC RushHour Screenshot.png


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
Retrieved from "https://prob.hhu.de/w/index.php?title=Rush_Hour_Puzzle&oldid=2258"