From: pimjager <pim@pimjager.nl>
Date: Thu, 16 Jun 2016 11:58:20 +0000 (+0200)
Subject: assignment2
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=57996dda796c79396999b3a9ba29d9dc08c5d5db;p=mc1516the.git

assignment2
---

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