Door het ONS hoofdstuk gegaan. En commentaar van Frits over Test Methods verwerkt.

biblio.bib

@@ -579,7 +579,7 @@
 
 @inproceedings{BosS18,
 	author    = {Petra van den Bos and
-	             Mari{\"{e}}lle Stoelinga},
+	             Marielle Stoelinga},
 	editor    = {Andrea Orlandini and
 	             Martin Zimmermann},
 	title     = {Tester versus Bug: {A} Generic Framework for Model-Based Testing via
@@ -587,6 +587,7 @@
 	booktitle = {Proceedings Ninth International Symposium on Games, Automata, Logics,
 	             and Formal Verification, GandALF 2018, Saarbr{\"{u}}cken, Germany,
 	             26-28th September 2018.},
+	publisher = {Open Publishing Association},
 	series    = {{EPTCS}},
 	volume    = {277},
 	pages     = {118--132},
@@ -1959,6 +1960,29 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{MurawskiRT18,
+	author    = {Andrzej S. Murawski and
+	             Steven J. Ramsay and
+	             Nikos Tzevelekos},
+	editor    = {Igor Potapov and
+	             Paul G. Spirakis and
+	             James Worrell},
+	title     = {Polynomial-Time Equivalence Testing for Deterministic Fresh-Register
+	             Automata},
+	booktitle = {43rd International Symposium on Mathematical Foundations of Computer
+	             Science, {MFCS} 2018, August 27-31, 2018, Liverpool, {UK}},
+	series    = {LIPIcs},
+	volume    = {117},
+	pages     = {72:1--72:14},
+	publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
+	year      = {2018},
+	url       = {https://doi.org/10.4230/LIPIcs.MFCS.2018.72},
+	doi       = {10.4230/LIPIcs.MFCS.2018.72},
+	timestamp = {Tue, 28 Aug 2018 15:28:12 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/mfcs/MurawskiRT18},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @phdthesis{DBLP:phd/de/Niese2003,
 	author    = {Oliver Niese},
 	title     = {An integrated approach to testing complex systems},

content/ordered-nominal-sets.tex

@@ -6,15 +6,17 @@
    reference=chap:ordered-nominal-sets]
 
 \midaligned{~
-\author{David Venhoek \\ Radboud University}
+\author[width=0.5\hsize]{David Venhoek \\ Radboud University}
-\author{Joshua Moerman \\ Radboud University}
+\author[width=0.5\hsize]{Joshua Moerman \\ Radboud University}
-\author{Jurriaan Rot \\ Radboud University}
+}
+\midaligned{~
+\author[width=0.5\hsize]{Jurriaan Rot \\ Radboud University}
 }
 
 \startabstract
-We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon.
+We show how to compute efficiently with nominal sets over the total order symmetry by developing a direct representation of such nominal sets and basic constructions thereon.
 In contrast to previous approaches, we work directly at the level of orbits, which allows for an accurate complexity analysis.
-The approach is implemented as the library \ONS{} (Ordered Nominal Sets).
+The approach is implemented as the library \ONS{}~(Ordered Nominal Sets).
 
 Our main motivation is nominal automata, which are models for recognising languages over infinite alphabets.
 We evaluate \ONS{} in two applications:
@@ -49,13 +51,14 @@ These implementations are very flexible, and the SMT solver does most of the hea
 Unfortunately, this comes at a cost as SMT solving is in general {\sc Pspace}-hard. 
 Since the formulas used to describe sets tend to grow as more calculations are done, running times can become unpredictable.
 
-In the current paper, we use a direct representation, based on symmetries and orbits, to represent nominal sets.
+In this chapter, we use a direct representation based on symmetries and orbits, to represent nominal sets.
 We focus on the \emph{total order symmetry}, where data values are rational numbers and can be compared for their order.
 Nominal automata over the total order symmetry are more expressive than automata over the equality symmetry (i.e., traditional register automata of \citenp[DBLP:journals/tcs/KaminskiF94]).
 A key insight is that the representation of nominal sets from \citet[DBLP:journals/corr/BojanczykKL14] becomes rather simple in the total order symmetry; each orbit is presented solely by a natural number, intuitively representing the number of variables or registers.
 
+\noindent
 Our main contributions include the following.
-\startitemize
+\startitemize[after]
 \item
 We develop the \emph{representation theory} of nominal sets over the total order symmetry.
 We give concrete representations of nominal sets, their products, and equivariant maps.
@@ -74,7 +77,7 @@ On the other hand, \LOIS{} and \NLambda{} are faster in minimising the structure
 In automata learning, the logical structure is not available a-priori, and \ONS{} is faster in most cases.
 \stopitemize
 
-The structure of the paper is as follows.
+The structure of this chapter is as follows.
 \in{Section}[sec:nomsets] contains background on nominal sets and their representation.
 \in{Section}[sec:total-order] describes the concrete representation of nominal sets, equivariant maps and products in the total order symmetry.
 \in{Section}[sec:impl] describes the implementation \ONS{} with complexity results, and \in{Section}[sec:appl] the evaluation of \ONS{} on algorithms for nominal automata. 
@@ -89,52 +92,57 @@ Nominal sets are infinite sets that carry certain symmetries, allowing a finite
 We recall their formalisation in terms of group actions, following \citet[DBLP:journals/corr/BojanczykKL14, Pitts13], to which we refer for an extensive introduction.
 
 
-\startsubsubsection
+\startsubsection
-  [title={Group actions.}]
+  [title={Group actions}]
 
 Let $G$ be a group and $X$ be a set.
-A \emph{(right) $G$-action} is a function ${\cdot} \colon X \times G \to X$ satisfying $x \cdot 1 = x$ and $(x \cdot g) \cdot h = x \cdot (g h)$ for all $x \in X$ and $g, h \in G$.
+A \emph{(left) $G$-action} is a function ${\cdot} \colon G \times X \to X$ satisfying $1 \cdot x = x$ and $(h g) \cdot x = h \cdot (g \cdot x)$ for all $x \in X$ and $g, h \in G$.
-A set $X$ with a $G$-action is called a \emph{$G$-set} and we often write $xg$ instead of $x \cdot g$.
+A set $X$ with a $G$-action is called a \emph{$G$-set} and we often write $g x$ instead of $g \cdot x$.
-The \emph{orbit} of an element $x \in X$ is the set $\{xg \mid g \in G\}$.
+The \emph{orbit} of an element $x \in X$ is the set $\{g x \mid g \in G\}$.
 A $G$-set is always a disjoint union of its orbits (in other words, the orbits partition the set).
 We say that $X$ is \emph{orbit-finite} if it has finitely many orbits, and we denote the number of orbits by $N(X)$.
 
-A map $f \colon X \to Y$ between $G$-sets is called \emph{equivariant} if it preserves the group action, i.e., for all $x\in X$ and $g \in G$ we have $f(x)g = f(xg)$.
+A map $f \colon X \to Y$ between $G$-sets is called \emph{equivariant} if it preserves the group action, i.e., for all $x \in X$ and $g \in G$ we have $g \cdot f(x) = f(g \cdot x)$.
 If an equivariant map $f$ is bijective, then $f$ is an \emph{isomorphism} and we write $X \cong Y$.
-A subset $Y\subseteq X$ is equivariant if the corresponding inclusion map is equivariant.
+A subset $Y \subseteq X$ is equivariant if the corresponding inclusion map is equivariant.
 The \emph{product} of two $G$-sets $X$ and $Y$ is given by the Cartesian
-product $X \times Y$ with the pointwise group action on it, i.e., $(x,y)g = (xg,yg)$.
+product $X \times Y$ with the point-wise group action on it, i.e., $g (x, y) = (g x, g y)$.
 Union and intersection of $X$ and $Y$ are well-defined if the two
 actions agree on their common elements. 
 
 
-\stopsubsubsection
+\stopsubsection
-\startsubsubsection
+\startsubsection
-  [title={Nominal sets.}]
+  [title={Nominal sets}]
 
-A \emph{data symmetry} is a pair $(\mathcal{D},G)$ where $\mathcal{D}$ is a set and $G$ is a subgroup of $\Sym(\mathcal{D})$, the group of bijections on $\mathcal{D}$.
+A \emph{data symmetry} is a pair $(\mathcal{D}, G)$ where $\mathcal{D}$ is a set and $G$ is a subgroup of $\Sym(\mathcal{D})$, the group of bijections on $\mathcal{D}$.
-Note that the group $G$ naturally acts on $\mathcal{D}$ by defining $x g = g(x)$.
+Note that the group $G$ naturally acts on $\mathcal{D}$ by defining $g x = g(x)$.
 In the most studied instance, called the \emph{equality symmetry}, $\mathcal{D}$ is a countably infinite set and $G = \Sym(\mathcal{D})$.
-In this paper, we will mostly focus on the \emph{total order symmetry} given by $\mathcal{D} = \Q$ and $G = \{\pi \mid \pi \in \Sym(\Q), \pi \text{ is monotone}\}$.
+In this chapter, we focus on the \emph{total order symmetry} given by $\mathcal{D} = \Q$ and $G = \{\pi \mid \pi \in \Sym(\Q), \pi \text{ is monotone}\}$.
 
 Let $(\mathcal{D}, G)$ be a data symmetry and $X$ be a $G$-set.
-A set of data values $S\subseteq \mathcal{D}$ is called a \emph{support} of an element $x \in X$ if for all $g\in G$ with $\forall s \in S: sg = s$ we have $xg = x$.
+A set of data values $S\subseteq \mathcal{D}$ is called a \emph{support} of an element $x \in X$ if for all $g\in G$ with $\forall s \in S: g s = s$ we have $g x = x$.
 A $G$-set $X$ is called \emph{nominal} if every element $x\in X$ has a finite support.
 
 \startexample
 We list several examples for the total order symmetry. 
 The set $\Q^2$ is nominal as each element $(q_1, q_2) \in \Q^2$ has the finite set $\{q_1, q_2\}$ as its support.
-The set has the following three orbits: $\{(q_1, q_2) \mid q_1 < q_2\}$, $\{(q_1, q_2) \mid q_1 > q_2\}$ and $\{(q_1, q_2) \mid q_1 = q_2\}$.
+The set has the following three orbits:
+\startformulas
+\startformula \{(q_1, q_2) \mid q_1 < q_2\} \stopformula
+\startformula \{(q_1, q_2) \mid q_1 = q_2\} \stopformula
+\startformula \{(q_1, q_2) \mid q_1 > q_2\}. \stopformula
+\stopformulas
 
 For a set $X$, the set of all subsets of size $n \in \N$ is denoted by $\mathcal{P}_n(X) = \{Y \subseteq X \mid \#Y = n\}$.
-The set $\mathcal{P}_n(\Q)$ is a single-orbit nominal set for each $n$, with the action defined by direct image: $Y g = \{ yg \mid y \in Y \}$. 
+The set $\mathcal{P}_n(\Q)$ is a single-orbit nominal set for each $n$, with the action defined by direct image: $g Y = \{ g y \mid y \in Y \}$.
 The group of monotone bijections also acts by direct image on the full power set $\mathcal{P}(\Q)$, but this is \emph{not} a nominal set.
 For instance, the set $\mathbb{Z} \in \mathcal{P}(\Q)$ of integers has no finite support.
 \stopexample
 
 
 If $S \subseteq \mathcal{D}$ is a support of an element $x \in X$, then any set $S' \subseteq \mathcal{D}$ such that $S \subseteq S'$ is also a support of $x$.
-A set $S \subseteq \mathcal{D}$ is a \emph{least finite support} of $x \in X$ if it is a support of $x$ and $S \subseteq S'$ for any support $S'$ of $x$.
+A set $S \subset \mathcal{D}$ is a \emph{least finite support} of $x \in X$ if it is a finite support of $x$ and $S \subseteq S'$ for any finite support $S'$ of $x$.
 The existence of least finite supports is crucial for representing orbits.
 Unfortunately, even when elements have a finite support, in general they do not always have a least finite support.
 A data symmetry $(\mathcal{D}, G)$ is said to \emph{admit least supports} if every element of every nominal set has a least finite support.
@@ -149,7 +157,7 @@ For an orbit-finite nominal set $X$, we define $\dim(X) = \max \{ \dim(x) \mid x
 For a single-orbit set $O$, observe that $\dim(O) = \dim(x)$ where $x$ is any element $x \in O$.
 
 
-\stopsubsubsection
+\stopsubsection
 \startsubsection
   [title={Representing nominal orbits},
    reference=subsec:nomorbit]
@@ -160,12 +168,12 @@ We only briefly report their definitions here.
 However, the reader can safely move to the concrete representation theory in \in{Section}[sec:total-order] with only a superficial understanding of \in{Theorem}[representation_tuple] below.
 
 The \emph{restriction} of an element $\pi \in G$ to a subset $C \subseteq \mathcal{D}$, written as $\pi|_C$, is the restriction of the function $\pi \colon \mathcal{D} \to \mathcal{D}$ to the domain $C$.
-The restriction of a group $G$ to a subset $C \subseteq \mathcal{D}$ is defined as $G|_C = \{\pi|_C \mid \pi \in G,\, C \pi = C\}$.
+The restriction of a group $G$ to a subset $C \subseteq \mathcal{D}$ is defined as $G|_C = \{\pi|_C \mid \pi \in G,\, \pi C = C\}$.
 The \emph{extension} of a subgroup $S \le G|_C$ is defined as $\ext_G(S) = \{\pi \in G \mid \pi|_C \in S\}$.
-For $C \subseteq \mathcal{D}$ and $S\le G|_C$, define $[C,S]^{ec} = \{\{sg \mid s \in \ext_G(S)\}\mid g\in G\}$, i.e., the set of right cosets of $\ext_G(S)$ in $G$.
+For $C \subseteq \mathcal{D}$ and $S\le G|_C$, define $[C,S]^{ec} = \{\{g s \mid s \in \ext_G(S)\}\mid g\in G\}$, i.e., the set of right cosets of $\ext_G(S)$ in $G$.
 Then $[C,S]^{ec}$ is a single-orbit nominal set.
 
-Using the above, we can formulate the representation theory from \citet[DBLP:journals/corr/BojanczykKL14] that we will use in the current paper.
+Using the above, we can formulate the representation theory from \citet[DBLP:journals/corr/BojanczykKL14].
 This gives a finite description for all single-orbit nominal sets $X$, namely a finite set $C$ together with some of its symmetries.
 
 \starttheorem[reference=representation_tuple]
@@ -175,7 +183,7 @@ Then there exists a subgroup $S \le G|_C$ such that $X \cong [C,S]^{ec}$.
 
 The proof by \citet[DBLP:journals/corr/BojanczykKL14] uses a bit of category theory:
 it establishes an equivalence of categories between single-orbit sets and the pairs $(C, S)$.
-We will not use the language of category theory much in order to keep the paper self-contained.
+We will not use the language of category theory much in order to keep the chapter self-contained.
 
 
 \stopsubsection
@@ -195,7 +203,7 @@ Hence, our data domain is $\Q$ and we take $G$ to be the group of monotone bijec
    reference=sec:orbits-and-nominal-set]
 
 From the representation in \in{Section}[subsec:nomorbit], we find that any single-orbit set $X$ can be represented as a tuple $(C,S)$.
-Our first observation is that the finite group of \quote{local symmetries}, $S$, in this representation is always trivial, i.e., $S = I$, where $I = \{1\}$ is the trivial group.
+Our first observation is that the finite group $S$ of \quote{local symmetries} in this representation is always trivial, i.e., $S = I$, where $I = \{1\}$ is the trivial group.
 This follows from the following lemma and $S \le G|_C$.
 
 \startlemma[reference=group_trivial]
@@ -222,8 +230,9 @@ Given a function $f \colon \N \to \N$, we define a nominal set $[f]^{o}$ by
 
 \startproposition[reference=thm:pres-nom]
 For every orbit-finite nominal set $X$, there is a function $f \colon \N \to \N$ such that $X \cong [f]^{o}$ and the set $\{n \mid f(n) \neq 0\}$ is finite.
-Furthermore, the mapping between $X$ and $f$ is one-to-one up to isomorphism of $X$ when restricting to $f \colon \N \to \N$ for which the set $\{n\mid f(n) \ne 0\}$ is finite.
+Furthermore, the mapping between $X$ and $f$ is one-to-one (up to isomorphism of nominal sets) when restricting to $f \colon \N \to \N$ for which the set $\{n\mid f(n) \ne 0\}$ is finite.
 \stopproposition
+
 The presentation in terms of a function $f \colon \N \to \N$ enforces that there are only finitely many orbits of any given dimension.
 The first part of the above proposition generalises to arbitrary nominal sets by replacing the codomain of $f$ by the class of all sets and adapting \in{Definition}[def:present-nom] accordingly.
 However, the resulting correspondence will no longer be one-to-one.
@@ -274,7 +283,7 @@ For every equivariant map $f \colon X \to Y$ between orbit-finite nominal sets $
 
 Consider the example function $\min \colon \mathcal{P}_3(\Q) \to \Q$ which returns the smallest element of a 3-element set.
 Note that both $\mathcal{P}_3(\Q)$ and $\Q$ are single orbits.
-Since for the orbit $\mathcal{P}_3(\Q)$ we only keep the smallest element of the support, we can thus represent the function $\min$ with $\{(\mathcal{P}_3(\Q), 100, \Q)\}$.
+Since for the orbit $\mathcal{P}_3(\Q)$ we only keep the smallest element of the support, we can thus represent the function $\min$ with $H = \{(\mathcal{P}_3(\Q), 100, \Q)\}$.
 
 
 \stopsubsection
@@ -351,7 +360,6 @@ For $X \cong [f]^{o}$ and $Y \cong [g]^{o}$ we have $X \times Y \cong [h]^{o}$,
 \startformula
 h(n) = \sum_{\startsubstack 0 \le i, j \le n \NR i+j \ge n \stopsubstack} f(i) g(j) {{n}\choose{j}}{{j}\choose{n-i}}.
 \stopformula
-\todo{choose-notatie klopt niet}
 \stoptheorem
 
 \startexample
@@ -359,7 +367,7 @@ To illustrate some aspects of the above representation, let us use it to calcula
 First, we observe that both $\Q$ and $S = \{(a,b) \in \Q^2 \mid a < b\}$ consist of a single orbit.
 Hence any orbit of the product corresponds to a triple $(P, \Q, S)$, where the string $P$ satisfies $|P|_L+|P|_B = \dim(\Q) = 1$ and $|P|_R+|P|_B = \dim(S) = 2$.
 We can now find the orbits of the product $\Q \times S$ by enumerating all strings satisfying these equations.
-This yields:
+This yields
 \startitemize
 \item LRR, corresponding to the orbit $\{(a,(b,c)) \mid a,b,c \in \Q, a < b < c\}$,
 \item RLR, corresponding to the orbit $\{(b,(a,c)) \mid a,b,c \in \Q, a < b < c\}$,
@@ -482,17 +490,17 @@ The software assumes these are equivariant, but this is not verified.
 \stoptabulate
 \stoptheorem
 
-\startproof
+\startproofnoqed
 Since most parts are proven similarly, we only include proofs for the first and last item.
 
-\emph{Membership.}
+\description{Membership.}
 To decide $x \in X$, we first construct the orbit containing $x$, which is done in constant time.
 Then we use a logarithmic lookup to decide whether this orbit is in our set data structure.
 Hence, membership checking is $O(\log(\Nsize(X)))$.
 
-\emph{Products.}
+\startdescription[title={Products.}]
 Calculating the product of two nominal sets is the most complicated construction.
-For each pair of orbits in the original sets $X$ and $Y$, all product orbits need to be generated.
+For each pair of orbits in the original sets $X$ and $Y$, all product strings need to be generated.
 Each product orbit itself is constructed in constant time.
 By generating these orbits in-order, the resulting set takes $O(\Nsize(X \times Y))$ time to construct.
 
@@ -501,7 +509,9 @@ Recall that orbits in a product are represented by strings of length at most $\d
 (If the string is shorter, we pad it with one of the symbols.)
 Since there are three symbols ($L, R$ and $B$), the product of $X$ and $Y$ will have at most $3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y)$ orbits.
 It follows that taking products has time complexity of $O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$.
-\stopproof
+\QED
+\stopdescription
+\stopproofnoqed
 
 
 \stopsubsection
@@ -526,7 +536,7 @@ We call this language the \emph{interval language} as a word $w \in \Q^{\ast}$ i
 This language contains arbitrarily long words.
 For this language it is crucial to work with an infinite alphabet as for each finite set $C \subset \Q$, the restriction $\Lint \cap C^{\ast}$ is just a finite language.
 Note that the language is equivariant: $w \in \Lint \iff wg \in \Lint$ for any monotone bijection $g$, because nested intervals are preserved by monotone maps.
-\footnote{The $G$-action on words is defined point-wise: $(w_1 \ldots w_n) g = (w_1 g) \ldots (w_n g)$.}
+\footnote{The $G$-action on words is defined point-wise: $g (w_1 \ldots w_n) = (g w_1) \ldots (g w_n)$.}
 Indeed, $\Lint$ is a nominal set, although it is not orbit-finite.
 
 Informally, the language $\Lint$ can be accepted by the automaton depicted in \in{Figure}[fig:lint-minimal].
@@ -538,7 +548,7 @@ Such a transition structure is made precise by the notion of nominal automata.
 \startplacefigure
   [title={Example automaton that accepts the language $\Lint$.},
    reference=fig:lint-minimal]
-\starttikzpicture[node distance=3.5cm]
+\hbox{\starttikzpicture[node distance=3.5cm]
 \node (S 0) [state] {$q_0$};
 \node (S 1) [state, right of=S 0] {$q_1(a)$};
 \node (S 2) [state, accepting, right of=S 1] {$q_2(a,b)$};
@@ -556,7 +566,7 @@ Such a transition structure is made precise by the notion of nominal automata.
 (S 3) edge[bend left] node[above left] {$c \le a$} (S 4)
 (S 3) edge[bend left=60] node[below right] {$c \ge b$} (S 4)
 (S 4) edge[loop below] node [below] {$a$} (S 4);
-\stoptikzpicture
+\stoptikzpicture}
 \stopplacefigure
 
 \startdefinition
@@ -575,18 +585,13 @@ The transition we described earlier can now be formally defined as $\delta(q_2(a
 By defining $\delta$ on all states accordingly and defining the final states as $F = \{ q_2(a, b) \mid a < b \in \Q \}$, we obtain a nominal deterministic automaton $(S, \Q, F, \delta)$.
 The state $q_0$ accepts the language $\Lint$.
 
-
-\startsubsubsection
-  [title={Testing.}]
-
 We implement two algorithms on nominal automata, minimisation and learning, to benchmark \ONS{}.
 The performance of \ONS{} is compared to two existing libraries for computing with nominal sets, \NLambda{} and \LOIS{}.
 The following automata will be used.
 
 
-\stopsubsubsection
+\startsubsubject
-\startsubsubsection
+  [title={Random automata}]
-  [title={Random automata.}]
 
 As a primary test suite, we generate random automata as follows.
 The input alphabet is always $\Q$ and the number of orbits and dimension $k$ of the state space $S$ are fixed.
@@ -599,9 +604,9 @@ The choices made here are arbitrary and only provide basic automata.
 We note that the automata are generated orbit-wise and this may favour our tool.
 
 
-\stopsubsubsection
+\stopsubsubject
-\startsubsubsection
+\startsubsubject
-  [title={Structured automata.}]
+  [title={Structured automata}]
 
 Besides random automata we wish to test the algorithms on more structured automata.
 We define the following automata.
@@ -614,19 +619,20 @@ The alphabet is defined by two orbits: $\{\kw{Put}(a) \mid a \in \Q \}$ and $\{\
 
 \description{$\Lmax$} The language $\Lmax = \{ w a \in \Q^{*} \mid a = \max(w_1, \dots, w_n) \}$ where the last symbol is the maximum of previous symbols.
 
-\description{$\Lint$} The language accepting a series of nested intervals, as defined above.
+\description{$\Lint$} The language accepting a series of nested intervals, as defined before.
 
 In \in{Table}[minimize_results] we report the number of orbits for each automaton.
-The first two classes of automata were previously used as test cases by \citet[MoermanS0KS17].
+The first two classes of automata are described in \in{Chapter}[chap:learning-nominal-automata].
 These two classes are also equivariant w.r.t. the equality symmetry.
-The extra bit of structure allows the automata to be encoded more efficiently, as we do not need to encode a transition for each orbit in $S \times A$.
+
+Extra structure allows the automata to be encoded more efficiently, as we do not need to encode a transition for each orbit in $S \times A$.
 Instead, a more symbolic encoding is possible.
 Both \LOIS{} and \NLambda{} allow to use this more symbolic representation.
 Our tool, \ONS{}, only works with nominal sets and the input data needs to be provided orbit-wise.
 Where applicable, the automata listed above were generated using the code from \citet[MoermanS0KS17], ported to the other libraries as needed.
 
 
-\stopsubsubsection
+\stopsubsubject
 \startsubsection
   [title={Minimising nominal automata}]
 
@@ -672,11 +678,11 @@ Filtering $S \times S$ using that then takes $O(\Nsize(S)^2 3^{2k})$.
 The time to compute $S \times S \times A$ dominates, hence each iteration of the loop takes $O(\Nsize(S)^2 \Nsize(A) 3^{5k})$.
 
 Next, we need to count the number of iterations of the loop.
-Each iteration of the loop gives rise to a new partition, which is a refinement of the previous partition.
+Each iteration of the loop gives rise to a new partition, refining the previous partition.
 Furthermore, every partition generated is equivariant. Note that this implies that each refinement of the partition does at least one of two things:
 distinguish between two orbits of $S$ previously in the same element(s) of the partition, or distinguish between two members of the same orbit previously in the same element of the partition.
-The first can happen only $\Nsize(S)-1$ times, as after that there are no more orbits lumped together.
+The former can happen only $\Nsize(S)-1$ times, as after that there are no more orbits lumped together.
-The second can only happen $\dim(S)$ times per orbit, because each such a distinction between elements is based on splitting on the value of one of the elements of the support.
+The latter can only happen $\dim(S)$ times per orbit, because each such a distinction between elements is based on splitting on the value of one of the elements of the support.
 Hence, after $\dim(S)$ times on a single orbit, all elements of the support are used up. Combining this, the longest chain of partitions of $S$ has length at most $O(k \Nsize(S))$.
 
 Since each partition generated in the loop is unique, the loop cannot run for more iterations than the length of the longest chain of partitions on $S$.
@@ -690,8 +696,8 @@ The complexity of \in{Algorithm}[alg:moore] for nominal automata is very similar
 This suggest that it is possible to further optimise an implementation with similar techniques used for ordinary automata.
 
 
-\startsubsubsection
+\startsubsubject
-  [title={Implementations.}]
+  [title={Implementations}]
 
 We implemented the minimisation algorithm in \ONS{}.
 For \NLambda{} and \LOIS{} we used their implementations of Moore's minimisation algorithm \citep[DBLP:journals/corr/KlinS16, DBLP:conf/cade/KopczynskiT16, DBLP:conf/popl/KopczynskiT17].
@@ -701,9 +707,9 @@ For \ONS{}, all automata were read from file.
 The output of these programs was manually checked to see if the minimisation was performed correctly.
 
 
-\stopsubsubsection
+\stopsubsubject
-\startsubsubsection
+\startsubsubject
-  [title={Results.}]
+  [title={Results}]
 
 The results (shown in \in{Table}[minimize_results]) for random automata show a clear advantage for \ONS{}, which is capable of running all supplied testcases in less than one second.
 This in contrast to both \LOIS{} and \NLambda{}, which take more than $2$ hours on the largest random automata.
@@ -711,29 +717,30 @@ This in contrast to both \LOIS{} and \NLambda{}, which take more than $2$ hours
 \placetable[here][minimize_results]
 {Running times for \in{Algorithm}[alg:moore] implemented in the three libraries.
 $N(S)$ is the size of the input and $N(S^{\text{min}})$ the size of the minimal automaton.
-For \ONS{}, the time used to generate the automaton is reported separately (in grey).}
+For \ONS{}, the time used to generate the automaton is reported separately (in grey).
-\starttabulate[|l|l|l|r|r|r|r|][distance=none]
+Timeouts are indicated by $\infty$.}
-\NC Type \NC $\Nsize(S)$ \NC $\Nsize(S^{\text{min}})$ \VL \ONS{} \NC \color[darkgray]{(Gen.)} \VL \NLambda{} \VL \LOIS{} \NC\NR
+\starttabulate[|l|c|c|cg{.}|cg{.}|cg{.}|cg{.}|][distance=none]
+\NC Type \NC $\Nsize(S)$ \NC $\Nsize(S^{\text{min}})$ \VL \ONS{} (s) \NC \color[darkgray]{Gen (s)} \VL \NLambda{} (s) \VL \LOIS{} (s) \NC\NR
 \HL
-\NC rand$_{5,1}$  (x10) \NC $5$  \NC n/a \VL $0.02$s \NC \color[darkgray]{n/a} \VL $0.82$s     \VL $3.14$s     \NC\NR
+\NC rand$_{5,1}$  (x10) \NC 5  \NC n/a \VL 0.02 \NC \color[darkgray]{n/a} \VL 0.82     \VL 3.14     \NC\NR
-\NC rand$_{10,1}$ (x10) \NC $10$ \NC n/a \VL $0.03$s \NC \color[darkgray]{n/a} \VL $17.03$s    \VL $1$m $32$s  \NC\NR
+\NC rand$_{10,1}$ (x10) \NC 10 \NC n/a \VL 0.03 \NC \color[darkgray]{n/a} \VL 17.03    \VL 92       \NC\NR
-\NC rand$_{10,2}$ (x10) \NC $10$ \NC n/a \VL $0.09$s \NC \color[darkgray]{n/a} \VL $35$m $14$s \VL $> 60$m     \NC\NR
+\NC rand$_{10,2}$ (x10) \NC 10 \NC n/a \VL 0.09 \NC \color[darkgray]{n/a} \VL 2114     \VL $\infty$ \NC\NR
-\NC rand$_{15,1}$ (x10) \NC $15$ \NC n/a \VL $0.04$s \NC \color[darkgray]{n/a} \VL $1$m $27$s  \VL $10$m $20$s \NC\NR
+\NC rand$_{15,1}$ (x10) \NC 15 \NC n/a \VL 0.04 \NC \color[darkgray]{n/a} \VL 87       \VL 620      \NC\NR
-\NC rand$_{15,2}$ (x10) \NC $15$ \NC n/a \VL $0.11$s \NC \color[darkgray]{n/a} \VL $55$m $46$s \VL $> 60$m     \NC\NR
+\NC rand$_{15,2}$ (x10) \NC 15 \NC n/a \VL 0.11 \NC \color[darkgray]{n/a} \VL 3346     \VL $\infty$ \NC\NR
-\NC rand$_{15,3}$ (x10) \NC $15$ \NC n/a \VL $0.46$s \NC \color[darkgray]{n/a} \VL $> 60$m     \VL $> 60$m     \NC\NR
+\NC rand$_{15,3}$ (x10) \NC 15 \NC n/a \VL 0.46 \NC \color[darkgray]{n/a} \VL $\infty$ \VL $\infty$ \NC\NR
 \HL
-\NC FIFO($2$) \NC $13$   \NC $6$   \VL $0.01$s  \NC \color[darkgray]{$0.01$s}  \VL $1.37$s    \VL $0.24$s    \NC\NR
+\NC FIFO($2$) \NC 13   \NC 6   \VL 0.01     \NC \color[darkgray]{0.01}  \VL 1.37  \VL 0.24  \NC\NR
-\NC FIFO($3$) \NC $65$   \NC $19$  \VL $0.38$s  \NC \color[darkgray]{$0.09$s}  \VL $11.59$s   \VL $2.4$s     \NC\NR
+\NC FIFO($3$) \NC 65   \NC 19  \VL 0.38     \NC \color[darkgray]{0.09}  \VL 11.59 \VL 2.4   \NC\NR
-\NC FIFO($4$) \NC $440$  \NC $94$  \VL $39.11$s \NC \color[darkgray]{$1.60$s}  \VL $1$m $16$s \VL $14.95$s   \NC\NR
+\NC FIFO($4$) \NC 440  \NC 94  \VL 39.11    \NC \color[darkgray]{1.60}  \VL 76    \VL 14.95 \NC\NR
-\NC FIFO($5$) \NC $3686$ \NC $635$ \VL $> 60$m  \NC \color[darkgray]{$39.78$s} \VL $6$m $42$s \VL $1$m $11$s \NC\NR
+\NC FIFO($5$) \NC 3686 \NC 635 \VL $\infty$ \NC \color[darkgray]{39.78} \VL 402   \VL 71    \NC\NR
 \HL
-\NC $ww(2)$ \NC $8$   \NC $8$   \VL $0.00$s  \NC \color[darkgray]{$0.00$s} \VL $0.14$s  \VL $0.03$s \NC\NR
+\NC $ww(2)$ \NC 8   \NC 8   \VL 0.00     \NC \color[darkgray]{0.00} \VL 0.14  \VL 0.03 \NC\NR
-\NC $ww(3)$ \NC $24$  \NC $24$  \VL $0.19$s  \NC \color[darkgray]{$0.02$s} \VL $0.88$s  \VL $0.16$s \NC\NR
+\NC $ww(3)$ \NC 24  \NC 24  \VL 0.19     \NC \color[darkgray]{0.02} \VL 0.88  \VL 0.16 \NC\NR
-\NC $ww(4)$ \NC $112$ \NC $112$ \VL $26.44$s \NC \color[darkgray]{$0.25$s} \VL $3.41$s  \VL $0.61$s \NC\NR
+\NC $ww(4)$ \NC 112 \NC 112 \VL 26.44    \NC \color[darkgray]{0.25} \VL 3.41  \VL 0.61 \NC\NR
-\NC $ww(5)$ \NC $728$ \NC $728$ \VL $> 60$m  \NC \color[darkgray]{$6.37$s} \VL $10.54$s \VL $1.80$s \NC\NR
+\NC $ww(5)$ \NC 728 \NC 728 \VL $\infty$ \NC \color[darkgray]{6.37} \VL 10.54 \VL 1.80 \NC\NR
 \HL
-\NC $\Lmax$ \NC $5$ \NC $3$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $2.06$s \VL $0.03$s \NC\NR
+\NC $\Lmax$ \NC 5 \NC 3 \VL 0.00 \NC \color[darkgray]{0.00} \VL 2.06 \VL 0.03 \NC\NR
-\NC $\Lint$ \NC $5$ \NC $5$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $1.55$s \VL $0.03$s \NC\NR
+\NC $\Lint$ \NC 5 \NC 5 \VL 0.00 \NC \color[darkgray]{0.00} \VL 1.55 \VL 0.03 \NC\NR
 \stoptabulate
 
 The results for structured automata show a clear effect of the extra structure.
@@ -742,7 +749,7 @@ In contrast, \ONS{} benefits little from the extra structure.
 Despite this, it remains viable: even for the larger cases it falls behind significantly only for the largest FIFO automaton and the two largest $ww$ automata.
 
 
-\stopsubsubsection
+\stopsubsubject
 \stopsubsection
 \startsubsection
   [title={Learning nominal automata}]
@@ -758,17 +765,18 @@ Formally, the oracle can answer two types of queries:
 \stopitemize
 With these queries, the \LStar{} algorithm can learn regular languages efficiently \citep[DBLP:journals/iandc/Angluin87].
 In particular, it learns the unique minimal automaton for $\lang$ using only finitely many queries.
-The \LStar{} algorithm has been generalised to \nLStar{} in order to learn \emph{nominal} regular languages \citep[MoermanS0KS17].
+The \LStar{} algorithm has been generalised to \nLStar{} in order to learn \emph{nominal} regular languages.
 In particular, it learns a nominal DFA (over an infinite alphabet) using only finitely many queries.
 We implement \nLStar{} in the presented library and compare it to its previous implementation in \NLambda{}.
 The algorithm is not polynomial, unlike the minimisation algorithm described above.
 However, the authors conjecture that there is a polynomial algorithm.
 \footnote{See \href{joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html} for a sketch of the polynomial algorithm.}
+\todo{\emph{The authors} ben ik...}
 For the correctness, termination, and comparison with other learning algorithms see \in{Chapter}[chap:learning-nominal-automata].
 
 
-\startsubsubsection
+\startsubsubject
-  [title={Implementations.}]
+  [title={Implementations}]
 
 Both implementations in \NLambda{} and \ONS{} are direct implementations of the pseudocode for \nLStar{} with no further optimisations.
 The authors of \LOIS{} implemented \nLStar{} in their library as well.
@@ -783,15 +791,15 @@ For that reason, we run the \NLambda{} implementation using both the equality sy
 For the languages $\Lmax$, $\Lint$ and the random automata, we can only use the total order symmetry.
 
 To run the \nLStar{} algorithm, we implement an external oracle for the membership queries.
-This is akin to the application of learning black box systems \citep[Vaandrager17].
+This is akin to the application of learning black box systems (see \citenp[Vaandrager17]).
 For equivalence queries, we constructed counterexamples by hand.
 All implementations receive the same counterexamples.
 We measure CPU time instead of real time, so that we do not account for the external oracle.
 
 
-\stopsubsubsection
+\stopsubsubject
-\startsubsubsection
+\startsubsubject
-  [title={Results.}]
+  [title={Results}]
 
 The results (\in{Table}[learning_results]) for random automata show an advantage for \ONS{}.
 Additionally, we report the number of membership queries,
@@ -807,31 +815,32 @@ It is interesting to see that these languages can be learned more efficiently by
 
 \placetable[here][learning_results]
 {Running times and number of membership queries for the \nLStar{} algorithm.
-For \NLambda{} we used two version: \NLambda{}$^{\mathit{ord}}$ uses the total order symmetry \NLambda{}$^{\mathit{eq}}$ uses the equality symmetry.}
+For \NLambda{} we used two version: \NLambda{}$^{\mathit{ord}}$ uses the total order symmetry \NLambda{}$^{\mathit{eq}}$ uses the equality symmetry.
-\starttabulate[|l|l|l|r|r|r|r|r|r|][distance=none]
+Timeouts are indicated by $\infty$.}
+\starttabulate[|l|c|c|cg(.)|r|cg(.)|r|cg(.)|r|][distance=none]
 \NC \NC \NC \VL \NC \ONS{} \VL \NC \NLambda{}$^{\mathit{ord}}$ \VL \NC \NLambda{}$^{\mathit{eq}}$ \NC\NR
-\NC Model \NC $\Nsize(S)$ \NC $\dim(S)$ \VL time \NC MQs \VL time \NC MQs \VL time \NC MQs \NC\NR
+\NC Model \NC $\Nsize(S)$ \NC $\dim(S)$ \VL time (s) \NC MQs \VL time (s) \NC MQs \VL time (s) \NC MQs \NC\NR
 \HL
-\NC rand$_{5,1}$ \NC $4$  \NC $1$ \VL $2$m $7$s  \NC $2321$   \VL $39$m $51$s \NC $1243$ \VL  \NC \NC\NR
+\NC rand$_{5,1}$ \NC 4  \NC 1 \VL 127      \NC 2321   \VL 2391     \NC 1243 \VL  \NC \NC\NR
-\NC rand$_{5,1}$ \NC $5$  \NC $1$ \VL $0.12$s    \NC $404$    \VL $40$m $34$s \NC $435$  \VL  \NC \NC\NR
+\NC rand$_{5,1}$ \NC 5  \NC 1 \VL 0.12     \NC 404    \VL 2434     \NC 435  \VL  \NC \NC\NR
-\NC rand$_{5,1}$ \NC $3$  \NC $0$ \VL $0.86$s    \NC $499$    \VL $30$m $19$s \NC $422$  \VL  \NC \NC\NR
+\NC rand$_{5,1}$ \NC 3  \NC 0 \VL 0.86     \NC 499    \VL 1819     \NC 422  \VL  \NC \NC\NR
-\NC rand$_{5,1}$ \NC $5$  \NC $1$ \VL $> 60$m    \NC n/a      \VL $> 60$m     \NC n/a    \VL  \NC \NC\NR
+\NC rand$_{5,1}$ \NC 5  \NC 1 \VL $\infty$ \NC n/a    \VL $\infty$ \NC n/a  \VL  \NC \NC\NR
-\NC rand$_{5,1}$ \NC $4$  \NC $1$ \VL $0.08$s    \NC $387$    \VL $34$m $57$s \NC $387$  \VL  \NC \NC\NR
+\NC rand$_{5,1}$ \NC 4  \NC 1 \VL 0.08     \NC 387    \VL 2097     \NC 387  \VL  \NC \NC\NR
 \HL
-\NC FIFO$(1)$    \NC $3$  \NC $1$ \VL $0.04$s    \NC $119$    \VL $3.17$s     \NC $119$  \VL $1.76$s    \NC $51$   \NC\NR
+\NC FIFO$(1)$    \NC 3  \NC 1 \VL 0.04     \NC 119    \VL 3.17     \NC 119  \VL 1.76     \NC 51   \NC\NR
-\NC FIFO$(2)$    \NC $6$  \NC $2$ \VL $1.73$s    \NC $2655$   \VL $6$m $32$s  \NC $3818$ \VL $40.00$s   \NC $434$  \NC\NR
+\NC FIFO$(2)$    \NC 6  \NC 2 \VL 1.73     \NC 2655   \VL 392      \NC 3818 \VL 40.00    \NC 434  \NC\NR
-\NC FIFO$(3)$    \NC $19$ \NC $3$ \VL $46$m $34$s\NC $298400$ \VL $> 60$m     \NC n/a    \VL $34$m $7$s \NC $8151$ \NC\NR
+\NC FIFO$(3)$    \NC 19 \NC 3 \VL 2794     \NC 298400 \VL $\infty$ \NC n/a  \VL 2047     \NC 8151 \NC\NR
 \HL
-\NC $ww(1)$      \NC $4$  \NC $1$ \VL $0.42$s    \NC $134$    \VL $2.49$s     \NC $77$   \VL $1.47$s   \NC $30$  \NC\NR
+\NC $ww(1)$      \NC 4  \NC 1 \VL 0.42     \NC 134    \VL 2.49     \NC 77   \VL 1.47     \NC 30   \NC\NR
-\NC $ww(2)$      \NC $8$  \NC $2$ \VL $4$m $26$s \NC $3671$   \VL $3$m $48$s  \NC $2140$ \VL $30.58$s  \NC $237$ \NC\NR
+\NC $ww(2)$      \NC 8  \NC 2 \VL 266      \NC 3671   \VL 228      \NC 2140 \VL 30.58    \NC 237  \NC\NR
-\NC $ww(3)$      \NC $24$ \NC $3$ \VL $> 60$m    \NC n/a      \VL $> 60$m     \NC n/a    \VL $> 60$m   \NC n/a \NC\NR
+\NC $ww(3)$      \NC 24 \NC 3 \VL $\infty$ \NC n/a    \VL $\infty$ \NC n/a  \VL $\infty$ \NC n/a  \NC\NR
 \HL
-\NC $\Lmax$      \NC $3$ \NC $1$  \VL $0.01$s    \NC $54$     \VL $3.58$s     \NC $54$   \VL \NC \NC\NR
+\NC $\Lmax$      \NC 3 \NC 1  \VL 0.01     \NC 54     \VL 3.58     \NC 54   \VL \NC \NC\NR
-\NC $\Lint$      \NC $5$ \NC $2$  \VL $0.59$s    \NC $478$    \VL $1$m $23$s  \NC $478$  \VL \NC \NC\NR
+\NC $\Lint$      \NC 5 \NC 2  \VL 0.59     \NC 478    \VL 83       \NC 478  \VL \NC \NC\NR
 \stoptabulate
 
 
-\stopsubsubsection
+\stopsubsubject
 \stopsubsection
 \stopsection
 \startsection
@@ -850,13 +859,13 @@ For programmers this means they can think of infinite sets without having to kno
 
 It is worth mentioning that an older (unreleased) version of \NLambda{} implemented nominal sets with orbits instead of SMT solvers \citep[DBLP:conf/popl/BojanczykBKL12].
 However, instead of characterising orbits (e.g., by its dimension), they represent orbits by a representative element.
-The authors of \NLambda{} have reported that the current version is faster \citep[DBLP:journals/corr/KlinS16].
+\citet[DBLP:journals/corr/KlinS16] reported that the current version is faster.
 
-The theoretical foundation of our work is the main representation theorem in \citep[DBLP:journals/corr/BojanczykKL14].
+The theoretical foundation of our work is the main representation theorem by \citet[DBLP:journals/corr/BojanczykKL14].
 We improve on that by instantiating it to the total order symmetry and distil a concrete representation of nominal sets.
-As far as we know, we provide the first implementation of the representation theory in \citep[DBLP:journals/corr/BojanczykKL14].
+As far as we know, we provide the first implementation of their representation theory.
 
-Another tool using nominal sets is Mihda \citep[FerrariMT05].
+Another tool using nominal sets is Mihda by \citet[FerrariMT05].
 Here, only the equality symmetry is implemented.
 This tool implements a translation from $\pi$-calculus to history-dependent automata (HD-automata) with the aim of minimisation and checking bisimilarity.
 The implementation in OCaml is based on \emph{named sets}, which are finite representations for nominal sets.
@@ -879,7 +888,7 @@ As a consequence, all the complexity required to deal with groups vanishes.
 Rather, the complexity is transferred to the input of our algorithms, because automata over the equality symmetry require more orbits when expressed over the total order symmetry.
 Another difference is that register automata allow for duplicate values in the registers.
 In nominal automata, such configurations will be encoded in different orbits.
-An interesting open problem is whether equivalence of unique-valued register automata is in {\sc Ptime} \citep[MurawskiRT15].
+\todo{Equivalentie is polynomiaal: \cite[MurawskiRT18].}
 
 Orthogonal to nominal automata, there is the notion of symbolic automata \citep[DBLP:conf/cav/DAntoniV17, MalerM17].
 These automata are also defined over infinite alphabets but they use predicates on transitions, instead of relying on symmetries.

content/test-methods.tex

@@ -5,17 +5,18 @@
   [title={FSM-based Test Methods},
    reference=chap:test-methods]
 
-In this chapter we will discuss some of the theory of test generation methods for black box conformance testing.
+In this chapter, we will discuss some of the theory of test generation methods for black box conformance testing.
 Since the systems we consider are black box, we cannot simply determine equivalence with a specification.
 The only way to gain confidence is to perform experiments on the system.
 A key aspect of test generation methods is the size and completeness of the test suites.
 On one hand, we want to cover as much as the specification as possible, hopefully ensuring that we find mistakes in any faulty implementation.
 On the other hand: testing takes time, so we want to minimise the size of a test suite.
 
+\todo{Theoretische bijdrage scherper maken}
 The test methods described here are well-known in the literature of FSM-based testing.
 They all share similar concepts, such as \emph{access sequences} and \emph{state identifiers}.
 In this chapter we will define these concepts, relate them with one another and show how to build test suites from these concepts.
-From this theoretical discussion we derive a new algorithm: the \emph{hybrid ADS methods}, which is applied on an industrial case study in \in{Chapter}[chap:applying-automata-learning].
+From this theoretical discussion we derive a new algorithm: the \emph{hybrid ADS methods}, which is applied to an industrial case study in \in{Chapter}[chap:applying-automata-learning].
 
 This chapter starts with the basics: Mealy machines, sequences and what it means to test a black box system.
 Then, starting from \in{Section}[sec:separating-sequences] we define several concepts, such as state identifiers, in order to distinguish one state from another.
@@ -23,7 +24,7 @@ These concepts are then combined in \in{Section}[sec:methods] to derive test sui
 In a similar vein, we define a novel test method in \in{Section}[sec:hybrid] and we discuss some of the implementation details of the \kw{hybrid-ads} tool.
 We summarise the various test methods in \in{Section}[sec:overview].
 All methods are proven to be $n$-complete in \in{Section}[sec:completeness].
-Finally, in \in{Section}[sec:discussion], we give related work.
+Finally, in \in{Section}[sec:discussion], we discuss related work.
 
 
 \startsection
@@ -37,7 +38,7 @@ $uv$ for the concatenation of two sequences $u, v \in I^{\ast}$ and $|u|$ for th
 For a sequence $w = uv$ we say that $u$ and $v$ are a prefix and suffix respectively.
 
 \startdefinition
-A \emph{Mealy machine} $M$ consists of a finite set of \emph{states} $S$, an \emph{initial state} $s_0 \in S$ and two functions:
+A (deterministic and complete) \emph{Mealy machine} $M$ consists of a finite set of \emph{states} $S$, an \emph{initial state} $s_0 \in S$ and two functions:
 \startitemize
 \item a \emph{transition function} $\delta \colon S \times I \to S$, and
 \item an \emph{output function} $\lambda \colon S \times I \to O$.
@@ -55,15 +56,13 @@ Two states $s$ and $t$ are \emph{equivalent} if they have equal behaviours, writ
 
 \startremark
 We will use the following conventions and notation.
-We often write $s \in M$ instead of $s \in S$ and for a second Mealy machine $M'$ its members are denoted $S', s'_0, \delta'$ and $\lambda'$.
+We often write $s \in M$ instead of $s \in S$ and for a second Mealy machine $M'$ its constituents are denoted $S', s'_0, \delta'$ and $\lambda'$.
 Moreover, if we have a state $s \in M$, we silently assume that $s$ is not a member of any other Mealy machine $M'$.
 (In other words, the behaviour of $s$ is determined by the state itself.)
 This eases the notation since we can write $s \sim t$ without needing to introduce a context.
 \stopremark
 
 An example Mealy machine is given in \in{Figure}[fig:running-example].
-We note that a Mealy machine is deterministic and complete by definition.
-This means that for each state $s$ and each word $w$, there is a unique state $t$ by running the word $w$ from $s$.
 
 \startplacefigure
   [title={An example specification with input $I=\{a,b,c\}$ and output $O=\{0,1\}$.},
@@ -102,10 +101,11 @@ This means that for each state $s$ and each word $w$, there is a unique state $t
 
 In conformance testing we have a specification modelled as a Mealy machine and an implementation (the system under test, or SUT) which we assume to behave as a Mealy machine.
 Tests, or experiments, are generated from the specification and applied to the implementation. We assume that we can reset the implementation before every test.
-If the output is different than the specified output, then we know the implementation is flawed.
+If the output is different from the specified output, then we know the implementation is flawed.
 The goals is to test as little as possible, while covering as much as possible.
 
 We assume the following
+\todo{Herhaling van paragraaf hiervoor}
 \startitemize[after]
 \item
 The system can be modelled as Mealy machine.
@@ -143,7 +143,7 @@ $||T|| = \sum\limits_{t \in max(T)} (|t| + 1)$.
 Consider the specification in \in{Figure}{a}[fig:incompleteness-example].
 This machine will always outputs a cup of coffee -- when given money.
 For any test suite we can make a faulty implementation which passes the test suite.
-A faulty implementation might look like \in{Figure}{b}[fig:incompleteness-example], where the machine starts to output bombs after $n$ steps.
+A faulty implementation might look like \in{Figure}{b}[fig:incompleteness-example], where the machine starts to output bombs after $n$ steps, where $n$ is larger than the length of the longest sequence in the suite.
 This shows that no test-suite can be complete and it justifies the following definition.
 
 \startplacefigure
@@ -196,12 +196,13 @@ This is crucial for black box testing, as we do not know the implementation, so
 
 Before we construct test suites, we discuss several types of useful sequences.
 All the following notions are standard in the literature, and the corresponding references will be given in \in{Section}[sec:methods], where we discuss the test generation methods using these notions.
-We fix a Mealy machine $M$.
+We fix a Mealy machine $M$ for the remainder of this chapter.
-For convenience we assume $M$ to be minimal, this implies that distinct states are, in fact, inequivalent.
+\todo{Checken of dit echt het geval is!}
+For convenience we assume $M$ to be minimal, so that distinct states are, in fact, inequivalent.
 All definitions can be generalised to non-minimal $M$, by replacing the word \quote{distinct} (or \quote{other}) with \quote{inequivalent}.
 
 \startdefinition
-Given a Mealy machine $M$ we define the following kinds of sequences.
+We define the following kinds of sequences.
 \startitemize
 \item Given two states $s, t$ in $M$ we say that $w$ is a \defn{separating sequence} if $\lambda(s, w) \neq \lambda(t, w)$.
 \item For a single state $s$ in $M$, a sequence $w$ is a \defn{unique input output sequence (UIO)} if for every other state $t$ in $M$ we have $\lambda(s, w) \neq \lambda(t, w)$.
@@ -237,7 +238,7 @@ As the example shows, we need sets of sequences and sometimes even sets of sets
 \footnote{A family of often written as $\{X_s\}_{s \in M}$ or simply $\{X_s\}_{s}$, meaning that for each state $s \in M$ we have a set $X_s$.}
 
 \startdefinition
-Given a Mealy machine $M$, we define the following kinds of sets of sequences.
+We define the following kinds of sets of sequences.
 We require that all sets are \emph{prefix-closed}, however, we only show the maximal sequences in examples.
 \footnote{Taking these sets to be prefix-closed makes many proofs easier.}
 \startitemize
@@ -255,6 +256,7 @@ We return to this notion in more detail in \in{Example}[ex:uio-counterexample].
 
 We may obtain a characterisation set by taking the union of state identifiers for each state.
 For every machine we can construct a set of harmonised state identifiers as will be shown in \in{Chapter}[chap:separating-sequences] and hence every machine has a characterisation set.
+\todo{Iets versimpelen}
 
 \startexample
 As mentioned before, state $s_2$ from \in{Figure}[fig:running-example] has a state identifier $\{aa, ac, b\}$.
@@ -361,8 +363,7 @@ Two states $x, y$ are \emph{$\Fam{W}$-equivalent}, written $x \sim_{\Fam{W}} y$,
 \stopitemize
 \stopdefinition
 
-Both relations are equivalence relations.
+The relation $\sim_W$ is an equivalence relation and $W \subseteq V$ implies that $V$ separates more states than $W$, i.e., $x \sim_V y \implies x \sim_W y$.
-Moreover, $W \subseteq V$ implies that $V$ separates more states than $W$, i.e., $x \sim_V y \implies x \sim_W y$.
 Clearly, if two states are equivalent (i.e., $s \sim t$), then for any set $W$ we have $s \sim_W t$.
 
 
@@ -375,7 +376,7 @@ Besides sequences which separate states, we also need sequences which brings a m
 \startdefinition
 An \emph{access sequence for $s$} is a word $w$ such that $\delta(s_0, w) = s$.
 A set $P$ consisting of an access sequence for each state is called a \emph{state cover}.
-If $P$ is a state cover, then $P \cdot I$ is called a \emph{transition cover}.
+If $P$ is a state cover, then the set $\{ p a \mid p \in P, a \in I \}$ is called a \emph{transition cover}.
 \stopdefinition
 
 
@@ -398,10 +399,13 @@ On families we define
 \item union: $\Fam{X} \cup \Fam{Y}$ is defined point-wise:
 $(\Fam{X} \cup \Fam{Y})_s = X_s \cup Y_s$,
 \item concatenation:
+\todo{Associativiteit?}
 $X \odot \Fam{Y} = \{ xy \mid x \in X, y \in Y_{\delta(s_0, x)} \}$, and
 \item refinement: $\Fam{X} ; \Fam{Y}$ defined by
+\footnote{We use the convention that $\cap$ binds stronger than $\cup$.
+In fact, all the operators here bind stronger than $\cup$.}
 \startformula
-(\Fam{X} ; \Fam{Y})_s = X_s \,\cup\, Y_s \cap \bigcup_{s \sim_{\Fam{X}} t} Y_t.
+(\Fam{X} ; \Fam{Y})_s = X_s \,\cup\, Y_s \!\cap\! \bigcup_{s \sim_{\Fam{X}} t} Y_t.
 \stopformula
 \stopitemize
 
@@ -435,7 +439,7 @@ Our hybrid ADS method uses a similar construction.
 
 There are many more test generation methods.
 Literature shows, however, that not all of them are complete.
-For example, the method by \citet[DBLP:journals/tosem/Bernhard94] are falsified by \citet[DBLP:journals/tosem/Petrenko97] and the UIO-method from \citet[DBLP:journals/cn/SabnaniD88] is shown to be incomplete by \citet[DBLP:conf/sigcomm/ChanVO89].
+For example, the method by \citet[DBLP:journals/tosem/Bernhard94] is falsified by \citet[DBLP:journals/tosem/Petrenko97], and the UIO-method from \citet[DBLP:journals/cn/SabnaniD88] is shown to be incomplete by \citet[DBLP:conf/sigcomm/ChanVO89].
 For that reason, completeness of the correct methods is shown in \in{Theorem}[thm:completeness].
 The proof is general enough to capture all the methods at once.
 We fix a state cover $P$ throughout this section and take the transition cover $Q = P \cdot I$.
@@ -446,6 +450,7 @@ We fix a state cover $P$ throughout this section and take the transition cover $
    reference=sec:w]
 
 After the work of \citet[Moore56], it was unclear whether a test suite of polynomial size could exist.
+\todo{Melden dat Moore een exp. suite gaf, en dat een poly suite open is.}
 Both \citet[DBLP:journals/tse/Chow78, Vasilevskii73] independently prove that such a test suite exists.
 \footnote{More precisely: the size of $T_{\text{W}}$ is polynomial in the size of the specification for each fixed $k$.}
 The W method is a very structured test suite construction.
@@ -453,8 +458,7 @@ It is called the W method as the characterisation set is often called $W$.
 
 \startdefinition
   [reference=w-method]
-Let $W$ be a characterisation set, the \defn{W test suite} is
+Given a characterisation set $W$, we define the \defn{W test suite} as
-defined as
 \startformula
 T_{\text{W}} = (P \cup Q) \cdot I^{\leq k} \cdot W .
 \stopformula
@@ -464,7 +468,7 @@ This -- and all following methods -- tests the machine in two phases.
 For simplicity, we explain these phases when $k = 0$.
 The first phase consists of the tests $P \cdot W$ and tests whether all states of the specification are (roughly) present in the implementation.
 The second phase is $Q \cdot W$ and tests whether the successor states are correct.
-Together, these two phases put enough constraints on the implementation to know that the implementation and specification coincide.
+Together, these two phases put enough constraints on the implementation to know that the implementation and specification coincide (provided that the implementation has no more states than the specification).
 
 
 \stopsubsection
@@ -472,14 +476,14 @@ Together, these two phases put enough constraints on the implementation to know
   [title={The Wp-method \cite[DBLP:journals/tse/FujiwaraBKAG91]},
    reference=sec:wp]
 
-\citet[DBLP:journals/tse/FujiwaraBKAG91] realised that one needs less tests in the second phase of the W method.
+\citet[DBLP:journals/tse/FujiwaraBKAG91] realised that one needs fewer tests in the second phase of the W method.
 Since we already know the right states are present after phase one, we only need to check if the state after a transition is consistent with the expected state.
 This justifies the use of state identifiers for each state.
 
 \startdefinition
   [reference={state-identifier,wp-method}]
-Let $\Fam{W}$ be a family of state identifiers, the \defn{Wp test suite} is
+Let $\Fam{W}$ be a family of state identifiers.
-defined as
+The \defn{Wp test suite} is defined as
 \startformula
 T_{\text{Wp}} = P \cdot I^{\leq k} \cdot \bigcup \Fam{W} \,\cup\, Q \cdot I^{\leq k}
 \odot \Fam{W}.
@@ -497,17 +501,19 @@ Once states are tested as such, we can use the smaller sets $W_s$ for testing tr
    reference=sec:hsi]
 
 The Wp-method in turn was refined by \citet[LuoPB95, YevtushenkoP90].
-They make use of so called \emph{harmonised} state identifiers, allowing to take state identifiers in the initial phase of the test suite.
+They make use of harmonised state identifiers, allowing to take state identifiers in the initial phase of the test suite.
+\todo{Even de chronologie checken.}
 
 \startdefinition
   [reference=hsi-method]
-Let $\Fam{H}$ be a separating family, the \defn{HSI test suite} is defined as
+Let $\Fam{H}$ be a separating family.
+We define the \defn{HSI test suite} by
 \startformula
 T_{\text{HSI}} = (P \cup Q) \cdot I^{\leq k} \odot \Fam{H}.
 \stopformula
 \stopdefinition
 
-Our newly described test method is an instance of the HSI-method.
+Our hybrid ADS method is an instance of the HSI-method as we define it here.
 However, \citet[LuoPB95, YevtushenkoP90] describe the HSI-method together with a specific way of generating the separating families.
 Namely, the set obtained by a splitting tree with shortest witnesses.
 
@@ -517,12 +523,13 @@ Namely, the set obtained by a splitting tree with shortest witnesses.
   [title={The ADS-method \cite[DBLP:journals/tc/LeeY94]},
    reference=sec:ads]
 
-As discussed before, when a Mealy machine admits a adaptive distinguishing sequence, only one test has to be performed for identifying a state.
+As discussed before, when a Mealy machine admits a adaptive distinguishing sequence, only a single test has to be performed for identifying a state.
 This is exploited in the ADS-method.
 
 \startdefinition
   [reference=ds-method]
-Let $\Fam{Z}$ be a separating family where every set is a singleton, the \defn{ADS test suite} is defined as
+Let $\Fam{Z}$ be an adaptive distinguishing sequence.
+The \defn{ADS test suite} is defined as
 \startformula
 T_{\text{ADS}} = (P \cup Q) \cdot I^{\leq k} \odot \Fam{Z}.
 \stopformula
@@ -549,12 +556,11 @@ T_{\text{UIOv}} = P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\
 
 One might think that using a single UIO sequence instead of the set $\bigcup \Fam{U}$ to verify the state is enough.
 In fact, this idea was used for the \emph{UIO-method} which defines the test suite $(P \cup Q) \cdot I^{\leq k} \odot \Fam{U}$.
-The following is a counterexample to such conjecture.
+The following is a counterexample, due to \citet[DBLP:conf/sigcomm/ChanVO89], to such conjecture.
-(This counterexample is due to \citenp[DBLP:conf/sigcomm/ChanVO89].)
 
 \startexample
   [reference=ex:uio-counterexample]
-The example in \in{Figure}[fig:uio-counterexample] shows that UIO-method does not define a 3-complete test suite.
+The Mealy machines in \in{Figure}[fig:uio-counterexample] shows that UIO-method does not define a 3-complete test suite.
 Take for example the UIOs $u_0 = aa, u_1 = a, u_2 = ba$ for the states $s_0, s_1, s_2$ respectively.
 The test suite then becomes $\{ aaaa, abba, baaa, bba \}$ and the faulty implementation passes this suite.
 This happens because the sequence $u_2$ is not an UIO in the implementation, and the state $s'_2$ simulates both UIOs $u_1$ and $u_2$.
@@ -599,6 +605,7 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
   [title={Example},
    reference=sec:all-example]
 
+\todo{Beetje raar om Example Example te hebben.}
 Let us compute all the previous test suites on the specification in \in{Figure}[fig:running-example].
 We will be testing without extra states, i.e., we construct 5-complete test suites.
 We start by defining the state and transition cover.
@@ -609,7 +616,7 @@ For this, we simply take all shortest sequences from the initial state to the ot
 \stopalign\stopformula
 
 As shown earlier, the set $W = \{ aa, ac, c \}$ is a characterisation set.
-The the W-method gives the following test suite of size 169:
+Then the W-method gives the following test suite of size 169:
 \startformula\startmathmatrix[n=2,align={left,left}]
 \NC T_{\text{W}} = \{ \NC aaaaa, aaaac, aaac, aabaa, aabac, aabc, aacaa, \NR
 \NC \NC aacac, aacc, abaa, abac, abc, acaa, acac, acc, baaaa, \NR
@@ -629,13 +636,13 @@ This defines the following family $\Fam{W}$:
 \stopformulas
 For the first part of the Wp test suite we need $\bigcup \Fam{W} = \{ aa, ac, c \}$.
 For the second part, we only combine the sequences in the transition cover with the corresponding suffixes.
-All in al we get a test suite of size 75:
+All in all we get a test suite of size 75:
 \startformula\startmathmatrix[n=2,align={left,left}]
 \NC T_{\text{Wp}} = \{ \NC aaaaa, aaaac, aaac, aabaa, aacaa, abaa, \NR
 \NC \NC acaa, baaac, baac, babaa, bacc, bbac, bcaa, caa \quad \} \NR
 \stopmathmatrix\stopformula
 
-For the HSI method we need a separating family.
+For the HSI method we need a separating family $\Fam{H}$.
 We pick the following sets:
 \startformulas
 \startformula H_0 = \{ aa, c \}     \stopformula
@@ -644,6 +651,7 @@ We pick the following sets:
 \startformula H_3 = \{ a, c \}      \stopformula
 \startformula H_4 = \{ aa, ac, c \} \stopformula
 \stopformulas
+(We repeat that these sets are prefix-closed, but we only show the maximal sequences.)
 Note that these sets are harmonised, unlike the family $\Fam{W}$.
 For example, the separating sequence $a$ is contained in both $H_1$ and $H_3$.
 This ensures that we do not have to consider $\bigcup \Fam{H}$ in the first part of the test suite.
@@ -696,14 +704,14 @@ Yet, all the test suites detect this error.
 When choosing the prefix $aaa$ (included in the transition cover), and suffix $aa$ (included in the characterisation set and state identifiers for $s_2$), we see that the specification outputs $10111$ and the implementation outputs $10110$.
 The sequence $aaaaa$ is the only sequence (in any of the test suites here) which detects this fault.
 
-If on the other hand, the $a$-transition from $s'_2$ would transition to $s'_4$, we need the suffix $ac$ as $aa$ will not detect the fault.
+Alternatively, the $a$-transition from $s'_2$ would transition to $s'_4$, we need the suffix $ac$ as $aa$ will not detect the fault.
 Since the sequences $ac$ is included in the state identifier for $s_2$, this fault would also be detected.
 This shows that it is sometimes necessary to include multiple sequences in the state identifier.
 
 Another approach to testing would be to enumerate all sequences up to a certain length.
 In this example, we need sequences of at least length 5.
 Consequently, the test suite contains 243 sequences and this boils down to a size of 1458.
-Such a brute-force approach is hence not scalable.
+Such a brute-force approach is not scalable.
 
 
 \stopsubsection
@@ -712,15 +720,15 @@ Such a brute-force approach is hence not scalable.
   [title={Hybrid ADS method},
    reference=sec:hybrid]
 
-In this section we describe a new test generation method for Mealy machines.
+In this section, we describe a new test generation method for Mealy machines.
-Its completeness will be proven in a later section, together with completeness for all methods defined in this section.
+Its completeness will be proven in \in{Theorem}[thm:completeness], together with completeness for all methods defined in the previous section.
 From a high level perspective, the method uses the algorithm by \cite[authoryears][DBLP:journals/tc/LeeY94] to obtain an ADS.
 If no ADS exists, their algorithm still provides some sequences which separates some inequivalent states.
 Our extension is to refine the set of sequences by using pairwise separating sequences.
 Hence, this method is a hybrid between the ADS-method and HSI-method.
 
 The reason we do this is the fact that the ADS-method generally constructs small test suites as experiments by \cite[authoryears][DBLP:journals/infsof/DorofeevaEMCY10] suggest.
-The test suites are small since an ads can identify a state with a single word, instead of a set of words which is generally needed.
+The test suites are small since an ADS can identify a state with a single word, instead of a set of words which is generally needed.
 Even if the ADS does not exist, using the partial result of Lee and Yannakakis' algorithm can reduce the size of test suites.
 
 We will now see the construction of this hybrid method.
@@ -730,7 +738,7 @@ This is a data structure which is used to construct separating families or adapt
 \startdefinition[reference=splitting-tree]
 A \defn{splitting tree (for $M$)} is a rooted tree where each node $u$ has
 \startitemize
-	\item a set of states $l(u) \subseteq M$, and
+	\item a non-empty set of states $l(u) \subseteq M$, and
 	\item if $u$ is not a leaf, a sequence $\sigma(u) \in I^{\ast}$.
 \stopitemize
 We require that if a node $u$ has children $C(u)$ then
@@ -828,7 +836,7 @@ Its $m$-completeness is proven in \in{Section}[sec:completeness].
 Let $P$ be a state cover, $\Fam{Z'}$ be a family of sets constructed with the Lee and Yannakakis algorithm, and $\Fam{H}$ be a separating family.
 The \defn{hybrid ADS} test suite is
 \startformula
-T_{\text{h-ADS}} = P \cdot I^{\leq k+1} \odot (\Fam{Z'} ; \Fam{H}).
+T_{\text{h-ADS}} = (P \cup Q) \cdot I^{\leq k} \odot (\Fam{Z'} ; \Fam{H}).
 \stopformula
 \stopdefinition
 
@@ -982,6 +990,8 @@ The following test suites are all $n+k$-complete:
 \stoptabulate}
 \stoptheorem
 
+\todo{Nog iets zeggen over $(P \cup Q) \cdot I^{\leq k} = P \cdot I^{\leq k+1}$?}
+
 It should be noted that the ADS-method is a specific instance of the HSI-method and similarly the UIOv-method is an instance of the Wp-method.
 What is generally meant by the Wp-method and HSI-method is the above formula together with a particular way to obtain the (harmonised) state identifiers.
 
@@ -1120,7 +1130,7 @@ The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
 
 \todo{Veel gerelateerd werk kan naar de grote intro.}
 
-In this chapter we have mostly considered classical test methods which are all based on prefixes and state identifiers.
+In this chapter, we have mostly considered classical test methods which are all based on prefixes and state identifiers.
 There are more recent methods which almost fit in the same framework.
 We mention the P \citep[SimaoP10], H \citep[DorofeevaEY05], and SPY \citep[SimaoPY09] methods.
 The P method construct a test suite by carefully considering sufficient conditions for a $p$-complete test suite (here $p \leq n$, where $n$ is the number of states).
@@ -1140,17 +1150,19 @@ Our method becomes complete by refining the tests with pairwise separating seque
 Some work is put into minimising the adaptive distinguishing sequences themselves.
 \citet[DBLP:journals/fmsd/TurkerY14] describe greedy algorithms which construct small adaptive distinguishing sequences.
 Moreover, they show that finding the minimal adaptive distinguishing sequence is NP-complete in general, even approximation is NP-complete.
-We expect that similar heuristics also exist for the other test methods and that it will improve the performance.
+We expect that similar heuristics also exist for the other test methods and that they will improve the performance.
 Note that minimal separating sequences do not guarantee a minimal test suite.
 In fact, we see that the hybrid ADS method outperforms the HSI method on the example in \in{Figure}[fig:running-example] since it prefers longer, but fewer, sequences.
 
 Some of the assumptions made at the start of this chapter have also been challenged.
 For non-deterministic Mealy machine, we mention the work of \citet[PetrenkoY14].
-For input/output transition systems with the \emph{ioco} relation we mention the work of \citet[BosJM17, SimaoP14].
+We also mention the work of \citet[BosJM17, SimaoP14] for input/output transition systems with the \emph{ioco} relation.
 In both cases, the test suites are still defined in the same way as in this chapter: prefixes followed by state identifiers.
 However, for non-deterministic systems, guiding an implementation into a state is harder as the implementation may choose its own path.
 For that reason, sequences are often replaced by automata, so that the testing can be adaptive.
+This adaptive testing is game-theoretic and the automaton provides a strategy.
 This game theoretic point of view is further investigated by \citet[BosS18].
+\todo{Niet zo helder.}
 The test suites generally are of exponential size, depending on how non-deterministic the systems are.
 
 The assumption that the implementation is resettable is also challenged early on.