(including intermediate states) of the composed system (so the product
construction of the three automata) showing a train approaching and finally
leaving the gate.}
-\includegraphics[width=\linewidth]{1a}
+\begin{figure}[h]
+ \centering
+ \includegraphics[width=.3\linewidth]{1a}
+ \caption{Timed transitions of the composed system}
+\end{figure}
\subsection*{1.b}
\emph{Consider the timed automaton in figure 1 of the paper ”Timed Automata” by
+\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{Model the game in UPPAAL model and show how to find solutions. Make sure
+you can solve at least the following positions:}
+
+
+\emph{A vessel where some chemical reaction takes place can be cooled by
+inserting two different rods, each with different cooling capacities. Only one
+rod can be inserted at a certain time. The vessel can be in three different
+states:\\
+\textbf{no rods:} then the temperature T evolves according to the differential
+equation $T'=0.1T − 10.0$.\\
+\textbf{with rod1}: equation is $T'=0.1T − 11.2$\\
+\textbf{with rod2}: equation is $T'=0.1T − 12.0$ (so rod2 cools better than
+rod1).\\
+A rod will be inserted if the temperature reaches 110 degrees. A rod that is in
+the vessel will be removed from the vessel if the temperature is between 102
+and 105 degrees. When a rod is removed, it cannot be used for 20 time units.\\
+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?}
+
+\subsection*{3.b}
+\emph{Someone forwards the idea that the fact that the \texttt{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?}