public final class AutomatonUtil
extends java.lang.Object
Modifier and Type | Method | Description |
---|---|---|
static <S,A extends OmegaAcceptance> |
asMutable(Automaton<S,A> automaton) |
|
static <A extends OmegaAcceptance> |
cast(java.lang.Object automaton,
java.lang.Class<A> acceptanceClass) |
|
static <S,A extends OmegaAcceptance> |
cast(java.lang.Object automaton,
java.lang.Class<S> stateClass,
java.lang.Class<A> acceptanceClass) |
|
static <S,A extends OmegaAcceptance> |
cast(Automaton<S,?> automaton,
java.lang.Class<A> acceptanceClass) |
|
static <S,A extends OmegaAcceptance> |
castMutable(java.lang.Object automaton,
java.lang.Class<S> stateClass,
java.lang.Class<A> acceptanceClass) |
|
static java.util.Optional<java.lang.Object> |
complete(MutableAutomaton<java.lang.Object,?> automaton,
java.util.BitSet rejectingAcceptance) |
|
static <S> java.util.Optional<S> |
complete(MutableAutomaton<S,?> automaton,
S sinkState,
java.util.BitSet rejectingAcceptance) |
Completes the automaton by adding a sink state obtained from the
sinkSupplier if
necessary. |
static java.util.function.Supplier<java.lang.Object> |
defaultSinkSupplier() |
|
static <S> void |
explore(MutableAutomaton<S,?> automaton,
java.lang.Iterable<S> states,
java.util.function.BiFunction<S,java.util.BitSet,? extends java.lang.Iterable<Edge<S>>> explorationFunction,
java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle) |
Adds the given states and all states transitively reachable through
explorationFunction
to the automaton. |
static <S> void |
explore(MutableAutomaton<S,?> automaton,
java.lang.Iterable<S> states,
java.util.function.BiFunction<S,java.util.BitSet,? extends java.lang.Iterable<Edge<S>>> explorationFunction,
java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle,
java.util.concurrent.atomic.AtomicInteger sizeCounter) |
Adds the given states and all states transitively reachable through
explorationFunction
to the automaton. |
static <S> void |
explore(MutableAutomaton<S,?> automaton,
java.lang.Iterable<S> states,
java.util.function.BiFunction<S,java.util.BitSet,java.lang.Iterable<Edge<S>>> explorationFunction) |
Adds the given states and all states transitively reachable through
explorationFunction
to the automaton. |
static <S> void |
exploreDeterministic(MutableAutomaton<S,?> automaton,
java.lang.Iterable<S> states,
java.util.function.BiFunction<S,java.util.BitSet,Edge<S>> explorationFunction,
java.util.concurrent.atomic.AtomicInteger sizeCounter) |
|
static <S> void |
exploreDeterministic(MutableAutomaton<S,?> automaton,
java.lang.Iterable<S> states,
java.util.function.BiFunction<S,java.util.BitSet,Edge<S>> explorationFunction,
java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle) |
|
static <S> void |
exploreDeterministic(MutableAutomaton<S,?> automaton,
java.lang.Iterable<S> states,
java.util.function.BiFunction<S,java.util.BitSet,Edge<S>> explorationFunction,
java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle,
java.util.concurrent.atomic.AtomicInteger sizeCounter) |
|
static <S> java.util.Set<S> |
exploreWithLabelledEdge(MutableAutomaton<S,?> automaton,
java.lang.Iterable<S> states,
java.util.function.Function<S,java.lang.Iterable<LabelledEdge<S>>> successorFunction) |
|
static <S> void |
forEachNonTransientEdge(Automaton<S,?> automaton,
java.util.function.BiConsumer<S,Edge<S>> action) |
|
static <S,A extends OmegaAcceptance> |
getIncompleteStates(Automaton<S,A> automaton) |
Determines all states which are incomplete, i.e.
|
static <S,A extends OmegaAcceptance> |
getReachableStates(Automaton<S,A> automaton) |
Returns all states reachable from the initial states.
|
static <S,A extends OmegaAcceptance> |
getReachableStates(Automaton<S,A> automaton,
java.util.Collection<? extends S> start) |
Returns all states reachable from the given set of states.
|
static java.lang.String |
toHoa(HoaPrintable printable) |
public static <A extends OmegaAcceptance> Automaton<java.lang.Object,A> cast(java.lang.Object automaton, java.lang.Class<A> acceptanceClass)
public static <S,A extends OmegaAcceptance> Automaton<S,A> cast(java.lang.Object automaton, java.lang.Class<S> stateClass, java.lang.Class<A> acceptanceClass)
public static <S,A extends OmegaAcceptance> Automaton<S,A> cast(Automaton<S,?> automaton, java.lang.Class<A> acceptanceClass)
public static <S,A extends OmegaAcceptance> MutableAutomaton<S,A> castMutable(java.lang.Object automaton, java.lang.Class<S> stateClass, java.lang.Class<A> acceptanceClass)
public static <S,A extends OmegaAcceptance> MutableAutomaton<S,A> asMutable(Automaton<S,A> automaton)
public static java.util.function.Supplier<java.lang.Object> defaultSinkSupplier()
public static java.util.Optional<java.lang.Object> complete(MutableAutomaton<java.lang.Object,?> automaton, java.util.BitSet rejectingAcceptance)
public static <S> java.util.Optional<S> complete(MutableAutomaton<S,?> automaton, S sinkState, java.util.BitSet rejectingAcceptance)
sinkSupplier
if
necessary. The sink state will be obtained, i.e. Supplier.get()
called exactly once, if
and only if a sink is added. This state will be returned wrapped in an Optional
, if
instead no state was added Optional.empty()
is returned. After adding the sink state,
the rejectingAcceptanceSupplier
is called to construct a rejecting self-loop. Note: The completion process considers unreachable states.
sinkState
- A sink state.rejectingAcceptance
- A rejecting acceptance.empty
if none was added.public static <S> void explore(MutableAutomaton<S,?> automaton, java.lang.Iterable<S> states, java.util.function.BiFunction<S,java.util.BitSet,java.lang.Iterable<Edge<S>>> explorationFunction)
explorationFunction
to the automaton. Note that if some reachable state is already present, the specified
transitions still get added, potentially introducing non-determinism. If two states of the
given states
can reach a particular state, the resulting transitions only get added
once.
states
- The starting states of the exploration.explorationFunction
- The function describing the transition relation.explore(MutableAutomaton, Iterable, BiFunction, Function, AtomicInteger)
public static <S> void explore(MutableAutomaton<S,?> automaton, java.lang.Iterable<S> states, java.util.function.BiFunction<S,java.util.BitSet,? extends java.lang.Iterable<Edge<S>>> explorationFunction, java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle)
explorationFunction
to the automaton. The sensitiveAlphabetOracle
is used to obtain the sensitive alphabet
of a particular state, which reduces the number of calls to the exploration function. The
oracle is allowed to return null
values, indicating that no alphabet restriction can be
obtained. Note that if some reachable state is already present, the specified transitions
still get added, potentially introducing non-determinism. If two states of the given
states
can reach a particular state, the resulting transitions only get added once.
states
- The starting states of the exploration.explorationFunction
- The function describing the transition relation.public static <S> void explore(MutableAutomaton<S,?> automaton, java.lang.Iterable<S> states, java.util.function.BiFunction<S,java.util.BitSet,? extends java.lang.Iterable<Edge<S>>> explorationFunction, java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle, java.util.concurrent.atomic.AtomicInteger sizeCounter)
explorationFunction
to the automaton. The sensitiveAlphabetOracle
is used to obtain the sensitive alphabet
of a particular state, which reduces the number of calls to the exploration function. The
oracle is allowed to return null
values, indicating that no alphabet restriction can be
obtained. Note that if some reachable state is already present, the specified transitions
still get added, potentially introducing non-determinism. If two states of the given
states
can reach a particular state, the resulting transitions only get added once.
states
- The starting states of the exploration.explorationFunction
- The function describing the transition relation.public static <S> void exploreDeterministic(MutableAutomaton<S,?> automaton, java.lang.Iterable<S> states, java.util.function.BiFunction<S,java.util.BitSet,Edge<S>> explorationFunction, java.util.concurrent.atomic.AtomicInteger sizeCounter)
public static <S> void exploreDeterministic(MutableAutomaton<S,?> automaton, java.lang.Iterable<S> states, java.util.function.BiFunction<S,java.util.BitSet,Edge<S>> explorationFunction, java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle)
public static <S> void exploreDeterministic(MutableAutomaton<S,?> automaton, java.lang.Iterable<S> states, java.util.function.BiFunction<S,java.util.BitSet,Edge<S>> explorationFunction, java.util.function.Function<S,java.util.BitSet> sensitiveAlphabetOracle, java.util.concurrent.atomic.AtomicInteger sizeCounter)
public static <S> java.util.Set<S> exploreWithLabelledEdge(MutableAutomaton<S,?> automaton, java.lang.Iterable<S> states, java.util.function.Function<S,java.lang.Iterable<LabelledEdge<S>>> successorFunction)
public static <S> void forEachNonTransientEdge(Automaton<S,?> automaton, java.util.function.BiConsumer<S,Edge<S>> action)
public static <S,A extends OmegaAcceptance> java.util.Map<S,ValuationSet> getIncompleteStates(Automaton<S,A> automaton)
automaton
- The automaton.public static <S,A extends OmegaAcceptance> java.util.Set<S> getReachableStates(Automaton<S,A> automaton)
automaton
- The automaton.getReachableStates(Automaton, Collection)
public static <S,A extends OmegaAcceptance> java.util.Set<S> getReachableStates(Automaton<S,A> automaton, java.util.Collection<? extends S> start)
automaton
- The automatonstart
- Starting states for the reachable states search.public static java.lang.String toHoa(HoaPrintable printable)