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.
+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
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.
+the intermediate example. Since in our model cars move non-deterministically,
+the intermediate challenge has a lot more possible moves.