Merge branch 'master' of gitlab.science.ru.nl:mlubbers/mc1516the
[mc1516the.git] / third.tex
index 5050d31..7bb7a3b 100644 (file)
--- a/third.tex
+++ b/third.tex
@@ -13,33 +13,33 @@ 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?}
+\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]
+\begin{figure}[ht]
        \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.