Nog meer todos gedaan

content/introduction.tex

@@ -58,7 +58,7 @@ In her framework, the learning algorithm may pose two types of queries to a \emp
 \description{Membership queries (MQs)}
 The learner poses such a query by providing a word $w \in \Sigma^{*}$ to the teacher.
 The teacher will then reply whether $w \in \lang$ or not.
-This type of query is often generalised to more general output, in these cases we consider $\lang \colon \Sigma^\ast \to O$ and the teacher replies whether $\lang(w)$.
+This type of query is often generalised to more general output, in these cases we consider $\lang \colon \Sigma^\ast \to O$ and the teacher replies with $\lang(w)$.
 In some papers, such a query is then called an \emph{output query}.
 
 \description{Equivalence queries (EQs)}
@@ -390,18 +390,18 @@ Additionally, they generalise the work on nominal sets to other symmetries.
 The symmetries we encounter in this thesis are listed below, but other symmetries can be found in the literature.
 The symmetry directly corresponds to the data values (and operations) used in an automaton.
 The data values are often called \emph{atoms}.
-\startitemize[after]
+\startbigitemize
 \item
-The \quotation{equality symmetry}.
+The \emph{equality symmetry}.
 Here the domain can be any countably infinite set.
 We can take, for example, the set of strings we used before as the domain from which we take passwords.
 No further structure is used on this domain, meaning that any value is just as good as any other.
 The symmetries therefore consist of all bijections on this domain.
 \item
-The \quotation{total order symmetry}.
+The \emph{total order symmetry}.
 In this case, we take a countable infinite set with a dense total order.
 Typically, this means we use the rational numbers, $\Q$, as data values and symmetries which respect the ordering.
-\stopitemize
+\stopbigitemize
 
 
 \startsubsection
@@ -415,14 +415,14 @@ For automata, this allows us to talk about symmetries on the state space, the se
 
 In order to implement these sets algorithmically, we impose two finiteness requirements.
 Both properties can be expressed using only the group action.
-\startitemize[after]
+\startbigitemize
 \item
 Each element is \emph{finitely supported}.
 A way to think of this requirement is that each element is \quotation{constructed} out of finitely many data values.
 \item
 The set is \emph{orbit-finite}.
 This means that we can choose finitely many elements such that any other element is a permuted version of one of those elements.
-\stopitemize
+\stopbigitemize
 
 If we wish to model the automaton from \in{Figure}[fig:login-system] as a nominal automaton, then we can simply define the state space as
 \startformula
@@ -464,6 +464,11 @@ This chapter introduces test generation methods which can be used for learning.
 The methods are presented in a uniform way, which allows to give a single proof of completeness for all these methods.
 Moreover, the uniform presentation gives room to develop new test generation methods.
 One particular contribution (besides the theoretical framework) is the new \emph{hybrid ADS} test generation method.
+The main contributions are:
+\startitemize[before, after]
+\item Uniform description of known methods: \in{Theorem}[thm:completeness] (p. \at[thm:completeness])
+\item New algorithm with implementation: \in{Section}[sec:hybrid-ads-impementation] (p. \at[sec:hybrid-ads-impementation])
+\stopitemize
 \stopdescription
 
 \startdescription[title={\in{Chapter}[chap:applying-automata-learning]: Applying automata learning to embedded control software.}]
@@ -471,10 +476,14 @@ In this chapter we will apply model learning to an industrial case study.
 It is a unique benchmark as it is much bigger than any of the applications seen before (3410 states and 77 inputs).
 This makes it challenging to learn a model and the main obstacle is finding counterexamples.
 Here, my main contribution is the new test generation method from \in{Chapter}[chap:test-methods].
+The main contributions are:
+\startitemize[before, after]
+\item Bla bla
+\stopitemize
 
-This is based on the following publication:
+\noindent This is based on the following publication:
 
