Class SPAs
- java.lang.Object
-
- net.automatalib.util.automaton.procedural.SPAs
-
-
Method Summary
All Methods Static Methods Concrete Methods 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)
static <I> ATRSequences<I>
computeATRSequences(SPA<?,I> spa)
Computes a set of access sequences, terminating sequences, and return sequences for a givenSPA
.static <I> ATRSequences<I>
computeATRSequences(SPA<?,I> spa, ProceduralInputAlphabet<I> alphabet)
Computes a set of access sequences, terminating sequences, and return sequences for a givenSPA
limited to the symbols of the givenProceduralInputAlphabet
.static <I> Map<I,Word<I>>
computeTerminatingSequences(SPA<?,I> spa, ProceduralInputAlphabet<I> alphabet)
static <I> @Nullable Word<I>
findSeparatingWord(SPA<?,I> spa1, SPA<?,I> spa2, ProceduralInputAlphabet<I> alphabet)
Computes a separating word for the two givenSPA
s, if existent.static <I> boolean
isMinimal(ProceduralInputAlphabet<I> alphabet, ATRSequences<I> atrSequences)
Checks if a pre-computed set ofATRSequences
of anSPA
is minimal.static <I> boolean
isMinimal(SPA<?,I> spa)
Convenience method forisMinimal(SPA, ProceduralInputAlphabet)
that usesInputAlphabetHolder.getInputAlphabet()
asalphabet
.static <I> boolean
isMinimal(SPA<?,I> spa, ProceduralInputAlphabet<I> alphabet)
Checks if a givenSPA
is redundancy-free, i.e. if for allprocedures
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 givenSPA
s are equivalent, i.e. whether there exists aseparating word
for them.static <I> ContextFreeModalProcessSystem<I,Void>
toCFMPS(SPA<?,I> spa)
Returns aContextFreeModalProcessSystem
-based view on the language of a givenSPA
such that there exists aw
-labeled path to the final node of the returned CFMPS' main procedure if and only ifw
is accepted by the givenSPA
.static <I> SEVPA<?,I>
toNSEVPA(SPA<?,I> spa)
static <I> OneSEVPA<?,I>
toOneSEVPA(SPA<?,I> spa)
-
-
-
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 givenSPA
. This is a convenience method forcomputeATRSequences(SPA, ProceduralInputAlphabet)
that automatically uses theinput alphabet
of the givenspa
.- Type Parameters:
I
- input symbol type- Parameters:
spa
- theSPA
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 givenSPA
limited to the symbols of the givenProceduralInputAlphabet
.- Type Parameters:
I
- input symbol type- Parameters:
spa
- theSPA
for which the sequences should be computedalphabet
- theProceduralInputAlphabet
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 givenSPA
a set of terminating sequences using the givenalphabet
. 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
- theSPA
to analyzealphabet
- theProceduralInputAlphabet
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 givenSPA
a set of access sequences and return sequences using the givenalphabet
. An access sequence (for procedure p) transfers anSPA
from its initial state to a state that is able to successfully execute a run of p, whereas the corresponding return sequence transfers theSPA
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
- theSPA
to analyzealphabet
- theProceduralInputAlphabet
whose symbols should be used for determining the access and return sequencesterminatingSequences
- aMap
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 forisMinimal(SPA, ProceduralInputAlphabet)
that usesInputAlphabetHolder.getInputAlphabet()
asalphabet
.- Type Parameters:
I
- input symbol type- Parameters:
spa
- theSPA
to check- Returns:
true
ifspa
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 givenSPA
is redundancy-free, i.e. if for allprocedures
there exists an access sequence, terminating sequence, and return sequence.
-
isMinimal
public static <I> boolean isMinimal(ProceduralInputAlphabet<I> alphabet, ATRSequences<I> atrSequences)
Checks if a pre-computed set ofATRSequences
of anSPA
is minimal.- Type Parameters:
I
- input symbol type- Parameters:
alphabet
- thealphabet
which should be used for computing the respective sequencesatrSequences
- the pre-computedATRSequences
- Returns:
true
ifspa
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 givenSPA
s are equivalent, i.e. whether there exists aseparating word
for them.- Type Parameters:
I
- input symbol type- Parameters:
spa1
- the firstSPA
spa2
- the secondSPA
alphabet
- theProceduralInputAlphabet
whose symbols should be considered for equivalence testing- Returns:
true
if the twoSPA
s 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 givenSPA
s, if existent. A separating word is aWord
such that oneSPA
behaves
different from the other.- Type Parameters:
I
- input symbol type- Parameters:
spa1
- the firstSPA
spa2
- the secondSPA
alphabet
- theProceduralInputAlphabet
whose symbols should be considered for computing the separating word- Returns:
- a separating word, if existent,
null
otherwise.
-
toCFMPS
public static <I> ContextFreeModalProcessSystem<I,Void> toCFMPS(SPA<?,I> spa)
Returns aContextFreeModalProcessSystem
-based view on the language of a givenSPA
such that there exists aw
-labeled path to the final node of the returned CFMPS' main procedure if and only ifw
is accepted by the givenSPA
. This allows one to model-check language properties ofSPA
s with tools such as M3C.- Type Parameters:
I
- input symbol type- Parameters:
spa
- theSPA
to convert- Returns:
- the
ContextFreeModalProcessSystem
-based view on the givenspa
.
-
-