Ack + Summary. En nog wat kleine typos.

biblio-web.bib

@@ -84,3 +84,14 @@
 	note      = {Source code},
 	url       = {https://github.com/Jaxan/nominal-lstar}
 }
+
+@inproceedings{applying-learning-data,
+	author    = {Wouter Smeenk and
+	             Joshua Moerman and
+	             Frits W. Vaandrager and
+	             David N. Jansen},
+	title     = {Applying Automata Learning to Embedded Control Software},
+	year      = {2015},
+	url       = {http://www.mbsd.cs.ru.nl/publications/papers/fvaan/ESM/},
+	note      = {Learned models and resources}
+}

content-other/acknowledgements.tex

@@ -6,22 +6,25 @@
    reference=chap:acknowledgements]
 
 Foremost, I would like to thank my supervisors.
-Having three of them ensured that there was always enough ideas to work on, theory to understand, papers to review, seminars to attend, and chats to have.
+Having three of them ensured that there were always enough ideas to work on, theory to understand, papers to review, seminars to attend, and chats to have.
 Frits, thank you for being a very motivating supervisor, pushing creativity, and being only a few meters away.
 It started with a small puzzle (trying a certain test algorithm to help with a case study), which was a great, hands-on start of my Ph.D..
-You introduced me to the field of model learning in a way which showcases both the theoretical and practical aspects.
+You introduced me to the field of model learning in a way that showcases both the theoretical and practical aspects.
 
-Alexandra, thank you for inviting me to London, Caribbean islands, hidden cocktail clubs, and the best food.
-You introduced me to abstract reasoning about state machines, the coalgebraic way.
+Alexandra, thanks for introducing me to abstract reasoning about state machines, the coalgebraic way.
 Although not directly shown in this thesis, this way of thinking has helped and you pushed me to pursuit clear reasoning.
-Besides the theoretical things I've learned, you have also taught me many personal lessons inside and outside of academia.
+Besides the theoretical things I've learned, you have also taught me many personal lessons inside and outside of academia; thanks for inviting me to London, Caribbean islands, hidden cocktail clubs, and the best food.
 And thanks for leaving me with Daniela and Matteo, who introduced me to nominal techniques, while you were on sabbatical.
 
 Bas, thanks for broadening my understanding of the topics touched upon in this thesis.
 Unfortunately, we have no papers together, but the connections you showed to logic, computational learning, and computability theory have influenced the thesis nevertheless.
 I am grateful for the many nice chats we had.
 
-At the first floor of the Mercator building, I had the pleasure of spending four years with fun office mates.
+I would like to thank the members of the manuscript committee, Bart, Ana, Falk, S\l{}awek, and Daniela.
+Rreading a thesis is undoubtedly a lot of work, so thank you for the effort and feedback you have given me.
+Thanks, also, to the additional members coming to {\nl Nijmegen\en} to oppose during the defence, Jan Friso, Jorge, and Paul.
+
+On the first floor of the Mercator building, I had the pleasure of spending four years with fun office mates.
 Michele, thanks for introducing me to the Ph.D. life, by always joking around.
 Hopefully, we can play a game of Briscola again.
 Alexis, many thanks for all the tasty {\it\nl proeverijen,\en} wheter it was beers, wines, {\nl poffertjes, kroketten\en}, or anything else.
@@ -34,16 +37,16 @@ Paul, thanks for being the kindest colleague I've had and for inviting us to you
 Rick, thanks for the algorithmic sparring, we had a great collaboration.
 Was there a more iconic duo on our floor?
 A good contender would be Petra and Ramon.
-Thanks for the fun we had with ioco, together with Jan.
+Thanks for the fun we had with ioco, together with Jan and Mari\"{e}lle.
 Nils, thanks for steering me towards probabilistic things and opening a door to Aachen.
-I am also very grateful for Jurriaan for bringing back some coalgebra and category theory to our floor, and hosting me in London.
+I am also very grateful to Jurriaan for bringing back some coalgebra and category theory to our floor, and hosting me in London.
 My other co-authors, Wouter, David, Bartek, Micha\l{}, and David, also deserve many credits for all the interesting discussion we had.
 Harco, thanks for the technical support.
-Special thanks go to Ingrid, for helping with the often-overlooked, but very important, administrative matters.
+Special thanks go to Ingrid, for helping with the often-overlooked, but important, administrative matters.
 
 Doing a Ph.D. would not be complete without a good amount of playing kicker, having {\nl borrels\en}, and eating cakes at the iCIS institute.
