Automaton<S,A>
, HoaPrintable
Views.ForwardingMutableAutomaton
public interface MutableAutomaton<S,A extends OmegaAcceptance> extends Automaton<S,A>
Automaton.Property
HoaPrintable.HoaOption
Modifier and Type | Method | Description |
---|---|---|
default void |
addAll(Automaton<S,?> automaton) |
|
default void |
addEdge(S source,
java.util.BitSet valuation,
Edge<? extends S> edge) |
Adds a transition from the
source state under valuation . |
default void |
addEdge(S source,
Edge<? extends S> edge) |
Adds a transition from the
source state under any valuation. |
void |
addEdge(S source,
ValuationSet valuations,
Edge<? extends S> edge) |
Adds transitions from the
source state under valuations . |
default void |
addInitialState(S state) |
Adds a
state to the set of initial states. |
void |
addInitialStates(java.util.Collection<? extends S> states) |
Adds given
states to the set of initial states. |
default void |
addState(S state) |
Adds a
state without outgoing edges to the set of states. |
void |
addStates(java.util.Collection<? extends S> states) |
Adds
states without outgoing edges to the set of states. |
default void |
remapEdges(java.util.function.BiFunction<? super S,Edge<S>,Edge<S>> updater) |
Remaps each edge of the automaton according to
updater . |
void |
remapEdges(java.util.Set<? extends S> states,
java.util.function.BiFunction<? super S,Edge<S>,Edge<S>> updater) |
Remaps each outgoing edge of the specified
states according to updater . |
void |
removeEdge(S source,
java.util.BitSet valuation,
S destination) |
Removes all transition from
source under valuation to destination . |
void |
removeEdge(S source,
ValuationSet valuations,
S destination) |
Removes all transition from
source under valuations to destination . |
default void |
removeEdges(S source,
S destination) |
Removes all transitions between
source and destination . |
default void |
removeState(S state) |
Removes a state and all transitions involving it from the automaton.
|
default boolean |
removeStates(java.util.Collection<? extends S> states) |
Removes the specified
states and all transitions involving them from the automaton. |
boolean |
removeStates(java.util.function.Predicate<? super S> states) |
Removes the specified
states and all transitions involving them from the automaton. |
default java.util.Set<S> |
removeUnreachableStates() |
Removes all states which are not reachable from the initial states and returns all removed
states.
|
default java.util.Set<S> |
removeUnreachableStates(java.util.Collection<? extends S> start) |
Removes all states which are not reachable from the specified
start set and returns all
removed states. |
void |
removeUnreachableStates(java.util.Collection<? extends S> start,
java.util.function.Consumer<? super S> removedStatesConsumer) |
Removes all states which are not reachable from the specified
start set, passing each
removed state to removedStatesConsumer , used for e.g. |
default void |
setInitialState(S state) |
Set the initial state of the automaton.
|
void |
setInitialStates(java.util.Collection<? extends S> states) |
Sets the set of initial states of the automaton.
|
default void |
setName(java.lang.String name) |
Sets the name of the automaton (optional operation).
|
containsState, containsStates, forEachEdge, forEachEdge, forEachLabelledEdge, forEachLabelledEdge, forEachState, getAcceptance, getEdge, getEdges, getEdges, getFactory, getInitialState, getInitialStates, getLabelledEdges, getPredecessors, getStates, getSuccessor, getSuccessorMap, getSuccessors, getSuccessors, getVariables, is, size, toHoa
getName, toHoa
default void addEdge(S source, Edge<? extends S> edge)
source
state under any valuation.source
- The source state. If is not already present, it gets added to the transition tableedge
- The respective edge, containing destination and acceptance information.default void addEdge(S source, java.util.BitSet valuation, Edge<? extends S> edge)
source
state under valuation
.source
- The source state. If is not already present, it gets added to the transition tablevaluation
- The valuation under which this transition is possible.edge
- The respective edge, containing destination and acceptance information.void addEdge(S source, ValuationSet valuations, Edge<? extends S> edge)
source
state under valuations
.source
- The source state. If is not already present, it gets added to the transition table.valuations
- The valuations under which this transition is possible.edge
- The respective edge, containing destination and acceptance information.default void addInitialState(S state)
state
to the set of initial states. Requires this state to be present in the
automaton.state
- The state to be added.java.lang.IllegalArgumentException
- If the specified state is not part of the automaton.addInitialStates(Collection)
void addInitialStates(java.util.Collection<? extends S> states)
states
to the set of initial states. Requires the states to be present in
the automaton.states
- The states to be added.java.lang.IllegalArgumentException
- If any of the specified states is not part of the automaton.default void addState(S state)
state
without outgoing edges to the set of states. If the state is already
present, nothing is changed.state
- The state to be added.addStates(Collection)
void addStates(java.util.Collection<? extends S> states)
states
without outgoing edges to the set of states. For already present states,
nothing is changed.states
- The states to be added.default void remapEdges(java.util.function.BiFunction<? super S,Edge<S>,Edge<S>> updater)
updater
.
The function is allowed to return null
which indicates that the edge should be
removed.
updater
- The remapping function.remapEdges(Set, BiFunction)
void remapEdges(java.util.Set<? extends S> states, java.util.function.BiFunction<? super S,Edge<S>,Edge<S>> updater)
states
according to updater
.
The function is allowed to return null
which indicates that the edge should be
removed. Requires all states
to be present in the automaton.
states
- The states whose outgoing edges are to be remapped.updater
- The remapping function.java.lang.IllegalArgumentException
- If any state specified is not present in the automaton.void removeEdge(S source, java.util.BitSet valuation, S destination)
source
under valuation
to destination
.
Requires both states to be present in the automaton.source
- The source state.valuation
- The valuation.destination
- The destination state.java.lang.IllegalArgumentException
- If either source
or destination
are not present in the automaton.removeEdge(Object, ValuationSet, Object)
void removeEdge(S source, ValuationSet valuations, S destination)
source
under valuations
to destination
.
Requires both states to be present in the automaton.source
- The source state.valuations
- The valuations.destination
- The destination state.java.lang.IllegalArgumentException
- If either source
or destination
are not present in the automaton.default void removeEdges(S source, S destination)
source
and destination
. Requires both states to
be present in the automaton.source
- The source state.destination
- The destination state.java.lang.IllegalArgumentException
- If either source
or destination
are not present in the automaton.default void removeState(S state)
state
- The state to be removed.removeStates(Collection)
default boolean removeStates(java.util.Collection<? extends S> states)
states
and all transitions involving them from the automaton.states
- The states to be removed.boolean removeStates(java.util.function.Predicate<? super S> states)
states
and all transitions involving them from the automaton.states
- The states to be removed.default java.util.Set<S> removeUnreachableStates()
removeUnreachableStates(Collection, Consumer)
default java.util.Set<S> removeUnreachableStates(java.util.Collection<? extends S> start)
start
set and returns all
removed states.removeUnreachableStates(Collection, Consumer)
void removeUnreachableStates(java.util.Collection<? extends S> start, java.util.function.Consumer<? super S> removedStatesConsumer)
start
set, passing each
removed state to removedStatesConsumer
, used for e.g. freeing of BDD nodes or
collecting them in a set.removeUnreachableStates(Collection)
default void setInitialState(S state)
state
- The new initial state.java.lang.IllegalArgumentException
- If the state
is not part of the automaton.void setInitialStates(java.util.Collection<? extends S> states)
states
- The new set of initial states (potentially empty)java.lang.IllegalArgumentException
- If any of the specified states
is not part of the automaton.default void setName(java.lang.String name)
name
- The new name of the automaton.java.lang.UnsupportedOperationException
- if the automaton does not support setting a name.