Merge branch 'master' of gitlab.science.ru.nl:mlubbers/mc1516the
[mc1516the.git] / third.tex
index e69de29..7bb7a3b 100644 (file)
--- a/third.tex
+++ b/third.tex
@@ -0,0 +1,45 @@
+\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 \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 $\pm0\%$ and
+$\pm1\%$.
+
+\begin{figure}[ht]
+       \centering
+       \includegraphics[width=.8\linewidth]{3}
+       \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 \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
+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.