Merge branch 'master' of gitlab.science.ru.nl:mlubbers/mc1516the

[mc1516the.git] / first.tex

diff --git a/first.tex b/first.tex
index 81f4f3a..0b7b519 100644 (file)
--- a/first.tex
+++ b/first.tex
@@ -4,7 +4,7 @@
 (including intermediate states) of the composed system (so the product
 construction of the three automata) showing a train approaching and finally
 leaving the gate.}
-\begin{figure}[h]
+\begin{figure}[ht]
        \centering
        \includegraphics[width=.3\linewidth]{1a}
        \caption{Timed transitions of the composed system}
@@ -12,11 +12,37 @@ 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, \emptyset, [x:=0] s_1\rangle$ and\\
+$e_1=\langle s_1, a, \emptyset, [y:=0] s_2\rangle$\\
+
+And we derive:\\
+\scalebox{.99}{\parbox{.5\linewidth}{%
+       \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\emptyset)\Uparrow)
+                               \wedge\emptyset\wedge [x<1])[x:=0])\\
+               =& succ(e_1, (([0\leq x\leq 4, 0\leq y]\Uparrow)
+                       \wedge\emptyset\wedge [x<1])[x:=0])\\
+               =& succ(e_1, [0\leq x<1, 0\leq y][x:=0])\\
+               =& succ(e_1, [x=0, 0\leq y])\\
+               =& ((([x=0, 0\leq y]\wedge [x<1])\Uparrow)
+                       \wedge [x<1]\wedge [x<1])[y:=0]\\
+               =& (([0\leq x<1, 0\leq y]\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
+               =& [0\leq 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
 initial state $(s0, [x = 0, y = 0])$.}
+\begin{figure}[ht]
+       \centering
+       \includegraphics[width=.7\linewidth]{1c}
+       \caption{Zone automaton}
+\end{figure}
+