Package de.learnlib.counterexample

Class GlobalSuffixFinders

java.lang.Object

de.learnlib.counterexample.GlobalSuffixFinders

public final class GlobalSuffixFinders
extends Object

A collection of suffix-based global counterexample analyzers.

See Also:

GlobalSuffixFinder

Field Summary

Fields

Modifier and Type	Field	Description
static GlobalSuffixFinder<@Nullable Object,@Nullable Object>	FIND_LINEAR	Adds the single suffix found by the access sequence transformation in ascending linear order.
static GlobalSuffixFinder<@Nullable Object,@Nullable Object>	FIND_LINEAR_ALLSUFFIXES	Adds the suffix found by the access sequence transformation in ascending linear order, and all of its suffixes.
static GlobalSuffixFinder<@Nullable Object,@Nullable Object>	FIND_LINEAR_REVERSE	Adds the single suffix found by the access sequence transformation in descending linear order.
static GlobalSuffixFinder<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable Object>	MALER_PNUELI	Adds all suffixes of the input word, as suggested by Maler & Pnueli.
static GlobalSuffixFinder<@Nullable Object,@Nullable Object>	RIVEST_SCHAPIRE	Adds the single suffix found by the access sequence transformation using binary search.
static GlobalSuffixFinder<@Nullable Object,@Nullable Object>	RIVEST_SCHAPIRE_ALLSUFFIXES	Adds the suffix found by the access sequence transformation using binary search, and all of its suffixes.
static GlobalSuffixFinder<@Nullable Object,@Nullable 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	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<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable Object> MALER_PNUELI

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

See Also:

findMalerPnueli(Query)

SHAHBAZ

public static final GlobalSuffixFinder<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable 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<@Nullable Object,@Nullable 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 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 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 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 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 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 to include all suffixes of the found suffix

Returns:

the distinguishing suffixes

See Also:

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

values

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