Test methods: voorbeeldjes in begin

content/test-methods.tex

@@ -17,14 +17,15 @@ Such amounts of states go beyond the comparative studies of, for example, \citet
 
 
 \startsection
-  [title={Words and Mealy machines}]
+  [title={Mealy machines and sequences}]
 
 We will focus on Mealy machines, as those capture many protocol specifications and reactive systems.
 Note that we restrict ourselves to deterministic and complete machines.
 
 We fix finite alphabets $I$ and $O$ of inputs respectively outputs.
-We use the usual notation for operations on words:
+We use the usual notation for operations on \emph{sequences} (also called words):
-$uv$ for the concatenation of two words $u, v \in I^{\ast}$ and $|u|$ for the length of $u$.
+$uv$ for the concatenation of two sequences $u, v \in I^{\ast}$ and $|u|$ for the length of $u$.
+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:
@@ -33,16 +34,21 @@ 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 to words as $\delta \colon S \times I^{\ast} \to S$ and $\lambda \colon S \times I^{\ast} \to O^{\ast}$.
+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}$:
-By abuse of notation we will often write $s \in M$ instead of $s \in S$ and leave out $S$ altogether.
+\startformula\startalign[n=4, align={right,left,right,left}]
+\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
+\stopalign\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.
 
 The \emph{behaviour} of a state $s$ is given by the output function $\lambda(s, -) \colon I^{\ast} \to O^{\ast}$.
 Two states $s$ and $t$ are \emph{equivalent} if they have equal behaviours, written $s \sim t$, and two Mealy machines are equivalent if their initial states are equivalent.
 \stopdefinition
 
-{\todo{Voorbeeld gebruiken in komende sectie: uios: $0: aa$, $1: a$, $2$ geen uio, $3: v$ en $4: ac$. Een char. set is $\{ aa, c, ac \}$. Geen ADS (want $2$ geen uio).}}
 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\}$.},
@@ -69,7 +75,7 @@ An example Mealy machine is given in \in{Figure}[fig:running-example].
 	(3) edge [bend right]    node [above] {${b}/0$} (0)
 	(3) edge [loop right]    node [right] {${c}/1$} (3)
 	(4) edge [bend left]     node [right] {${a}/1$} (3)
-	(4) edge [loop right]    node [right] {${b}/1$} (4)
+	(4) edge [loop right]    node [right] {${b}/0$} (4)
 	(4) edge [bend right]    node [above] {${c}/0$} (0);
 \stoptikzpicture
 }
@@ -79,11 +85,19 @@ An example Mealy machine is given in \in{Figure}[fig:running-example].
 \startsubsection
   [title={Testing}]
 
-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 \cite[DBLP:journals/tc/LeeY94].
+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 are generated from the specification and applied to the implementation. We assume that we can reset the implementation before every test.
+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.
 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.}
+
+We assume the following
+\startitemize
+\item
+The system can be modelled as Mealy machine.
+In particular, this means it is \emph{deterministic} and \emph{complete}.
+\item
+We are able to reset the system, i.e., bring it back to the initial state.
+\stopitemize
 
 \startdefinition[reference=test-suite]
 A \emph{test suite} is a finite subset $T \subseteq I^{\ast}$.
@@ -95,8 +109,8 @@ We denote the set of maximal tests of $T$ with $max(T)$.
 \stopdefinition
 
 The maximal tests are the only tests in $T$ we actually have to apply to our SUT as we can record the intermediate outputs.
-Also note that we do not have to consider outputs in the test suite, as those follow from the deterministic specification.
+Also note that we do not have to encode outputs in the test suite, as those follow from the deterministic specification.
-We define the size of a test suite as usual \cite[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:conf/hase/Petrenko0GHO14].
+We define the size of a test suite as usual \citep[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:conf/hase/Petrenko0GHO14].
 The size of a test suite is measured as the sum of the lengths of all its maximal tests plus one reset per test.
 
 \startdefinition[reference=test-suite-size]
