Module net.automatalib.util

Package net.automatalib.util.automaton.procedural

Class SPAs

java.lang.Object

net.automatalib.util.automaton.procedural.SPAs

public final class SPAs
extends Object

Operations on SPAs.

Method Summary

Modifier and Type	Method	Description
static <I> Pair<Map<I,Word<I>>,Map<I,Word<I>>>	computeAccessAndReturnSequences(SPA<?,I> spa, ProceduralInputAlphabet<I> alphabet, Map<I,Word<I>> terminatingSequences)	Computes for a given SPA a set of access sequences and return sequences using the given alphabet.
static <I> ATRSequences<I>	computeATRSequences(SPA<?,I> spa)	Computes a set of access sequences, terminating sequences, and return sequences for a given SPA.
static <I> ATRSequences<I>	computeATRSequences(SPA<?,I> spa, ProceduralInputAlphabet<I> alphabet)	Computes a set of access sequences, terminating sequences, and return sequences for a given SPA limited to the symbols of the given ProceduralInputAlphabet.
static <I> Map<I,Word<I>>	computeTerminatingSequences(SPA<?,I> spa, ProceduralInputAlphabet<I> alphabet)	Computes for a given SPA a set of terminating sequences using the given alphabet.
static <I> @Nullable Word<I>	findSeparatingWord(SPA<?,I> spa1, SPA<?,I> spa2, ProceduralInputAlphabet<I> alphabet)	Computes a separating word for the two given SPAs, if existent.
static <I> boolean	isMinimal(ProceduralInputAlphabet<I> alphabet, ATRSequences<I> atrSequences)	Checks if a pre-computed set of ATRSequences of an SPA is minimal.
static <I> boolean	isMinimal(SPA<?,I> spa)	Convenience method for isMinimal(SPA, ProceduralInputAlphabet) that uses InputAlphabetHolder.getInputAlphabet() as alphabet.
static <I> boolean	isMinimal(SPA<?,I> spa, ProceduralInputAlphabet<I> alphabet)	Checks if a given SPA is redundancy-free, i.e. if for all procedures there exists an access sequence, terminating sequence, and return sequence.
static <I> boolean	testEquivalence(SPA<?,I> spa1, SPA<?,I> spa2, ProceduralInputAlphabet<I> alphabet)	Checks if the two given SPAs are equivalent, i.e. whether there exists a separating word for them.
static <I> ContextFreeModalProcessSystem<I,Void>	toCFMPS(SPA<?,I> spa)	Returns a ContextFreeModalProcessSystem-based view on the language of a given SPA such that there exists a w-labeled path to the final node of the returned CFMPS' main procedure if and only if w is accepted by the given SPA.
static <I> SEVPA<?,I>	toNSEVPA(SPA<?,I> spa)	Transforms the given SPA into a language-equivalent N-SEVPA.
static <I> OneSEVPA<?,I>	toOneSEVPA(SPA<?,I> spa)	Transforms the given SPA into a language-equivalent OneSEVPA.

Methods inherited from class java.lang.Object

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

Method Detail

computeATRSequences

public static <I> ATRSequences<I> computeATRSequences(SPA<?,I> spa)

Computes a set of access sequences, terminating sequences, and return sequences for a given SPA. This is a convenience method for computeATRSequences(SPA, ProceduralInputAlphabet) that automatically uses the input alphabet of the given spa.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA for which the sequences should be computed

Returns:

an ATRSequences object which contains the respective sequences.

See Also:

computeATRSequences(SPA, ProceduralInputAlphabet)

computeATRSequences

public static <I> ATRSequences<I> computeATRSequences(SPA<?,I> spa,
                                                      ProceduralInputAlphabet<I> alphabet)

Computes a set of access sequences, terminating sequences, and return sequences for a given SPA limited to the symbols of the given ProceduralInputAlphabet.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA for which the sequences should be computed

alphabet - the ProceduralInputAlphabet whose symbols should be used for computing the respective sequences

Returns:

an ATRSequences object which contains the respective sequences.

See Also:

computeAccessAndReturnSequences(SPA, ProceduralInputAlphabet, Map), computeTerminatingSequences(SPA, ProceduralInputAlphabet)

computeTerminatingSequences

public static <I> Map<I,Word<I>> computeTerminatingSequences(SPA<?,I> spa,
                                                                   ProceduralInputAlphabet<I> alphabet)

Computes for a given SPA a set of terminating sequences using the given alphabet. Terminating sequences transfer a procedure from its initial state to an accepting state. This method furthermore checks that the hierarchy of calls is well-defined, i.e. it only includes procedural invocations p for determining a terminating sequence if p has a valid terminating sequence itself.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA to analyze

alphabet - the ProceduralInputAlphabet whose symbols should be used for determining the terminating sequences

Returns:

