Class SPMMs
- java.lang.Object
-
- net.automatalib.util.automaton.procedural.SPMMs
-
-
Method Summary
All Methods Static Methods Concrete Methods Modifier and Type Method Description static <I,O>
Map<I,Word<I>>computeAccessSequences(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet, Map<I,Word<I>> terminatingSequences)
static <I,O>
ATSequences<I>computeATSequences(SPMM<?,I,?,O> spmm)
Computes a set of access sequences and terminating sequences for a givenSPMM
.static <I,O>
ATSequences<I>computeATSequences(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet)
Computes a set of access sequences and return sequences for a givenSPMM
limited to the symbols of the givenProceduralInputAlphabet
.static <I,O>
Map<I,Word<I>>computeTerminatingSequences(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet)
static <I,O>
@Nullable Word<I>findSeparatingWord(SPMM<?,I,?,O> spmm1, SPMM<?,I,?,O> spmm2, ProceduralInputAlphabet<I> alphabet)
Computes a separating word for the two givenSPMM
s, if existent.static <I,O>
booleanisValid(SPMM<?,I,?,O> spmm)
Checks whether the givenSPMM
is valid, This is a convenience method forisValid(SPMM, ProceduralInputAlphabet)
that uses theinput alphabet
of the givenSPMM
.static <I,O>
booleanisValid(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet)
Checks whether the givenSPMM
is valid with respect to the givenProceduralInputAlphabet
, i.e., whether itsprocedures
are error-closed, return-closed, and call-closed.static <I,O>
booleantestEquivalence(SPMM<?,I,?,O> spmm1, SPMM<?,I,?,O> spmm2, ProceduralInputAlphabet<I> alphabet)
Checks if the two givenSPMM
s are equivalent, i.e. whether there exists aseparating word
for them.
-
-
-
Method Detail
-
computeATSequences
public static <I,O> ATSequences<I> computeATSequences(SPMM<?,I,?,O> spmm)
Computes a set of access sequences and terminating sequences for a givenSPMM
. This is a convenience method forcomputeATSequences(SPMM, ProceduralInputAlphabet)
that automatically uses theinput alphabet
of the givenspmm
.- Type Parameters:
I
- input symbol type- Parameters:
spmm
- theSPMM
for which the sequences should be computed- Returns:
- an
ATSequences
object which contains the respective sequences. - See Also:
computeATSequences(SPMM, ProceduralInputAlphabet)
-
computeATSequences
public static <I,O> ATSequences<I> computeATSequences(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet)
Computes a set of access sequences and return sequences for a givenSPMM
limited to the symbols of the givenProceduralInputAlphabet
.- Type Parameters:
I
- input symbol typeO
- output symbol type- Parameters:
spmm
- theSPMM
for which the sequences should be computedalphabet
- theProceduralInputAlphabet
whose symbols should be used for computing the respective sequences- Returns:
- an
ATSequences
object which contains the respective sequences. - See Also:
computeAccessSequences(SPMM, ProceduralInputAlphabet, Map)
,computeTerminatingSequences(SPMM, ProceduralInputAlphabet)
-
computeTerminatingSequences
public static <I,O> Map<I,Word<I>> computeTerminatingSequences(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet)
Computes for a givenSPMM
the set of terminating sequences using the givenalphabet
. Terminating sequences transfer a procedure from its initial state to a returnable 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 typeO
- output symbol type- Parameters:
spmm
- theSPMM
to analyzealphabet
- theProceduralInputAlphabet
whose symbols should be used for computing 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.
-
computeAccessSequences
public static <I,O> Map<I,Word<I>> computeAccessSequences(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet, Map<I,Word<I>> terminatingSequences)
Computes for a givenSPMM
a set of access sequences using the SPMMalphabet
. An access sequence (for procedure p) transfers anSPMM
from its initial state to a state that is able to successfully execute a run of p. This method furthermore checks that potentially nested calls are well-defined, i.e. it only includes procedural invocations p for determining access sequences if p has a valid terminating sequence and therefore can be expanded correctly.- Type Parameters:
I
- input symbol typeO
- output symbol type- Parameters:
spmm
- theSPMM
to analyzealphabet
- theProceduralInputAlphabet
whose symbols should be used for computing the access sequencesterminatingSequences
- aMap
of call symbols to terminating sequences used to expand nested invocations in access sequences- Returns:
- A map from procedures (restricted to the call symbols of the given alphabet) to the access sequences. This map may be partial as some procedures may not have well-defined access sequences for the given alphabet.
-
isValid
public static <I,O> boolean isValid(SPMM<?,I,?,O> spmm)
Checks whether the givenSPMM
is valid, This is a convenience method forisValid(SPMM, ProceduralInputAlphabet)
that uses theinput alphabet
of the givenSPMM
.- Type Parameters:
I
- input symbol typeO
- output symbol type- Parameters:
spmm
- theSPMM
to analyze- Returns:
true
ifspmm
is valid,false
otherwise.- See Also:
isValid(SPMM, ProceduralInputAlphabet)
-
isValid
public static <I,O> boolean isValid(SPMM<?,I,?,O> spmm, ProceduralInputAlphabet<I> alphabet)
Checks whether the givenSPMM
is valid with respect to the givenProceduralInputAlphabet
, i.e., whether itsprocedures
are error-closed, return-closed, and call-closed.A procedure is considered error-closed iff any transition that emits an
error output
transitions the procedure into a sink state that continues to output theerror output
.A procedure is considered return-closed iff the
return symbol
transitions the procedure into a sink state that continues to output theerror output
.A procedure is considered call-closed iff any transition labeled with a non-terminating
call symbol
transitions the procedure into a sink state that continues to output theerror output
.- Type Parameters:
I
- input symbol typeO
- output symbol type- Parameters:
spmm
- theSPMM
to analyzealphabet
- theProceduralInputAlphabet
whose symbols should be used for checking validity- Returns:
true
ifspmm
is valid,false
otherwise.
-
testEquivalence
public static <I,O> boolean testEquivalence(SPMM<?,I,?,O> spmm1, SPMM<?,I,?,O> spmm2, ProceduralInputAlphabet<I> alphabet)
Checks if the two givenSPMM
s are equivalent, i.e. whether there exists aseparating word
for them.- Type Parameters:
I
- input symbol typeO
- output symbol type- Parameters:
spmm1
- the firstSPMM
spmm2
- the secondSPMM
alphabet
- theProceduralInputAlphabet
whose symbols should be used for checking equivalence- Returns:
true
if the twoSPMM
s are equivalent,false
otherwise.- See Also:
findSeparatingWord(SPMM, SPMM, ProceduralInputAlphabet)
-
findSeparatingWord
public static <I,O> @Nullable Word<I> findSeparatingWord(SPMM<?,I,?,O> spmm1, SPMM<?,I,?,O> spmm2, ProceduralInputAlphabet<I> alphabet)
Computes a separating word for the two givenSPMM
s, if existent. A separating word is aWord
such that oneSPMM
behaves
different from the other.- Type Parameters:
I
- input symbol typeO
- output symbol type- Parameters:
spmm1
- the firstSPMM
spmm2
- the secondSPMM
alphabet
- theProceduralInputAlphabet
whose symbols should be used for computing the separating word- Returns:
- a separating word, if existent,
null
otherwise.
-
-