From c8da55aee100fb534767fa8370dc2feec8b1654b Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 24 Jun 2016 11:11:33 +0200
Subject: [PATCH] hoi

---
 Makefile       |  5 ++++-
 first.tex      | 32 +++++++++++++++++++++-----------
 img/.gitignore |  1 +
 img/1c.dot     | 18 ++++++++++++++++++
 third.tex      |  2 +-
 5 files changed, 45 insertions(+), 13 deletions(-)
 create mode 100644 img/.gitignore
 create mode 100644 img/1c.dot

diff --git a/Makefile b/Makefile
index 6d3f8bf..487241c 100644
--- 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
--- 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
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
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
--- 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}
-- 
2.20.1