From 59609544e15404436a49649e1cf6b8c363f6867e Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Mon, 30 Nov 2015 16:30:29 +0100 Subject: [PATCH] initial commit, started with the exercises --- .gitignore | 4 ++ mbt_exercises/Makefile | 19 ++++++ mbt_exercises/mbt.tex | 139 +++++++++++++++++++++++++++++++++++++++++ mbt_exercises/pre.tex | 9 +++ 4 files changed, 171 insertions(+) create mode 100644 .gitignore create mode 100644 mbt_exercises/Makefile create mode 100644 mbt_exercises/mbt.tex create mode 100644 mbt_exercises/pre.tex 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} -- 2.20.1