Worked on very first chapters (stubs)

content.tex

@@ -10,9 +10,7 @@
 \completelistoftables
 \completelistofalgorithms
 
-\chapter{Intro}
+\component content/introduction
-\section{Learning and Testing}
-\section{Nominal Techniques}
 \component content/test-methods
 \component content/applying-automata-learning
 \component content/minimal-separating-sequences

content/introduction.tex

@@ -0,0 +1,28 @@
+\project thesis
+\startcomponent introduction
+
+\startchapter
+  [title={Pakkende titel},
+   reference=chap:introduction]
+
+\startsection
+  [title={Learning and Testing}]
+
+\todo{Gekopieerd van test methods paper.}
+
+Finite state machine conformance testing is a core topic in testing literature that is relevant for communication protocols and other reactive systems.
+The combination of conformance testing and automata learning is applied in practice and it proves to be an effective way of finding bugs \cite[Joeri], replacing legacy software \cite[Philips], or inferring models to be used in model checking \cite[MeinkeSindhu].
+
+Several model learning applications:
+learning embedded controller software \cite[DBLP:conf/icfem/SmeenkMVJ15], learning the TCP protocol \cite[DBLP:conf/cav/Fiterau-Brostean16] and learning the MQTT protocol \cite[DBLP:conf/icst/TapplerAB17].
+
+
+\stopsection
+\startsection
+  [title={Nominal Techniques}]
+
+
+\stopsection
+\referencesifcomponent
+\stopchapter
+\stopcomponent

content/minimal-separating-sequences.tex

