Finished 3

[mc1516the.git] / third.tex

diff --git a/third.tex b/third.tex
index 5681ce0..5050d31 100644 (file)
--- a/third.tex
+++ b/third.tex
@@ -17,7 +17,29 @@ no rod is yet available, the system goes into a state Overheating.}
 \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?}
 
+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\%.
+
+\begin{figure}[h]
+       \centering
+       \includegraphics[width=.8\linewidth]{3}
+       \label{fig:uppaal3}
+       \caption{Modeling vessel and rods in \UPPAAL{}}
+\end{figure}
+
 \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?}
+
+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.
\ No newline at end of file