From 57996dda796c79396999b3a9ba29d9dc08c5d5db Mon Sep 17 00:00:00 2001 From: pimjager Date: Thu, 16 Jun 2016 13:58:20 +0200 Subject: [PATCH] assignment2 --- exam.tex | 1 + second.tex | 44 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+) diff --git a/exam.tex b/exam.tex index 331d5d9..0b961f1 100644 --- a/exam.tex +++ b/exam.tex @@ -5,6 +5,7 @@ \usepackage{url} \newcommand{\UPPAAL}{\textsc{UPPAAL}} +\let\tt\texttt \graphicspath{{img/}} \DeclareGraphicsExtensions{.eps} diff --git a/second.tex b/second.tex index 7422751..6a7deb2 100644 --- a/second.tex +++ b/second.tex @@ -7,4 +7,48 @@ 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}{l | r r } + \hline + intermediate & ±5 seconds & 78 mb\\ + hard & ±0.1 seconds & 50 mb\\ + website 1 & \multicolumn{2}{c}{Not solvable}\\ + website 2 & ±0.2 seconds & 50 mb\\ + \hline +\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. \ No newline at end of file -- 2.20.1