From 02f744ac32db57838cf238be0fbb2e5f05b70861 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 14 Jun 2016 11:10:48 +0200 Subject: [PATCH] update document --- exam.tex | 1 + first.tex | 6 +++++- second.tex | 10 ++++++++++ third.tex | 23 +++++++++++++++++++++++ 4 files changed, 39 insertions(+), 1 deletion(-) diff --git a/exam.tex b/exam.tex index 8ac1d88..331d5d9 100644 --- a/exam.tex +++ b/exam.tex @@ -2,6 +2,7 @@ \usepackage[a4paper]{geometry} \usepackage{graphicx} +\usepackage{url} \newcommand{\UPPAAL}{\textsc{UPPAAL}} diff --git a/first.tex b/first.tex index 6c231cd..81f4f3a 100644 --- a/first.tex +++ b/first.tex @@ -4,7 +4,11 @@ (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 diff --git a/second.tex b/second.tex index e69de29..7422751 100644 --- a/second.tex +++ b/second.tex @@ -0,0 +1,10 @@ +\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:} + + diff --git a/third.tex b/third.tex index e69de29..5681ce0 100644 --- a/third.tex +++ b/third.tex @@ -0,0 +1,23 @@ +\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?} -- 2.20.1