+\emph{Rush Hour is a puzzle where on a $6\times6$ board trucks and cars are
+placed in an initial position. The goal is to move the vehicles forward and
+backward in such a way that the red car can leave the board at the exit on the
+right. Here you see a picture: and here you find more information, including
+the possibility to play online: \url{http://thinkfun.com/products/rush-hour/}}
+
+\emph{Model the game in UPPAAL model and show how to find solutions. Make sure
+you can solve at least the following positions:}
+
+\subsection*{Model}
+
+Our model can be found in \tt{2.xml} and traces for solving the intermediate
+puzzle, the hard puzzle and the second puzzle from the provided website can be
+found in \tt{2intermediateTrace.xtr, 2hardTrace.xtr} and
+\tt{2website2Trace.xtr} respectively.
+
+Our model is centered around a global state \tt{bool grid[6][6]} which tracks
+for each square if part of a car is on it or not. There is a player which
+starts the game and stops the game when the red car is at the exit. The player
+starts the game if all cars have registered their presence on the grid.
+
+Cars are modeled as either vertical or horizontal variants. Both behave exactly
+the same, apart from the obvious difference that horizontal cars move along the
+x-axis, while vertical cars move along the y-axis. From their start state cars
+first register themselves on the grid and sync on a \tt{reg!}.
+Figure~\ref{fig:car} shows the \UPPAAL{} model of a vertical car. The player
+(Figure~\ref{fig:player})
+counts the \tt{reg}s and broadcasts \tt{start!} as all cars have registered.
+Cars then non-deterministically move either up/right or down/left.
+
+The red car is a special case of a horizontal car, which always runs on the
+fourth row and syncs \tt{finish!} when it is at the exit.
+
+\begin{figure}[h]
+ \centering
+ \includegraphics[width=.5\linewidth]{2vertCar}
+ \caption{Modeling a vertical car in UPPAAL}\label{fig:car}
+\end{figure}
+
+\begin{figure}[h]
+ \centering
+ \includegraphics[width=.5\linewidth]{2player}
+ \caption{Modeling the player in UPPAAL}\label{fig:player}
+\end{figure}
+
+\subsection*{Results}
+Our model is quite fast in solving the provided puzzles. It can solve the
+intermediate and hard puzzles from the exercise and the second puzzle from the
+website, the first puzzle however can not be solved by our model.
+
+\begin{tabular}{lrr}
+ \toprule
+ puzzle & time & memory\\
+ \midrule
+ intermediate & $\pm5$ seconds & $78$ mb\\
+ hard & $\pm0.1$ seconds & $50$ mb\\
+ website 1 & \multicolumn{2}{c}{Not solvable}\\
+ website 2 & $\pm0.2$ seconds & $50$ mb\\
+ \bottomrule
+\end{tabular}
+
+It might seem unexpected that the intermediate result runs (considerably)
+slower than the two harder challenges. The exact reason for this is unknown to
+us, however it might be because the intermediate challenge has considerably
+more cars than the other two challenges (13 vs. 7 and 9). This means that the
+state space of possible moves and possible car positions is much larger in the
+the intermediate example. Since in our model cars move non-deterministically,
+the intermediate challenge has a lot more possible moves.
repositories / mc1516the.git / blobdiff