-\emph{Rush Hour is a puzzle where on a 6x6 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{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}
+\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 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.
+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.
+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.
+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
+\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
+\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
+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
+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.
Initial temperature is 102 degrees. The objective is to keep the temperature
between 102 and 110 degrees. If the temperature is going up to 110 degrees but
no rod is yet available, the system goes into a state Overheating.}
+
\subsection*{3.a}
-\emph{Specify the system in \UPPAAL. Show that unfortunately it may reach state
-\texttt{Overheating}. What is the chance this happens within 100 time units?}
+\emph{Specify the system in \UPPAAL{}. Show that unfortunately it may reach
+state \tt{Overheating}. What is the chance this happens within 100 time units?}
Figure~\ref{fig:uppaal3} shows our \UPPAAL{} specification of the vessel and
-rods. It is also included in \tt{3.xml}.
-Here \tt{t, r1} and \tt{r2} are simple \tt{clock}s tracking the
-temperature and idle times for rod1 and rod2. When querying for
-\tt{Pr [<=100] (<> v.overheating)} \UPPAAL{} gives a probability interval of
-$[0.0486043,0.148433]$ with a confidence of 0.95. The chance of overheating
-in 100 time units thus lies between ±0\% and ±1\%.
+rods. It is also included in \tt{3.xml}. Here \tt{t, r1} and \tt{r2} are
+simple \tt{clock}s tracking the temperature and idle times for rod1 and rod2.
+When querying for \tt{Pr [<=100] (<> v.overheating)} \UPPAAL{} gives a
+probability interval of $[0.0486043,0.148433]$ with a confidence of $0.95$. The
+chance of overheating in 100 time units thus lies between $\pm0\%$ and
+$\pm1\%$.
\begin{figure}[h]
\centering
\includegraphics[width=.8\linewidth]{3}
- \label{fig:uppaal3}
- \caption{Modeling vessel and rods in \UPPAAL{}}
+ \caption{Modeling vessel and rods in \UPPAAL}\label{fig:uppaal3}
\end{figure}
\subsection*{3.b}
-\emph{Someone forwards the idea that the fact that the \texttt{Overheating}
+\emph{Someone forwards the idea that the fact that the \tt{Overheating}
state can be reached is due to rod2 cooling too well, and proposes to replace
rod2 by a rod that is similar to rod1. What do you think of this idea?}
At first this idea appears to make sense. If rod2 cools too well then rod1 does
-not have time to recover when rod2 is done cooling. When we replace rod2 with a
+not have time to recover when rod2 is done cooling. When we replace rod2 with a
rod which has the same cooling constant ($T'=0.1T − 11.2$) as rod1 in the model
then running the same query returns an interval of $[0,0.0973938]$, so chances
appear to have decreased a bit, but there still is a considerable chance of
-overheating.
\ No newline at end of file
+overheating.
repositories / mc1516the.git / commitdiff