Class SBAs
- java.lang.Object
-
- net.automatalib.util.automaton.procedural.SBAs
-
-
Method Summary
All Methods Static Methods Concrete Methods Modifier and Type Method Description static <I> Map<I,Word<I>>
computeAccessSequences(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet, Map<I,Word<I>> terminatingSequences)
static <I> ATSequences<I>
computeATSequences(SBA<?,I> sba)
Computes a set of access sequences and terminating sequences for a givenSBA
.static <I> ATSequences<I>
computeATSequences(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
Computes a set of access sequences and terminating sequences for a givenSBA
limited to the symbols of the givenProceduralInputAlphabet
.static <I> Map<I,Word<I>>
computeTerminatingSequences(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
static <I> @Nullable Word<I>
findSeparatingWord(SBA<?,I> sba1, SBA<?,I> sba2, ProceduralInputAlphabet<I> alphabet)
Computes a separating word for the two givenSBA
s, if existent.static <I> boolean
isValid(SBA<?,I> sba)
Checks whether the givenSBA
is valid, This is a convenience method forisValid(SBA, ProceduralInputAlphabet)
that uses theinput alphabet
of the givenSBA
.static <I> boolean
isValid(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
Checks whether the givenSBA
is valid with respect to the givenProceduralInputAlphabet
, i.e., whether itsprocedures
are prefix-closed, return-closed, and call-closed.static <I> SPA<?,I>
reduce(SBA<?,I> sba)
Reduces a givenSBA
to its well-matched language.static <I> SPA<?,I>
reduce(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
Reduces a givenSBA
to its well-matched language restricted to the symbols of the givenProceduralInputAlphabet
.static <I> boolean
testEquivalence(SBA<?,I> sba1, SBA<?,I> sba2, ProceduralInputAlphabet<I> alphabet)
Checks if the two givenSBA
s are equivalent, i.e. whether there exists aseparating word
for them.static <I> ContextFreeModalProcessSystem<I,Void>
toCFMPS(SBA<?,I> sba)
Returns aContextFreeModalProcessSystem
-based view on the language of a givenSBA
such that there exists aw
-labeled path in the returned CFMPS if and only ifw
is accepted by the givenSBA
.
-
-
-
Method Detail
-
computeATSequences
public static <I> ATSequences<I> computeATSequences(SBA<?,I> sba)
Computes a set of access sequences and terminating sequences for a givenSBA
. This is a convenience method forcomputeATSequences(SBA, ProceduralInputAlphabet)
that automatically uses theinput alphabet
of the givensba
.- Type Parameters:
I
- input symbol type- Parameters:
sba
- theSBA
for which the sequences should be computed- Returns:
- an
ATSequences
object which contains the respective sequences. - See Also:
computeATSequences(SBA, ProceduralInputAlphabet)
-
computeATSequences
public static <I> ATSequences<I> computeATSequences(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
Computes a set of access sequences and terminating sequences for a givenSBA
limited to the symbols of the givenProceduralInputAlphabet
.- Type Parameters:
I
- input symbol type- Parameters:
sba
- theSBA
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(SBA, ProceduralInputAlphabet, Map)
,computeTerminatingSequences(SBA, ProceduralInputAlphabet)
-
computeTerminatingSequences
public static <I> Map<I,Word<I>> computeTerminatingSequences(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
Computes for a givenSBA
a 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 type- Parameters:
sba
- theSBA
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.
-
computeAccessSequences
public static <I> Map<I,Word<I>> computeAccessSequences(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet, Map<I,Word<I>> terminatingSequences)
Computes for a givenSBA
a set of access sequences using the givenalphabet
. An access sequence (for procedure p) transfers anSBA
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 type- Parameters:
sba
- theSBA
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.
-
isValid
public static <I> boolean isValid(SBA<?,I> sba)
Checks whether the givenSBA
is valid, This is a convenience method forisValid(SBA, ProceduralInputAlphabet)
that uses theinput alphabet
of the givenSBA
.- Type Parameters:
I
- input symbol type- Parameters:
sba
- theSBA
to analyze- Returns:
true
ifsba
is valid,false
otherwise.- See Also:
isValid(SBA, ProceduralInputAlphabet)
-
isValid
public static <I> boolean isValid(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
Checks whether the givenSBA
is valid with respect to the givenProceduralInputAlphabet
, i.e., whether itsprocedures
are prefix-closed, return-closed, and call-closed.A procedure is considered prefix-closed iff any continuation of a rejected word is rejected as well.
A procedure is considered return-closed iff any continuation beyond the
return symbol
is rejected.A procedure is considered call-closed iff any continuation beyond a non-terminating
call symbol
is rejected.- Type Parameters:
I
- input symbol type- Parameters:
sba
- theSBA
to analyzealphabet
- theProceduralInputAlphabet
whose symbols should be used for checking validity- Returns:
true
ifsba
is valid,false
otherwise.
-
testEquivalence
public static <I> boolean testEquivalence(SBA<?,I> sba1, SBA<?,I> sba2, ProceduralInputAlphabet<I> alphabet)
Checks if the two givenSBA
s are equivalent, i.e. whether there exists aseparating word
for them.- Type Parameters:
I
- input symbol type- Parameters:
sba1
- the firstSPMM
sba2
- the secondSPMM
alphabet
- theProceduralInputAlphabet
whose symbols should be used for checking equivalence- Returns:
true
if the twoSBA
s are equivalent,false
otherwise.- See Also:
findSeparatingWord(SBA, SBA, ProceduralInputAlphabet)
-
findSeparatingWord
public static <I> @Nullable Word<I> findSeparatingWord(SBA<?,I> sba1, SBA<?,I> sba2, ProceduralInputAlphabet<I> alphabet)
Computes a separating word for the two givenSBA
s, if existent. A separating word is aWord
such that oneSBA
behaves
different from the other.- Type Parameters:
I
- input symbol type- Parameters:
sba1
- the firstSBA
sba2
- the secondSBA
alphabet
- theProceduralInputAlphabet
whose symbols should be considered for computing the separating word- Returns:
- a separating word, if existent,
null
otherwise.
-
reduce
public static <I> SPA<?,I> reduce(SBA<?,I> sba)
Reduces a givenSBA
to its well-matched language. This is a convenience method forreduce(SBA, ProceduralInputAlphabet)
that uses theinput alphabet
of the givenSBA
.- Type Parameters:
I
- input symbol type- Parameters:
sba
- theSBA
to reduce- Returns:
- the reduced
SBA
in form of anSPA
- See Also:
reduce(SBA, ProceduralInputAlphabet)
-
reduce
public static <I> SPA<?,I> reduce(SBA<?,I> sba, ProceduralInputAlphabet<I> alphabet)
Reduces a givenSBA
to its well-matched language restricted to the symbols of the givenProceduralInputAlphabet
. The reducedSBA
only accepts aWord
iff it is (minimally) well-matched and accepted by the originalSBA
as well.- Type Parameters:
I
- input symbol type- Parameters:
sba
- theSBA
to reducealphabet
- theProceduralInputAlphabet
whose symbols should be considered for reduction- Returns:
- the reduced
SBA
in form of anSPA
-
toCFMPS
public static <I> ContextFreeModalProcessSystem<I,Void> toCFMPS(SBA<?,I> sba)
Returns aContextFreeModalProcessSystem
-based view on the language of a givenSBA
such that there exists aw
-labeled path in the returned CFMPS if and only ifw
is accepted by the givenSBA
. This allows one to model-check language properties ofSBA
s with tools such as M3C.- Type Parameters:
I
- input symbol type- Parameters:
sba
- theSBA
to convert- Returns:
- the
ContextFreeModalProcessSystem
-based view on the givensba
.
-
-