de.learnlib.counterexamples

Class GlobalSuffixFinders

java.lang.Object

de.learnlib.counterexamples.GlobalSuffixFinders

public final class GlobalSuffixFinders
extends Object

A collection of suffix-based global counterexample analyzers.

Author:

Malte Isberner

See Also:

GlobalSuffixFinder

Field Summary

Fields

Modifier and Type	Field and Description
static GlobalSuffixFinder<Object,Object>	FIND_LINEAR Adds the single suffix found by the access sequence transformation in ascending linear order.
static GlobalSuffixFinder<Object,Object>	FIND_LINEAR_ALLSUFFIXES Adds the suffix found by the access sequence transformation in ascending linear order, and all of its suffixes.
static GlobalSuffixFinder<Object,Object>	FIND_LINEAR_REVERSE Adds the single suffix found by the access sequence transformation in descending linear order.
static GlobalSuffixFinder<Object,Object>	FIND_LINEAR_REVERSE_ALLSUFFIXES Adds the suffix found by the access sequence transformation in descending linear order, and all of its suffixes.
static GlobalSuffixFinder<Object,Object>	MALER_PNUELI Adds all suffixes of the input word, as suggested by Maler & Pnueli.
static GlobalSuffixFinder<Object,Object>	RIVEST_SCHAPIRE Adds the single suffix found by the access sequence transformation using binary search.
static GlobalSuffixFinder<Object,Object>	RIVEST_SCHAPIRE_ALLSUFFIXES Adds the suffix found by the access sequence transformation using binary search, and all of its suffixes.
static GlobalSuffixFinder<Object,Object>	SHAHBAZ Adds all suffixes of the remainder of the input word, after stripping a maximal one-letter extension of an access sequence.

Method Summary

Modifier and Type	Method and Description
static <I,D> List<Word<I>>	findLinear(Query<I,D> ceQuery, AccessSequenceTransformer<I> asTransformer, SuffixOutput<I,D> hypOutput, MembershipOracle<I,D> oracle, boolean allSuffixes) Returns the suffix (plus all of its suffixes, if allSuffixes is true) found by the access sequence transformation in ascending linear order.
static <I,D> List<Word<I>>	findLinearReverse(Query<I,D> ceQuery, AccessSequenceTransformer<I> asTransformer, SuffixOutput<I,D> hypOutput, MembershipOracle<I,D> oracle, boolean allSuffixes) Returns the suffix (plus all of its suffixes, if allSuffixes is true) found by the access sequence transformation in descending linear order.
static <I,D> List<Word<I>>	findMalerPnueli(Query<I,D> ceQuery) Returns all suffixes of the counterexample word as distinguishing suffixes, as suggested by Maler & Pnueli.
static <I,O> List<Word<I>>	findRivestSchapire(Query<I,O> ceQuery, AccessSequenceTransformer<I> asTransformer, SuffixOutput<I,O> hypOutput, MembershipOracle<I,O> oracle, boolean allSuffixes) Returns the suffix (plus all of its suffixes, if allSuffixes is true) found by the binary search access sequence transformation.
static <I,D> List<Word<I>>	findShahbaz(Query<I,D> ceQuery, AccessSequenceTransformer<I> asTransformer) Returns all suffixes of the counterexample word as distinguishing suffixes, after stripping a maximal one-letter extension of an access sequence, as suggested by Shahbaz.
static <I,D> GlobalSuffixFinder<I,D>	fromLocalFinder(LocalSuffixFinder<I,D> localFinder) Transforms a LocalSuffixFinder into a global one.
static <I,D> GlobalSuffixFinder<I,D>	fromLocalFinder(LocalSuffixFinder<I,D> localFinder, boolean allSuffixes) Transforms a LocalSuffixFinder into a global one.
static <I,D> List<Word<I>>	suffixesForLocalOutput(Query<I,D> ceQuery, int localSuffixIdx) Transforms a suffix index returned by a LocalSuffixFinder into a list containing the single distinguishing suffix.
static <I,D> List<Word<I>>	suffixesForLocalOutput(Query<I,D> ceQuery, int localSuffixIdx, boolean allSuffixes) Transforms a suffix index returned by a LocalSuffixFinder into a list of distinguishing suffixes.
static GlobalSuffixFinder<Object,Object>[]	values()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

