From def489dbcf463db0afe0b1db8f9379bf88516294 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Mon, 30 Nov 2015 18:04:30 +0100 Subject: [PATCH] added proof bit --- mbt_exercises/mbt.tex | 81 ++++++++++++++++++++++++++++++------------- mbt_exercises/pre.tex | 3 +- 2 files changed, 59 insertions(+), 25 deletions(-) diff --git a/mbt_exercises/mbt.tex b/mbt_exercises/mbt.tex index 18857c5..8efa296 100644 --- a/mbt_exercises/mbt.tex +++ b/mbt_exercises/mbt.tex @@ -97,42 +97,75 @@ \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_2 & 0 & 1 & 0 & 0\cr + P_3 & 0 & 0 & 1 & 0\cr P_4 & 0 & 0 & 1 & 1\cr }$ \item - $P_1=\xymatrix{ + $P_1=\xymatrix@C=1pc@R=1pc{ \ar[dr]&\\ - & s_0\ar[d]^a\\ - & s_1\ar[d]^b\\ - & s_2\ar[d]^c\\ - & s_3\\ + & *+[o][F-]{s_0}\ar[d]^a\\ + & *+[o][F-]{s_1}\ar[d]^b\\ + & *+[o][F-]{s_2}\ar[d]^c\\ + & *+[o][F-]{s_3}\\ }$ - $P_2=\xymatrix{ + $P_2=\xymatrix@C=1pc@R=1pc{ \ar[dr]&\\ - & s_0\ar[d]^a\\ - & s_1\ar[d]^b\\ - & s_2\ar[dl]^c\ar[dr]^d\\ - s_3 & & s_4\\ + & *+[o][F-]{s_0}\ar[d]^a\\ + & *+[o][F-]{s_1}\ar[d]^b\\ + & *+[o][F-]{s_2}\ar[dl]_c\ar[dr]^d\\ + *+[o][F-]{s_3} & & *+[o][F-]{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_3=\xymatrix@C=1pc@R=1pc{ + \ar[dr] &\\ + & *+[o][F-]{s_0}\ar[d]^a\\ + & *+[o][F-]{s_1}\ar[dl]_b\ar[dr]^b\\ + *+[o][F-]{s_2}\ar[d]^c & & *+[o][F-]{s_3}\ar[d]^d\\ + *+[o][F-]{s_4} & & *+[o][F-]{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 + $P_4=\xymatrix@C=1pc@R=1pc{ + \ar[dr] &\\ + & *+[o][F-]{s_0}\ar[dl]_a\ar[dr]^a\\ + *+[o][F-]{s_2}\ar[d]^b & & *+[o][F-]{s_3}\ar[d]^b\\ + *+[o][F-]{s_4}\ar[d]^c & & *+[o][F-]{s_5}\ar[d]^d\\ + *+[o][F-]{s_6} & & *+[o][F-]{s_7} }$ \end{enumerate} \subsection{Testing equivalences} +\begin{enumerate}[a)] + \item + \begin{align*} + \sigma\in traces(p)\leftrightarrow + p\text{ \bf after }\sigma\text{ \bf refuses }\emptyset\\ + \sigma\in traces(p)\leftrightarrow + \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in + \emptyset:p'\cancel{\overset{a}{\rightarrow}} & & 2.\\ + \sigma\in traces(p)\leftrightarrow + \exists p':p\overset{\sigma}{\Rightarrow}p'\\ + \sigma\in \{\sigma\in L^*|p\overset{\sigma}{\Rightarrow}\}\leftrightarrow + \exists p':p\overset{\sigma}{\Rightarrow}p'& & \square\\ + \end{align*} + \item + \begin{align*} + p\text{ \bf after }\sigma\text{ \bf refuses } A\leftrightarrow + \sigma\cdot A\in Ftraces(p)\\ + \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in + A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow + \sigma\cdot A\in Ftraces(p) & & 2.\\ + \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in + A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow + \sigma\cdot A\in \{\psi\in(L\cup + \mathcal{P}(L))^*|p\overset{\sigma}{\Rightarrow}\} & & 4.\\ + \end{align*} + \item + \begin{align*} + \end{align*} + \item + \begin{align*} + \end{align*} +\end{enumerate} + \subsection{Testing equivalences} \subsection{Testing equivalences} diff --git a/mbt_exercises/pre.tex b/mbt_exercises/pre.tex index 59d2e91..723347a 100644 --- a/mbt_exercises/pre.tex +++ b/mbt_exercises/pre.tex @@ -1,7 +1,8 @@ -\documentclass{article} +\documentclass[twocolumn]{article} \usepackage{enumerate} \usepackage{amssymb} +\usepackage{cancel} \usepackage{amsmath} \usepackage{a4wide} \usepackage{xypic} -- 2.20.1