From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 21 Jun 2016 18:35:23 +0000 (+0200)
Subject: 1b misschien
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=f35657b9be8245e8998b309110827a3b47b55a1f;p=mc1516the.git

1b misschien
---

diff --git a/exam.tex b/exam.tex
index 71bd941..6ef77e8 100644
--- a/exam.tex
+++ b/exam.tex
@@ -4,6 +4,7 @@
 \usepackage{geometry}
 \usepackage{graphicx}
 \usepackage{url}
+\usepackage{amsmath}
 
 \newcommand{\UPPAAL}{\textsc{UPPAAL}}
 \let\tt\texttt
diff --git a/first.tex b/first.tex
index 81f4f3a..0a9cd85 100644
--- a/first.tex
+++ b/first.tex
@@ -12,10 +12,26 @@ leaving the gate.}
 
 \subsection*{1.b}
 \emph{Consider the timed automaton in figure 1 of the paper ”Timed Automata” by
-Rajeev Alur. Suppose initially we have a zone $(s0, [0 \leq x \leq 4, 0 \leq y
+Rajeev Alur. Suppose initially we have a zone $(s0, [0\leq x\leq 4, 0\leq y
 \leq 3])$. Give the zone after a sequence a.b and show the intermediate steps
 in the derivation.}
 
+We define:\\
+$e_0=\langle s_0, a, [], [x:=0] s_1\rangle$ and\\
+$e_1=\langle s_1, a, [], [y:=0] s_2\rangle$\\
+
+And we derive:\\
+\begin{align*}
+	succ(e_1, succ(e_0, [0\leq x\leq 4, 0\leq y])) =&
+		succ(e_1, ((([0\leq x\leq 4, 0\leq y]\wedge [])\Uparrow)\wedge []\wedge [x<1])[x:=0])\\
+	=& succ(e_1, (([0\leq x\leq 4, 0\leq y]\Uparrow)\wedge []\wedge [x<1])[x:=0])\\
+	=& succ(e_1, ([0\leq x<1, 0\leq y])[x:=0])\\
+	=& succ(e_1, [x=1, 0\leq y][x:=0])\\
+	=& ((([x=1, 0\leq y]\wedge [x<1])\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
+	=& (([x=1, 0\leq y]\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
+	=& [x<1, y=0]
+\end{align*}
+
 \subsection*{1.c}
 \emph{Consider the timed automaton in figure 1 of the paper \emph{Timed
 Automata} by Rajeev Alur. Give the zone automaton of the timed automaton, with