@@ -114,7 +128,7 @@ Consider the specification in \in{Figure}{a}[fig:incompleteness-example].
 This machine will always produce zeroes.
 For any test suite we can make a faulty implementation which passes the test suite.
 Such an implementation might look like \in{Figure}{b}[fig:incompleteness-example] with $n$ big enough.
-This justifies the following definition.
+This shows that no test-suite can be complete and it justifies the following definition.
 
 \startplacefigure
   [title={A basic example showing that finite test suites are incomplete. The implementation on the right will pass any test suite if we choose $n$ big enough.},
@@ -164,40 +178,64 @@ 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 convenience we assume $M$ to be minimal, this implies that distinct states are, in fact, inequivalent.
-All definitions can be generalised to non-minimal $M$, by replacing distinct (or other) with inequivalent.
+All definitions can be generalised to non-minimal $M$, by replacing the word \quote{distinct} (or \quote{other}) with \quote{inequivalent}.
 
-\startitemize[after, before]
+\startdefinition
-\item Given two states $s, t$ of $M$ we say that $w$ is a \defn{separating sequence} if $\lambda(s, w) \neq \lambda(t, w)$.
+Given a Mealy machine $M$ we define the following kinds of sequences.
-\item For a single state $s$, a sequence $w$ is a \defn{unique input output sequence (UIO)} if for every other state $t$ we have $\lambda(s, w) \neq \lambda(t, w)$.
+\startitemize
-\item Finally, a \defn{(preset) distinguishing sequence (DS)} is a single sequence $w$ which separates all states, i.e., for every distinct pair $s, t$ of $M$ we have $\lambda(s, w) \neq \lambda(t, w)$.
+\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)$.
+\item Finally, a \defn{(preset) distinguishing sequence (DS)} is a single sequence $w$ which separates all states of $M$, i.e., for every distinct pair $s, t$ in $M$ we have $\lambda(s, w) \neq \lambda(t, w)$.
 \stopitemize
+\stopdefinition
 
-\todo{Misschien in een definition env zetten? Of in descriptions.}
 The above list is ordered from weaker to stronger notions, i.e., every distinguishing sequence is an UIO sequence for every state.
 Similarly, an UIO for a state $s$ is a separating sequence for $s$ and any other $t$.
 Separating sequences always exist for inequivalent states and finding them efficiently is the topic of \in{Chapter}[chap:separating-sequences].
 On the other hand, UIOs and DSs do not always exist for a machine.
-\todo{For example, ...}.
 
-In order to separate multiple states at once, we might need sets of states.
+\startexample
-This brings us to the following notions.
+For the machine in \in{Figure}[fig:running-example], we note that state $s_0$ and $s_2$ are separated by the sequence $aa$ (but not by any shorter sequence).
+In fact, the sequence $aa$ is an UIO for state $s_0$ since it is the only state outputting $10$ on that input.
+However, state $s_2$ has no UIO:
+If the sequence were to start with $b$ or $c$, state $s_3$ and $s_4$ respectively have equal transition, which makes it impossible to separate those states after the first symbol.
+If it starts with an $a$, states $s_3$ and $s_4$ are swapped and we make no progress in distinguishing these states from $s_2$.
+Since $s_2$ has no UIO, the machine as a whole does not admit a DS.
 
-\startitemize[after, before]
+In this example, all other states actually have UIOs.
-\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.
+For the states $s_0, s_1, s_3$ and $s_4$, we can pick the sequences $aa, a, c$ and $ac$ respectively.
+In order to separate $s_2$ from the other state, we have to pick multiple sequences.
+For instance, the set $\{aa, ac, c\}$ will separate $s_2$ from all other states.
+\stopexample
+
+\startdefinition
+As the example shows, we need sets of sequences and sometimes even sets of sets of sqeuences -- called \emph{families}.
+\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$.}
+Given a Mealy machine $M$, we define the following kinds of sets of sequences.
+\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.
 \item A \defn{state identifier} for a state $s$ is a set $W$ which contains a separating sequence for every other state $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 sometimes called a \defn{separating family}.
 \todo{Equivalently: $x \sim_\Fam{X} y$ implies $x \sim y$}
 \todo{Preciezer zijn over prefixes...}