A map from procedures (restricted to the call symbols of the given alphabet) to the terminating sequences. This map may be partial as some procedures may not have a well-defined terminating sequence for the given alphabet.

computeAccessAndReturnSequences

public static <I> Pair<Map<I,Word<I>>,Map<I,Word<I>>> computeAccessAndReturnSequences(SPA<?,I> spa,
                                                                                                        ProceduralInputAlphabet<I> alphabet,
                                                                                                        Map<I,Word<I>> terminatingSequences)

Computes for a given SPA a set of access sequences and return sequences using the given alphabet. An access sequence (for procedure p) transfers an SPA from its initial state to a state that is able to successfully execute a run of p, whereas the corresponding return sequence transfers the SPA to the global accepting state from an accepting state of p. This method furthermore checks that potentially nested calls are well-defined, i.e. it only includes procedural invocations p for determining access/return sequences if p has a valid terminating sequence and therefore can be expanded correctly.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA to analyze

alphabet - the ProceduralInputAlphabet whose symbols should be used for determining the access and return sequences

terminatingSequences - a Map of call symbols to terminating sequences used to expand nested invocations in access sequences

Returns:

A pair of maps from procedures (restricted to the call symbols of the given alphabet) to the access/return sequences. These maps may be partial as some procedures may not have well-defined access/terminating sequences for the given alphabet.

isMinimal

public static <I> boolean isMinimal(SPA<?,I> spa)

Convenience method for isMinimal(SPA, ProceduralInputAlphabet) that uses InputAlphabetHolder.getInputAlphabet() as alphabet.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA to check

Returns:

true if spa is redundancy-free, false otherwise.

See Also:

isMinimal(SPA, ProceduralInputAlphabet)

isMinimal

public static <I> boolean isMinimal(SPA<?,I> spa,
                                    ProceduralInputAlphabet<I> alphabet)

Checks if a given SPA is redundancy-free, i.e. if for all procedures there exists an access sequence, terminating sequence, and return sequence.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA to check

alphabet - the alphabet whose symbols should be used for computing the respective sequences

Returns:

true if spa is redundancy-free, false otherwise.

isMinimal

public static <I> boolean isMinimal(ProceduralInputAlphabet<I> alphabet,
                                    ATRSequences<I> atrSequences)

Checks if a pre-computed set of ATRSequences of an SPA is minimal.

Type Parameters:

I - input symbol type

Parameters:

alphabet - the alphabet which should be used for computing the respective sequences

atrSequences - the pre-computed ATRSequences

Returns:

true if spa is redundancy-free, false otherwise.

See Also:

isMinimal(SPA, ProceduralInputAlphabet)

testEquivalence

public static <I> boolean testEquivalence(SPA<?,I> spa1,
                                          SPA<?,I> spa2,
                                          ProceduralInputAlphabet<I> alphabet)

Checks if the two given SPAs are equivalent, i.e. whether there exists a separating word for them.

Type Parameters:

I - input symbol type

Parameters:

spa1 - the first SPA

spa2 - the second SPA

alphabet - the ProceduralInputAlphabet whose symbols should be considered for equivalence testing

Returns:

true if the two SPAs are equivalent, false otherwise.

See Also:

findSeparatingWord(SPA, SPA, ProceduralInputAlphabet)

findSeparatingWord

public static <I> @Nullable Word<I> findSeparatingWord(SPA<?,I> spa1,
                                                       SPA<?,I> spa2,
                                                       ProceduralInputAlphabet<I> alphabet)

Computes a separating word for the two given SPAs, if existent. A separating word is a Word such that one SPA behaves different from the other.

Type Parameters:

I - input symbol type

Parameters:

spa1 - the first SPA

spa2 - the second SPA

alphabet - the ProceduralInputAlphabet whose symbols should be considered for computing the separating word

Returns:

a separating word, if existent, null otherwise.

toOneSEVPA

public static <I> OneSEVPA<?,I> toOneSEVPA(SPA<?,I> spa)

Transforms the given SPA into a language-equivalent OneSEVPA.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA to transform

Returns:

the language-equivalent OneSEVPA

toNSEVPA

public static <I> SEVPA<?,I> toNSEVPA(SPA<?,I> spa)

Transforms the given SPA into a language-equivalent N-SEVPA.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA to transform

Returns:

the language-equivalent N-SEVPA

toCFMPS

public static <I> ContextFreeModalProcessSystem<I,Void> toCFMPS(SPA<?,I> spa)

Returns a ContextFreeModalProcessSystem-based view on the language of a given SPA such that there exists a w-labeled path to the final node of the returned CFMPS' main procedure if and only if w is accepted by the given SPA. This allows one to model-check language properties of SPAs with tools such as M3C.

Type Parameters:

I - input symbol type

Parameters:

spa - the SPA to convert

Returns:

the ContextFreeModalProcessSystem-based view on the given spa.