Package net.automatalib.util.automaton.vpa

Class OneSEVPAs

java.lang.Object

net.automatalib.util.automaton.vpa.OneSEVPAs

public final class OneSEVPAs
extends Object

Operations on OneSEVPAs.

Method Summary

Modifier and Type	Method	Description
static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I>	and(OneSEVPA<L1,I> sevpa1, OneSEVPA<L2,I> sevpa2, VPAlphabet<I> alphabet)	Returns a view on the conjunction ("and") of two OneSEVPAs.
static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I>	combine(OneSEVPA<L1,I> sevpa1, OneSEVPA<L2,I> sevpa2, VPAlphabet<I> alphabet, AcceptanceCombiner combiner)	Most general way of combining two OneSEVPAs.
static <L,I> @Nullable Word<I>	computeAccessSequence(OneSEVPA<L,I> sevpa, VPAlphabet<I> alphabet, Predicate<? super L> predicate)	Computes an access sequence over the given alphabet (if existent) such that it reaches a location of the given SEVPA that satisfies the given predicate.
static <L,I> ArrayStorage<Word<I>>	computeAccessSequences(OneSEVPA<L,I> sevpa, VPAlphabet<I> alphabet)	Computes all access sequences over the given alphabet (if existent) to the locations of the given SEVPA.
static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I>	equiv(OneSEVPA<L1,I> sevpa1, OneSEVPA<L2,I> sevpa2, VPAlphabet<I> alphabet)	Returns a view on the equivalence ("<=>") of two OneSEVPAs.
static <L,I> @Nullable Word<I>	findAcceptedWord(OneSEVPA<L,I> sevpa, VPAlphabet<I> alphabet)	Returns a well-matched word (over the given alphabet) that is accepted by the given SEVPA, if existent.
static <L,I> Collection<Pair<Word<I>,Word<I>>>	findCharacterizingSet(OneSEVPA<L,I> sevpa, VPAlphabet<I> alphabet)	Computes a characterizing set for the given SEVPA.
static <L,I> List<L>	findReachableLocations(OneSEVPA<L,I> sevpa, VPAlphabet<I> alphabet)	Returns a list of locations that are reachable from the initial location of the given SEVPA via symbols of the given alphabet.
static <L,I> @Nullable Word<I>	findRejectedWord(OneSEVPA<L,I> sevpa, VPAlphabet<I> alphabet)	Returns a well-matched word (over the given alphabet) that is rejected by the given SEVPA, if existent.
static <I> @Nullable Word<I>	findSeparatingWord(OneSEVPA<?,I> sevpa1, OneSEVPA<?,I> sevpa2, VPAlphabet<I> alphabet)	Finds a separating word for two SEVPAs, if existent.
static <L,I> @Nullable Pair<Word<I>,Word<I>>	findSeparatingWord(OneSEVPA<L,I> sevpa, L init1, L init2, VPAlphabet<I> alphabet)	Finds a separating word for two locations of a SEVPAs, if existent.
static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I>	impl(OneSEVPA<L1,I> sevpa1, OneSEVPA<L2,I> sevpa2, VPAlphabet<I> alphabet)	Returns a view on the implication ("=>") of two OneSEVPAs.
static <I> DefaultOneSEVPA<I>	minimize(OneSEVPA<?,I> sevpa, VPAlphabet<I> alphabet)	Minimizes the given OneSEVPA over the given alphabet.
static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I>	or(OneSEVPA<L1,I> sevpa1, OneSEVPA<L2,I> sevpa2, VPAlphabet<I> alphabet)	Returns a view on the disjunction ("or") of two OneSEVPAs.
static <I> boolean	testEquivalence(OneSEVPA<?,I> sevpa1, OneSEVPA<?,I> sevpa2, VPAlphabet<I> alphabet)	Tests whether two SEVPAs are equivalent, i.e. whether there exists a separating word for the two given SEVPAs.
static <AI,CI> net.automatalib.util.automaton.vpa.SPAConverter.ConversionResult<AI,CI>	toSPA(OneSEVPA<?,AI> sevpa, VPAlphabet<AI> alphabet, CI mainProcedure, SymbolMapper<AI,CI> symbolMapper, boolean minimize)	Converts a given SEVPA into an SPA by concretizing the (abstract) behavior of the SEVPA into the (concrete) behavior of an SPA which can be described by the copy-rule semantics of (instrumented) context-free grammars.
static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I>	xor(OneSEVPA<L1,I> sevpa1, OneSEVPA<L2,I> sevpa2, VPAlphabet<I> alphabet)	Returns a view on the exclusive-or ("xor") of two OneSEVPAs.

Methods inherited from class java.lang.Object

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

Method Detail

and

public static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I> and(OneSEVPA<L1,I> sevpa1,
                                                                            OneSEVPA<L2,I> sevpa2,
                                                                            VPAlphabet<I> alphabet)

