diff --git a/content/introduction.tex b/content/introduction.tex index 51614d6..4b1ba88 100644 --- a/content/introduction.tex +++ b/content/introduction.tex @@ -229,19 +229,19 @@ More background and other related problems, as well as their complexity results, In the following example we model a record player as a finite state machine. We will not model the audible output -- that would depend not only on the device, but also the record one chooses to play. -Instead, we the only observation we can make is seeing how fast the turntable spins. -The device has two buttons: a start-stop button (\playstop) and a speed toggle (\spin) which chooses between $33 \frac{1}{3}$ rpm and $45$ rpm. -When turned on, the system should start playing immediately at $33 \frac{1}{3}$ rpm -- this is useful for DJing. -The system has four states as depicted in \in{Figure}[fig:record-player]. +Instead, the only observation we can make is looking how fast the turntable spins. +The device has two buttons: a start-stop button (\playstop) and a speed button (\spin) which toggles between $33 \frac{1}{3}$ rpm and $45$ rpm. +When turned on, the system starts playing immediately at $33 \frac{1}{3}$ rpm -- this is useful for DJing. +The intended behaviour of the records player has four states as depicted in \in{Figure}[fig:record-player]. \startplacefigure [title={Behaviour of a record player modelled as a finite state machine.}, reference=fig:record-player] \hbox{\starttikzpicture[node distance=4cm, bend angle=10] - \node[state, initial, align=center] (tl) {slow\\spinning}; - \node[state, right of=tl, align=center] (tr) {fast\\spinning}; - \node[state, below of=tl, align=center] (bl) {no\\spinning}; - \node[state, right of=bl, align=center] (br) {no\\spinning}; + \node[state, initial above, align=center] (tl) {slow\\spinning}; + \node[state, right of=tl, align=center] (tr) {fast\\spinning}; + \node[state, below of=tl, align=center] (bl) {no\\spinning}; + \node[state, right of=bl, align=center] (br) {no\\spinning}; \path[->] (tl) edge [bend right] node [left] {\playstop} (bl) @@ -255,7 +255,60 @@ The system has four states as depicted in \in{Figure}[fig:record-player]. \stoptikzpicture} \stopplacefigure -\todo{I want to give an example (by giving a state machine) of why black box testing is hard.} +Let us consider some faults which could be present in an implementation with four states. +In \in{Figure}[fig:faulty-record-players] two flawed records players are given. +In the first (\in{Figure}{a}[fig:faulty-record-players]) the sequence \playstop\,\spin\,\spin\, leads us to the wrong state. +However, this is not immediately observable, the turntable is in a non-spinning state as it should be. +The fault is only visible when we press \playstop\, once more: now the turntable is spinning fast instead of slow. +The sequence \playstop\,\spin\,\spin\,\playstop\, is a counterexample. +In the second example (\in{Figure}{b}[fig:faulty-record-players]), the fault is again not immediately obvious: after pressing \spin\,\playstop\, we are in the wrong state as observably by pressing \playstop. +Here, the counterexample is \spin\,\playstop\,\playstop. + +When a model of the implementation is given, it is not hard to find counterexamples. +However, in a black box setting we do not have such a model. +In order test whether a black box system is equivalent to a model, we somehow need to test all possible counterexamples. +In this example, a test suite should at least include the sequences \playstop\,\spin\,\spin\,\playstop\, and \spin\,\playstop\,\playstop. + +\startplacefigure + [title={Two faulty record players.}, + reference=fig:faulty-record-players] +\startcombination[nx=2, ny=1, location=top, distance=1.5cm] +{\hbox{\starttikzpicture[node distance=3cm, bend angle=10] + \node[state, initial above, align=center] (tl) {slow\\spinning}; + \node[state, right of=tl, align=center] (tr) {fast\\spinning}; + \node[state, below of=tl, align=center] (bl) {no\\spinning}; + \node[state, right of=bl, align=center] (br) {no\\spinning}; + + \path[->] + (tl) edge [bend right] node [left] {\playstop} (bl) + (tl) edge [bend right] node [below] {\spin} (tr) + (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 [bend right] node [left] {\playstop} (br) + (br) edge [bend right] node [right] {\playstop} (tr) + (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}; + \node[state, right of=tl, align=center] (tr) {fast\\spinning}; + \node[state, below of=tl, align=center] (bl) {no\\spinning}; + \node[state, right of=bl, align=center] (br) {no\\spinning}; + + \path[->] + (tl) edge [bend right] node [left] {\playstop} (bl) + (tl) edge [bend right] node [below] {\spin} (tr) + (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=red] node [below right] {\playstop} (bl) + (br) edge [bend right] node [right] {\playstop} (tr) + (br) edge [bend right] node [above] {\spin} (bl); +\stoptikzpicture}}{b} +\stopcombination +\stopplacefigure + + \todo{I want to move some related work from the second chapter to here}. diff --git a/environment/notation.tex b/environment/notation.tex index f7a91a6..304fdd3 100644 --- a/environment/notation.tex +++ b/environment/notation.tex @@ -13,7 +13,7 @@ \define\bomb{\!\scale[height=.65em]{\symbol[fontawesome][]}} % bomb \define\money{\scale[height=.6em]{\symbol[fontawesome][eur]}\,} % euro sign + space -\define\playstop{\scale[height=.5em]{\symbol[fontawesome][play]}\scale[height=.5em]{\symbol[fontawesome][pause]}} % play / stop symbol +\define\playstop{\scale[height=.5em]{\raise.15ex\hbox{\symbol[fontawesome][play]\symbol[fontawesome][pause]}}} % play / stop symbol \define\spin{\scale[height=.6em]{\symbol[fontawesome][repeat]}} % spinning symbol %\define\spin{\kw{spd}} % spinning symbol