-\item Following the definitions in \cite[DBLP:journals/tc/LeeY94], a separating family where each set is a singleton is an \defn{adaptive distinguishing sequence} (ads).
+\item Following the definitions of \citet[DBLP:journals/tc/LeeY94], a separating family where each set is a singleton is an \defn{adaptive distinguishing sequence} (ADS).
 An ads is of special interest since they can identify a state using a single word.
 \stopitemize
+\stopdefinition
 
 These notions are again related.
 We obtain a characterisation set by taking the union of state identifiers for each state.
 For every machine we can construct a set of harmonized state identifiers as will be shown in \in{Chapter}[chap:separating-sequences] and hence every machine has a characterisation set.
 However, an adaptive distinguishing sequence may not exist.
-\todo{Voorbeeld}
+
+\startexample
+As mentioned before, state $s_2$ from \in{Figure}[fig:running-example] has a state identifier $\{aa, ac, b\}$.
+In fact, this set is a characterisation set for the whole machine.
+Since the other states have UIOs, we can pick singleton sets as state identifiers.
+For example, state $s_0$ has the UIO $aa$, so a state identifier for $s_0$ is $\{ aa \}$.
+There is no ADS for this machine.
+\stopexample
 
 Besides sequences which separate states, we also need sequences which brings a machine to specified states.
 
@@ -232,16 +270,15 @@ $x \sim_\Fam{X} y$ if $\lambda(x,w) = \lambda(y,w)$ for all $w \in X_x \cap X_y$
 \todo{Hangt af van $M$, maar is nog niet gefixed}
 \stopitemize
 
-Given a specification $M$ (with states $S$) we define two operations.
+Given a specification $M$ we define two operations.
 We omit $M$ from the notation as the specification is always clear from the context.
 \startitemize[after]
 \item concatenation:
 $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
 \startformula
-(\Fam{X} ; \Fam{Y})_s = X_s \cup \bigcup_{y \sim_\Fam{X} x} D(\Fam{Y}, x, y),
+(\Fam{X} ; \Fam{Y})_s = X_s \,\cup\, Y_s \cap \bigcup_{s \sim_{\Fam{X}} t} Y_t.
 \stopformula
-where $D(\Fam{Y}, x, y) = Pref\{w \mid \lambda(x,w) \neq \lambda(y,w), w \in Y_x \cap Y_y\}$.
 \stopitemize
 
 The latter construction is new and will be used to define a hybrid test generation method in \in{Section}[sec:hybrid].
@@ -264,7 +301,7 @@ For all families $\Fam{X}$ and $\Fam{Y}$:
 
 In this section, we briefly review the classical conformance testing methods:
 the W, Wp, UIO, UIOv, HSI, ADS methods.
-Our method described is very similar to some of these methods, so we will relate them by describing them uniformly.
+Our hybrid ADS method described is very similar to some of these methods, so we will relate them by describing them uniformly.
 
 There are many more test generation methods.
 Literature shows, however, that not all of them are complete.
@@ -284,12 +321,12 @@ Possibly one of the earliest $m$-complete test methods.
 \startdefinition
   [reference=w-method]
 Let $W$ be a characterization set, the \defn{W test suite} is
-defined as $(P \cup Q) \cdot I^{\leq k} \cdot W$.
+defined as
+\startformula
+(P \cup Q) \cdot I^{\leq k} \cdot W .
+\stopformula
 \stopdefinition
 
-If we have a separating family $\Fam{W}$, we can obtain a characterization
-set by flattening: take $W = \bigcup \Fam{W}$.
-
 
 \stopsubsection
 \startsubsection