Related werk in test methods

biblio-eigen.bib

@@ -92,3 +92,26 @@
 	biburl    = {https://dblp.org/rec/bib/conf/popl/MoermanS0KS17},
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
+
+@inproceedings{BosJM17,
+	author    = {Petra van den Bos and
+	             Ramon Janssen and
+	             Joshua Moerman},
+	editor    = {Nina Yevtushenko and
+	             Ana Rosa Cavalli and
+	             H{\"{u}}sn{\"{u}} Yenig{\"{u}}n},
+	title     = {$n$-Complete Test Suites for {IOCO}},
+	booktitle = {Testing Software and Systems - 29th {IFIP} {WG} 6.1 International
+	             Conference, {ICTSS} 2017, St. Petersburg, Russia, October 9-11, 2017,
+	             Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {10533},
+	pages     = {91--107},
+	publisher = {Springer},
+	year      = {2017},
+	url       = {https://doi.org/10.1007/978-3-319-67549-7\_6},
+	doi       = {10.1007/978-3-319-67549-7\_6},
+	timestamp = {Mon, 25 Sep 2017 17:37:19 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/pts/BosJM17},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}

biblio.bib

@@ -577,6 +577,27 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{BosS18,
+	author    = {Petra van den Bos and
+	             Mari{\"{e}}lle Stoelinga},
+	editor    = {Andrea Orlandini and
+	             Martin Zimmermann},
+	title     = {Tester versus Bug: {A} Generic Framework for Model-Based Testing via
+	             Games},
+	booktitle = {Proceedings Ninth International Symposium on Games, Automata, Logics,
+	             and Formal Verification, GandALF 2018, Saarbr{\"{u}}cken, Germany,
+	             26-28th September 2018.},
+	series    = {{EPTCS}},
+	volume    = {277},
+	pages     = {118--132},
+	year      = {2018},
+	url       = {https://doi.org/10.4204/EPTCS.277.9},
+	doi       = {10.4204/EPTCS.277.9},
+	timestamp = {Tue, 16 Oct 2018 10:05:10 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1809-03098},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/popl/BotincanB13,
 	author    = {Matko Botincan and
 	             Domagoj Babic},
@@ -832,6 +853,27 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DorofeevaEY05,
+	author    = {Rita Dorofeeva and
+	             Khaled El{-}Fakih and
+	             Nina Yevtushenko},
+	editor    = {Farn Wang},
+	title     = {An Improved Conformance Testing Method},
+	booktitle = {Formal Techniques for Networked and Distributed Systems - {FORTE}
+	             2005, 25th {IFIP} {WG} 6.1 International Conference, Taipei, Taiwan,
+	             October 2-5, 2005, Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {3731},
+	pages     = {204--218},
+	publisher = {Springer},
+	year      = {2005},
+	url       = {https://doi.org/10.1007/11562436\_16},
+	doi       = {10.1007/11562436\_16},
+	timestamp = {Tue, 26 Jun 2018 14:10:59 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/forte/DorofeevaEY05},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/infsof/DorofeevaEMCY10,
 	author    = {Rita Dorofeeva and
 	             Khaled El{-}Fakih and
@@ -1101,6 +1143,21 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{GrozSPO16,
+	author    = {Roland Groz and
+	             Nicolas Bremond and
+	             Adenilso da Silva Sim{\~{a}}o},
+	editor    = {Olgierd Unold and
+	             Witold Dyrka and
+	             Wojciech Wieczorek},
+	title     = {Inferring {FSM} Models of Systems Without Reset},
+	booktitle = {International Conference on Grammatical Inference, ICGI 2018},
+	pages     = {30--43},
+	publisher = {Proceedings of Machine Learning Research},
+	year      = {2018},
+	note      = {Wachten op doi?}
+}
+
 @inproceedings{DBLP:conf/fmco/HansenKLMPS10,
 	author    = {Helle Hvid Hansen and
 	             Jeroen Ketema and
@@ -1915,8 +1972,8 @@
   booktitle = {15th International {IEEE} Symposium on High-Assurance Systems Engineering,
                {HASE} 2014, Miami Beach, FL, USA, January 9-11, 2014},
   pages     = {249--253},
+  publisher = {{IEEE} Computer Society},
   year      = {2014},
-	crossref  = {DBLP:conf/hase/2014},
   url       = {https://doi.org/10.1109/HASE.2014.46},
   doi       = {10.1109/HASE.2014.46},
   timestamp = {Thu, 25 May 2017 00:41:35 +0200},
@@ -1924,15 +1981,19 @@
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
-@proceedings{DBLP:conf/hase/2014,
+@inproceedings{PetrenkoY14,
-	title     = {15th International {IEEE} Symposium on High-Assurance Systems Engineering,
+	author    = {Alexandre Petrenko and
+	             Nina Yevtushenko},
+	title     = {Adaptive Testing of Nondeterministic Systems with {FSM}},
+	booktitle = {15th International {IEEE} Symposium on High-Assurance Systems Engineering,
 	             {HASE} 2014, Miami Beach, FL, USA, January 9-11, 2014},
+	pages     = {224--228},
 	publisher = {{IEEE} Computer Society},
 	year      = {2014},
-	url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6754245},
+	url       = {https://doi.org/10.1109/HASE.2014.39},
-	isbn      = {978-1-4799-3465-2},
+	doi       = {10.1109/HASE.2014.39},
-	timestamp = {Tue, 02 Dec 2014 17:13:28 +0100},
+	timestamp = {Thu, 25 May 2017 00:41:35 +0200},
-	biburl    = {https://dblp.org/rec/bib/conf/hase/2014},
+	biburl    = {https://dblp.org/rec/bib/conf/hase/PetrenkoY14},
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
@@ -2102,6 +2163,64 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{SimaoPY09,
+	author    = {Adenilso da Silva Sim{\~{a}}o and
+	             Alexandre Petrenko and
+	             Nina Yevtushenko},
+	editor    = {Manuel N{\'{u}}{\~{n}}ez and
+	             Paul Baker and
+	             Mercedes G. Merayo},
+	title     = {Generating Reduced Tests for {FSMs} with Extra States},
+	booktitle = {Testing of Software and Communication Systems, 21st {IFIP} {WG} 6.1
+	             International Conference, {TESTCOM} 2009 and 9th International Workshop,
+	             {FATES} 2009, Eindhoven, The Netherlands, November 2-4, 2009. Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {5826},
+	pages     = {129--145},
+	publisher = {Springer},
+	year      = {2009},
+	url       = {https://doi.org/10.1007/978-3-642-05031-2\_9},
+	doi       = {10.1007/978-3-642-05031-2\_9},
+	timestamp = {Tue, 26 Jun 2018 14:11:07 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/pts/SimaoPY09},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{SimaoP10,
+	author    = {Adenilso da Silva Sim{\~{a}}o and
+	             Alexandre Petrenko},
+	title     = {Fault Coverage-Driven Incremental Test Generation},
+	journal   = {Comput. J.},
+	volume    = {53},
+	number    = {9},
+	pages     = {1508--1522},
+	year      = {2010},
+	url       = {https://doi.org/10.1093/comjnl/bxp073},
+	doi       = {10.1093/comjnl/bxp073},
+	timestamp = {Sat, 20 May 2017 00:22:27 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/cj/SimaoP10},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{SimaoP14,
+	author    = {Adenilso da Silva Sim{\~{a}}o and
+	             Alexandre Petrenko},
+	editor    = {Holger Schlingloff and
+	             Alexander K. Petrenko},
+	title     = {Generating Complete and Finite Test Suite for ioco: {Is} It Possible?},
+	booktitle = {Proceedings Ninth Workshop on Model-Based Testing, {MBT} 2014, Grenoble,
+	             France, 6 April 2014.},
+	series    = {{EPTCS}},
+	volume    = {141},
+	pages     = {56--70},
+	year      = {2014},
+	url       = {https://doi.org/10.4204/EPTCS.141.5},
+	doi       = {10.4204/EPTCS.141.5},
+	timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/corr/SimaoP14},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @techreport{ShinwellP05,
 	title     = {Fresh objective {Caml} user manual},
 	author    = {Mark R. Shinwell and

content/test-methods.tex

@@ -11,9 +11,9 @@ A key aspect of such methods is the size of the obtained test suite.
 On one hand we want to cover as much as the specification as possible.
 On the other hand: testing takes time, so we want to minimise the size of a test suite.
 
-Challenges such as scalability remain an issue in the field.
+The test methods described here are well-known in the literature of FSM-based testing.
-As we see in the case study of the next chapter, real world software components can consist of thousands of states.
+They all share similar concepts, such as access sequences and state identifiers.
-Such amounts of states go beyond the comparative studies of, for example, \citet[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:journals/infsof/EndoS13].
+In this chapter we will define these concepts, relate them with one another and show how to build test suites from these concepts.
 
 
 \startsection
@@ -34,11 +34,11 @@ A \emph{Mealy machine} $M$ consists of a finite set of \emph{states} $S$, an \em
 \item an \emph{output function} $\lambda \colon S \times I \to O$.
 \stopitemize
 
-Both functions are extended inductively to sequences as $\delta \colon S \times I^{\ast} \to S$ and $\lambda \colon S \times I^{\ast} \to O^{\ast}$:
+Both the transition function and output function are extended inductively to sequences as $\delta \colon S \times I^{\ast} \to S$ and $\lambda \colon S \times I^{\ast} \to O^{\ast}$:
-\startformula\startalign[n=4, align={right,left,right,left}]
+\startformula\startmathmatrix[n=4, align={right,left,right,left},distance=1pt]
 \NC \delta(s, \epsilon) \NC = s \NC\quad \lambda(s, \epsilon) \NC = \epsilon \NR
-\NC \delta(s, aw) \NC = \delta(\delta(s, a), w) \NC\quad \lambda(s, aw) \NC = \lambda(s, a)\lambda(\delta(s, a), w) \NR
+\NC \delta(s, aw) \NC = \delta(\delta(s, a), w) \NC\qquad \lambda(s, aw) \NC = \lambda(s, a)\lambda(\delta(s, a), w) \NR
-\stopalign\stopformula
+\stopmathmatrix\stopformula
 By abuse of notation we will often write $s \in M$ instead of $s \in S$.
 For a second Mealy machine $M'$ its members are denoted $S', s'_0, \delta'$ and $\lambda'$ by convention.
 
@@ -474,13 +474,12 @@ For this, we simply take all shortest sequences from the initial state to the ot
 
 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:
-%\setupformulas[split=yes,hang=auto]
+\startformula\startmathmatrix[n=2,align={left,left}]
-\startformula
+\NC T_{\text{W}} = \{ \NC aaaaa, aaaac, aaac, aabaa, aabac, aabc, aacaa, \NR
-T_{\text{W}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aabac, aabc, aacaa, \breakhere
+\NC \NC aacac, aacc, abaa, abac, abc, acaa, acac, acc, baaaa, \NR
-aacac, aacc, abaa, abac, abc, acaa, acac, acc, baaaa, \breakhere
+\NC \NC baaac, baac, babaa, babac, babc, bacaa, bacac, bacc, \NR
-baaac, baac, babaa, babac, babc, bacaa, bacac, bacc, \breakhere
+\NC \NC bbaa, bbac, bbc, bcaa, bcac, bcc, caa, cac, cc \quad \} \NR
-bbaa, bbac, bbc, bcaa, bcac, bcc, caa, cac, cc \} \breakhere
+\stopmathmatrix\stopformula
-\stopformula
 
 With the Wp-method we get to choose a different state identifier per state.
 Since many states have an UIO, we can use them as state identifiers.
@@ -495,10 +494,10 @@ This defines the following family $\Fam{W}$:
 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:
-\startformula
+\startformula\startmathmatrix[n=2,align={left,left}]
-T_{\text{Wp}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aacaa, abaa, acaa, \breakhere
+\NC T_{\text{Wp}} = \{ \NC aaaaa, aaaac, aaac, aabaa, aacaa, abaa, \NR
-baaac, baac, babaa, bacc, bbac, bcaa, caa \} \breakhere
+\NC \NC acaa, baaac, baac, babaa, bacc, bbac, bcaa, caa \quad \} \NR
-\stopformula
+\stopmathmatrix\stopformula
 
 For the HSI method we need a separating family.
 We pick the following sets:
@@ -513,11 +512,11 @@ 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.
 When combining this with the corresponding prefixes, we obtain the HSI test suite of size 125:
-\startformula
+\startformula\startmathmatrix[n=2,align={left,left}]
-T_{\text{HSI}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aabc, aacaa, \breakhere
+\NC T_{\text{HSI}} = \{ \NC aaaaa, aaaac, aaac, aabaa, aabc, aacaa, aacc, \NR
-aacc, abaa, abc, acaa, acc, baaaa, baaac, baac, babaa, \breakhere
+\NC \NC abaa, abc, acaa, acc, baaaa, baaac, baac, babaa, \NR
-babc, baca, bacc, bbaa, bbac, bbc, bcaa, bcc, caa, cc \} \breakhere
+\NC \NC babc, baca, bacc, bbaa, bbac, bbc, bcaa, bcc, caa, cc \quad \} \NR
-\stopformula
+\stopmathmatrix\stopformula
 On this particular example the Wp method outperforms the HSI method.
 The reason is that many states have UIOs and we picked those to be the state identifiers.
 In general, however, UIOs may not exist (and finding them is hard).
@@ -700,21 +699,20 @@ From the splitting tree in \in{Figure}[fig:example-splitting-tree], we obtain th
 From the figure above we obtain the family $\Fam{Z'}$.
 These families and the refinement $\Fam{Z'}; \Fam{H}$ are given below:
 
-\starttabulate[|l|l|l|]
+\startformula\startmathmatrix[n=3,align={left,left,left},distance=1cm]
-\NC $H_0 = \{aa,c\}$    \NC $Z'_0 = \{aa\}$ \NC $(Z';H)_0 = \{aa\}$     \NC\NR
+\NC H_0 = \{aa,c\}    \NC Z'_0 = \{aa\} \NC (Z';H)_0 = \{aa\}      \NR
-\NC $H_1 = \{a\}$       \NC $Z'_1 = \{a\}$  \NC $(Z';H)_1 = \{a\}$      \NC\NR
+\NC H_1 = \{a\}       \NC Z'_1 = \{a\}  \NC (Z';H)_1 = \{a\}       \NR
-\NC $H_2 = \{aa,ac,c\}$ \NC $Z'_2 = \{aa\}$ \NC $(Z';H)_2 = \{aa,ac,c\}$ \NC\NR
+\NC H_2 = \{aa,ac,c\} \NC Z'_2 = \{aa\} \NC (Z';H)_2 = \{aa,ac,c\} \NR
-\NC $H_3 = \{a,c\}$     \NC $Z'_3 = \{aa\}$ \NC $(Z';H)_3 = \{aa,c\}$  \NC\NR
+\NC H_3 = \{a,c\}     \NC Z'_3 = \{aa\} \NC (Z';H)_3 = \{aa,c\}    \NR
-\NC $H_4 = \{aa,ac,c\}$ \NC $Z'_4 = \{aa\}$ \NC $(Z';H)_4 = \{aa,ac,c\}$   \NC\NR
+\NC H_4 = \{aa,ac,c\} \NC Z'_4 = \{aa\} \NC (Z';H)_4 = \{aa,ac,c\} \NR
-\stoptabulate
+\stopmathmatrix\stopformula
-\todo{In startformula/startalign zetten}
 
 With the separating family $\Fam{Z}'; \Fam{H}$ we obtain the following test suite of size 96:
-\startformula
+\startformula\startmathmatrix[n=2,align={left,left}]
-T_{\text{h-ADS}} = \{ \alignhere aaaaa, aaaac, aaac, aabaa, aacaa, abaa, acaa, \breakhere
+\NC T_{\text{h-ADS}} = \{ \NC aaaaa, aaaac, aaac, aabaa, aacaa, abaa, acaa, \NR
-baaaa, baaac, baac, babaa, bacaa, bacc, bbaa, bbac, \breakhere
+\NC \NC baaaa, baaac, baac, babaa, bacaa, bacc, bbaa, bbac, \NR
-bbc, bcaa, caa \} \breakhere
+\NC \NC bbc, bcaa, caa \quad \} \NR
-\stopformula
+\stopmathmatrix\stopformula
 
 We note that this is indeed smaller than the HSI test suite.
 In particular, we have a smaller state identifier for $s_0$: $\{ aa \}$ instead of $\{ aa, c \}$.
@@ -731,6 +729,25 @@ We note that \in{Algorithm}[alg:hybrid] is implemented a bit more efficiently, a
 For constructing the splitting trees in the first place, we use Moore's minimisation algorithm and the algorithms by \citet[DBLP:journals/tc/LeeY94].
 
 
+\stopsubsection
+\startsubsection
+  [title={When $k$ is not known}]
+
+In many of the applications such as learning, no bound on the number of states of the SUT was known.
+In such cases it is possible to randomly select test cases from an infinite test suite.
+Unfortunately, we lose the theoretical guarantees of completeness with random generation.
+Still, as we will see in \in{Chapter}[chap:applying-automata-learning], this can work really well.
+
+We can randomly test cases as follows.
+In the above definition for the hybrid ADS test suite we replace $I^{\leq k}$ by $I^{\ast}$ to obtain an infinite test suite.
+Then we sample tests as follows:
+\startitemize[n]
+\item sample an element $p$ from $P$ uniformly,
+\item sample a word $w$ from $I^{\ast}$ with a geometric distribution, and
+\item sample uniformly from $(\Fam{Z'} ; \Fam{H})_s$ for the state $s = \delta(s_0, pw)$.
+\stopitemize
+
+
 \stopsubsection
 \stopsection
 \startsection
@@ -810,7 +827,8 @@ The next lemma gives sufficient conditions for a test suite of the given anatomy
 complete.
 We then prove that these conditions hold for the test suites in this paper.
 
-\startlemma
+\startproposition
+  [reference=prop:completeness]
 Let $\Fam{W}$ and $\Fam{W'}$ be two families of words and $P$ a state cover for $M$.
 Let $T = P \cdot I^{\leq k} \odot \Fam{W} \,\cup\, P \cdot I^{\leq k+1} \odot \Fam{W'}$ be a test suite.
 If
@@ -821,7 +839,7 @@ If
 \stopitemize
 then $M$ and $M'$ are equivalent.
 \todo{Puntje 2 verdient meer aandacht?}
-\stoplemma
+\stopproposition
 \startproof
 First, we prove that $P \cdot I^{\leq k}$ reaches all states in $M'$.
 For $p, q \in P$ and $x = \delta(s_0, p), y = \delta(s_0, q)$ such that $x \not\sim_{W_x \cap W_y} y$, we also have $\delta'(m'_0, p) \not\sim_{W_x \cap W_y} \delta'(m'_0, q)$ in the implementation $M'$.
@@ -893,58 +911,52 @@ The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
 
 \stopsection
 \startsection
-  [title={Related Work and discussion}]
+  [title={Related Work and Discussion}]
 
-\todo{Opnieuw lezen, want verouderd. Voeg toe: non-det, no-reset, transition tour, checking sequence. Future work: benchmarks (ref benchmark wiki).}
+In this chapter we have mostly considered classical test methods which are all based on prefixes and state identifiers.
-Comparison of test methods already appeared in the recent papers by \citet[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:journals/infsof/EndoS13].
+There are more recent methods which almost fit in the same framework.
-Their work is mainly evaluated on randomly generated Mealy machines.
+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).
-Many of the methods described here are benchmarked on small Mealy machines in \cite[DBLP:journals/infsof/DorofeevaEMCY10] and \cite[DBLP:journals/infsof/EndoS13].
+It does not generalise to extra states, but it seems to construct very small test suites.
-Additionally, they included the P, H an SPY methods.
+The H method is a refinement of the HSI method where state identifiers for a testing transitions are reconsidered.
-Unfortunately, the P and H methods do not fit naturally in the overview presented in \in{Section}[sec:overview].
+(Note that \in{Proposition}[prop:completeness] allows for a different family when testing transitions.)
-The P method is not able to test for extra states, making it less usable.
+Last, the SPY method builds upon the HSI-method and changes the prefixes in order to minimise the size of a test suite, exploiting overlap in test sequences.
-And the H method \todo{?}
-The SPY method builds upon the HSI-method and changes the prefixes in order to minimise the size of a test suite, exploiting overlap in test sequences.
 We believe that this technique is independent of the HSI-method and can in fact be applied to all methods presented in this paper.
 As such, the SPY method should be considered as an optimisation technique, orthogonal to the work in this paper.
 
-More recently, a novel test method was devised which uses incomplete distinguishing sequences \cite[DBLP:journals/cj/HieronsT15].
+Recently, \citet[DBLP:journals/cj/HieronsT15] devise a novel test method which is based on incomplete distinguishing sequences and is similar to the hybrid ADS method.
 They use sequences which can be considered to be adaptive distinguishing sequences on a subset of the state space.
 With several of those one can cover the whole state space, obtaining a $m$-complete test suite.
-This is a bit dual to our approach, as our \quotation{incomplete} adaptive distinguishing sequences define a course partition of the state space.
+This is a bit dual to our approach, as our \quotation{incomplete} adaptive distinguishing sequences define a course partition of the complete state space.
 Our method becomes complete by refining the tests with pairwise separating sequences.
 
-Some work is put into minimizing the adaptive distinguishing sequences themselves.
+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.
-\todo{We expect that similar
+Moreover, they show that finding the minimal adaptive distinguishing sequence is NP-complete in general, even approximation is NP-complete.
-	heuristics also exist for the other test methods and that it will improve the
+We expect that similar heuristics also exist for the other test methods and that it will improve the performance.
-	performance.}
+Note that minimal separating sequences do not guarantee a minimal test suite.
-However, they show that finding the minimal adaptive distinguishing sequence is NP-complete in general, even approximation is NP-complete.
+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.
-We would like to incorporate their greedy algorithms in our implementation.
+
-\todo{Noem minimal sep seqs. Dit is niet genoeg voor een minimal test suite.}
+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].
+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 game theoretic point of view is further investigated by \citet[BosS18].
+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.
+If the machine has no reliable reset (or the reset is too expensive), one tests the system with a single \emph{checking sequence}.
+\citet[DBLP:journals/tc/LeeY94] give a randomised algorithm for constructing such a checking sequence using adaptive distinguishing sequences.
+There is a similarity with the randomised algorithm by \citet[DBLP:journals/iandc/RivestS93] for learning non-resettable automata.
+Recently, \citet[GrozSPO16] give a deterministic learning algorithm for non-resettable machines based on adaptive distinguishing sequences.
+
+Many of the methods described here are benchmarked on small or random Mealy machines by \citet[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:journals/infsof/EndoS13].
+The benchmarks are of limited scope, the machine from \in{Chapter}[chap:applying-automata-learning], for instance, is neither small nor random.
+For this reason, we started to collect more realistic benchmarks at \href{http://automata.cs.ru.nl/}.
 
 
-\startsubsection
-  [title={When $k$ is not known}]
-
-In many of the applications such as learning, no bound on the number of states of the SUT was known.
-In such cases it is possible to randomly select test cases from an infinite test suite.
-Unfortunately, we lose the theoretical guarantees of completeness with random generation.
-Still, as we will see in \in{Chapter}[chap:applying-automata-learning], this can work really well.
-
-We can randomly test cases as follows.
-In the above definition for the hybrid ADS test suite we replace $I^{\leq k}$ by $I^{\ast}$ to obtain an infinite test suite.
-Then we sample tests as follows:
-\startitemize[n]
-\item sample an element $p$ from $P$ uniformly,
-\item sample a word $w$ from $I^{\ast}$ with a geometric distribution, and
-\item sample uniformly from $(\Fam{Z'} ; \Fam{H})_s$ for the state $s = \delta(s_0, pw)$.
-\stopitemize
-This random testing method is also implemented in the \kw{hybrid ADS} tool.
-\todo{Hoe te verwijzen?}
-
-
-\stopsubsection
 \stopsection
 \referencesifcomponent
 \stopchapter

environment/bib.tex

@@ -1,5 +1,11 @@
 \startenvironment bib
 
+% https://wiki.contextgarden.net/Question_marks_in_bibliography_entries
+\def\gobblestop#1#2{#1}
+\def\killstop{%
+  \aftergroup\gobblestop
+  }
+
 \usebtxdefinitions[apa]
 \usebtxdataset[../biblio.bib]
 \usebtxdataset[../biblio-eigen.bib]
@@ -12,6 +18,7 @@
 \btxremapauthor [Michal Szynwelski] [Micha\l{} Szynwelski]
 \btxremapauthor [Slawomir Lasota] [S\l{}awomir Lasota]
 \btxremapauthor [Eryk Kopczynski] [Eryk Kopczy\'nski]
+\btxremapauthor [Adenilso da Silva Simão] [Adenilso Simão]
 
 \def\citenp[#1]{\cite[left=,right=][#1]}   % Bla and Foo, 2015
 \def\citet[#1]{\cite[authoryears][#1]}     % Bla and Foo (2015)