joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Stijl: tikz shorten transities. Indentatie

Browse source
This commit is contained in:
Joshua Moerman 2019-01-05 14:02:29 +01:00
parent 92444f1c0f
commit 1fa8596be1
8 changed files with 29 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
content/applying-automata-learning.tex
View file

@ -31,6 +31,7 @@ To the best of our knowledge, this is the first paper in which active automata l
\page \page
\noindent
Once they have high-level models of the behaviour of software components, software engineers can construct better software in less time. Once they have high-level models of the behaviour of software components, software engineers can construct better software in less time.
A key problem in practice, however, is the construction of models for existing software components, for which no or only limited documentation is available. A key problem in practice, however, is the construction of models for existing software components, for which no or only limited documentation is available.

8
content/introduction.tex
View file

@ -245,7 +245,7 @@ The intended behaviour of the records player has four states as depicted in \in{
\node[state, below of=tl, align=center] (bl) {no\\spinning}; \node[state, below of=tl, align=center] (bl) {no\\spinning};
\node[state, right of=bl, align=center] (br) {no\\spinning}; \node[state, right of=bl, align=center] (br) {no\\spinning};
\path[->] \path[trans]
(tl) edge [bend right] node [left] {\playstop} (bl) (tl) edge [bend right] node [left] {\playstop} (bl)
(tl) edge [bend right] node [below] {\spin} (tr) (tl) edge [bend right] node [below] {\spin} (tr)
(bl) edge [bend right] node [right] {\playstop} (tl) (bl) edge [bend right] node [right] {\playstop} (tl)
@ -281,7 +281,7 @@ In this example, a test suite should at least include the sequences \playstop\,\
\node[state, below of=tl, align=center] (bl) {no\\spinning}; \node[state, below of=tl, align=center] (bl) {no\\spinning};
\node[state, right of=bl, align=center] (br) {no\\spinning}; \node[state, right of=bl, align=center] (br) {no\\spinning};
\path[->] \path[trans]
(tl) edge [bend right] node [left] {\playstop} (bl) (tl) edge [bend right] node [left] {\playstop} (bl)
(tl) edge [bend right] node [below] {\spin} (tr) (tl) edge [bend right] node [below] {\spin} (tr)
(bl) edge [bend right] node [right] {\playstop} (tl) (bl) edge [bend right] node [right] {\playstop} (tl)
@ -297,7 +297,7 @@ In this example, a test suite should at least include the sequences \playstop\,\
\node[state, below of=tl, align=center] (bl) {no\\spinning}; \node[state, below of=tl, align=center] (bl) {no\\spinning};
\node[state, right of=bl, align=center] (br) {no\\spinning}; \node[state, right of=bl, align=center] (br) {no\\spinning};
\path[->] \path[trans]
(tl) edge [bend right] node [left] {\playstop} (bl) (tl) edge [bend right] node [left] {\playstop} (bl)
(tl) edge [bend right] node [below] {\spin} (tr) (tl) edge [bend right] node [below] {\spin} (tr)
(bl) edge [bend right] node [right] {\playstop} (tl) (bl) edge [bend right] node [right] {\playstop} (tl)
@ -346,7 +346,7 @@ We will only informally discuss its semantics for now.
\node[state with output,right of=0] (1) {$q_1$ \nodepart{lower} $r$}; \node[state with output,right of=0] (1) {$q_1$ \nodepart{lower} $r$};
\node[state with output,right of=1] (2) {$q_2$ \nodepart{lower} $r$}; \node[state with output,right of=1] (2) {$q_2$ \nodepart{lower} $r$};
\path[->] \path[trans]
(0) edge [loop below] node [below] {$\ast$ / \checknok} (0) edge [loop below] node [below] {$\ast$ / \checknok}
(0) edge node [above, align=center] {$\kw{sign-up}(p)$ / \checkok \\ set $r := p$} (1) (0) edge node [above, align=center] {$\kw{sign-up}(p)$ / \checkok \\ set $r := p$} (1)
(1) edge [loop below] node [below] {$\ast$ / \checknok} (1) edge [loop below] node [below] {$\ast$ / \checknok}

26
content/learning-nominal-automata.tex
View file

@ -26,7 +26,7 @@ An implementation using a recently developed Haskell library for nominal computa
\page \page
\noindent
Automata are a well established computational abstraction with a wide range of applications, including modelling and verification of (security) protocols, hardware, and software systems. Automata are a well established computational abstraction with a wide range of applications, including modelling and verification of (security) protocols, hardware, and software systems.
In an ideal world, a model would be available before a system or protocol is deployed in order to provide ample opportunity for checking important properties that must hold and only then the actual system would be synthesised from the verified model. In an ideal world, a model would be available before a system or protocol is deployed in order to provide ample opportunity for checking important properties that must hold and only then the actual system would be synthesised from the verified model.
Unfortunately, this is not at all the reality: Unfortunately, this is not at all the reality:
@ -202,7 +202,7 @@ where $q_0 = row(\epsilon) = \{ \epsilon \mapsto 0 \}$:
\stoptikzpicture}}{} \stoptikzpicture}}{}
{\hbox{\starttikzpicture {\hbox{\starttikzpicture
\node[initial,state,initial text={$\autom_1 = $}] (q0) {$q_0$}; \node[initial,state,initial text={$\autom_1 = $}] (q0) {$q_0$};
\path (q0) edge[loop right] node[right] {$a,b$} (q0); \path[trans] (q0) edge[loop right] node[right] {$a,b$} (q0);
\stoptikzpicture} \stoptikzpicture}
}{} }{}
\stopcombination} \stopcombination}
@ -264,7 +264,7 @@ The new table is closed and consistent and a new hypothesis $\autom_2$ is constr
\node[state,right of=q0] (q1) {$q_1$}; \node[state,right of=q0] (q1) {$q_1$};
\node[state,accepting,below of=q1] (q2) {$q_2$}; \node[state,accepting,below of=q1] (q2) {$q_2$};
\path[->] \path[trans]
(q0) edge[loop below] node[below] {$b$} (q0) (q0) edge[loop below] node[below] {$b$} (q0)
(q0) edge[bend right] node[above] {$a$} (q1) (q0) edge[bend right] node[above] {$a$} (q1)
(q1) edge[bend right] node[above] {$b$} (q0) (q1) edge[bend right] node[above] {$b$} (q0)
@ -337,7 +337,7 @@ The new hypothesis is $\autom_3$.
\node[state,below of=q0] (q2) {$q_2$}; \node[state,below of=q0] (q2) {$q_2$};
\node[state,accepting,right of=q2] (q3) {$q_3$}; \node[state,accepting,right of=q2] (q3) {$q_3$};
\path[->] \path[trans]
(q0) edge[bend left] node[above] {$a$} (q1) (q0) edge[bend left] node[above] {$a$} (q1)
(q1) edge[bend left] node[above] {$b$} (q0) (q1) edge[bend left] node[above] {$b$} (q0)
(q1) edge node[right] {$a$} (q3) (q1) edge node[right] {$a$} (q3)
@ -362,7 +362,7 @@ One more step brings us to the correct hypothesis $\autom_4$ (details are omitte
\node[state,accepting,right= 30pt of q0] (q3) {$q_3$}; \node[state,accepting,right= 30pt of q0] (q3) {$q_3$};
\node[state,right of=q3] (q4) {$q_4$}; \node[state,right of=q3] (q4) {$q_4$};
\path[->] \path[trans]
(q0) edge node[above left] {$a$} (q1) (q0) edge node[above left] {$a$} (q1)
(q1) edge node[above right] {$a$} (q3) (q1) edge node[above right] {$a$} (q3)
(q0) edge node[below left] {$b$} (q2) (q0) edge node[below left] {$b$} (q2)
@ -394,7 +394,7 @@ Classical theory of finite automata does not apply to this kind of languages, bu
\node[state,accepting,right of=qb] (q3) {$q_3$}; \node[state,accepting,right of=qb] (q3) {$q_3$};
\node[state,right of=q3] (q4) {$q_4$}; \node[state,right of=q3] (q4) {$q_4$};
\path[->] \path[trans]
(q0) edge node[above left] {$a$} (qa) (q0) edge node[above left] {$a$} (qa)
(qa) edge node[above right] {$a$} (q3) (qa) edge node[above right] {$a$} (q3)
(q0) edge node[above] {$b$} (qb) (q0) edge node[above] {$b$} (qb)
@ -419,7 +419,7 @@ This automaton is infinite, but it can be finitely presented in a variety of way
\node[state,right of=q3] (q4) {$q_4$}; \node[state,right of=q3] (q4) {$q_4$};
\node[above = 0pt of qx] (qa) {$\forall x \in A$}; \node[above = 0pt of qx] (qa) {$\forall x \in A$};
\path[->] \path[trans]
(q0) edge node[above] {$x$} (qx) (q0) edge node[above] {$x$} (qx)
(qx) edge node[above] {$x$} (q3) (qx) edge node[above] {$x$} (q3)
(q3) edge node[above] {$A$} (q4) (q3) edge node[above] {$A$} (q4)
@ -500,7 +500,7 @@ Then, by {\bf (P2)}, $row(\pi(a))(\epsilon) = row(a)(\epsilon) = 0$, for all $\p
\stoptikzpicture}}{} \stoptikzpicture}}{}
{\hbox{\starttikzpicture {\hbox{\starttikzpicture
\node[initial,state,initial text={$\autom'_1 = $}] (q0) {$q_0$}; \node[initial,state,initial text={$\autom'_1 = $}] (q0) {$q_0$};
\path (q0) edge[loop right] node[right] {$A$} (q0); \path[trans] (q0) edge[loop right] node[right] {$A$} (q0);
\stoptikzpicture}}{} \stoptikzpicture}}{}
\stopcombination} \stopcombination}
@ -576,7 +576,7 @@ The hypothesis automaton is
\node[state,accepting,right of=qx] (q2) {$q_2$}; \node[state,accepting,right of=qx] (q2) {$q_2$};
\node[right of=q2] (dummy) {$\forall x \in A$}; \node[right of=q2] (dummy) {$\forall x \in A$};
\path[->] \path[trans]
(q0) edge[bend left] node[above] {$x$} (qx) (q0) edge[bend left] node[above] {$x$} (qx)
(qx) edge[bend left] node[above] {$\neq x$} (q0) (qx) edge[bend left] node[above] {$\neq x$} (q0)
(qx) edge node[above] {$x$} (q2) (qx) edge node[above] {$x$} (q2)
@ -931,7 +931,7 @@ In particular our algorithm is easily adapted to include optimisations such as t
\node[state, right of=q0] (q1) {$q_{1,x}$}; \node[state, right of=q0] (q1) {$q_{1,x}$};
\node[state, accepting, below of=q1] (q2) {$q_{2, x, y}$}; \node[state, accepting, below of=q1] (q2) {$q_{2, x, y}$};
\path[->] \path[trans]
(q0) edge [bend left] node [above] {$x$} (q1) (q0) edge [bend left] node [above] {$x$} (q1)
(q1) edge [bend left] node [above] {$x$} (q0) (q1) edge [bend left] node [above] {$x$} (q0)
(q1) edge [bend left] node [right] {$y$} (q2) (q1) edge [bend left] node [right] {$y$} (q2)
@ -1623,7 +1623,7 @@ The minimal nominal DFA for $\text{FIFO}_2$ is given in \in{Figure}[fig:fifo2].
\node[state, accepting, right of=q1] (q2) {$q_{2, x, y}$}; \node[state, accepting, right of=q1] (q2) {$q_{2, x, y}$};
\node[state, below=1cm of q0] (bot) {$\bot$}; \node[state, below=1cm of q0] (bot) {$\bot$};
\path[->] \path[trans]
(q0) edge[bend left=15] node[above] {$\kw{push}(x)$} (q1) (q0) edge[bend left=15] node[above] {$\kw{push}(x)$} (q1)
(q1) edge[bend left=15] node[below] {$\kw{pop}(x)$} (q0) (q1) edge[bend left=15] node[below] {$\kw{pop}(x)$} (q0)
(q1) edge[bend left=15] node[above] {$\kw{push}(y)$} (q2) (q1) edge[bend left=15] node[above] {$\kw{push}(y)$} (q2)
@ -1661,7 +1661,7 @@ Despite this \nNLStar{} is able to learn the automaton shown in \in{Figure}[fig:
\node[state, right of=q0] (q1) {$q_{1,x}'$}; \node[state, right of=q0] (q1) {$q_{1,x}'$};
\node[state, accepting, right of=q1] (q2) {$q_{2}'$}; \node[state, accepting, right of=q1] (q2) {$q_{2}'$};
\path[->] \path[trans]
(q0) edge[bend left=15] node[above] {$x$} (q1) (q0) edge[bend left=15] node[above] {$x$} (q1)
(q1) edge[bend left=15] node[below] {$\EAlph$} (q0) (q1) edge[bend left=15] node[below] {$\EAlph$} (q0)
(q1) edge[bend left=15] node[above] {$x$} (q2) (q1) edge[bend left=15] node[above] {$x$} (q2)
@ -1772,7 +1772,7 @@ For instance, we can give an automaton over the substitution monad that recognis
\node[state, accepting, right of=qys] (q1) {$q_1$}; \node[state, accepting, right of=qys] (q1) {$q_1$};
\node[state, right of=q1] (q2) {$q_2$}; \node[state, right of=q1] (q2) {$q_2$};
\path[->] \path[trans]
(q0) edge node[above] {$x$} (qxp) (q0) edge node[above] {$x$} (qxp)
(qxp) edge[bend right] node[above] {$y$} (qxyp) (qxp) edge[bend right] node[above] {$y$} (qxyp)
(qxp) edge[bend left] node[above] {$x,[y \mapsto x]$} (qxyp) (qxp) edge[bend left] node[above] {$x,[y \mapsto x]$} (qxyp)

6
content/minimal-separating-sequences.tex
View file

@ -27,7 +27,7 @@ algorithm is empirically verified and compared to the traditional algorithm.
\page \page
\noindent
In diverse areas of computer science and engineering, systems can be modelled by \emph{finite state machines} (FSMs). In diverse areas of computer science and engineering, systems can be modelled by \emph{finite state machines} (FSMs).
One of the cornerstones of automata theory is minimisation of such machines -- and many variation thereof. One of the cornerstones of automata theory is minimisation of such machines -- and many variation thereof.
In this process one obtains an equivalent minimal FSM, where states are different if and only if they have different behaviour. In this process one obtains an equivalent minimal FSM, where states are different if and only if they have different behaviour.
@ -214,7 +214,7 @@ We continue until $T$ is complete.
\stopexample \stopexample
\startplacefigure \startplacefigure
[title={A FSM (a) and a complete splitting tree for it (b).}, [title={An FSM (a) and a complete splitting tree for it (b).},
reference=fig:automaton-tree] reference=fig:automaton-tree]
\startcombination[2*1] \startcombination[2*1]
{\hbox{\starttikzpicture {\hbox{\starttikzpicture
@ -224,7 +224,7 @@ We continue until $T$ is complete.
\node[state] (3) [below right of=2] {$s_3$}; \node[state] (3) [below right of=2] {$s_3$};
\node[state] (4) [below left of=3] {$s_4$}; \node[state] (4) [below left of=3] {$s_4$};
\node[state] (5) [below right of=0] {$s_5$}; \node[state] (5) [below right of=0] {$s_5$};
\path[->] \path[trans]
(0) edge [loop left] node [left] {${b}/0$} (0) edge [loop left] node [left] {${b}/0$}
(0) edge [bend right] node [right] {${a}/0$} (1) (0) edge [bend right] node [right] {${a}/0$} (1)
(1) edge node [above] {${a}/1$} (2) (1) edge node [above] {${a}/1$} (2)

4
content/ordered-nominal-sets.tex
View file

@ -28,7 +28,7 @@ In both cases, \ONS{} is competitive compared to existing implementations and ou
\page \page
\noindent
Automata over infinite alphabets are natural models for programs with unbounded data domains. Automata over infinite alphabets are natural models for programs with unbounded data domains.
Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[BojanczykKL14, DAntoniV17, GrigoreT16, KaminskiF94, MontanariP97, Segoufin06] and references therein). Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[BojanczykKL14, DAntoniV17, GrigoreT16, KaminskiF94, MontanariP97, Segoufin06] and references therein).
Typical infinite alphabets include sequence numbers, timestamps, and identifiers. Typical infinite alphabets include sequence numbers, timestamps, and identifiers.
@ -555,7 +555,7 @@ Such a transition structure is made precise by the notion of nominal automata.
\node (S 3) [state, right of=S 2] {$q_3(a,b)$}; \node (S 3) [state, right of=S 2] {$q_3(a,b)$};
\node (S 4) [state, below=1.5cm of S 2] {$q_4$}; \node (S 4) [state, below=1.5cm of S 2] {$q_4$};
\path[->] \path[trans]
(S 0) edge node[above] {$a$} (S 1) (S 0) edge node[above] {$a$} (S 1)
(S 1) edge node[above] {$b > a$} (S 2) (S 1) edge node[above] {$b > a$} (S 2)
(S 1) edge[bend right] node[below left] {$b \le a$} (S 4) (S 1) edge[bend right] node[below left] {$b \le a$} (S 4)

4
content/separated-nominal-automata.tex
View file

@ -26,7 +26,7 @@ This chapter is based on the following submission:
\noindent\cite[entry][MoermanR19] \noindent\cite[entry][MoermanR19]
\page \page
\noindent
Nominal sets are abstract sets which allow one to reason over sets with names, in terms of permutations and symmetries. Nominal sets are abstract sets which allow one to reason over sets with names, in terms of permutations and symmetries.
Since their introduction in computer science by \citet[GabbayP99], they Since their introduction in computer science by \citet[GabbayP99], they
have been widely used for implementing and reasoning over syntax with binders (see the book of \citenp[Pitts13]). have been widely used for implementing and reasoning over syntax with binders (see the book of \citenp[Pitts13]).
@ -683,7 +683,7 @@ The language accepted by this automaton assigns to a word $w$ the first element
\node[state with output, right of=2] (3) {$a b c$ \nodepart{lower} $o = a$}; \node[state with output, right of=2] (3) {$a b c$ \nodepart{lower} $o = a$};
\node[state with output, below=.5cm of 0] (s) {$\perp$ \nodepart{lower} $o = {\perp}$}; \node[state with output, below=.5cm of 0] (s) {$\perp$ \nodepart{lower} $o = {\perp}$};
\path[->] \path[trans]
(0) edge [bend right] node [below] {$\Put(a)$} (1) (0) edge [bend right] node [below] {$\Put(a)$} (1)
(0) edge node [left] {$\Pop$} (s) (0) edge node [left] {$\Pop$} (s)
(1) edge [bend right] node [above] {$\Pop$} (0) (1) edge [bend right] node [above] {$\Pop$} (0)

6
environment/headers.tex
View file

@ -33,15 +33,15 @@
\defineenumeration[theorem][text=Theorem] \defineenumeration[theorem][text=Theorem]
\defineenumeration[corollary][text=Corollary] \defineenumeration[corollary][text=Corollary]
\setupenumeration[definition,remark,example,lemma,proposition,theorem,corollary] \setupenumeration[definition,remark,example,lemma,proposition,theorem,corollary]
[alternative=serried, width=fit, right=., counter=lemmata, indenting=yes] [alternative=serried, width=fit, right=., counter=lemmata, indenting=yes, indentnext=no]
% Don't reset sections in new part % Don't reset sections in new part
\definestructureresetset[default][1,0,1][1] % reset part, not chapter, section \definestructureresetset[default][1,0,1][1] % reset part, not chapter, section
\setuphead[sectionresetset=default] \setuphead[sectionresetset=default]
\define\QED{\hfill$\square$} \define\QED{\hfill$\square$}
\definestartstop[proof][before={{\it Proof. }}, after={\QED}] \definestartstop[proof][before={{\it Proof. }}, after={\QED\blank[big]\noindentation}]
\definestartstop[proofnoqed][before={{\it Proof. }}, after={}] \definestartstop[proofnoqed][before={{\it Proof. }}, after={\blank[big]\noindentation}]
% Front matter met i, ii, etc % Front matter met i, ii, etc

2
environment/tikz.tex
View file

@ -8,7 +8,7 @@
% defaults % defaults
\tikzset{node distance=2cm} % 'shorten >=2pt' only for automata \tikzset{node distance=2cm} % 'shorten >=2pt' only for automata
\tikzset{/pgfplots/table/search path={data,../data}} \tikzset{/pgfplots/table/search path={data,../data}}
\tikzset{initial text=} \tikzset{initial text=, every initial by arrow/.style={shorten >=1pt}}
% observation table % observation table
\tikzset{obs table/.style={matrix of math nodes, ampersand replacement=\&, column 1/.style={anchor=base west}}} \tikzset{obs table/.style={matrix of math nodes, ampersand replacement=\&, column 1/.style={anchor=base west}}}