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 theMutableAutomatoninterface or an on-the-fly view fromViewscan 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
IllegalArgumentExceptionon 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 interfaceAutomaton.EdgeMapVisitor<S>static interfaceAutomaton.EdgeTreeVisitor<S>static interfaceAutomaton.EdgeVisitor<S>static classAutomaton.PreferredEdgeAccessstatic classAutomaton.Propertystatic interfaceAutomaton.Visitor<S>
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description default voidaccept(Automaton.EdgeMapVisitor<S> visitor)default voidaccept(Automaton.EdgeTreeVisitor<S> visitor)default voidaccept(Automaton.EdgeVisitor<S> visitor)default voidaccept(Automaton.Visitor<S> visitor)Traverse all edges of the automaton using the preferred visitor style.Aacceptance()Returns the acceptance condition of this automaton.default Edge<S>edge(S state, BitSet valuation)Returns the successor edge of the specifiedstateunder 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 specifiedstateunder any valuation.Set<Edge<S>>edges(S state, BitSet valuation)Returns the successor edges of the specifiedstateunder the givenvaluation.ValuationTree<Edge<S>>edgeTree(S state)Returns a decision-tree with nodes labelled by literals and sets of edges as leaves.ValuationSetFactoryfactory()Set<S>initialStates()Returns the set of initial states, which can potentially be empty.default booleanis(Automaton.Property property)default Stringname()default SonlyInitialState()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 intsize()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 Ssuccessor(S state, BitSet valuation)Returns the successor of the specifiedstateunder 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 specifiedstateunder 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 anNoSuchElementExceptionif there is no andIllegalStateExceptionif 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_VALUEelements, 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 specifiedstateunder 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 specifiedstateunder 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
nullif none. - See Also:
edgeMap(Object)
-
edges
Set<Edge<S>> edges(S state)
Returns all successor edges of the specifiedstateunder 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 specifiedstateunder 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 specifiedstateunder 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
nullif 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 aListcontaining all supportedPreferredEdgeAccessordered 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)
-
-