-\cite[entry][DBLP:conf/icfem/SmeenkMVJ15].
+\noindent \cite[entry][DBLP:conf/icfem/SmeenkMVJ15].
 \stopdescription
 
 \startdescription[title={\in{Chapter}[chap:minimal-separating-sequences]: Minimal separating sequences for all pairs of states.}]

content/test-methods.tex

@@ -80,7 +80,7 @@ An example Mealy machine is given in \in{Figure}[fig:running-example].
 	\node[state] (3) [above right = of 0] {$s_3$};
 	\node[state] (4) [below right = of 0] {$s_4$};
 	\node        (5) [above = of 0] {};
-	\path[->]
+	\path[trans]
 	(5) edge (0)
 	(0) edge [bend left=]    node [below] {${a}/1$} (1)
 	(0) edge [bend right]    node [below] {${b}/0$} (4)
@@ -148,7 +148,7 @@ This shows that no test-suite can be complete and it justifies the following def
 {\hbox{
 	\starttikzpicture
 	\node[state] (0) {$s_0$};
-	\path[->]
+	\path[trans]
 	(0) edge [loop] node [below] {\money $/$ \coffee} (0);
 	\stoptikzpicture
 }} {(a)}
@@ -158,7 +158,7 @@ This shows that no test-suite can be complete and it justifies the following def
 	\node[state] (1) [right of=0] {$s'_1$};
 	\node        (2) [right of=1] {$\cdots$};
 	\node[state] (3) [right of=2] {$s'_n$};
-	\path[->]
+	\path[trans]
 	(0) edge [bend left] node [below] {\money $/$ \coffee} (1)
 	(1) edge [bend left] node [below] {\money $/$ \coffee} (2)
 	(2) edge [bend left] node [below] {\money $/$ \coffee} (3)
@@ -191,8 +191,8 @@ 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$ for the remainder of this chapter.
-\todo{Checken of dit echt het geval is!}
 For convenience, we assume $M$ to be minimal, so that distinct states are, in fact, inequivalent.
+(Or put differently: $s \sim t$ implies $s = t$.)
 All definitions can be generalised to non-minimal $M$, by replacing the word \quote{distinct} (or \quote{other}) with \quote{inequivalent}.
 
 \startdefinition
@@ -237,22 +237,22 @@ We require that all sets are \emph{prefix-closed}, however, we only show the max
 \footnote{Taking these sets to be prefix-closed makes many proofs easier.}
 \startitemize
 \item A set of sequences $W$ is a called a \defn{characterisation set} if it contains a separating sequence for each pair of distinct states in $M$.
-\item A \defn{state identifier} for a state $s \in M$ is a set $W_s$ which contains a separating sequence for every other state $t \in M$.
+\item A \defn{state identifier} for a state $s \in M$ is a set $W_s$ such that for every $t \in M$ a separating sequence for $s$ and $t$ exists in $W_s$.
-\todo{anders formuleren, want de sequence moet $s$ en $t$ onderscheiden.}
+\item A set of state identifiers $\{ W_s \}_{s}$ is \defn{harmonised} if $W_s \cap W_t$ contains a separating sequence for states $s$ and $t$.
-\item A set of state identifiers $\{ W_s \}_{s}$ is \defn{harmonised} if a separating sequence $w$ for states $s$ and $t$ exists in both $W_s$ and $W_t$.
 This is also called a \defn{separating family}.
-\todo{Iets formeler opschrijven?}
 \stopitemize
 \stopdefinition
 
+A state identifier $W_s$ will be used to test against a single state.
+In contrast to a characterisation set, it only include sequences which are relevant for $s$.
 The property of being harmonised might seem a bit strange.
-This property ensure that the same tests are used for different states.
+This property ensures that the same tests are used for different states.
 This extra consistency within a test suite is necessary for some test methods.
 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.
+We may obtain a characterisation set by simply considering every pair of states and look for a difference.
-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.
+However, it turns out a harmonised set of state identifiers exists for every machine and this can be constructed very efficiently (\in{Chapter}[chap:separating-sequences]).
-\todo{Iets versimpelen}
+From a set of state identifiers we may obtain a characterisation set by taking the union of all those sets.
 
 \startexample
 As mentioned before, state $s_2$ from \in{Figure}[fig:running-example] has a state identifier $\{aa, ac, b\}$.
@@ -292,17 +292,17 @@ To further separate the states, the sequences continues with either a $b$ or ano
 And so on.
 
 \startplacefigure
-  [title={(a): A Mealy machine with an ADS and (b): the tree structure of this ADS. },
+  [title={(a): A Mealy machine with an ADS and (b): the tree structure of this ADS.},
    list={A Mealy machine and its ADS.},
    reference=fig:ads-example]
-\startcombination[2*1]
+\startcombination[nx=2, location=middle, distance=.5cm]
 {\hbox{
 \starttikzpicture
 	\node[initial, state] (0)     {$s_0$};
 	\node[state] (1) [right=of 0] {$s_1$};
 	\node[state] (2) [below=of 1] {$s_2$};
 	\node[state] (3) [left =of 2] {$s_3$};
-	\path[->]
+	\path[trans]
 	(0) edge node [above] {$a/0, b/0$} (1)
 	(1) edge node [right] {$a/1$}      (2)
 	(2) edge node [above] {$a/0, b/0$} (3)
@@ -362,6 +362,27 @@ Two states $x, y$ are \emph{$\Fam{W}$-equivalent}, written $x \sim_{\Fam{W}} y$,
 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$.
 Clearly, if two states are equivalent (i.e., $s \sim t$), then for any set $W$ we have $s \sim_W t$.
 
+\startlemma[reference=lem:relation-characterisation]
+The relations $\sim_W$ and $\sim_{\Fam{W}}$ can be used to \emph{define} characterisation sets and separating families.
+Concretely:
+\startitemize
+\item
+$W$ is a characterisation set if and only if for all $s, t$ in $M$, $s \sim_W t$ implies $s \sim t$.
+\item
+$\Fam{W}$ is a separating family if and only if for all $s, t$ in $M$, $s \sim_{\Fam{W}} t$ implies $s \sim t$.
+\stopitemize
+\stoplemma
+\startproof
+\todo{Verhelderen (zie ook Sectie 5)}
+\startitemize
+\item
+$W$ is a characterisation set by definition means $s \not\sim t \implies s \not\sim_W t$ as $W$ contains a separating sequence (if it exists at all).
+This is equivalent to $s \sim_W t \implies s \sim t$.
+\item
+The same argument holds for a separating family by considering $W_s \cap W_t$.
+\stopitemize
+\stopproof
+
 
 \stopsubsection
 \startsubsection
@@ -381,7 +402,6 @@ If $P$ is a state cover, then the set $\{ p a \mid p \in P, a \in I \}$ is calle
   [title={Constructions on sets of sequences}]
 
 In order to define a test suite modularly, we introduce notation for combining sets of words.
-We fix a specification $M$.
 For sets of words $X$ and $Y$, we define
 \startitemize[after]
 \item their concatenation $X \cdot Y = \{ xy \mid x \in X, y \in Y \}$,
@@ -394,8 +414,7 @@ On families we define
 \item flattening: $\bigcup \Fam{X} = \{ x \mid x \in X_s, s \in S \}$,
 \item union: $\Fam{X} \cup \Fam{Y}$ is defined point-wise:
 $(\Fam{X} \cup \Fam{Y})_s = X_s \cup Y_s$,
-\item concatenation:
+\item concatenation\footnote{We will often see the combination $P \cdot I \odot \Fam{X}$, this should be read as $(P \cdot I) \odot \Fam{X}$.}:
-\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$.
@@ -420,7 +439,28 @@ For all families $\Fam{X}$ and $\Fam{Y}$:
 \stopitemize
 \stoplemma
 \startproof
-\todo{Kort uitschrijven}
+For the first item, note that there are no states $t$ such that $s \sim_{\Fam{X}} t$ and $s \not\sim_{\Fam{X}} t$.
+Consequently, the union is empty, and the expression simplifies to
+\startformula (\Fam{X} ; \Fam{X})_s = X_s \cup (X_s \cap \emptyset) = X_s . \stopformula
+
+If $\Fam{X}$ is a separating family, then the only $t$ for which $s \sim_{\Fam{X}} t$ hold are $t$ such that $s \sim t$ (\in{Lemma}[lem:relation-characterisation]).
+But $s \sim t$ is ruled out by $s \not\sim_{\Fam{Y}} t$, and again so
+\startformula (\Fam{X} ; \Fam{Y})_s = X_s \cup (Y_s \cap \emptyset) = X_s . \stopformula
+
+For the last item, suppose that $s \sim_{\Fam{X} ; \Fam{Y}} t$.
+Then $s$ and $t$ agree on every sequence in $(\Fam{X} ; \Fam{Y})_s \cap (\Fam{X} ; \Fam{Y})_t$.
+We distinguish two cases:
+\startitemize
+\item
+Suppose $s \sim_{\Fam{X}} t$, then $Y_s \cap Y_t \subseteq (\Fam{X} ; \Fam{Y})_s \cap (\Fam{X} ; \Fam{Y})_t$.
+And so $s$ and $t$ agree on $Y_s \cap Y_t$, meaning $s \sim_{\Fam{Y}} t$.
+Since $\Fam{Y}$ is a separating family, we have $s \sim t$.
+\item
+Suppose $s \not\sim_{\Fam{X}} t$.
+This contradicts $s \sim_{\Fam{X} ; \Fam{Y}} t$, since $X_s \cap X_t \subseteq (\Fam{X} ; \Fam{Y})_s \cap (\Fam{X} ; \Fam{Y})_t$.
+\stopitemize
+We conclude that $s \sim t$.
+This proves that $\Fam{X}; \Fam{Y}$ is a separating family.
 \stopproof
 
 
@@ -513,7 +553,7 @@ T_{\text{HSI}} = (P \cup Q) \cdot I^{\leq k} \odot \Fam{H}.
 Our hybrid ADS method is an instance of the HSI-method as we define it here.
 However, \citet[LuoPB95, PetrenkoYLD93] 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.
-\todo{The hybrid ADS method does not refine the HSI method defined in the more restricted sense.}
+The hybrid ADS method does not refine the HSI method defined in the more restricted sense.
 
 
 \stopsubsection
@@ -564,17 +604,17 @@ The test suite then becomes $\{ aaaa, abba, baaa, bba \}$ and the faulty impleme
 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$.
 Hence we also want to check that a state does not behave as one of the other states, and therefore we use $\bigcup \Fam{U}$.
 With the same UIOs as above, the resulting UIOv test suite for the specification in \in{Figure}[fig:uio-counterexample] is $\{aaaa, aba, abba, baaa, bba\}$ of size $23$.
-\todo{Eerste example met size? Herhalen dat we reset tellen.}
+(Recall that we also count resets when measuring the size.)
 
 \startplacefigure
   [title={An example where the UIO method is not complete.},
    reference=fig:uio-counterexample]
-\startcombination[2*1]
+\startcombination[nx=2, distance=1cm]
 {\hbox{\starttikzpicture[node distance=2.5cm, bend angle=18]
   \node[state,initial,initial text=] (0) {$s_0$};
   \node[state] (1) [above right of=0] {$s_1$};
   \node[state] (2) [below right of=1] {$s_2$};
-  \path[->]
+  \path[trans]
   (0) edge [bend left ] node [left ] {${a}/0$} (1)
   (0) edge [bend right] node [below] {${b}/1$} (2)
   (1) edge [bend left ] node [left ] {${a}/1$} (0)
@@ -586,7 +626,7 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
   \node[state,initial,initial text=] (0) {$s'_0$};
   \node[state] (1) [above right of=0] {$s'_1$};
   \node[state] (2) [below right of=1] {$s'_2$};
-  \path[->]
+  \path[trans]
   (0) edge [bend left ] node [left ] {${a}/0$} (1)
   (0) edge [bend right] node [below] {${b}/1$} (2)
   (1) edge [bend left ] node [left ] {${a}/1$} (0)
@@ -601,10 +641,9 @@ With the same UIOs as above, the resulting UIOv test suite for the specification
 
 \stopsubsection
 \startsubsection
-  [title={Example},
+  [title={All test suites for \in{Figure}[fig:running-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.
@@ -628,29 +667,29 @@ The transition cover is simply constructed by extending each access sequence wit
 	\node[state] (3) [above right = of 0] {$s_3$};
 	\node[state] (4) [below right = of 0] {$s_4$};
 	\node        (5) [above = of 0] {};
-	\path[->]
+	\path[trans]
-	(5) edge (0)
+	(5) edge node [right] {$\epsilon$} (0)
 	(0) edge [bend left=] node [below] {${a}/1$} (1)
 	(0) edge [bend right] node [below] {${b}/0$} (4)
 	(1) edge              node [left ] {${a}/0$} (2)
-	(4) edge [bend left]  node [right] {${a}/1$} (3)
+	(4) edge [bend left]  node [right] {${a}/1$} (3);
-	(0) edge [loop below, color=gray] node [below] {${c}/0$} (0)
+	\path[trans, color=gray]
-	(1) edge [bend left, color=gray]  node [above] {${b}/0$, ${c}/0$} (0)
+	(0) edge [loop below] node [below] {${c}/0$} (0)
-	(2) edge [bend right, color=gray] node [below] {${b}/0$, ${c}/0$} (0)
+	(1) edge [bend left]  node [above] {${b}/0$, ${c}/0$} (0)
-	(2) edge [loop left, color=gray]  node [left ] {${a}/1$} (1)
+	(2) edge [bend right] node [below] {${b}/0$, ${c}/0$} (0)
-	(3) edge [bend left=30, color=gray] node [right] {${a}/1$} (4)
+	(2) edge [loop left]  node [left ] {${a}/1$} (1)
-	(3) edge [bend right, color=gray] node [above] {${b}/0$} (0)
+	(3) edge [bend left=30] node [right] {${a}/1$} (4)
-	(3) edge [loop right, color=gray] node [right] {${c}/1$} (3)
+	(3) edge [bend right] node [above] {${b}/0$} (0)
-	(4) edge [loop right, color=gray] node [right] {${b}/0$} (4)
+	(3) edge [loop right] node [right] {${c}/1$} (3)
-	(4) edge [bend right, color=gray] node [above] {${c}/0$} (0);
+	(4) edge [loop right] node [right] {${b}/0$} (4)
+	(4) edge [bend right] node [above] {${c}/0$} (0);
 \stoptikzpicture
 }
 \stopplacefigure
 
-
 As shown earlier, the set $W = \{ aa, ac, c \}$ is a characterisation set.
-Then the W-method gives the following test suite of size 169:
+The W-method, which simply combines $P \cup Q$ with $W$, gives the following test suite of size 169:
-\todo{Definitie herhalen?}
+
 \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
@@ -713,7 +752,7 @@ The UIO method and ADS method are not applicable in this example because state $
 	\node[state] (3) [above right = of 0] {$s'_3$};
 	\node[state] (4) [below right = of 0] {$s'_4$};
 	\node        (5) [above = of 0] {};
-	\path[->]
+	\path[trans]
 	(5) edge (0)
 	(0) edge [bend left]  node [below] {$a/1$} (1)
 	(0) edge [bend right] node [below] {$b/0$} (4)
@@ -946,7 +985,8 @@ We also observe that one of the state identifiers grew in length: $\{ aa, c \}$
 
 \stopsubsection
 \startsubsection
-  [title={Implementation}]
+  [title={Implementation},
+   reference=sec:hybrid-ads-impementation]
 
 All the algorithms concerning the hybrid ADS-method have been implemented and can be found at
 \citeurl[hybrid-ads-code].
@@ -1024,7 +1064,7 @@ 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}$?}
+Each of the methods in the right column can be written simpler as $P \cdot I^{\leq k+1} \odot \Fam{H}$, since $Q = P \cdot I$.
 
 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.
@@ -1047,14 +1087,11 @@ For the W, Wp, HSI and hybrid ADS methods we obtained test suites of size 169, 7
    reference=sec:completeness]
 
 In this section, we will prove $n$-completeness of the discussed test methods.
-We fix a specification $M$ which has a minimal representative with $n$ states and an implementation $M'$ with at most $n+k$ states.
-We assume that all states are reachable from the initial state in both machines (i.e., both are \defn{connected}).
-
 Before we dive into the proof, we give some background on the proof-principle of bisimulation.
 The original proofs of completeness often involve an inductive argument (on the length of words) inlined with arguments about characterisation sets.
 This can be hard to follow and so we prefer a proof based on bisimulations, which defers the inductive argument to a general statement about bisimulation.
 Many notions of bisimulation exist in the theory of labelled transition systems, but for Mealy machines there is just one simple definition.
-We give the definition and the main proof principle, all of which can be found in \citep[Rutten98].
+We give the definition and the main proof principle, all of which can be found in a paper by \citet[Rutten98].
 
 \startdefinition
 Let $M$ be a Mealy machine.
@@ -1065,15 +1102,31 @@ A relation $R \subseteq S \times S$ is called a \defn{bisimulation} if for every
 \stopitemize
 \stopdefinition
 
-\startlemma
+\startlemma[reference=lem:bisim]
-If two states $s, t$ are related by a bisimulation $R$, then $s \sim t$.
+If two states $s, t$ are related by a bisimulation, then $s \sim t$.
 \stoplemma
 
-\todo{Kunnen net zo goed even up to definieren.}
+We use a slight generalisation of the bisimulation proof technique, callend \emph{bisimulation up-to}.
-
-In the following proof, we use a slight generalisation of the bisimulation proof technique, callend \emph{bisimulation up-to}.
 This allows one to give a smaller set $R$ which extends to a bisimulation.
 A good introduction of these up-to techniques is given by \citet[BonchiP15] or the thesis of \citet[Rot17].
+In our case we use bisimulation \emph{up-to equivalence}.
+The following lemma can be found in the given references.
+
+\startdefinition
+Let $M$ be a Mealy machine.
+A relation $R \subseteq S \times S$ is called a \defn{bisimulation up-to equivalence} if for every $(s, t) \in R$ we have
+\startitemize
+\item equal outputs: $\lambda(s, a) = \lambda(t, a)$ for all $a \in I$, and
+\item related successor states: $(\delta(s, a), \delta(t, a)) \in R$ \emph{or} $\delta(s, a) \sim \delta(t, a)$ for all $a \in I$.
+\stopitemize
+\stopdefinition
+
+\startlemma[reference=lem:bisim-upto]
+Any bisimulation up-to equivalence is contained in a bisimulation.
+\stoplemma
+
+We fix a specification $M$ which has a minimal representative with $n$ states and an implementation $M'$ with at most $n+k$ states.
+We assume that all states are reachable from the initial state in both machines (i.e., both are \defn{connected}).
 
 The next proposition gives sufficient conditions for a test suite of a certain shape to be
 complete.
@@ -1114,23 +1167,24 @@ So we have:
 \startformula s_2 \sim_{W'_{s_2}} i_2 \sim_{W_t} t. \stopformula
 By the second assumption, we conclude that $s_2 \sim t$.
 So $s_2 \sim t$ and $(t, i) \in R$, which means that $R$ is a bisimulation up-to equivalence.
-Using the theory of up-to techniques \cite[BonchiP15] we know that there exists a bisimulation relation containing $R$.
+Moreover, $R$ contains the pair $(s_0, s'_0)$.
-In particular, the initial $s_0$ and $s'_0$ are bisimilar.
+By using \in{Lemma}[lem:bisim-upto] and \in{Lemma}[lem:bisim], we conclude that the initial $s_0$ and $s'_0$ are equivalent.
-And so the machines $M$ and $M'$ are equivalent.
 \stopproof
 
 Before we show that the conditions hold for the test methods, we reflect on the above proof first.
 This proof is very similar to the completeness proof by \citet[Chow78].
-(In fact, it is also similar to Lemma 4 by \citet[Angluin87] which proves termination in the L* learning algorithm. This correspondence was noted by \citet[BergGJLRS05].)
+\footnote{In fact, it is also similar to Lemma 4 by \citet[Angluin87] which proves termination in the L* learning algorithm. This correspondence was noted by \citet[BergGJLRS05].}
 In the first part we argue that all states are visited by using some sort of counting and reachability argument.
 Then in the second part we show the actual equivalence.
 To the best of the authors knowledge, this is first $m$-completeness proof which explicitly uses the concept of a bisimulation.
 Using a bisimulation allows us to slightly generalise and use bisimulation up-to equivalence, dropping the the often-assumed requirement that $M$ is minimal.
 
+\todo{Refer naar lemma uit eerste sectie}.
+
 \startlemma
 Let $\Fam{W'}$ be a family of state identifiers for $M$.
 Define the family $\Fam{W}$ by $W_s = \bigcup \Fam{W'}$.
-Then the conditions (1) and (2) in the previous lemma are satisfied.
+Then the conditions (1) and (2) in \in{Proposition}[prop:completeness] are satisfied.
 \stoplemma
 \startproof
 The first condition we note that $W_x \cap W_y = W_x = W_y$, and so $x \sim_{W_x \cap W_y} y$ implies $x \sim_{W_x} y$, now by definition of state identifier we get $x \sim y$.
@@ -1146,7 +1200,7 @@ The W, Wp, and UIOv test suites are $n+k$-complete.
 
 \startlemma
 Let $\Fam{H}$ be a separating family and take $\Fam{W} = \Fam{W'} = \Fam{H}$.
-Then the conditions (1) and (2) in the previous lemma are satisfied.
+Then the conditions (1) and (2) in \in{Proposition}[prop:completeness] are satisfied.
 \stoplemma
 \startproof
 Let $x \sim_{H_x \cap H_y} y$, then by definition of separating family $x \sim y$.
@@ -1198,7 +1252,6 @@ However, for non-deterministic systems, guiding an implementation into a state i
 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.

environment.tex

@@ -18,8 +18,8 @@
 
 \mainlanguage[en]
 
-%\setupindenting[yes, medium]
+\setupindenting[yes, medium]
-\setupwhitespace[medium]
+%\setupwhitespace[medium]
 
 \definefloat[algorithm][algorithms]
 
@@ -43,7 +43,7 @@ This chapter is based on the following publication:
 \setupitemize[2,joinedup,nowhite,autointro]
 % For more whitespace between items
 \defineitemgroup[bigitemize]
-\setupitemgroup[bigitemize][2,autointro]
+\setupitemgroup[bigitemize][2,autointro,indentnext]
 
 % Standaard \colon had niet veel ruimte
 \define\colon{{\,{:}\,\,}}

environment/tikz.tex

@@ -13,6 +13,8 @@
 % observation table
 \tikzset{obs table/.style={matrix of math nodes, ampersand replacement=\&, column 1/.style={anchor=base west}}}
 
+\tikzset{trans/.style={->, shorten >=1pt}}
+
 % This command is used to draw the internal data structure for the minimal separating sequences paper
 \define[5]\gasblock{
 \fill (#1-0.495,{(3-#3)*0.75+0.5}) [rounded corners=0.2cm] -- (#1-0.495,{(3-#3)*0.75+0.655}) -- (#2-0.505,{(3-#3)*0.75+0.655}) [sharp corners] -- (#2-0.505,{(3-#3)*0.75+0.5}) [rounded corners=0.2cm] -- (#2-0.505,{(3-#3)*0.75+0.645}) -- (#1-0.495,{(3-#3)*0.75+0.645}) [sharp corners] -- cycle;