Package owl.automaton

Class HashMapAutomaton<S,A extends EmersonLeiAcceptance>

java.lang.Object

owl.automaton.HashMapAutomaton<S,A>

All Implemented Interfaces:

Automaton<S,A>, MutableAutomaton<S,A>

public final class HashMapAutomaton<S,A extends EmersonLeiAcceptance>
extends Object
implements MutableAutomaton<S,A>

Nested Class Summary

Nested classes/interfaces inherited from interface owl.automaton.Automaton

Automaton.Property

Method Summary

Modifier and Type	Method	Description
A	acceptance()	Returns the acceptance condition of this automaton.
void	acceptance(A acceptance)
void	addEdge(S source, BddSet valuations, Edge<? extends S> edge)	Adds transitions from the source state under valuations.
void	addInitialState(S initialState)	Add an initial state to the automaton.
void	addState(S state)	Adds a state without outgoing edges to the set of states.
List<String>	atomicPropositions()
static <S,A extends EmersonLeiAcceptance> HashMapAutomaton<S,A>	copyOf(Automaton<S,A> source)
static <S,A extends EmersonLeiAcceptance> HashMapAutomaton<S,A>	create(List<String> atomicPropositions, A acceptance)	Creates an empty automaton with given acceptance condition.
static <S,A extends EmersonLeiAcceptance> HashMapAutomaton<S,A>	create(List<String> atomicPropositions, BddSetFactory vsFactory, A acceptance)	Creates an empty automaton with given acceptance condition.
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.
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.
Set<S>	initialStates()	Returns the set of initial states, which can potentially be empty.
void	initialStates(Collection<? extends S> initialStates)	Sets the set of initial states of the automaton.
void	removeEdge(S source, BddSet valuations, S destination)	Removes all transition from source under valuations to destination.
void	removeInitialState(S initialState)
void	removeStateIf(Predicate<? super S> stateFilter)	Removes the specified states and all transitions involving them from the automaton.
Set<S>	states()	The set of all from the initial states reachable states in this automaton.
Set<S>	successors(S state)	Returns all successors of the specified state.
void	trim()	Removes unreachable states and adjust internal data structures after mutation.
void	updateEdges(BiFunction<S,Edge<S>,Edge<S>> updater)	Remaps each edge of the automaton according to updater.
void	updateEdges(Set<? extends S> states, BiFunction<? super S,Edge<S>,Edge<S>> f)	Remaps each outgoing edge of the specified states according to updater.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface owl.automaton.Automaton

initialState, is, predecessors, successor, successors

Methods inherited from interface owl.automaton.MutableAutomaton

addEdge, removeEdge, removeState, updateAcceptance

Method Detail

acceptance

public A acceptance()

Description copied from interface: Automaton

Returns the acceptance condition of this automaton.

Specified by:

acceptance in interface Automaton<S,A extends EmersonLeiAcceptance>

Returns:

The acceptance.

atomicPropositions

public List<String> atomicPropositions()

Specified by:

atomicPropositions in interface Automaton<S,A extends EmersonLeiAcceptance>

acceptance

public void acceptance(A acceptance)

Specified by:

acceptance in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

initialStates

public Set<S> initialStates()

Description copied from interface: Automaton

Returns the set of initial states, which can potentially be empty.

Specified by:

initialStates in interface Automaton<S,A extends EmersonLeiAcceptance>

Returns:

The set of initial states.

initialStates

public void initialStates(Collection<? extends S> initialStates)

Description copied from interface: MutableAutomaton

Sets the set of initial states of the automaton.

Specified by:

initialStates in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

initialStates - The new set of initial states (potentially empty)

addInitialState

public void addInitialState(S initialState)

Description copied from interface: MutableAutomaton

Add an initial state to the automaton.

Specified by:

addInitialState in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

initialState - The added initial state.

removeInitialState

public void removeInitialState(S initialState)

Specified by:

removeInitialState in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

states

public Set<S> states()

Description copied from interface: Automaton

The set of all from the initial states reachable states in this automaton.

Specified by:

states in interface Automaton<S,A extends EmersonLeiAcceptance>

Returns:

All reachable states

addState

public void addState(S state)

Description copied from interface: MutableAutomaton

Adds a state without outgoing edges to the set of states. If the state is already present, nothing is changed.

Specified by:

addState in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The state to be added.

removeStateIf

public void removeStateIf(Predicate<? super S> stateFilter)

Description copied from interface: MutableAutomaton

Removes the specified states and all transitions involving them from the automaton.

