Package owl.automaton

Interface Automaton<S,A extends EmersonLeiAcceptance>

Type Parameters:

S - the type of the states of the automaton

A - the type of the omega-acceptance condition of the automaton

All Known Subinterfaces:

Game<S,A>, MutableAutomaton<S,A>, ZielonkaTreeTransformations.AutomatonWithZielonkaTreeLookup<S,A>

All Known Implementing Classes:

AbstractMemoizingAutomaton, AbstractMemoizingAutomaton.EdgeImplementation, AbstractMemoizingAutomaton.EdgeMapImplementation, AbstractMemoizingAutomaton.EdgesImplementation, AbstractMemoizingAutomaton.EdgeTreeImplementation, AbstractMemoizingAutomaton.PartitionedEdgeTreeImplementation, DeterministicConstructions.CoSafety, DeterministicConstructions.CoSafetySafety, DeterministicConstructions.CoSafetySafetyRoundRobin, DeterministicConstructions.GfCoSafety, DeterministicConstructions.Safety, DeterministicConstructions.SafetyCoSafety, DeterministicConstructions.SafetyCoSafetyRoundRobin, DeterministicConstructions.Tracking, EmptyAutomaton, HashMapAutomaton, NonDeterministicConstructions.CoSafety, NonDeterministicConstructions.FgSafety, NonDeterministicConstructions.GfCoSafety, NonDeterministicConstructions.Safety, NonDeterministicConstructions.Tracking, SimulationGame, SingletonAutomaton

public interface Automaton<S,A extends EmersonLeiAcceptance>

An automaton over infinite words.

This interface provides an explicit representation of an automaton with a optional symbolic encoding of transitions.

The base interface providing read access to an automaton. If mutation is required either the MutableAutomaton interface or an on-the-fly view from Views can be used.

The methods of the interface are always referring to the set of states reachable from the initial states, i.e., states() and 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, expensive to check this for on-the-fly constructed automata. Therefore, it would be wrong to write a program that depends on this exception for its correctness: this should be only used to detect bugs.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static class	Automaton.Property

Method Summary

Modifier and Type	Method	Description
A	acceptance()	Returns the acceptance condition of this automaton.
List<String>	atomicPropositions()
default Edge<S>	edge(S state, BitSet valuation)	Returns the successor edge of the specified state under the given valuation.
Map<Edge<S>,BddSet>	edgeMap(S state)	Returns a mapping from all outgoing edges to their valuations of the specified state.
default Set<Edge<S>>	edges(S state)	Returns all successor edges of the specified state under any valuation.
Set<Edge<S>>	edges(S state, BitSet valuation)	Returns the successor edges of the specified state under the given valuation.
MtBdd<Edge<S>>	edgeTree(S state)	Returns a decision-tree with nodes labelled by literals and sets of edges as leaves.
BddSetFactory	factory()	Returns the backing engine for the symbolic representation of edges.
default S	initialState()	Returns the initial state.
Set<S>	initialStates()	Returns the set of initial states, which can potentially be empty.
default boolean	is(Automaton.Property property)
default Set<S>	predecessors(S successor)	Returns the predecessors of the specified successor.
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 specified state under the given valuation.
default Set<S>	successors(S state)	Returns all successors of the specified state.
default Set<S>	successors(S state, BitSet valuation)	Returns the successors of the specified state under the given valuation.

Method Detail

acceptance

A acceptance()

Returns the acceptance condition of this automaton.

Returns:

The acceptance.

atomicPropositions

List<String> atomicPropositions()

factory

BddSetFactory factory()

Returns the backing engine for the symbolic representation of edges. Only this engine might be used for the access to edges.

Returns:

The symbolic engine used to generate BddSets.

initialState

default S initialState()

Returns the initial state. Returns null if there is no and IllegalStateException if there are multiple initial states.

Returns:

The unique initial state or null.

Throws:

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.

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 specified state under the given valuation.

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 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 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

default Set<Edge<S>> edges(S state)

Returns all successor edges of the specified state under any valuation.

Parameters:

state - The starting state of the edges.

Returns:

The set of edges originating from state

edgeMap

Map<Edge<S>,BddSet> edgeMap(S state)

Returns a mapping from all outgoing edges to their valuations of the specified state.

Parameters:

state - The state.

Returns:

All labelled edges of the state.

edgeTree

MtBdd<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 specified state under the given valuation.

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 specified state under the given valuation. 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 successors() 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 specified state.

Parameters:

state - The starting state of the transition.

Returns:

The successor set.

predecessors

default Set<S> predecessors(S successor)

Returns the predecessors of the specified successor.

Parameters:

successor - The successor for which the predecessor set needs to be computed.

Returns:

The predecessor set.

is

default boolean is(Automaton.Property property)