HoaPrintable
Game<S,A>
, MutableAutomaton<S,A>
StreamingAutomaton
, Views.ForwardingAutomaton
, Views.ForwardingMutableAutomaton
public interface Automaton<S,A extends OmegaAcceptance> extends HoaPrintable
Modifier and Type | Interface | Description |
---|---|---|
static class |
Automaton.Property |
HoaPrintable.HoaOption
Modifier and Type | Method | Description |
---|---|---|
default boolean |
containsState(S state) |
Determines whether the automaton contains the given
state . |
default boolean |
containsStates(java.util.Collection<? extends S> states) |
Determines whether the automaton contains all the given
states . |
default void |
forEachEdge(java.util.function.BiConsumer<S,Edge<S>> action) |
|
default void |
forEachEdge(S state,
java.util.function.Consumer<Edge<S>> action) |
|
default void |
forEachLabelledEdge(TriConsumer<S,Edge<S>,ValuationSet> action) |
|
default void |
forEachLabelledEdge(S state,
java.util.function.BiConsumer<Edge<S>,ValuationSet> action) |
|
default void |
forEachState(java.util.function.Consumer<S> action) |
|
A |
getAcceptance() |
Returns the acceptance condition of this automaton.
|
default Edge<S> |
getEdge(S state,
java.util.BitSet valuation) |
Returns the successor edge of the specified
state under the given valuation . |
default java.util.Set<Edge<S>> |
getEdges(S state) |
Returns all successor edges of the specified
state under any valuation. |
default java.util.Set<Edge<S>> |
getEdges(S state,
java.util.BitSet valuation) |
Returns the successor edges of the specified
state under the given valuation . |
ValuationSetFactory |
getFactory() |
|
default S |
getInitialState() |
Returns the initial state.
|
java.util.Set<S> |
getInitialStates() |
Returns the set of initial states, which can potentially be empty.
|
java.util.Collection<LabelledEdge<S>> |
getLabelledEdges(S state) |
Returns all successors of the specified
state . |
default java.util.Set<S> |
getPredecessors(S state) |
|
java.util.Set<S> |
getStates() |
Returns all states in this automaton.
|
default S |
getSuccessor(S state,
java.util.BitSet valuation) |
|
default java.util.Map<S,ValuationSet> |
getSuccessorMap(S state) |
|
default java.util.Set<S> |
getSuccessors(S state) |
|
default java.util.Set<S> |
getSuccessors(S state,
java.util.BitSet valuation) |
|
default java.util.List<java.lang.String> |
getVariables() |
|
default boolean |
is(Automaton.Property property) |
|
default int |
size() |
Returns the number of states of this automaton (its cardinality).
|
default void |
toHoa(jhoafparser.consumer.HOAConsumer consumer,
java.util.EnumSet<HoaPrintable.HoaOption> options) |
getName, toHoa
default boolean containsState(S state)
state
.state
- The state to be checked.default boolean containsStates(java.util.Collection<? extends S> states)
states
.states
- The states to be checked.default void forEachLabelledEdge(S state, java.util.function.BiConsumer<Edge<S>,ValuationSet> action)
default void forEachLabelledEdge(TriConsumer<S,Edge<S>,ValuationSet> action)
default void forEachState(java.util.function.Consumer<S> action)
A getAcceptance()
@Nullable default Edge<S> getEdge(S state, java.util.BitSet valuation)
Returns the successor edge of the specified state
under the given valuation
.
Returns some edge if there is a non-deterministic choice in this state for the specified
valuation.
If you want to check if this is the unique edge use the getEdges() method.
state
- The starting state of the transition.valuation
- The valuation.null
if none.getLabelledEdges(Object)
default java.util.Set<Edge<S>> getEdges(S state)
state
under any valuation.state
- The starting state of the edges.state
default java.util.Set<Edge<S>> getEdges(S state, java.util.BitSet valuation)
state
under the given valuation
.state
- The starting state of the transition.valuation
- The valuation.ValuationSetFactory getFactory()
default S getInitialState()
IllegalStateException
if there a no or multiple
initial states.java.util.NoSuchElementException
- If there is no initial state.java.lang.IllegalArgumentException
- If there is no unique initial state.getInitialStates()
java.util.Set<S> getInitialStates()
java.util.Collection<LabelledEdge<S>> getLabelledEdges(S state)
state
.state
- The state.java.util.Set<S> getStates()
default java.util.Map<S,ValuationSet> getSuccessorMap(S state)
default java.util.List<java.lang.String> getVariables()
getVariables
in interface HoaPrintable
default boolean is(Automaton.Property property)
default int size()
Integer.MAX_VALUE
elements, returns
Integer.MAX_VALUE
.default void toHoa(jhoafparser.consumer.HOAConsumer consumer, java.util.EnumSet<HoaPrintable.HoaOption> options)
toHoa
in interface HoaPrintable