-Thanks to all of you, Markus, Bram, Marc, Sam, Bas, Joost, Dan, Giso, Baris, Simone, Manxia, Leon, Jacopo, Gabriel, Paulus, Marcos, Bas, and Henning.
-\footnote[random]{In no particular order. This lists are randomised.}
+Thanks to all of you, Markus, Bram, Marc, Sam, Bas, Joost, Dan, Giso, Baris, Simone, Aleks, Manxia, Leon, Jacopo, Gabriel, Michael, Paulus, Marcos, Bas, and Henning.
+\footnote[random]{In no particular order. These lists are randomised.}
 
 Thanks to people I have met across the channel (which hopefully will remain part of the EU): Benni, Nath, Kareem, Rueben, Louis, Borja, Fred, Tobias, Paul, Gerco, and Carsten,
 for the theoretical adventure, but also for joining me to {\it Phonox} and other parties in London.
@@ -57,11 +60,11 @@ My gratitude extends to all the people I have met at summer schools and conferen
 I had a lot of fun learning about different cultures, languages, and different ways of doing research.
 Hope we meet again!
 
-I would also like to thanks all my friends, for hosting me, cooking excellent dinners, or otherwise having fun with me, thank you, Edo, Gabe, Saskia, Stijn, Sandra, Geert, Nick, Marco, Carmen, and Wesley.
-Thanks to Marlon, Hannah, Wouter, Dennis, and others from \#RU for {\nl borrels\en} and jams.
-Thanks to Ragnar, Julian, Jeroen, Vincent, and others from the BAPC for algorithmic fun.
+I would also like to thanks all my friends, for hosting me, cooking excellent dinners, or otherwise having fun with me, thank you, Nick, Edo, Gabe, Saskia, Stijn, Sandra, Geert, Marco, Carmen, and Wesley.
+Thanks to Marlon, Hannah, Wouter, Dennis, Christiaan, and others from \#RU for {\nl borrels\en}, bouldering, and jams.
+Thanks to Ragnar, Josse, Julian, Jeroen, Vincent, and others from the BAPC for algorithmic fun.
 
-Thanks to my parents, Kees and Irene, and my brother, David, for visiting me in {\nl Nijmegen\en} a few times.
+Thanks to my parents, Kees and Irene, and my brother, David, and his wife, Germa, for their love and support.
 My gratitude extends to my family in law, Ine, Wim, Jolien and Jesse.
 My final words of praise go to Tessa, my wife, I am very happy to have you on my side.
 You inspire me in many ways, and I enjoy doing all the fun stuff we do.

content-other/summary.tex

@@ -47,7 +47,7 @@ Dit zou gebruikt kunnen worden om zulke automaten sneller te leren.
 
 {\it Automata learning} plays a more and more prominent role in the field of software verification.
 Learning algorithms are able to automatically explore the behaviour of software.
-By revealing interesting properties of the software, these algorithms can create models the, otherwise unknown, software.
+By revealing interesting properties of the software, these algorithms can create models of the, otherwise unknown, software.
 These learned models can, in turn, be inspected and analysed, which often leads to finding bugs and inconsistencies in the software.
 
 An important tool which we need when learning software is {\it test generation.}
@@ -59,13 +59,13 @@ However, our tests have to be {\it complete:} if the hypothesis fails to model t
 The first few chapters explain black box testing of automata.
 We present a theoretical framework in which we can compare existing {\it $n$-complete test generation methods.}
 From this comparison, we are able to define a new, efficient algorithm.
-In an industrial case study on embedded printer software, we show that this new algorithm works well for finding counterexamples in the hypothesis.
+In an industrial case study on embedded printer software, we show that this new algorithm works well for finding counterexamples for the hypothesis.
 Besides the test generation, we show that one of the subproblems -- finding the shortest sequences to separate states -- can be solved very efficiently.
 
 The second part of this thesis is on the theory of formal languages and automata with {\it infinite alphabets}.
 This, too, is discussed in the context of automata learning.
 Many pieces of software make use of identifiers or sequence numbers.
-These are used, for example, in order to distinguish differen users or messages.
+These are used, for example, in order to distinguish different users or messages.
 Ideally, we would like to model such systems with infinitely many identifiers, as we do not know beforehand how many of them will be used.
 
 Using the theory of {\it nominal sets}, we show that learning algorithms can easily be generalised to automata with infinite alphabets.

content/applying-automata-learning.tex

@@ -114,7 +114,7 @@ Preliminary evidence suggests that our adaptation of Lee \& Yannakakis' algorith
 During recent years most researchers working on active automata learning focused their efforts on efficient algorithms and tools for the construction of hypothesis models.
 Our work shows that if we want to further scale automata learning to industrial applications, we also need better algorithms for finding counterexamples for incorrect hypotheses.
 Following \citet[BergGJLRS05], our work shows that the context of automata learning provides both new challenges and new opportunities for the application of testing algorithms.
