Class AbstractMemoizingAutomaton<S,A extends EmersonLeiAcceptance>
- java.lang.Object
-
- owl.automaton.AbstractMemoizingAutomaton<S,A>
-
- Type Parameters:
S- the state typeA- 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 theAutomatoninterface 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, andAbstractMemoizingAutomaton.EdgeMapImplementation. It is recommended to extendAbstractMemoizingAutomaton.EdgeTreeImplementation.
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description static classAbstractMemoizingAutomaton.EdgeImplementation<S,A extends EmersonLeiAcceptance>This class provides a skeletal implementation of theAutomatoninterface to minimize the effort required to implement this interface.static classAbstractMemoizingAutomaton.EdgeMapImplementation<S,A extends EmersonLeiAcceptance>This class provides a skeletal implementation of theAutomatoninterface to minimize the effort required to implement this interface.static classAbstractMemoizingAutomaton.EdgesImplementation<S,A extends EmersonLeiAcceptance>This class provides a skeletal implementation of theAutomatoninterface to minimize the effort required to implement this interface.static classAbstractMemoizingAutomaton.EdgeTreeImplementation<S,A extends EmersonLeiAcceptance>This class provides a skeletal implementation of theAutomatoninterface to minimize the effort required to implement this interface.static classAbstractMemoizingAutomaton.PartitionedEdgeTreeImplementation<A,B,C extends EmersonLeiAcceptance>This class provides a skeletal implementation of theAutomatoninterface 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 Aacceptanceprotected List<String>atomicPropositionsprotected BddSetFactoryfactoryprotected Set<S>initialStates
-
Method Summary
All Methods Static Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description Aacceptance()Returns the acceptance condition of this automaton.List<String>atomicPropositions()Edge<S>edge(S state, BitSet valuation)Returns the successor edge of the specifiedstateunder the givenvaluation.Map<Edge<S>,BddSet>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.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 voidexplorationCompleted()BddSetFactoryfactory()Returns the backing engine for the symbolic representation of edges.SinitialState()Returns the initial state.Set<S>initialStates()Returns the set of initial states, which can potentially be empty.booleanis(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.Ssuccessor(S state, BitSet valuation)Returns the successor of the specifiedstateunder the givenvaluation.Set<S>successors(S state)Returns all successors of the specifiedstate.Set<S>successors(S state, BitSet valuation)Returns the successors of the specifiedstateunder the givenvaluation.-
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
-
factory
protected final BddSetFactory factory
-
-
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- fooA- bar- Parameters:
automaton- the automaton- Returns:
- a caching instance.
-
edgeTree
public final MtBdd<Edge<S>> edgeTree(S state)
Description copied from interface:AutomatonReturns a decision-tree with nodes labelled by literals and sets of edges as leaves.- Specified by:
edgeTreein interfaceAutomaton<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:AutomatonReturns a mapping from all outgoing edges to their valuations of the specifiedstate.- Specified by:
edgeMapin interfaceAutomaton<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:AutomatonReturns 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
Automaton.edges(Object, BitSet)method.- Specified by:
edgein interfaceAutomaton<S,A extends EmersonLeiAcceptance>- Parameters:
state- The starting state of the transition.valuation- The valuation.- Returns:
- A successor edge or
nullif none. - See Also:
Automaton.edgeMap(Object)
-
edges
public final Set<Edge<S>> edges(S state, BitSet valuation)
Description copied from interface:AutomatonReturns the successor edges of the specifiedstateunder the givenvaluation.- Specified by:
edgesin interfaceAutomaton<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:AutomatonReturns all successor edges of the specifiedstateunder any valuation.- Specified by:
edgesin interfaceAutomaton<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:AutomatonReturns 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 successors() method.
- Specified by:
successorin interfaceAutomaton<S,A extends EmersonLeiAcceptance>- Parameters:
state- The starting state of the transition.valuation- The valuation.- Returns:
- A successor or
nullif none.
-
successors
public final Set<S> successors(S state, BitSet valuation)
Description copied from interface:AutomatonReturns the successors of the specifiedstateunder the givenvaluation.- Specified by:
successorsin interfaceAutomaton<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:AutomatonReturns all successors of the specifiedstate.- Specified by:
successorsin interfaceAutomaton<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:AutomatonReturns the acceptance condition of this automaton.- Specified by:
acceptancein interfaceAutomaton<S,A extends EmersonLeiAcceptance>- Returns:
- The acceptance.
-
atomicPropositions
public final List<String> atomicPropositions()
- Specified by:
atomicPropositionsin interfaceAutomaton<S,A extends EmersonLeiAcceptance>
-
factory
public final BddSetFactory factory()
Description copied from interface:AutomatonReturns the backing engine for the symbolic representation of edges. Only this engine might be used for the access to edges.- Specified by:
factoryin interfaceAutomaton<S,A extends EmersonLeiAcceptance>- Returns:
- The symbolic engine used to generate BddSets.
-
initialState
public final S initialState()
Description copied from interface:AutomatonReturns the initial state. Returns null if there is no andIllegalStateExceptionif there are multiple initial states.- Specified by:
initialStatein interfaceAutomaton<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:AutomatonReturns the set of initial states, which can potentially be empty.- Specified by:
initialStatesin interfaceAutomaton<S,A extends EmersonLeiAcceptance>- Returns:
- The set of initial states.
-
states
public final Set<S> states()
Description copied from interface:AutomatonThe set of all from the initial states reachable states in this automaton.- Specified by:
statesin interfaceAutomaton<S,A extends EmersonLeiAcceptance>- Returns:
- All reachable states
-
is
public boolean is(Automaton.Property property)
- Specified by:
isin interfaceAutomaton<S,A extends EmersonLeiAcceptance>
-
explorationCompleted
protected void explorationCompleted()
-
-