X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=first.tex;h=0b7b519890e31cc3fa7cece6636039117a278351;hb=c8da55aee100fb534767fa8370dc2feec8b1654b;hp=0a9cd853ef5073b38ef8d4fbb793c82e74ea7b54;hpb=f35657b9be8245e8998b309110827a3b47b55a1f;p=mc1516the.git

diff --git a/first.tex b/first.tex
index 0a9cd85..0b7b519 100644
--- 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}
@@ -17,22 +17,32 @@ Rajeev Alur. Suppose initially we have a zone $(s0, [0\leq x\leq 4, 0\leq y
 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$\\
+$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:\\
-\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*}
+\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}
+