mirror of
https://github.com/2martens/uni.git
synced 2026-05-06 11:26:25 +02:00
181 lines
6.8 KiB
TeX
181 lines
6.8 KiB
TeX
\documentclass[10pt,a4paper,oneside,ngerman,numbers=noenddot]{scrartcl}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage[utf8x]{inputenc}
|
|
\usepackage[ngerman]{babel}
|
|
\usepackage{amsmath}
|
|
\usepackage{amsfonts}
|
|
\usepackage{amssymb}
|
|
\usepackage{paralist}
|
|
\usepackage{gauss}
|
|
\usepackage{pgfplots}
|
|
\usepackage[locale=DE,exponent-product=\cdot,detect-all]{siunitx}
|
|
\usepackage{tikz}
|
|
\usetikzlibrary{automata,matrix,fadings,calc,positioning,decorations.pathreplacing,arrows,decorations.markings,petri,shapes}
|
|
\usepackage{polynom}
|
|
\usepackage{multirow}
|
|
\usepackage[german]{fancyref}
|
|
\usepackage{morefloats}
|
|
\usepackage{lmerge}
|
|
\polyset{style=C, div=:,vars=x}
|
|
\pgfplotsset{compat=1.8}
|
|
\pagenumbering{arabic}
|
|
% ensures that paragraphs are separated by empty lines
|
|
\parskip 12pt plus 1pt minus 1pt
|
|
\parindent 0pt
|
|
% define how the sections are rendered
|
|
\def\thesection{13.\arabic{section})}
|
|
\def\thesubsection{\arabic{subsection}.}
|
|
\def\thesubsubsection{(\alph{subsubsection})}
|
|
% some matrix magic
|
|
\makeatletter
|
|
\renewcommand*\env@matrix[1][*\c@MaxMatrixCols c]{%
|
|
\hskip -\arraycolsep
|
|
\let\@ifnextchar\new@ifnextchar
|
|
\array{#1}}
|
|
\makeatother
|
|
|
|
\tikzset{
|
|
place/.style={
|
|
circle,
|
|
thick,
|
|
draw=black,
|
|
fill=white,
|
|
minimum size=6mm,
|
|
font=\bfseries
|
|
},
|
|
transitionH/.style={
|
|
rectangle,
|
|
thick,
|
|
draw=black,
|
|
fill=white,
|
|
minimum width=8mm,
|
|
inner ysep=4pt,
|
|
font=\bfseries
|
|
},
|
|
transitionV/.style={
|
|
rectangle,
|
|
thick,
|
|
fill=black,
|
|
minimum height=8mm,
|
|
inner xsep=2pt
|
|
}
|
|
}
|
|
|
|
\renewcommand{\vec}[1]{\underline{#1}}
|
|
|
|
\begin{document}
|
|
\author{Benjamin Kuffel, Jim Martens\\Gruppe 6}
|
|
\title{Hausaufgaben zum 26. Januar}
|
|
\maketitle
|
|
|
|
\setcounter{section}{3}
|
|
\section{} % 13.4
|
|
\subsection{}
|
|
Die Prozessgraphen für \(t_6\) und \(t_7\) befinden sich auf \fref{fig:t6-graph} bzw. \fref{fig:t7-graph}.
|
|
|
|
Es existiert dabei folgende Bisimulationsrelation: \(\mathbb{B} = \{(c, \partial_H(c)), (b \cdot c, \partial_H(b \cdot c)), (b \cdot c, \partial_H((b + b) \cdot c)), ((a + b) \leftmerge (b \cdot c), \partial_H((a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c))\}\)
|
|
\begin{figure}
|
|
\begin{tikzpicture}[node distance=1cm]
|
|
\node (t6-start) {\((a + b) \leftmerge (b \cdot c)\)};
|
|
\node (bc) [below=of t6-start] {\(b \cdot c\)};
|
|
\node (c) [below=of bc] {\(c\)};
|
|
\node (finish) [below=of c] {\(\surd\)};
|
|
|
|
\path[->] (t6-start) edge[bend right] node[left] {\(a\)} (bc)
|
|
(t6-start) edge[bend left] node[right] {\(b\)} (bc)
|
|
(bc) edge node[right] {\(b\)} (c)
|
|
(c) edge node[right] {\(c\)} (finish);
|
|
\end{tikzpicture}
|
|
\caption{Prozessgraph von \(t_6\)}
|
|
\label{fig:t6-graph}
|
|
\end{figure}
|
|
|
|
\begin{figure}
|
|
\begin{tikzpicture}[node distance=1cm]
|
|
\node (start) {\(\partial_H((a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c)\)};
|
|
\node (a-left) [below left=of start] {\(\partial_H((b + b) \cdot c)\)};
|
|
\node (de-right) [below right=of start] {\(\partial_H(b \cdot c)\)};
|
|
\node (c) [below=3 of start] {\(\partial_H(c)\)};
|
|
\node (finish) [below=of c] {\(\surd\)};
|
|
|
|
\path[->] (start) edge node[above left] {\(a\)} (a-left)
|
|
(start) edge node[above right] {\(f\)} (de-right)
|
|
(a-left) edge[bend right] node[below left] {\(b\)} (c)
|
|
(a-left) edge[bend left] node[above right] {\(b\)} (c)
|
|
(de-right) edge node[above left] {\(b\)} (c)
|
|
(c) edge node[right] {\(c\)} (finish);
|
|
\end{tikzpicture}
|
|
\caption{Prozessgraph von \(t_7\)}
|
|
\label{fig:t7-graph}
|
|
\end{figure}
|
|
|
|
\subsection{}
|
|
Nachweis des ersten Übergangs:
|
|
\begin{alignat*}{2}
|
|
&\; a \overset{a}{\rightarrow} \surd \\
|
|
T^{\surd}_{+R} &\; a + b \overset{a}{\rightarrow} \surd \\
|
|
T^{\surd}_{\leftmerge} &\; (a + b) \leftmerge b \cdot c \overset{a}{\rightarrow} b \cdot c
|
|
\end{alignat*}
|
|
|
|
Nachweis des zweiten Übergangs:
|
|
\begin{alignat*}{2}
|
|
T_{\parallel \gamma}^{\surd \surd} &&\; d \parallel e \overset{f}{\rightarrow} \surd \\
|
|
T^{\surd}_{.} &&\; (d \parallel e) \cdot b \overset{f}{\rightarrow} b \\
|
|
T_{+L} &&\; a \leftmerge (b + b) + (d \parallel e) \cdot b \overset{f}{\rightarrow} b \\
|
|
T_{.} &&\; (a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c \overset{f}{\rightarrow} b \cdot c \\
|
|
T_{\partial} &&\; \partial_H((a \leftmerge (b + b) + (d \parallel e) \cdot b) \cdot c) \overset{f}{\rightarrow} \partial_H(b \cdot c)
|
|
\end{alignat*}
|
|
|
|
\subsection{}
|
|
Die folgende Umformung wurde so weit es möglich war gezeigt.
|
|
\begin{alignat*}{2}
|
|
&& (a + b) \leftmerge (b \cdot c) \\
|
|
&\overset{LM2}{=}& (a + b) \cdot (b \cdot c) \\
|
|
&\overset{A5}{=}& ((a + b) \cdot b) \cdot c \\
|
|
&\overset{A4}{=}& (a \cdot b + b \cdot b) \cdot c \\
|
|
&\overset{LM2}{=}& (a \leftmerge b + b \cdot b) \cdot c \\
|
|
&\overset{A3}{=}& (a \leftmerge (b + b) + (b \cdot b + b \cdot b)) \cdot c \\
|
|
&\overset{LM2}{=}& (a \leftmerge (b + b) + (b \leftmerge b + b \leftmerge b)) \cdot c
|
|
\end{alignat*}
|
|
|
|
\setcounter{section}{5}
|
|
\section{} % 13.6
|
|
\subsection{}
|
|
Umformen von \(X\):
|
|
\begin{alignat*}{2}
|
|
X &=& (a + b) \cdot Y + c \cdot X \\
|
|
X &=& a \cdot Y + b \cdot Y + c \cdot X
|
|
\end{alignat*}
|
|
|
|
Umformen von \(Y\):
|
|
\begin{alignat*}{2}
|
|
Y &=& X \cdot d + e \\
|
|
Y &=& (a \cdot Y + b \cdot Y + c \cdot X) \cdot d + e
|
|
\end{alignat*}
|
|
\(Y\) lässt sich nicht in die notwendige Form überführen. Daher ist \(E\) keine geschützte rekursive Spezifikation.
|
|
|
|
\subsection{}
|
|
\begin{tikzpicture}[node distance=1cm]
|
|
\node (start) {\(\langle X|E \rangle\)};
|
|
\node (y) [right=of start] {\(\langle Y|E \rangle\)};
|
|
\node (finish) [below=of y] {\(\surd\)};
|
|
|
|
\path[->] (start) edge[bend left] node[above] {\(a\)} (y)
|
|
(start) edge[bend right] node[below] {\(b\)} (y)
|
|
(start) edge[loop left] node[left] {\(c\)} (start)
|
|
(y) edge node[right] {\(e\)} (finish)
|
|
(y) edge[loop above] node[above] {\(a\)} (y)
|
|
(y) edge[loop right] node[right] {\(b\)} (y)
|
|
(y) edge[bend left=90] node[below] {\(c\)} (start);
|
|
\end{tikzpicture}
|
|
|
|
\subsection{}
|
|
Ableiten des Übergangs:
|
|
\begin{alignat*}{2}
|
|
&\; c \overset{c}{\rightarrow} \surd \\
|
|
T^{\surd}_{.} &\; c \cdot \langle X|E \rangle \cdot d \overset{c}{\rightarrow} \langle X|E \rangle \cdot d \\
|
|
T_{X} &\; \langle X|E \rangle \cdot d \overset{c}{\rightarrow} \langle X|E \rangle \cdot d \\
|
|
T_{Y} &\; \langle Y|E \rangle \overset{c}{\rightarrow} \langle X|E \rangle \cdot d
|
|
\end{alignat*}
|
|
\end{document}
|
|
|