Package owl.automaton

Class AbstractMemoizingAutomaton<S,A extends EmersonLeiAcceptance>

java.lang.Object

owl.automaton.AbstractMemoizingAutomaton<S,A>

Type Parameters:

S - the state type

A - the acceptance condition type

All Implemented Interfaces:

Automaton<S,A>

Direct Known Subclasses:

AbstractMemoizingAutomaton.EdgeMapImplementation, AbstractMemoizingAutomaton.EdgesImplementation, AbstractMemoizingAutomaton.EdgeTreeImplementation, AbstractMemoizingAutomaton.PartitionedEdgeTreeImplementation

public abstract class AbstractMemoizingAutomaton<S,A extends EmersonLeiAcceptance>
extends Object
implements Automaton<S,A>

This class provides a skeletal implementation of the Automaton interface to minimize the effort required to implement this interface.

It assumes that the automaton is immutable, i.e., the set of initial states, the transition relation, and the acceptance condition is fixed. It makes use of this assumption by caching the set of states and by memoizing the transition relation as MtBdd.

Depending on the computation of the transition relation different sub-classes are available: AbstractMemoizingAutomaton.EdgeImplementation, AbstractMemoizingAutomaton.EdgesImplementation, AbstractMemoizingAutomaton.EdgeTreeImplementation, and AbstractMemoizingAutomaton.EdgeMapImplementation. It is recommended to extend AbstractMemoizingAutomaton.EdgeTreeImplementation.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	AbstractMemoizingAutomaton.EdgeImplementation<S,A extends EmersonLeiAcceptance>	This class provides a skeletal implementation of the Automaton interface to minimize the effort required to implement this interface.
static class	AbstractMemoizingAutomaton.EdgeMapImplementation<S,A extends EmersonLeiAcceptance>	This class provides a skeletal implementation of the Automaton interface to minimize the effort required to implement this interface.
static class	AbstractMemoizingAutomaton.EdgesImplementation<S,A extends EmersonLeiAcceptance>	This class provides a skeletal implementation of the Automaton interface to minimize the effort required to implement this interface.
static class	AbstractMemoizingAutomaton.EdgeTreeImplementation<S,A extends EmersonLeiAcceptance>	This class provides a skeletal implementation of the Automaton interface to minimize the effort required to implement this interface.
static class	AbstractMemoizingAutomaton.PartitionedEdgeTreeImplementation<A,B,C extends EmersonLeiAcceptance>	This class provides a skeletal implementation of the Automaton interface to minimize the effort required to implement this interface.

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

Automaton.Property

Field Summary

Fields

Modifier and Type	Field	Description
protected A	acceptance
protected List<String>	atomicPropositions
protected BddSetFactory	factory
protected Set<S>	initialStates

Method Summary

Modifier and Type	Method	Description
A	acceptance()	Returns the acceptance condition of this automaton.
List<String>	atomicPropositions()
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.
protected abstract MtBdd<Edge<S>>	edgeTreeImpl(S state)
protected void	explorationCompleted()
BddSetFactory	factory()	Returns the backing engine for the symbolic representation of edges.
S	initialState()	Returns the initial state.
Set<S>	initialStates()	Returns the set of initial states, which can potentially be empty.
boolean	is(Automaton.Property property)
static <S,A extends EmersonLeiAcceptance> AbstractMemoizingAutomaton<S,A>	memoizingAutomaton(Automaton<S,A> automaton)	Wrap any automaton into a MemoizingAutomaton to make use of the internal caching mechanism and to guarantee immutability after full exploration.
Set<S>	states()	The set of all from the initial states reachable states in this automaton.
S	successor(S state, BitSet valuation)	Returns the successor of the specified state under the given valuation.
Set<S>	successors(S state)	Returns all successors of the specified state.
Set<S>	successors(S state, BitSet valuation)	Returns the successors of the specified state under the given valuation.

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

predecessors

Field Detail

acceptance

protected final A extends EmersonLeiAcceptance acceptance

initialStates

protected final Set<S> initialStates

factory

protected final BddSetFactory factory

atomicPropositions

protected final List<String> atomicPropositions

Method Detail

memoizingAutomaton

public static <S,A extends EmersonLeiAcceptance> AbstractMemoizingAutomaton<S,A> memoizingAutomaton(Automaton<S,A> automaton)

Wrap any automaton into a MemoizingAutomaton to make use of the internal caching mechanism and to guarantee immutability after full exploration. The reference to the backing automaton is dropped once the automaton is completely explored.

Type Parameters:

S - foo

A - bar

Parameters:

automaton - the automaton

Returns:

a caching instance.

edgeTree

public final 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.

edgeMap

public final 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.

edge

@Nullable
public final 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 final 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.

edges

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

successor

@Nullable
public final S successor(S state,
                         BitSet valuation)

Description copied from interface: Automaton

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.

Specified by:

successor in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The starting state of the transition.

valuation - The valuation.

Returns:

A successor or null if none.

successors

public final Set<S> successors(S state,
                               BitSet valuation)

Description copied from interface: Automaton

Returns the successors of the specified state under the given valuation.

Specified by:

successors in interface Automaton<S,A extends EmersonLeiAcceptance>

Parameters:

state - The starting state of the transition.

valuation - The valuation.

Returns:

The successor set.

successors

public final 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.

acceptance

public final 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 final List<String> atomicPropositions()

Specified by:

atomicPropositions in interface Automaton<S,A extends EmersonLeiAcceptance>

factory

public final 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.

initialState

public final S initialState()

Description copied from interface: Automaton

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

Specified by:

initialState in interface Automaton<S,A extends EmersonLeiAcceptance>

Returns:

The unique initial state or null.

See Also:

Automaton.initialStates()

initialStates

public final 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.

states

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

is

public boolean is(Automaton.Property property)

Specified by:

is in interface Automaton<S,A extends EmersonLeiAcceptance>

edgeTreeImpl

protected abstract MtBdd<Edge<S>> edgeTreeImpl(S state)

explorationCompleted

protected void explorationCompleted()