(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}
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}
+