From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 30 Nov 2015 15:30:29 +0000 (+0100)
Subject: initial commit, started with the exercises
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=59609544e15404436a49649e1cf6b8c363f6867e;p=tt1516.git

initial commit, started with the exercises
---

59609544e15404436a49649e1cf6b8c363f6867e
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1c43ba2
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,4 @@
+*.fmt
+*.log
+*.aux
+*.pdf
diff --git a/mbt_exercises/Makefile b/mbt_exercises/Makefile
new file mode 100644
index 0000000..0fdd7b7
--- /dev/null
+++ b/mbt_exercises/Makefile
@@ -0,0 +1,19 @@
+LATEX:=latex
+DOCUMENT:=mbt
+
+.SECONDARY: $(DOCUMENT).fmt
+
+all: $(DOCUMENT).pdf
+
+%.pdf: %.dvi
+	dvipdfm $<
+
+%.dvi: %.tex %.fmt
+	$(LATEX) $(basename $@)
+	$(LATEX) $(basename $@)
+
+%.fmt: pre.tex
+	$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
+
+clean:
+	$(RM) -v $(addprefix $(DOCUMENT).,fmt aux bbl blg dvi log out toc pdf snm nav)
diff --git a/mbt_exercises/mbt.tex b/mbt_exercises/mbt.tex
new file mode 100644
index 0000000..18857c5
--- /dev/null
+++ b/mbt_exercises/mbt.tex
@@ -0,0 +1,139 @@
+%&mbt
+\begin{document}
+
+\section{Theory of Labelled Transition Systems}
+\subsection{Testing equivalences}
+\begin{enumerate}[a)]
+	\item $\bordermatrix{
+			~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
+			Q_1 & 1\cr
+			Q_2 & 0 & 1\cr
+			Q_3 & 0 & 0 & 1\cr
+			Q_4 & 0 & 0 & 0 & 1\cr
+			Q_5 & 0 & 0 & 0 & 0 & 1\cr
+		}$
+	\item $\bordermatrix{
+			~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
+			Q_1 & 1\cr
+			Q_2 & 0 & 1\cr
+			Q_3 & 0 & 1 & 1\cr
+			Q_4 & 0 & 1 & 1 & 1\cr
+			Q_5 & 0 & 1 & 1 & 1 & 1\cr
+		}$
+	\item $\bordermatrix{
+			~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
+			Q_1 & 1\cr
+			Q_2 & 0 & 1\cr
+			Q_3 & 0 & 1 & 1\cr
+			Q_4 & 0 & 1 & 1 & 1\cr
+			Q_5 & 0 & 1 & 1 & 1 & 1\cr
+		}$
+	\item You can discriminate $Q_1$ from all the others by running the
+		trace $a\rightarrow c$. $Q_2$ can be discriminated from the
+		rest by running $a\rightarrow b\rightarrow c$ because
+		$Q_3,Q_4$ and $Q_5$ may refuse the last $c$. To
+		discriminate $Q_3$ you can run $a\rightarrow c$ since
+		$Q_4$ and $Q_5$ may refuse $c$. To discriminate $Q_4$ you need
+		to be able to go back. You can then discriminate by running
+		$a\rightarrow c$ and then go back and run $b\rightarrow c$.
+		This trace can only be accepted by $Q_4$.
+	\item $\bordermatrix{
+			~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
+			Q_1 & 1\cr
+			Q_2 & 0 & 1\cr
+			Q_3 & 0 & 0 & 1\cr
+			Q_4 & 0 & 1 & 1 & 1\cr
+			Q_5 & 0 & 1 & 1 & 1 & 1\cr
+		}$
+	\item See $d)$.
+	\item $\bordermatrix{
+			~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
+			Q_1 & 1\cr
+			Q_2 & 0 & 1\cr
+			Q_3 & 0 & 0 & 1\cr
+			Q_4 & 0 & 0 & 0 & 1\cr
+			Q_5 & 0 & 0 & 0 & 1 & 1\cr
+		}$
+	\item All processes as explained in $d)$.
+	\item $\bordermatrix{
+			i\setminus s & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
+			Q_1 & 1 & 0 & 0 & 0 & 0\cr
+			Q_2 & 1 & 1 & 1 & 1 & 1\cr
+			Q_3 & 1 & 1 & 1 & 1 & 1\cr
+			Q_4 & 1 & 1 & 1 & 1 & 1\cr
+			Q_5 & 1 & 1 & 1 & 1 & 1\cr
+		}$
+\end{enumerate}
+
+\subsection{Testing equivalences}
+\begin{enumerate}[a)]
+	\item $\bordermatrix{
+			~ & P_1 & P_2 & P_3 & P_4\cr
+			P_1 & 1\cr
+			P_2 & 0 & 1\cr
+			P_3 & 0 & 0 & 1\cr
+			P_4 & 0 & 0 & 0 & 1\cr
+		}$
+	\item $\bordermatrix{
+			~ & P_1 & P_2 & P_3 & P_4\cr
+			P_1 & 1\cr
+			P_2 & 0 & 1\cr
+			P_3 & 0 & 1 & 1\cr
+			P_4 & 0 & 1 & 1 & 1\cr
+		}$
+	\item Trace $a\rightarrow b\rightarrow c$ may refuse in $P_3$ and $P_4$
+		but not in $P_2$. $P_3$ and $P_4$ can only be distinguished if
+		you are allowed to go back. If the trace $a\rightarrow
+		b\rightarrow c$ accepts you can go back to the state after $a$
+		and try $b\rightarrow d$. This might only accept in $P_3$.
+	\item $\bordermatrix{
+			~ & P_1 & P_2 & P_3 & P_4\cr
+			P_1 & 1\cr
+			P_2 & 0 & 1\cr
+			P_3 & 0 & 0 & 1\cr
+			P_4 & 0 & 0 & 1 & 1\cr
+		}$
+	\item All processes.
+	\item $\bordermatrix{
+			i\setminus s& P_1 & P_2 & P_3 & P_4\cr
+			P_1 & 1 & 0 & 0 & 0\cr
+			P_2 & 0 & 1 & \cr
+			P_3 & 0 & 0 & 1\cr
+			P_4 & 0 & 0 & 1 & 1\cr
+		}$
+	\item
+		$P_1=\xymatrix{
+			\ar[dr]&\\
+			       & s_0\ar[d]^a\\
+			       & s_1\ar[d]^b\\
+			       & s_2\ar[d]^c\\
+			       & s_3\\
+		}$
+		$P_2=\xymatrix{
+			\ar[dr]&\\
+			       & s_0\ar[d]^a\\
+			       & s_1\ar[d]^b\\
+			       & s_2\ar[dl]^c\ar[dr]^d\\
+			s_3    & & s_4\\
+		}$
+		$P_3=\xymatrix{
+			\ar[dr]     &\\
+			            & s_0\ar[d]^a\\
+			            & s_1\ar[dl]^b\ar[dr]^b\\
+			s_2\ar[d]^c & & s_3\ar[d]^d\\
+			s_4         & & s_5\\
+		}$
+		$P_4=\xymatrix{
+			\ar[dr]     &\\
+				    & s_0\ar[dl]^a\ar[dr]^a\\
+			s_2\ar[d]^b & & s_3\ar[d]^b\\
+			s_4\ar[d]^c & & s_5\ar[d]^d\\
+			s_6         & & s_7
+		}$
+\end{enumerate}
+
+\subsection{Testing equivalences}
+\subsection{Testing equivalences}
+\subsection{Testing equivalences}
+
+\end{document}
diff --git a/mbt_exercises/pre.tex b/mbt_exercises/pre.tex
new file mode 100644
index 0000000..59d2e91
--- /dev/null
+++ b/mbt_exercises/pre.tex
@@ -0,0 +1,9 @@
+\documentclass{article}
+
+\usepackage{enumerate}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{a4wide}
+\usepackage{xypic}
+
+\everymath{\displaystyle}