second.tex

   1 \emph{Rush Hour is a puzzle where on a $6\times6$ board trucks and cars are
   2 placed in an initial position. The goal is to move the vehicles forward and
   3 backward in such a way that the red car can leave the board at the exit on the
   4 right. Here you see a picture: and here you find more information, including
   5 the possibility to play online: \url{http://thinkfun.com/products/rush-hour/}}
   6
   7 \emph{Model the game in UPPAAL model and show how to find solutions. Make sure
   8 you can solve at least the following positions:}
   9
  10 \subsection*{Model}
  11
  12 Our model can be found in \tt{2.xml} and traces for solving the intermediate
  13 puzzle, the hard puzzle and the second puzzle from the provided website can be
  14 found in \tt{2intermediateTrace.xtr, 2hardTrace.xtr} and
  15 \tt{2website2Trace.xtr} respectively.
  16
  17 Our model is centered around a global state \tt{bool grid[6][6]} which tracks
  18 for each square if part of a car is on it or not. There is a player which
  19 starts the game and stops the game when the red car is at the exit. The player
  20 starts the game if all cars have registered their presence on the grid.
  21
  22 Cars are modeled as either vertical or horizontal variants. Both behave exactly
  23 the same, apart from the obvious difference that horizontal cars move along the
  24 x-axis, while vertical cars move along the y-axis. From their start state cars
  25 first register themselves on the grid and sync on a \tt{reg!}.
  26 Figure~\ref{fig:car} shows the \UPPAAL{} model of a vertical car. The player
  27 (Figure~\ref{fig:player})
  28 counts the \tt{reg}s and broadcasts \tt{start!} as all cars have registered.
  29 Cars then non-deterministically move either up/right or down/left.
  30
  31 The red car is a special case of a horizontal car, which always runs on the
  32 fourth row and syncs \tt{finish!} when it is at the exit.
  33
  34 \begin{figure}[h]
  35         \centering
  36         \includegraphics[width=.5\linewidth]{2vertCar}
  37         \caption{Modeling a vertical car in UPPAAL}\label{fig:car}
  38 \end{figure}
  39
  40 \begin{figure}[h]
  41         \centering
  42         \includegraphics[width=.5\linewidth]{2player}
  43         \caption{Modeling the player in UPPAAL}\label{fig:player}
  44 \end{figure}
  45
  46 \subsection*{Results}
  47 Our model is quite fast in solving the provided puzzles. It can solve the
  48 intermediate and hard puzzles from the exercise and the second puzzle from the
  49 website, the first puzzle however can not be solved by our model.
  50
  51 \begin{tabular}{lrr}
  52         \toprule
  53         puzzle & time & memory\\
  54         \midrule
  55         intermediate    & $\pm5$ seconds & $78$ mb\\
  56         hard                    & $\pm0.1$ seconds & $50$ mb\\
  57         website 1               & \multicolumn{2}{c}{Not solvable}\\
  58         website 2               & $\pm0.2$ seconds & $50$ mb\\
  59         \bottomrule
  60 \end{tabular}
  61
  62 It might seem unexpected that the intermediate result runs (considerably)
  63 slower than the two harder challenges. The exact reason for this is unknown to
  64 us, however it might be because the intermediate challenge has considerably
  65 more cars than the other two challenges (13 vs. 7 and 9). This means that the
  66 state space of possible moves and possible car positions is much larger in the
  67 the intermediate example. Since in our model cars move non-deterministically,
  68 the intermediate challenge has a lot more possible moves.