MALER_PNUELI

public static final GlobalSuffixFinder<Object,Object> MALER_PNUELI

Adds all suffixes of the input word, as suggested by Maler & Pnueli.

See Also:

findMalerPnueli(Query)

SHAHBAZ

public static final GlobalSuffixFinder<Object,Object> SHAHBAZ

Adds all suffixes of the remainder of the input word, after stripping a maximal one-letter extension of an access sequence.

See Also:

findShahbaz(Query, AccessSequenceTransformer)

FIND_LINEAR

public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR

Adds the single suffix found by the access sequence transformation in ascending linear order.

See Also:

findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)

FIND_LINEAR_ALLSUFFIXES

public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR_ALLSUFFIXES

Adds the suffix found by the access sequence transformation in ascending linear order, and all of its suffixes.

See Also:

findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)

FIND_LINEAR_REVERSE

public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR_REVERSE

Adds the single suffix found by the access sequence transformation in descending linear order.

See Also:

findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)

FIND_LINEAR_REVERSE_ALLSUFFIXES

public static final GlobalSuffixFinder<Object,Object> FIND_LINEAR_REVERSE_ALLSUFFIXES

Adds the suffix found by the access sequence transformation in descending linear order, and all of its suffixes.

See Also:

findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)

RIVEST_SCHAPIRE

public static final GlobalSuffixFinder<Object,Object> RIVEST_SCHAPIRE

Adds the single suffix found by the access sequence transformation using binary search.

See Also:

findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)

RIVEST_SCHAPIRE_ALLSUFFIXES

public static final GlobalSuffixFinder<Object,Object> RIVEST_SCHAPIRE_ALLSUFFIXES

Adds the suffix found by the access sequence transformation using binary search, and all of its suffixes.

See Also:

findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)

Method Detail

fromLocalFinder

public static <I,D> GlobalSuffixFinder<I,D> fromLocalFinder(LocalSuffixFinder<I,D> localFinder)

Transforms a LocalSuffixFinder into a global one. This is a convenience method, behaving like fromLocalFinder(LocalSuffixFinder, boolean).

See Also:

fromLocalFinder(LocalSuffixFinder, boolean)

fromLocalFinder

public static <I,D> GlobalSuffixFinder<I,D> fromLocalFinder(LocalSuffixFinder<I,D> localFinder,
                                                            boolean allSuffixes)

Transforms a LocalSuffixFinder into a global one. Since local suffix finders only return a single suffix, suffix-closedness of the set of distinguishing suffixes might not be preserved. Note that for correctly implemented local suffix finders, this does not impair correctness of the learning algorithm. However, without suffix closedness, intermediate hypothesis models might be non-canonical, if no additional precautions are taken. For that reasons, the allSuffixes parameter can be specified to control whether or not the list returned by GlobalSuffixFinder.findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle) of the returned global suffix finder should not only contain the single suffix, but also all of its suffixes, ensuring suffix-closedness.

Parameters:

localFinder - the local suffix finder

allSuffixes - whether or not all suffixes of the found local suffix should be added

Returns:

a global suffix finder using the analysis method from the specified local suffix finder

suffixesForLocalOutput

public static <I,D> List<Word<I>> suffixesForLocalOutput(Query<I,D> ceQuery,
                                                         int localSuffixIdx)

Transforms a suffix index returned by a LocalSuffixFinder into a list containing the single distinguishing suffix.

suffixesForLocalOutput