-All the models for the ESM case study together with the learning and testing statistics are available at \href{http://www.mbsd.cs.ru.nl/publications/papers/fvaan/ESM/}, as a benchmark for both the automata learning and testing communities.
+All the models for the ESM case study together with the learning and testing statistics are available at \citeurl[applying-learning-data], as a benchmark for both the automata learning and testing communities.
 It is now also included in the automata wiki at \citeurl[automata-wiki].
 
 

content/introduction.tex

@@ -288,7 +288,7 @@ In this example, a test suite should include sequences such as \playstop\,\spin\
   (tr) edge [bend right] node [above] {\spin}     (tl)
   (tr) edge [bend right] node [left]  {\playstop} (br)
   (br) edge [bend right] node [right] {\playstop} (tr)
-  (br) edge [loop below, color=darkred]  node [above] {\spin} (br);
+  (br) edge [loop below, color=red]  node [above] {\spin} (br);
 \stoptikzpicture}}{(a)}
 {\hbox{\starttikzpicture[node distance=3cm, bend angle=10]
   \node[state, initial above, align=center] (tl) {slow\\spinning};
@@ -302,7 +302,7 @@ In this example, a test suite should include sequences such as \playstop\,\spin\
   (bl) edge [bend right] node [right] {\playstop} (tl)
   (bl) edge [bend right] node [below] {\spin}     (br)
   (tr) edge [bend right] node [above] {\spin}     (tl)
-  (tr) edge [color=darkred]  node [below right] {\playstop} (bl)
+  (tr) edge [color=red]  node [below right] {\playstop} (bl)
   (br) edge [bend right] node [right] {\playstop} (tr)
   (br) edge [bend right] node [above] {\spin}     (bl);
 \stoptikzpicture}}{(b)}

content/separated-nominal-automata.tex

@@ -319,7 +319,7 @@ For associativity and unitality of the $\sb$-action, we simply note that it is
 directly defined by left multiplication of $\sb$ which is associative and unital.
 This concludes that $F(X)$ is an $\sb$-set.
 \stopdescription
-\startdescription{$F(X)$ is an nominal $\sb$ set.}
+\startdescription{$F(X)$ is a nominal $\sb$ set.}
 Given an element $[m, x] \in F(X)$ and a $\perm$-support $C$ of $x$, we will prove that $m \cdot C$ 
 is an $\sb$-support for $[m, x]$.
 Suppose that we have $m_1, m_2 \in \sb$ such that $m_1|_{m\cdot C} = m_2|_{m\cdot C}$.
@@ -561,7 +561,7 @@ By Currying and the adjunction we arrive at $\phi$:
 \stopdefinition
 
 With this map we can prove a generalisation of \in{Theorem}[thm:adjunction].
-In particular, the following lemma generalises the one-to-one correspondence between maps $X \to U(Y)$ and maps $F(X) \to Y$.
+In particular, the following theorem generalises the one-to-one correspondence between maps $X \to U(Y)$ and maps $F(X) \to Y$.
 First, it shows that this correspondence is $\perm$-equivariant.
 Second, it extends the correspondence to all finitely supported maps and not just the equivariant ones.
 
@@ -831,7 +831,7 @@ $L = U(\overline{S})$.
 \stoptheorem
 \startproof
 If follows from the one-to-one correspondence in \in{Theorem}[thm:extension]:
-one the bottom there are two language ($L$ and $U(\overline{S})$), while there is only the restriction of $L$ on the top.
+on the bottom there are two languages ($L$ and $U(\overline{S})$), while there is only the restriction of $L$ on the top.
 We conclude that $L = U(\overline{S})$.
 \stopproof
 

content/test-methods.tex

@@ -677,7 +677,7 @@ The transition cover is simply constructed by extending each access sequence wit
 	(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);
-	\path[trans, color=grijs]
+	\path[trans, color=lgrijs]
 	(0) edge [loop below] node [below] {${c}/0$} (0)
 	(1) edge [bend left]  node [above] {${b}/0$, ${c}/0$} (0)
 	(2) edge [bend right] node [below] {${b}/0$, ${c}/0$} (0)
@@ -763,7 +763,7 @@ The UIO-method and ADS-method are not applicable in this example because state $
 	(0) edge [loop below] node [below] {$c/0$} (0)
 	(1) edge              node [left ] {$a/0$} (2)
 	(1) edge [bend left]  node [above] {$b/0$, $c/0$} (0)
-	(2) edge [bend right] node [below] {\color[darkred]{$a/1$}, $b/0$, $c/0$} (0)
+	(2) edge [bend right] node [below] {\color[red]{$a/1$}, $b/0$, $c/0$} (0)
 	(3) edge [bend left]  node [right] {$a/1$} (4)
 	(3) edge [bend right] node [above] {$b/0$} (0)
 	(3) edge [loop right] node [right] {$c/1$} (3)