de.learnlib.counterexamples

Interface LocalSuffixFinder<I,D>

Type Parameters:

I - input symbol type upper bound

D - output domain type upper bound

All Known Implementing Classes:

AcexLocalSuffixFinder

public interface LocalSuffixFinder<I,D>

Suffix-based local counterexample analyzer.

Given a query (u, v) which is a counterexample (i.e., the suffix-output for (u,v) is distinct from the target system's output for (u,v)), it calculates the index i of the suffix such that w[i:] (w = uv) still allows to expose a behavioral difference for an adequate prefix. This adequate prefix can be determined as {w[:i]}, where {.} denotes the access sequence of the corresponding word.

The effect of adding such a suffix can be described as follows: {w[:i]} and {w[:i-1]}w[i-1] both lead to the same state in the hypothesis, but a local suffix finder chooses the index i such that the output for ({w[:i]}, w[i:]) and ({w[:i-1]}w[i-1], w[i:]) will differ. Hence, the transition to the state reached by {w[:i]} from {w[:i-1]} is disproved.

Please note that the type parameters of these class only constitute upper bounds for the respective input symbol and output classes, denoting the requirements of the process in general. A suffix finder which does not exploit any properties of the used classes will implement this interface with <Object,Object> generic arguments only. The genericity is still maintained due to the RI and RO generic parameters in the findSuffixIndex(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle) method.

Author:

Malte Isberner

Method Summary

Modifier and Type	Method and Description
<RI extends I,RD extends D> int	findSuffixIndex(Query<RI,RD> ceQuery, AccessSequenceTransformer<RI> asTransformer, SuffixOutput<RI,RD> hypOutput, MembershipOracle<RI,RD> oracle) Finds, for a given counterexample, a "split index", such that: - the part of the query word before this index leads to the state being split - the part of the query word from this index on is a suffix capable of splitting this state.

Method Detail

findSuffixIndex

<RI extends I,RD extends D> int findSuffixIndex(Query<RI,RD> ceQuery,
                                                AccessSequenceTransformer<RI> asTransformer,
                                                SuffixOutput<RI,RD> hypOutput,
                                                MembershipOracle<RI,RD> oracle)

Finds, for a given counterexample, a "split index", such that: - the part of the query word before this index leads to the state being split - the part of the query word from this index on is a suffix capable of splitting this state.

Type Parameters:

RI - real input symbol class used for *this* counterexample analysis

RD - real output class used for *this* counterexample analysis

Parameters:

ceQuery - the counterexample query that triggered the refinement. Note that the same restrictions as in LearningAlgorithm.refineHypothesis(de.learnlib.oracles.DefaultQuery) apply.

asTransformer - an AccessSequenceTransformer used for access sequence transformation, if applicable.

hypOutput - interface to the output generation of the hypothesis, with the aim of comparing outputs of the hypothesis and the SUL.

oracle - interface to the System Under Learning (SUL).

Returns:

an adequate split index, or -1 if the counterexample could not be analyzed.