Specified by:

removeStateIf in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

stateFilter - The states to be removed.

edge

@Nullable
public Edge<S> edge(S state,
                    BitSet valuation)

Description copied from interface: Automaton

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 Automaton.edges(Object, BitSet) method.

Specified by:

edge in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The starting state of the transition.

valuation - The valuation.

Returns:

A successor edge or null if none.

See Also:

Automaton.edgeMap(Object)

edges

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

Description copied from interface: Automaton

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

Specified by:

edges in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The starting state of the edges.

Returns:

The set of edges originating from state

edgeMap

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

Description copied from interface: Automaton

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

Specified by:

edgeMap in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The state.

Returns:

All labelled edges of the state.

edgeTree

public MtBdd<Edge<S>> edgeTree(S state)

Description copied from interface: Automaton

Returns a decision-tree with nodes labelled by literals and sets of edges as leaves.

Specified by:

edgeTree in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The state.

Returns:

A tree.

successors

public Set<S> successors(S state)

Description copied from interface: Automaton

Returns all successors of the specified state.

Specified by:

successors in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The starting state of the transition.

Returns:

The successor set.

addEdge

public void addEdge(S source,
                    BddSet valuations,
                    Edge<? extends S> edge)

Description copied from interface: MutableAutomaton

Adds transitions from the source state under valuations.

Specified by:

addEdge in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

source - The source state.

valuations - The valuations under which this transition is possible.

edge - The respective edge, containing destination and acceptance information.

removeEdge

public void removeEdge(S source,
                       BddSet valuations,
                       S destination)

Description copied from interface: MutableAutomaton

Removes all transition from source under valuations to destination. Requires both states to be present in the automaton.

Specified by:

removeEdge in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

source - The source state.

valuations - The valuations.

destination - The destination state.

updateEdges

public void updateEdges(Set<? extends S> states,
                        BiFunction<? super S,Edge<S>,Edge<S>> f)

Description copied from interface: MutableAutomaton

Remaps each outgoing edge of the specified states according to updater.

The function is allowed to return null which indicates that the edge should be removed. Requires all states to be present in the automaton.

Specified by:

updateEdges in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

states - The states whose outgoing edges are to be remapped.

f - The remapping function. The updater needs to be stateless, since it might be called with unreachable states.

updateEdges

public void updateEdges(BiFunction<S,Edge<S>,Edge<S>> updater)

Description copied from interface: MutableAutomaton

Remaps each edge of the automaton according to updater.

The function is allowed to return null which indicates that the edge should be removed.

Specified by:

updateEdges in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

Parameters:

updater - The remapping function. The updater needs to be stateless, since it might be called with unreachable states.

See Also:

MutableAutomaton.updateEdges(Set, BiFunction)

factory

public BddSetFactory factory()

Description copied from interface: Automaton

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

Specified by:

factory in interface Automaton<S,A extends EmersonLeiAcceptance>

Returns:

The symbolic engine used to generate BddSets.

trim

public void trim()

Description copied from interface: MutableAutomaton

Removes unreachable states and adjust internal data structures after mutation.

Specified by:

trim in interface MutableAutomaton<S,A extends EmersonLeiAcceptance>

create

public static <S,A extends EmersonLeiAcceptance> HashMapAutomaton<S,A> create(List<String> atomicPropositions,
                                                                                          A acceptance)

Creates an empty automaton with given acceptance condition.

Type Parameters:

S - The states of the automaton.

A - The acceptance condition of the automaton.

Returns:

Empty automaton with the specified parameters.

create

public static <S,A extends EmersonLeiAcceptance> HashMapAutomaton<S,A> create(List<String> atomicPropositions,
                                                                                          BddSetFactory vsFactory,
                                                                                          A acceptance)

Creates an empty automaton with given acceptance condition. The valuationSetFactory is used as transition backend.

Type Parameters:

S - The states of the automaton.

A - The acceptance condition of the automaton.

Parameters:

acceptance - The acceptance of the new automaton.

vsFactory - The alphabet.

Returns:

Empty automaton with the specified parameters.

copyOf

public static <S,A extends EmersonLeiAcceptance> HashMapAutomaton<S,A> copyOf(Automaton<S,A> source)

edges

public Set<Edge<S>> edges(S state,
                          BitSet valuation)

Description copied from interface: Automaton

Returns the successor edges of the specified state under the given valuation.

Specified by:

edges in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The starting state of the transition.

valuation - The valuation.

Returns:

The successor edges, possibly empty.