Returns a view on the conjunction ("and") of two OneSEVPAs.

Parameters:

sevpa1 - the first SEVPA

sevpa2 - the second SEVPA

alphabet - the input alphabet

Returns:

a view representing the conjunction of the specified OneSEVPAs

combine

public static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I> combine(OneSEVPA<L1,I> sevpa1,
                                                                                OneSEVPA<L2,I> sevpa2,
                                                                                VPAlphabet<I> alphabet,
                                                                                AcceptanceCombiner combiner)

Most general way of combining two OneSEVPAs. The AcceptanceCombiner specified via the combiner parameter specifies how acceptance values of the OneSEVPAs will be combined to an acceptance value in the resulting ProductOneSEVPA.

Parameters:

sevpa1 - the first SEVPA

sevpa2 - the second SEVPA

alphabet - the input alphabet

combiner - combination method for acceptance values

Returns:

a view representing the given combination of the specified OneSEVPAs

or

public static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I> or(OneSEVPA<L1,I> sevpa1,
                                                                           OneSEVPA<L2,I> sevpa2,
                                                                           VPAlphabet<I> alphabet)

Returns a view on the disjunction ("or") of two OneSEVPAs.

Parameters:

sevpa1 - the first SEVPA

sevpa2 - the second SEVPA

alphabet - the input alphabet

Returns:

a view representing the disjunction of the specified OneSEVPAs

xor

public static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I> xor(OneSEVPA<L1,I> sevpa1,
                                                                            OneSEVPA<L2,I> sevpa2,
                                                                            VPAlphabet<I> alphabet)

Returns a view on the exclusive-or ("xor") of two OneSEVPAs.

Parameters:

sevpa1 - the first SEVPA

sevpa2 - the second SEVPA

alphabet - the input alphabet

Returns:

a view representing the exclusive-or of the specified OneSEVPAs

equiv

public static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I> equiv(OneSEVPA<L1,I> sevpa1,
                                                                              OneSEVPA<L2,I> sevpa2,
                                                                              VPAlphabet<I> alphabet)

Returns a view on the equivalence ("<=>") of two OneSEVPAs.

Parameters:

sevpa1 - the first SEVPA

sevpa2 - the second SEVPA

alphabet - the input alphabet

Returns:

a view representing the equivalence of the specified OneSEVPAs

impl

public static <L1,L2,I> OneSEVPA<Pair<L1,L2>,I> impl(OneSEVPA<L1,I> sevpa1,
                                                                             OneSEVPA<L2,I> sevpa2,
                                                                             VPAlphabet<I> alphabet)

Returns a view on the implication ("=>") of two OneSEVPAs.

Parameters:

sevpa1 - the first SEVPA

sevpa2 - the second SEVPA

alphabet - the input alphabet

Returns:

a view representing the implication of the specified OneSEVPAs

minimize

public static <I> DefaultOneSEVPA<I> minimize(OneSEVPA<?,I> sevpa,
                                              VPAlphabet<I> alphabet)

Minimizes the given OneSEVPA over the given alphabet. This method does not modify the given OneSEVPA, but returns the minimized version as a new instance.

Note: the method currently does not support partial OneSEVPAs.

Parameters:

sevpa - the SEVPA to be minimized

alphabet - the input alphabet to consider for minimization (this will also be the input alphabet of the resulting automaton)

Returns:

a minimized version of the specified OneSEVPA

computeAccessSequence

public static <L,I> @Nullable Word<I> computeAccessSequence(OneSEVPA<L,I> sevpa,
                                                                  VPAlphabet<I> alphabet,
                                                                  Predicate<? super L> predicate)

Computes an access sequence over the given alphabet (if existent) such that it reaches a location of the given SEVPA that satisfies the given predicate.

Type Parameters:

L - the location type

I - input symbol type

Parameters:

sevpa - the SEVPA

alphabet - the alphabet symbols to consider

predicate - the predicate to satisfy

Returns:

an access sequence as such that predicate.test(sevpa.getState(as).getLocation()) == true, or null if such a sequence does not exist.

computeAccessSequences

public static <L,I> ArrayStorage<Word<I>> computeAccessSequences(OneSEVPA<L,I> sevpa,
                                                                       VPAlphabet<I> alphabet)

Computes all access sequences over the given alphabet (if existent) to the locations of the given SEVPA.

Type Parameters:

L - the location type

I - input symbol type

Parameters:

sevpa - the SEVPA

alphabet - the alphabet symbols to consider

Returns:

a list of access sequences, indexed by their respective id.

testEquivalence

public static <I> boolean testEquivalence(OneSEVPA<?,I> sevpa1,
                                          OneSEVPA<?,I> sevpa2,
                                          VPAlphabet<I> alphabet)

Tests whether two SEVPAs are equivalent, i.e. whether there exists a separating word for the two given SEVPAs.

Type Parameters:

I - input symbol type

