initial commit, started with the exercises

diff --git a/.gitignore b/.gitignore
new file mode 100644 (file)
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 (file)
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 (file)
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 (file)
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}