Interface Automaton<S,A extends OmegaAcceptance>
-
- Type Parameters:
S
- the type of the states of the automatonA
- the type of the omega-acceptance condition of the automaton
- All Known Subinterfaces:
EdgesAutomatonMixin<S,A>
,Game<S,A>
,LabelledEdgesAutomatonMixin<S,A>
,MutableAutomaton<S,A>
- All Known Implementing Classes:
AbstractAutomaton
,ImplicitCachedStatesAutomaton
,Views.AutomatonView
public interface Automaton<S,A extends OmegaAcceptance>
The base interface providing read access to an automaton. If mutation is required either theMutableAutomaton
interface or an on-the-fly view fromViews
can be used.The methods of the interface are always referring to the set of states reachable from the initial states, especially
size()
,states()
,accept(EdgeVisitor)
,accept(HybridVisitor)
,accept(HybridVisitor)
,predecessors(Object)
only refer to the from the initial states reachable set.All methods throw an
IllegalArgumentException
on a best-effort basis if they detect that a state given as an argument is not reachable from the initial states. Note that this behavior cannot be guaranteed, as it is, generally speaking, extremely expensive to check this for on-the-fly constructed automata. Therefore, it would be wrong to write a program that depended on this exception for its correctness: this should be only used to detect bugs.Further, every state-related operation (e.g.,
successors(Object)
) should be unique, while edge-related operations may yield duplicates. For example,forEachEdge(Object, Consumer)
may yield the same state-edge pair multiple times.
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static interface
Automaton.EdgeVisitor<S>
static interface
Automaton.HybridVisitor<S>
static interface
Automaton.LabelledEdgeVisitor<S>
static class
Automaton.Property
static interface
Automaton.Visitor<S>
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description default void
accept(Automaton.EdgeVisitor<S> visitor)
default void
accept(Automaton.HybridVisitor<S> visitor)
Traverse all edges of the automaton using the preferred visitor style.default void
accept(Automaton.LabelledEdgeVisitor<S> visitor)
A
acceptance()
Returns the acceptance condition of this automaton.default Edge<S>
edge(S state, BitSet valuation)
Returns the successor edge of the specifiedstate
under the givenvaluation
.Collection<Edge<S>>
edges(S state)
Returns all successor edges of the specifiedstate
under any valuation.Collection<Edge<S>>
edges(S state, BitSet valuation)
Returns the successor edges of the specifiedstate
under the givenvaluation
.ValuationSetFactory
factory()
default void
forEachEdge(S state, Consumer<Edge<S>> action)
default void
forEachLabelledEdge(S state, BiConsumer<Edge<S>,ValuationSet> action)
Set<S>
initialStates()
Returns the set of initial states, which can potentially be empty.default boolean
is(Automaton.Property property)
Collection<LabelledEdge<S>>
labelledEdges(S state)
Returns all labelled edges of the specifiedstate
.default String
name()
default S
onlyInitialState()
Returns the initial state.default Set<S>
predecessors(S state)
Returns the predecessors of the specifiedstate
.boolean
prefersLabelled()
Indicate if the automaton implements a fast computation (e.g.default int
size()
Returns the number of reachable states of this automaton (its cardinality).Set<S>
states()
The set of all from the initial states reachable states in this automaton.default S
successor(S state, BitSet valuation)
Returns the successor of the specifiedstate
under the givenvaluation
.Set<S>
successors(S state)
Returns all successors of the specifiedstate
.default Set<S>
successors(S state, BitSet valuation)
Returns the successors of the specifiedstate
under the givenvaluation
.
-
-
-
Method Detail
-
name
default String name()
-
acceptance
A acceptance()
Returns the acceptance condition of this automaton.- Returns:
- The acceptance.
-
factory
ValuationSetFactory factory()
-
onlyInitialState
default S onlyInitialState()
Returns the initial state. Throws anNoSuchElementException
if there is no andIllegalStateException
if there are multiple initial states.- Returns:
- The unique initial state.
- Throws:
NoSuchElementException
- If there is no initial state.IllegalStateException
- If there are multiple initial states.- See Also:
initialStates()
-
initialStates
Set<S> initialStates()
Returns the set of initial states, which can potentially be empty.- Returns:
- The set of initial states.
-
size
default int size()
Returns the number of reachable states of this automaton (its cardinality). If this set contains more thanInteger.MAX_VALUE
elements, it returnsInteger.MAX_VALUE
.- Returns:
- the number of elements in this set (its cardinality)
- See Also:
states()
-
states
Set<S> states()
The set of all from the initial states reachable states in this automaton.- Returns:
- All reachable states
-
edges
Collection<Edge<S>> edges(S state, BitSet valuation)
Returns the successor edges of the specifiedstate
under the givenvaluation
.- Parameters:
state
- The starting state of the transition.valuation
- The valuation.- Returns:
- The successor edges, possibly empty.
-
edge
@Nullable default Edge<S> edge(S state, BitSet valuation)
Returns the successor edge of the specifiedstate
under the givenvaluation
. 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
edges(Object, BitSet)
method.- Parameters:
state
- The starting state of the transition.valuation
- The valuation.- Returns:
- A successor edge or
null
if none. - See Also:
labelledEdges(Object)
-
edges
Collection<Edge<S>> edges(S state)
Returns all successor edges of the specifiedstate
under any valuation.- Parameters:
state
- The starting state of the edges.- Returns:
- The set of edges originating from
state
-
labelledEdges
Collection<LabelledEdge<S>> labelledEdges(S state)
Returns all labelled edges of the specifiedstate
.- Parameters:
state
- The state.- Returns:
- All labelled edges of the state.
-
forEachLabelledEdge
default void forEachLabelledEdge(S state, BiConsumer<Edge<S>,ValuationSet> action)
-
successors
default Set<S> successors(S state, BitSet valuation)
Returns the successors of the specifiedstate
under the givenvaluation
.- Parameters:
state
- The starting state of the transition.valuation
- The valuation.- Returns:
- The successor set.
-
successor
@Nullable default S successor(S state, BitSet valuation)
Returns the successor of the specifiedstate
under the givenvaluation
. Returns some state 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 getSuccessors() method.
- Parameters:
state
- The starting state of the transition.valuation
- The valuation.- Returns:
- A successor or
null
if none.
-
successors
Set<S> successors(S state)
Returns all successors of the specifiedstate
.- Parameters:
state
- The starting state of the transition.- Returns:
- The successor set.
-
predecessors
default Set<S> predecessors(S state)
Returns the predecessors of the specifiedstate
.- Parameters:
state
- The starting state of the transition.- Returns:
- The predecessor set.
-
accept
default void accept(Automaton.EdgeVisitor<S> visitor)
-
accept
default void accept(Automaton.LabelledEdgeVisitor<S> visitor)
-
accept
default void accept(Automaton.HybridVisitor<S> visitor)
Traverse all edges of the automaton using the preferred visitor style. The iteration order is not specified and can be arbitrary.- Parameters:
visitor
- the visitor.
-
prefersLabelled
boolean prefersLabelled()
Indicate if the automaton implements a fast computation (e.g. symbolic) of labelled edges. Returnstrue
, if the automaton advices to uselabelledEdges(Object)
andaccept(LabelledEdgeVisitor)
for accessing all outgoing edges of a state.- Returns:
- The preferred traversal method.
-
is
default boolean is(Automaton.Property property)
-
-