Parameters:

sevpa1 - the one SEVPA to consider

sevpa2 - the other SEVPA to consider

alphabet - the input symbols to consider

Returns:

true if the SEVPA are equivalent, false otherwise.

See Also:

findSeparatingWord(OneSEVPA, OneSEVPA, VPAlphabet)

findAcceptedWord

public static <L,I> @Nullable Word<I> findAcceptedWord(OneSEVPA<L,I> sevpa,
                                                             VPAlphabet<I> alphabet)

Returns a well-matched word (over the given alphabet) that is accepted by the given SEVPA, if existent.

Type Parameters:

L - location type

I - input symbol type

Parameters:

sevpa - the SEVPA to consider

alphabet - the input symbols to consider

Returns:

a well-matched word w such that sevpa.accepts(w) == true, null if such a word does not exist.

findRejectedWord

public static <L,I> @Nullable Word<I> findRejectedWord(OneSEVPA<L,I> sevpa,
                                                             VPAlphabet<I> alphabet)

Returns a well-matched word (over the given alphabet) that is rejected by the given SEVPA, if existent.

Type Parameters:

L - location type

I - input symbol type

Parameters:

sevpa - the SEVPA to consider

alphabet - the input symbols to consider

Returns:

a well-matched word w such that sevpa.accepts(w) == false, null if such a word does not exist.

findReachableLocations

public static <L,I> List<L> findReachableLocations(OneSEVPA<L,I> sevpa,
                                                         VPAlphabet<I> alphabet)

Returns a list of locations that are reachable from the initial location of the given SEVPA via symbols of the given alphabet.

Type Parameters:

L - location type

I - input symbol type

Parameters:

sevpa - the SEVPA to consider

alphabet - the input symbols to consider

Returns:

a list of locations that are reachable via symbols of the given alphabet

findSeparatingWord

public static <I> @Nullable Word<I> findSeparatingWord(OneSEVPA<?,I> sevpa1,
                                                       OneSEVPA<?,I> sevpa2,
                                                       VPAlphabet<I> alphabet)

Finds a separating word for two SEVPAs, if existent. A separating word is a word that exposes a different acceptance behavior between the two SEVPAs.

Type Parameters:

I - input symbol type

Parameters:

sevpa1 - the one SEVPA to consider

sevpa2 - the other SEVPA to consider

alphabet - the input symbols to consider

Returns:

a separating word, or null if no such word could be found.

findSeparatingWord

public static <L,I> @Nullable Pair<Word<I>,Word<I>> findSeparatingWord(OneSEVPA<L,I> sevpa,
                                                                                   L init1,
                                                                                   L init2,
                                                                                   VPAlphabet<I> alphabet)

Finds a separating word for two locations of a SEVPAs, if existent. A separating word is a word that exposes a different acceptance behavior between the two SEVPAs. Note that the separating word for two explicit locations consists of a prefix and a suffix since locations are typically distinguished in regard to the syntactical congruence.

Type Parameters:

L - location type

I - input symbol type

Parameters:

sevpa - the SEVPA to consider

init1 - the one location to consider

init2 - the other location to consider

alphabet - the input symbols to consider

Returns:

a separating word for the two locations, or null if no such word could be found.

findCharacterizingSet

public static <L,I> Collection<Pair<Word<I>,Word<I>>> findCharacterizingSet(OneSEVPA<L,I> sevpa,
                                                                                        VPAlphabet<I> alphabet)

Computes a characterizing set for the given SEVPA. Note that the characterizing words consist of a prefix and a suffix since locations are typically distinguished in regard to the syntactical

Type Parameters:

L - location type

I - input symbol type

Parameters:

sevpa - the SEVPA for which to determine the characterizing set

alphabet - the input symbols to consider

Returns:

a list containing the characterizing words

toSPA

public static <AI,CI> net.automatalib.util.automaton.vpa.SPAConverter.ConversionResult<AI,CI> toSPA(OneSEVPA<?,AI> sevpa,
                                                                                                                VPAlphabet<AI> alphabet,
                                                                                                                CI mainProcedure,
                                                                                                                SymbolMapper<AI,CI> symbolMapper,
                                                                                                                boolean minimize)

Converts a given SEVPA into an SPA by concretizing the (abstract) behavior of the SEVPA into the (concrete) behavior of an SPA which can be described by the copy-rule semantics of (instrumented) context-free grammars.

Type Parameters:

AI - abstract input symbol type

CI - concrete input symbol type

Parameters:

sevpa - the SEVPA to consider

alphabet - the input symbols to consider

mainProcedure - the concrete input symbol that should be used to represent the main procedure of the constructed SPA

symbolMapper - a symbol mapper to translate the abstract SEVPA symbols to concrete SPA symbols

minimize - a flat indicating, whether the constructed SPA should be minimized

Returns:

a SPAConverter.ConversionResult containing the relevant data of this conversion