@@ -664,7 +664,7 @@ We note that different slopes imply different complexity classes, since both axe
 
 \startplacefigure
   [title={Running time in seconds of \in{Algorithm}[alg:increase-k] (grey) and \in{Algorithm}[alg:increase-k-v3] (black).},
-   list={Running time in seconds of \in{Algorithms}[alg:increase-k, alg:increase-k-v3].}
+   list={Running time of \in{Algorithms}[alg:increase-k] and \in{}[alg:increase-k-v3].},
    reference=fig:results]
 \startcombination[2*1]
 {\starttikzpicture

content/test-methods.tex

@@ -8,6 +8,17 @@
 \startsection
   [title={Preliminaries}]
 
+In this chapter we will discuss some of the theory of test generation methods.
+From this theoretical discussion we derive a new algorithm: the \emph{hybrid ads methods}, which is applied on a case study in \in{Chapter}[chap:applying-automata-learning].
+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.
+As we see in the case study of the next chapter, real world software components can consist of thousands of states.
+Such amounts of states go beyond the comparative studies of, for example, \citet[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:journals/infsof/EndoS13].
+
+
 \startsubsection
   [title={Words and Mealy machines}]
 
@@ -41,9 +52,7 @@ An example Mealy machine is given in \in{Figure}[fig:running-example].
    list={An example specification.},
    reference=fig:running-example]
 \hbox{
-\starttikzpicture[shorten >=2pt,node distance=0.9cm and 3cm,bend angle=20]
+\starttikzpicture[node distance=0.9cm and 3cm,bend angle=20]
-	\tikzstyle{every state}=[draw=black,text=black,inner
-	sep=2pt,minimum size=12pt,initial text=]
 	\node[state] (0) {$s_0$};
 	\node[state] (1) [above left = of 0] {$s_1$};
 	\node[state] (2) [below left = of 0] {$s_2$};
@@ -78,6 +87,7 @@ In conformance testing we have a specification modelled as a Mealy machine and a
 Tests 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.
 The goals is to test as little as possible, while covering as much as possible.
+\todo{Aannames in een itemize zetten en in rel/fut work bespreken.}
 
 \startdefinition[reference=test-suite]
 A \emph{test suite} is a finite subset $T \subseteq I^{\ast}$.
@@ -116,18 +126,14 @@ This justifies the following definition.
    reference=fig:incompleteness-example]
 \startcombination[2*1]
 {\hbox{
-	\starttikzpicture[shorten >=2pt,node distance=2cm]
+	\starttikzpicture
-	\tikzstyle{every state}=[draw=black,text=black,inner
-	sep=2pt,minimum size=12pt,initial text=]
 	\node[state] (0) {$s_0$};
 	\path[->]
 	(0) edge [loop] node [below] {${a}/0$} (0);
 	\stoptikzpicture
 }} {(a)}
 {\hbox{
-	\starttikzpicture[shorten >=2pt,node distance=2cm]
+	\starttikzpicture
-	\tikzstyle{every state}=[draw=black,text=black,inner
-	sep=2pt,minimum size=12pt,initial text=]
 	\node[state] (0) {$s'_0$};
 	\node[state] (1) [right of=0] {$s'_1$};
 	\node        (2) [right of=1] {$\cdots$};
@@ -266,11 +272,10 @@ Our method described is very similar to some of these methods, so we will relate
 
 There are many more test generation methods.
 Literature shows, however, that not all of them are complete.
-For example, the methods in \cite[DBLP:journals/tosem/Bernhard94] are falsified by \cite[DBLP:journals/tosem/Petrenko97] and the UIO-method \cite[DBLP:journals/cn/SabnaniD88] is shown to be incomplete in \cite[DBLP:conf/sigcomm/ChanVO89].
+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 that reason, completeness of the correct methods is shown (again) in the next section.
+For that reason, completeness of the correct methods is shown in the next section.
 We fix a state cover $P$ throughout this section and take the transition cover $Q = P \cdot I$.
-
+\todo{In v1 gebruik ik een andere volgorde: UIOv, Wp, HSI, ADS. Ook voorbeeld uitrekenen.}
-\todo{Gebruik de volgorde en uitleg zoals in versie 1 van dit paper. Inclusief tegenvoorbeeld voor de UIO methode.}
 
 
 \startsubsection
@@ -278,6 +283,7 @@ We fix a state cover $P$ throughout this section and take the transition cover $
    reference=sec:w]
 
 Possibly one of the earliest $m$-complete test methods.
+\todo{Opmerking over Moore's vermoeden?}
 
 \startdefinition
   [reference=w-method]
@@ -361,6 +367,46 @@ Let $\Fam{U} = \{ \text{a single UIO for } s \}_{s \in S}$ be a family of UIO se
 $P \cdot I^{\leq k} \cdot \bigcup \Fam{U} \,\cup\, Q \cdot I^{\leq k} \odot \Fam{U}$.
 \stopdefinition
 
+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 UIO-method which defines the test suite $(P \cup Q) \cdot I^{\leq k} \odot \Fam{U}$.
+The example in \in{Figure}[fig:uio-counterexample] shows that this does not necessarily define a 3-complete test suite (this example is due to \citenp[DBLP:conf/sigcomm/ChanVO89]).
+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$.
+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$.
+
+\startplacefigure
+  [title={An example where the UIO method is not complete.},
+   reference=fig:uio-counterexample]
+\startcombination[2*1]
+{\hbox{\starttikzpicture
+  \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[->]
+  (0) edge [bend left=20 ] node [left ] {${a}/0$} (1)
+  (0) edge [bend right=15] node [below] {${b}/1$} (2)
+  (1) edge [bend left=20 ] node [left ] {${a}/1$} (0)
+  (1) edge [bend right=20] node [right] {${b}/1$} (2)
+  (2) edge [bend right=20] node [below] {${a}/0$} (0)
+  (2) edge [bend right=15] node [right] {${b}/1$} (1);
+\stoptikzpicture}} {Specification}
+{\hbox{\starttikzpicture
+  \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[->]
+  (0) edge [bend left=20 ] node [left ] {${a}/0$} (1)
+  (0) edge [bend right=15] node [below] {${b}/1$} (2)
+  (1) edge [bend left=20 ] node [left ] {${a}/1$} (0)
+  (1) edge [loop         ] node [above] {${b}/1$} (1)
+  (2) edge [bend right=20] node [below] {${a}/0$} (0)
+  (2) edge [bend right=15] node [right] {${b}/1$} (1);
+\stoptikzpicture}} {Implementation}
+\stopcombination
+\stopplacefigure
+
 
 \stopsubsection
 \startsubsection
@@ -391,14 +437,14 @@ A \defn{splitting tree (for $M$)} is a rooted tree where each node $u$ has
 We require that if a node $u$ has children $C(u)$ then
 \startitemize
 	\item the sets of states of the children of $u$ partition $l(u)$, i.e., the set
-	$P(u) = \{l(v) \,|\, v \in C(u)\}$ is a partition of $l(u)$, and
+	$P(u) = \{l(v) \,|\, v \in C(u)\}$ is a \todo{non-trivial} partition of $l(u)$, and
 	\item the sequence $\sigma(u)$ witnesses the partition $P(u)$, meaning that
 	$\lambda(s, \sigma(u)) = \lambda(t, \sigma(u))$ iff $p = q$ for all $s \in p, t \in q$ for all $p, q \in P(u)$.
 \stopitemize
 A splitting tree is called \defn{complete} if all inequivalent states belong to	different leaves.
 \stopdefinition
 
-Efficient construction of a splitting tree is described in more detail in \in{Chapter}[chap:separating-sequences].
+Efficient construction of a splitting tree is described in more detail in \in{Chapter}[chap:minimal-separating-sequences].
 Briefly, the splitting tree records the execution of a partition refinement algorithm (such as Moore's or Hopcroft's algorithm).
 Each non-leaf node encode a \defn{split} together with a witness, which is a separating sequence for its children.
 From such a tree we can construct a state identifier for a state by locating the leaf containing that state and collecting all the sequences you read when traversing to the root.
@@ -480,6 +526,7 @@ By \in{Lemma}[lemma:refinement-props] we note the following: in the best case th
 With the hybrid family we can define the test suite as follows.
 In words, the suite consists of tests of the form $p w s$, where $p$ brings the SUT to a certain state, $w$ is to detect $k$ extra states and $s$ is to identify the state.
 Its $m$-completeness is proven in \in{Section}[sec:completeness].
+\todo{https://gitlab.science.ru.nl/moerman/hybrid-ads}
 
 \startdefinition
 Let $P$ be a state cover,
@@ -594,9 +641,6 @@ The following test suites are all $n+k$-complete:
 \todo{Iets zeggen over de hybrid UIO method.}
 \todo{Geef groottes van suites voor het voorbeeld. Merk op dat ADS and UIOv niet van toepassing zijn (state 2 heeft geen UIO)}
 
-The incomplete \defn{UIO test suite} is defined as $(P \cup Q) \cdot I^{\leq k} \odot \Fam{U}$, incompleteness is shown in \cite[DBLP:conf/sigcomm/ChanVO89].
-\todo{In UIOv sectie.}
-
 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.
 
@@ -715,7 +759,7 @@ The HSI, ADS and hybrid ADS test suites are $n+k$-complete.
 \startsection
   [title={Related Work and discussion}]
 
-\todo{Opnieuw lezen, want verouderd. Voeg toe: non-det, no-reset.}
+\todo{Opnieuw lezen, want verouderd. Voeg toe: non-det, no-reset, transition tour, checking sequence. Future work: benchmarks (ref benchmark wiki).}
 Comparison of test methods already appeared in the recent papers \cite[DBLP:journals/infsof/DorofeevaEMCY10] and \cite[DBLP:journals/infsof/EndoS13].
 Their work is mainly evaluated on randomly generated Mealy machines.
 We continue their work by evaluating on many specifications from industry.
@@ -743,6 +787,7 @@ In \cite[DBLP:journals/fmsd/TurkerY14] the authors describe greedy algorithms wh
 	performance.}
 However, they show that finding the minimal adaptive distinguishing sequence is NP-complete, even approximation is NP-complete.
 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.}
 
 
 \startsubsection
@@ -768,46 +813,7 @@ Then we sample tests as follows:
 \todo{Future work? Meer benchmarks? Andere automaat-modellen?}
 
 
-\stopsection
-\startsection
-  [title={Applications},
-   reference=sec:applications]
-
-\todo{Kan waarschijnlijk weg. In de introductie wordt gepraat over toepassingen van leren (zie Vaandrager (2017).}
-The presented test generation methods is implemented and used in a couple of applications.
-The implementation can be found on {\tt https://gitlab.science.ru.nl/moerman/hybrid-ads}.
-
-This implementations has been used in several model learning applications:
-learning embedded controller software \cite[DBLP:conf/icfem/SmeenkMVJ15], learning the TCP protocol \cite[DBLP:conf/cav/Fiterau-Brostean16] and learning the MQTT protocol \cite[DBLP:conf/icst/TapplerAB17].
-
-
 \stopsection
 \referencesifcomponent
 \stopchapter
 \stopcomponent
-
-% \begin{algorithm}[h]
-%     \DontPrintSemicolon
-%     \KwIn{A Mealy machine $M$}
-%     \KwResult{A (in)complete valid splitting tree $T$}
-%     initialize $T$ with single node\;
-%     \While{true}{
-%       \ForEach{symbol $a \in I$ and leaf $u \in T$}{
-%         \If{if $\lambda(l(u), a)$ hits two or more outputs and $\delta \times \lambda(-, a)$ is injective on $l(u)$}{
-%           split $u$ accordingly\;
-%           store $a$ as a witness in $\sigma(u)$\;
-%         } \ElseIf{$\delta(l(u), a)$ lands in labels of different leaves and $\delta \times \lambda(-, a)$ is injective on $l(u)$}{
-%           $v \leftarrow lca(\delta(l(u), a))$\;
-%           split $u$ similar to $v$\;
-%           store $a \sigma(v)$ as witness in $\sigma(u)$\;
-%         }
-%       }
-%       \If{no split has been made}{
-%         \Return{constructed tree}
-%       }
-%     }
-%     \caption{(Simplified) algorithm by Lee and Yannakakis. Similarly to
-%     algorithm~\ref{moore} this creates a splitting tree, but additionally only
-%     allows \emph{valid} splits.}
-%     \label{lee-yannakakis}
-% \end{algorithm}

environment.tex

@@ -55,7 +55,7 @@
 \define[1]\todo{\color[red]{\ss \bf #1}}
 \define[1]\label{\todo{\tt \\label #1}}
 
-\define\referencesifcomponent{\doifnotmode{everything}{\section{References}\placelistofpublications}}
+\define\referencesifcomponent{\doifnotmode{everything}{\startsubject[title={References}]\placelistofpublications\stopsubject}}
 
 \usemodule[algorithmic]
 \setupalgorithmic[align=middle,numbercolor=darkgray] % center line numbers