mirror of
https://github.com/Jaxan/hybrid-ads.git
synced 2025-04-27 15:07:45 +02:00
61 lines
3.6 KiB
TeX
61 lines
3.6 KiB
TeX
\subsubsection{Augmented DS-method}
|
|
\label{sec:randomPrefix}
|
|
|
|
In order to reduce the number of tests, Chow~\cite{Ch78} and
|
|
Vasilevskii~\cite{vasilevskii1973failure} pioneered the so called W-method. In
|
|
their framework a test query consists of a prefix $p$ bringing the SUL to a
|
|
specific state, a (random) middle part $m$ and a suffix $s$ assuring that the
|
|
SUL is in the appropriate state. This results in a test suite of the form $P
|
|
I^{\leq k} W$, where $P$ is a set of (shortest) access sequences, $I^{\leq k}$
|
|
the set of all sequences of length at most $k$, and $W$ is a characterization
|
|
set. Classically, this characterization set is constructed by taking the set of
|
|
all (pairwise) separating sequences. For $k=1$ this test suite is complete in
|
|
the sense that if the SUL passes all tests, then either the SUL is equivalent to
|
|
the specification or the SUL has strictly more states than the specification. By
|
|
increasing $k$ we can check additional states.
|
|
|
|
We tried using the W-method as implemented by LearnLib to find counterexamples.
|
|
The generated test suite, however, was still too big in our learning context.
|
|
Fujiwara et al \cite{FBKAG91} observed that it is possible to let the set $W$ depend on the state the
|
|
SUL is supposed to be. This allows us to only take a subset of $W$ which
|
|
is relevant for a specific state. This slightly reduces the test suite which is
|
|
as powerful as the full test suite. This methods is known as the Wp-method. More
|
|
importantly, this observation allows for generalizations where we can carefully
|
|
pick the suffixes.
|
|
|
|
In the presence of an (adaptive) distinguishing sequence one can take $W$ to be a
|
|
single suffix, greatly reducing the test suite. Lee and Yannakakis \cite{LYa94} describe an
|
|
algorithm (which we will refer to as the LY algorithm) to efficiently
|
|
construct this sequence, if it exists. In our case, unfortunately, most
|
|
hypotheses did not enjoy existence of an adaptive distinguishing sequence. In
|
|
these cases the incomplete result from the LY algorithm still contained a lot of
|
|
information which we augmented by pairwise separating sequences.
|
|
|
|
\begin{figure}
|
|
\centering \includegraphics[width=\textwidth]{hyp_20_partial_ds.pdf}
|
|
\caption{A small part of an incomplete distinguishing sequence as produced by
|
|
the LY algorithm. Leaves contain a set of possible initial states, inner nodes
|
|
have input sequences and edges correspond to different output symbols (of
|
|
which we only drew some), where Q stands for quiescence.}
|
|
\label{fig:distinguishing-sequence}
|
|
\end{figure}
|
|
|
|
As an example we show an incomplete adaptive distinguishing sequence for one of
|
|
the hypothesis in Figure~\ref{fig:distinguishing-sequence}. When we apply the
|
|
input sequence I46 I6.0 I10 I19 I31.0 I37.3 I9.2 and observe outputs O9 O3.3 Q ...
|
|
O28.0, we know for sure that the SUL was in state 788. Unfortunately not all
|
|
path lead to a singleton set. When for instance we apply the sequence I46 I6.0
|
|
I10 and observe the outputs O9 O3.14 Q, we know for sure that the SUL was in one
|
|
of the states 18, 133, 1287 or 1295. In these cases we have to perform more
|
|
experiments and we resort to pairwise separating sequences.
|
|
|
|
We note that this augmented DS-method is in the worst case not any better than
|
|
the classical Wp-method. In our case, however, it greatly reduced the test
|
|
suites.
|
|
|
|
Once we have our set of suffixes, which we call $Z$ now, our test algorithm
|
|
works as follows. The algorithm first exhausts the set $P I^{\leq 1} Z$. If this
|
|
does not provide a counterexample, we will randomly pick test queries from $P
|
|
I^2 I^\ast Z$, where the algorithm samples uniformly from $P$, $I^2$ and $Z$ (if
|
|
$Z$ contains more that $1$ sequence for the supposed state) and with a geometric
|
|
distribution on $I^\ast$.
|