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:
EdgeMapAutomatonMixin<S,A>
,EdgesAutomatonMixin<S,A>
,EdgeTreeAutomatonMixin<S,A>
,Game<S,A>
,MutableAutomaton<S,A>
- All Known Implementing Classes:
AbstractCachedStatesAutomaton
,AbstractImplicitAutomaton
,DeterministicConstructions.CoSafety
,DeterministicConstructions.FgSafety
,DeterministicConstructions.GCoSafety
,DeterministicConstructions.GfCoSafety
,DeterministicConstructions.Safety
,DeterministicConstructions.Tracking
,ImplicitNonDeterministicEdgeTreeAutomaton
,LegacyFactory
,NonDeterministicConstructions.CoSafety
,NonDeterministicConstructions.FgSafety
,NonDeterministicConstructions.GfCoSafety
,NonDeterministicConstructions.Safety
,NonDeterministicConstructions.Tracking
,TwoPartAutomaton
,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(EdgeMapVisitor)
,accept(EdgeTreeVisitor)
,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.
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static interface
Automaton.EdgeMapVisitor<S>
static interface
Automaton.EdgeTreeVisitor<S>
static interface
Automaton.EdgeVisitor<S>
static class
Automaton.PreferredEdgeAccess
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.EdgeMapVisitor<S> visitor)
default void
accept(Automaton.EdgeTreeVisitor<S> visitor)
default void
accept(Automaton.EdgeVisitor<S> visitor)
default void
accept(Automaton.Visitor<S> visitor)
Traverse all edges of the automaton using the preferred visitor style.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
.Map<Edge<S>,ValuationSet>
edgeMap(S state)
Returns a mapping from all outgoing edges to their valuations of the specifiedstate
.Set<Edge<S>>
edges(S state)
Returns all successor edges of the specifiedstate
under any valuation.Set<Edge<S>>
edges(S state, BitSet valuation)
Returns the successor edges of the specifiedstate
under the givenvaluation
.ValuationTree<Edge<S>>
edgeTree(S state)
Returns a decision-tree with nodes labelled by literals and sets of edges as leaves.ValuationSetFactory
factory()
Set<S>
initialStates()
Returns the set of initial states, which can potentially be empty.default boolean
is(Automaton.Property property)
default String
name()
default S
onlyInitialState()
Returns the initial state.default Set<S>
predecessors(S successor)
Returns the predecessors of the specifiedsuccessor
.List<Automaton.PreferredEdgeAccess>
preferredEdgeAccess()
Indicate if the automaton implements a fast (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
.default 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
Set<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:
edgeMap(Object)
-
edges
Set<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
-
edgeMap
Map<Edge<S>,ValuationSet> edgeMap(S state)
Returns a mapping from all outgoing edges to their valuations of the specifiedstate
.- Parameters:
state
- The state.- Returns:
- All labelled edges of the state.
-
edgeTree
ValuationTree<Edge<S>> edgeTree(S state)
Returns a decision-tree with nodes labelled by literals and sets of edges as leaves.- Parameters:
state
- The state.- Returns:
- A tree.
-
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
default 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 successor)
Returns the predecessors of the specifiedsuccessor
.- Parameters:
successor
- The successor for which the predecessor set needs to be computed.- Returns:
- The predecessor set.
-
accept
default void accept(Automaton.EdgeVisitor<S> visitor)
-
accept
default void accept(Automaton.EdgeMapVisitor<S> visitor)
-
accept
default void accept(Automaton.EdgeTreeVisitor<S> visitor)
-
accept
default void accept(Automaton.Visitor<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.
-
preferredEdgeAccess
List<Automaton.PreferredEdgeAccess> preferredEdgeAccess()
Indicate if the automaton implements a fast (e.g. symbolic) computation of edges. Returns aList
containing all supportedPreferredEdgeAccess
ordered by their preference. Meaning the element at first position (index 0) is the most preferred. Accordingly algorithms can change the use ofedges(Object, BitSet)
,edgeMap(Object)
, oredgeTree(Object)
for accessing all outgoing edges of a state. This information is also used to dispatch to the right visitor style.- Returns:
- An ordered list of the traversal methods. It always contains a complete list
-
is
default boolean is(Automaton.Property property)
-
-