hoi

diff --git a/Makefile b/Makefile
index 6d3f8bf..487241c 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,9 +1,12 @@
 exam.pdf: exam.dvi
        dvips -f < $< | ps2pdf - > $@
 
-exam.dvi: exam.tex first.tex second.tex third.tex
+exam.dvi: exam.tex first.tex second.tex third.tex img/1c.eps
        latex $<
        latex $<
 
+img/%.eps: img/%.dot
+       dot -Teps < $< > $@
+
 clean:
        $(RM) -v $(addprefix exam.,pdf aux log dvi)

diff --git a/first.tex b/first.tex
index a5f505b..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}
@@ -21,18 +21,28 @@ $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\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*}
+\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}
+

diff --git a/img/.gitignore b/img/.gitignore
new file mode 100644 (file)
index 0000000..dd1a13b
--- /dev/null
+++ b/img/.gitignore
@@ -0,0 +1 @@
+1c.eps

diff --git a/img/1c.dot b/img/1c.dot
new file mode 100644 (file)
index 0000000..772954f
--- /dev/null
+++ b/img/1c.dot
@@ -0,0 +1,18 @@
+digraph {
+       rankdir=LR;
+       s0a [label="s0a: {x=0,y=0}"]
+       s1a [label="s1a: {x=0,y=0}"]
+       s2 [label="s2: {0<=x=1,y=0}"]
+       s3 [label="s3: {0<=x=0,y=0}"]
+
+       s0b [label="s0b: {0<=x<1,0<=y<2}"]
+       s1b [label="s1b: {x=0,0<=y<2}"]
+
+       s0a -> s1a
+       s1a -> s2
+       s2 -> s3
+
+       s3 -> s0b
+       s0b -> s1b
+       s1b -> s3
+}

diff --git a/third.tex b/third.tex
index 8642319..7bb7a3b 100644 (file)
--- a/third.tex
+++ b/third.tex
@@ -26,7 +26,7 @@ probability interval of $[0.0486043,0.148433]$ with a confidence of $0.95$. The
 chance of overheating in 100 time units thus lies between $\pm0\%$ and
 $\pm1\%$.
 
-\begin{figure}[h]
+\begin{figure}[ht]
        \centering
        \includegraphics[width=.8\linewidth]{3}
        \caption{Modeling vessel and rods in \UPPAAL}\label{fig:uppaal3}