X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=second.tex;h=21dc782c168522ad0f5bed6b515a18355d68128f;hb=0ac1a13a095828aa6a69e174b569933747de3393;hp=e69de29bb2d1d6434b8b29ae775ad8c2e48c5391;hpb=971f4330c1fbd2ed86144fa066a0e122ee527efd;p=mc1516the.git

diff --git a/second.tex b/second.tex
index e69de29..21dc782 100644
--- a/second.tex
+++ b/second.tex
@@ -0,0 +1,55 @@
+\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!}. The player
+counts these \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.
+
+\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 our model does not contain any heuristics, thus
+cars move non-deterministically, the intermediate challenge has a lot more
+possible moves.