Automaton<S,A>
, MutableAutomaton<S,A>
, HoaPrintable
public abstract static class Views.ForwardingMutableAutomaton<S,A extends OmegaAcceptance,B extends OmegaAcceptance> extends Views.ForwardingAutomaton<S,A,B,MutableAutomaton<S,B>> implements MutableAutomaton<S,A>
Automaton.Property
HoaPrintable.HoaOption
automaton
Modifier | Constructor | Description |
---|---|---|
protected |
ForwardingMutableAutomaton(MutableAutomaton<S,B> automaton) |
Modifier and Type | Method | Description |
---|---|---|
void |
addEdge(S source,
java.util.BitSet valuation,
Edge<? extends S> edge) |
Adds a transition from the
source state under valuation . |
void |
addEdge(S source,
ValuationSet valuations,
Edge<? extends S> edge) |
Adds transitions from the
source state under valuations . |
void |
addInitialStates(java.util.Collection<? extends S> states) |
Adds given
states to the set of initial states. |
void |
addStates(java.util.Collection<? extends S> states) |
Adds
states without outgoing edges to the set of states. |
void |
remapEdges(java.util.Set<? extends S> states,
java.util.function.BiFunction<? super S,Edge<S>,Edge<S>> f) |
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 . |
void |
removeEdges(S source,
S destination) |
Removes all transitions between
source and destination . |
boolean |
removeStates(java.util.function.Predicate<? super S> states) |
Removes the specified
states and all transitions involving them from the automaton. |
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. |
void |
setInitialStates(java.util.Collection<? extends S> states) |
Sets the set of initial states of the automaton.
|
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
addAll, addEdge, addInitialState, addState, remapEdges, removeState, removeStates, removeUnreachableStates, removeUnreachableStates, setInitialState, setName
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getFactory, getInitialStates, getLabelledEdges, getStates
protected ForwardingMutableAutomaton(MutableAutomaton<S,B> automaton)
public void addEdge(S source, java.util.BitSet valuation, Edge<? extends S> edge)
MutableAutomaton
source
state under valuation
.addEdge
in interface MutableAutomaton<S,A extends OmegaAcceptance>
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.public void addEdge(S source, ValuationSet valuations, Edge<? extends S> edge)
MutableAutomaton
source
state under valuations
.addEdge
in interface MutableAutomaton<S,A extends OmegaAcceptance>
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.public void addInitialStates(java.util.Collection<? extends S> states)
MutableAutomaton
states
to the set of initial states. Requires the states to be present in
the automaton.addInitialStates
in interface MutableAutomaton<S,A extends OmegaAcceptance>
states
- The states to be added.public void addStates(java.util.Collection<? extends S> states)
MutableAutomaton
states
without outgoing edges to the set of states. For already present states,
nothing is changed.addStates
in interface MutableAutomaton<S,A extends OmegaAcceptance>
states
- The states to be added.public void remapEdges(java.util.Set<? extends S> states, java.util.function.BiFunction<? super S,Edge<S>,Edge<S>> f)
MutableAutomaton
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.
remapEdges
in interface MutableAutomaton<S,A extends OmegaAcceptance>
states
- The states whose outgoing edges are to be remapped.f
- The remapping function.public void removeEdge(S source, java.util.BitSet valuation, S destination)
MutableAutomaton
source
under valuation
to destination
.
Requires both states to be present in the automaton.removeEdge
in interface MutableAutomaton<S,A extends OmegaAcceptance>
source
- The source state.valuation
- The valuation.destination
- The destination state.MutableAutomaton.removeEdge(Object, ValuationSet, Object)
public void removeEdge(S source, ValuationSet valuations, S destination)
MutableAutomaton
source
under valuations
to destination
.
Requires both states to be present in the automaton.removeEdge
in interface MutableAutomaton<S,A extends OmegaAcceptance>
source
- The source state.valuations
- The valuations.destination
- The destination state.public void removeEdges(S source, S destination)
MutableAutomaton
source
and destination
. Requires both states to
be present in the automaton.removeEdges
in interface MutableAutomaton<S,A extends OmegaAcceptance>
source
- The source state.destination
- The destination state.public boolean removeStates(java.util.function.Predicate<? super S> states)
MutableAutomaton
states
and all transitions involving them from the automaton.removeStates
in interface MutableAutomaton<S,A extends OmegaAcceptance>
states
- The states to be removed.public void removeUnreachableStates(java.util.Collection<? extends S> start, java.util.function.Consumer<? super S> removedStatesConsumer)
MutableAutomaton
start
set, passing each
removed state to removedStatesConsumer
, used for e.g. freeing of BDD nodes or
collecting them in a set.removeUnreachableStates
in interface MutableAutomaton<S,A extends OmegaAcceptance>
MutableAutomaton.removeUnreachableStates(Collection)
public void setInitialStates(java.util.Collection<? extends S> states)
MutableAutomaton
setInitialStates
in interface MutableAutomaton<S,A extends OmegaAcceptance>
states
- The new set of initial states (potentially empty)