diff --git a/content/applying-automata-learning.tex b/content/applying-automata-learning.tex index c97ce1f..3cb425d 100644 --- a/content/applying-automata-learning.tex +++ b/content/applying-automata-learning.tex @@ -31,6 +31,7 @@ To the best of our knowledge, this is the first paper in which active automata l \page +\noindent 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. diff --git a/content/introduction.tex b/content/introduction.tex index e7925d9..b88252d 100644 --- a/content/introduction.tex +++ b/content/introduction.tex @@ -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, right of=bl, align=center] (br) {no\\spinning}; - \path[->] + \path[trans] (tl) edge [bend right] node [left] {\playstop} (bl) (tl) edge [bend right] node [below] {\spin} (tr) (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, right of=bl, align=center] (br) {no\\spinning}; - \path[->] + \path[trans] (tl) edge [bend right] node [left] {\playstop} (bl) (tl) edge [bend right] node [below] {\spin} (tr) (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, right of=bl, align=center] (br) {no\\spinning}; - \path[->] + \path[trans] (tl) edge [bend right] node [left] {\playstop} (bl) (tl) edge [bend right] node [below] {\spin} (tr) (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=1] (2) {$q_2$ \nodepart{lower} $r$}; - \path[->] + \path[trans] (0) edge [loop below] node [below] {$\ast$ / \checknok} (0) edge node [above, align=center] {$\kw{sign-up}(p)$ / \checkok \\ set $r := p$} (1) (1) edge [loop below] node [below] {$\ast$ / \checknok} diff --git a/content/learning-nominal-automata.tex b/content/learning-nominal-automata.tex index ffa6caa..ba61511 100644 --- a/content/learning-nominal-automata.tex +++ b/content/learning-nominal-automata.tex @@ -26,7 +26,7 @@ An implementation using a recently developed Haskell library for nominal computa \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. 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: @@ -202,7 +202,7 @@ where $q_0 = row(\epsilon) = \{ \epsilon \mapsto 0 \}$: \stoptikzpicture}}{} {\hbox{\starttikzpicture \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} }{} \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,accepting,below of=q1] (q2) {$q_2$}; -\path[->] +\path[trans] (q0) edge[loop below] node[below] {$b$} (q0) (q0) edge[bend right] node[above] {$a$} (q1) (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,accepting,right of=q2] (q3) {$q_3$}; -\path[->] +\path[trans] (q0) edge[bend left] node[above] {$a$} (q1) (q1) edge[bend left] node[above] {$b$} (q0) (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,right of=q3] (q4) {$q_4$}; -\path[->] +\path[trans] (q0) edge node[above left] {$a$} (q1) (q1) edge node[above right] {$a$} (q3) (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,right of=q3] (q4) {$q_4$}; -\path[->] +\path[trans] (q0) edge node[above left] {$a$} (qa) (qa) edge node[above right] {$a$} (q3) (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[above = 0pt of qx] (qa) {$\forall x \in A$}; -\path[->] +\path[trans] (q0) edge node[above] {$x$} (qx) (qx) edge node[above] {$x$} (q3) (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}}{} {\hbox{\starttikzpicture \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}}{} \stopcombination} @@ -576,7 +576,7 @@ The hypothesis automaton is \node[state,accepting,right of=qx] (q2) {$q_2$}; \node[right of=q2] (dummy) {$\forall x \in A$}; -\path[->] +\path[trans] (q0) edge[bend left] node[above] {$x$} (qx) (qx) edge[bend left] node[above] {$\neq x$} (q0) (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, accepting, below of=q1] (q2) {$q_{2, x, y}$}; - \path[->] + \path[trans] (q0) edge [bend left] node [above] {$x$} (q1) (q1) edge [bend left] node [above] {$x$} (q0) (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, below=1cm of q0] (bot) {$\bot$}; - \path[->] + \path[trans] (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[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, accepting, right of=q1] (q2) {$q_{2}'$}; - \path[->] + \path[trans] (q0) edge[bend left=15] node[above] {$x$} (q1) (q1) edge[bend left=15] node[below] {$\EAlph$} (q0) (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, right of=q1] (q2) {$q_2$}; - \path[->] + \path[trans] (q0) edge node[above] {$x$} (qxp) (qxp) edge[bend right] node[above] {$y$} (qxyp) (qxp) edge[bend left] node[above] {$x,[y \mapsto x]$} (qxyp) diff --git a/content/minimal-separating-sequences.tex b/content/minimal-separating-sequences.tex index c96a02c..a0f3ece 100644 --- a/content/minimal-separating-sequences.tex +++ b/content/minimal-separating-sequences.tex @@ -27,7 +27,7 @@ algorithm is empirically verified and compared to the traditional algorithm. \page - +\noindent 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. 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 \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] \startcombination[2*1] {\hbox{\starttikzpicture @@ -224,7 +224,7 @@ We continue until $T$ is complete. \node[state] (3) [below right of=2] {$s_3$}; \node[state] (4) [below left of=3] {$s_4$}; \node[state] (5) [below right of=0] {$s_5$}; - \path[->] + \path[trans] (0) edge [loop left] node [left] {${b}/0$} (0) edge [bend right] node [right] {${a}/0$} (1) (1) edge node [above] {${a}/1$} (2) diff --git a/content/ordered-nominal-sets.tex b/content/ordered-nominal-sets.tex index d726da2..eff9768 100644 --- a/content/ordered-nominal-sets.tex +++ b/content/ordered-nominal-sets.tex @@ -28,7 +28,7 @@ In both cases, \ONS{} is competitive compared to existing implementations and ou \page - +\noindent 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). 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 4) [state, below=1.5cm of S 2] {$q_4$}; -\path[->] +\path[trans] (S 0) edge node[above] {$a$} (S 1) (S 1) edge node[above] {$b > a$} (S 2) (S 1) edge[bend right] node[below left] {$b \le a$} (S 4) diff --git a/content/separated-nominal-automata.tex b/content/separated-nominal-automata.tex index 7cb396d..8e03bcf 100644 --- a/content/separated-nominal-automata.tex +++ b/content/separated-nominal-automata.tex @@ -26,7 +26,7 @@ This chapter is based on the following submission: \noindent\cite[entry][MoermanR19] \page - +\noindent 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 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, below=.5cm of 0] (s) {$\perp$ \nodepart{lower} $o = {\perp}$}; - \path[->] + \path[trans] (0) edge [bend right] node [below] {$\Put(a)$} (1) (0) edge node [left] {$\Pop$} (s) (1) edge [bend right] node [above] {$\Pop$} (0) diff --git a/environment/headers.tex b/environment/headers.tex index bd06e66..293e2d5 100644 --- a/environment/headers.tex +++ b/environment/headers.tex @@ -33,15 +33,15 @@ \defineenumeration[theorem][text=Theorem] \defineenumeration[corollary][text=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 \definestructureresetset[default][1,0,1][1] % reset part, not chapter, section \setuphead[sectionresetset=default] \define\QED{\hfill$\square$} -\definestartstop[proof][before={{\it Proof. }}, after={\QED}] -\definestartstop[proofnoqed][before={{\it Proof. }}, after={}] +\definestartstop[proof][before={{\it Proof. }}, after={\QED\blank[big]\noindentation}] +\definestartstop[proofnoqed][before={{\it Proof. }}, after={\blank[big]\noindentation}] % Front matter met i, ii, etc diff --git a/environment/tikz.tex b/environment/tikz.tex index 0efafd8..9f0c5b8 100644 --- a/environment/tikz.tex +++ b/environment/tikz.tex @@ -8,7 +8,7 @@ % defaults \tikzset{node distance=2cm} % 'shorten >=2pt' only for automata \tikzset{/pgfplots/table/search path={data,../data}} -\tikzset{initial text=} +\tikzset{initial text=, every initial by arrow/.style={shorten >=1pt}} % observation table \tikzset{obs table/.style={matrix of math nodes, ampersand replacement=\&, column 1/.style={anchor=base west}}}