public static <I,D> List<Word<I>> suffixesForLocalOutput(Query<I,D> ceQuery,
                                                         int localSuffixIdx,
                                                         boolean allSuffixes)

Transforms a suffix index returned by a LocalSuffixFinder into a list of distinguishing suffixes. This list always contains the corresponding local suffix. Since local suffix finders only return a single suffix, suffix-closedness of the set of distinguishing suffixes might not be preserved. Note that for correctly implemented local suffix finders, this does not impair correctness of the learning algorithm. However, without suffix closedness, intermediate hypothesis models might be non-canonical, if no additional precautions are taken. For that reasons, the allSuffixes parameter can be specified to control whether or not the list returned by GlobalSuffixFinder.findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle) of the returned global suffix finder should not only contain the single suffix, but also all of its suffixes, ensuring suffix-closedness.

findMalerPnueli

public static <I,D> List<Word<I>> findMalerPnueli(Query<I,D> ceQuery)

Returns all suffixes of the counterexample word as distinguishing suffixes, as suggested by Maler & Pnueli.

Parameters:

ceQuery - the counterexample query

Returns:

all suffixes of the counterexample input

findShahbaz

public static <I,D> List<Word<I>> findShahbaz(Query<I,D> ceQuery,
                                              AccessSequenceTransformer<I> asTransformer)

Returns all suffixes of the counterexample word as distinguishing suffixes, after stripping a maximal one-letter extension of an access sequence, as suggested by Shahbaz.

Parameters:

ceQuery - the counterexample query

asTransformer - the access sequence transformer

Returns:

all suffixes from the counterexample after stripping a maximal one-letter extension of an access sequence.

findLinear

public static <I,D> List<Word<I>> findLinear(Query<I,D> ceQuery,
                                             AccessSequenceTransformer<I> asTransformer,
                                             SuffixOutput<I,D> hypOutput,
                                             MembershipOracle<I,D> oracle,
                                             boolean allSuffixes)

Returns the suffix (plus all of its suffixes, if allSuffixes is true) found by the access sequence transformation in ascending linear order.

Parameters:

ceQuery - the counterexample query

asTransformer - the access sequence transformer

hypOutput - interface to the hypothesis output

oracle - interface to the SUL output

allSuffixes - whether or not to include all suffixes of the found suffix

Returns:

the distinguishing suffixes

See Also:

LocalSuffixFinders.findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)

findLinearReverse

public static <I,D> List<Word<I>> findLinearReverse(Query<I,D> ceQuery,
                                                    AccessSequenceTransformer<I> asTransformer,
                                                    SuffixOutput<I,D> hypOutput,
                                                    MembershipOracle<I,D> oracle,
                                                    boolean allSuffixes)

Returns the suffix (plus all of its suffixes, if allSuffixes is true) found by the access sequence transformation in descending linear order.

Parameters:

ceQuery - the counterexample query

asTransformer - the access sequence transformer

hypOutput - interface to the hypothesis output

oracle - interface to the SUL output

allSuffixes - whether or not to include all suffixes of the found suffix

Returns:

the distinguishing suffixes

See Also:

LocalSuffixFinders.findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)

findRivestSchapire

public static <I,O> List<Word<I>> findRivestSchapire(Query<I,O> ceQuery,
                                                     AccessSequenceTransformer<I> asTransformer,
                                                     SuffixOutput<I,O> hypOutput,
                                                     MembershipOracle<I,O> oracle,
                                                     boolean allSuffixes)

Returns the suffix (plus all of its suffixes, if allSuffixes is true) found by the binary search access sequence transformation.

Parameters:

ceQuery - the counterexample query

asTransformer - the access sequence transformer

hypOutput - interface to the hypothesis output

oracle - interface to the SUL output

allSuffixes - whether or not to include all suffixes of the found suffix

Returns:

the distinguishing suffixes

See Also:

LocalSuffixFinders.findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)

values

public static GlobalSuffixFinder<Object,Object>[] values()