Package owl.translations.canonical
Class DeterministicConstructions.GfCoSafety
- java.lang.Object
-
- owl.automaton.AbstractCachedStatesAutomaton<S,A>
-
- owl.translations.canonical.DeterministicConstructions.GfCoSafety
-
- All Implemented Interfaces:
Automaton<RoundRobinState<EquivalenceClass>,GeneralizedBuchiAcceptance>
,EdgeTreeAutomatonMixin<RoundRobinState<EquivalenceClass>,GeneralizedBuchiAcceptance>
- Enclosing class:
- DeterministicConstructions
public static class DeterministicConstructions.GfCoSafety extends AbstractCachedStatesAutomaton<S,A>
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from interface owl.automaton.Automaton
Automaton.EdgeMapVisitor<S>, Automaton.EdgeTreeVisitor<S>, Automaton.EdgeVisitor<S>, Automaton.PreferredEdgeAccess, Automaton.Property, Automaton.Visitor<S>
-
-
Field Summary
-
Fields inherited from interface owl.automaton.EdgeTreeAutomatonMixin
ACCESS_MODES
-
-
Constructor Summary
Constructors Constructor Description GfCoSafety(Factories factories, boolean unfold, Set<? extends Formula> formulas, boolean generalized)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description GeneralizedBuchiAcceptance
acceptance()
Returns the acceptance condition of this automaton.Edge<RoundRobinState<EquivalenceClass>>
edge(RoundRobinState<EquivalenceClass> state, BitSet valuation)
Returns the successor edge of the specifiedstate
under the givenvaluation
.Set<Edge<S>>
edges(S state, BitSet valuation)
Returns the successor edges of the specifiedstate
under the givenvaluation
.ValuationTree<Edge<RoundRobinState<EquivalenceClass>>>
edgeTree(RoundRobinState<EquivalenceClass> state)
Returns a decision-tree with nodes labelled by literals and sets of edges as leaves.ValuationSetFactory
factory()
Set<S>
initialStates()
Returns the set of initial states, which can potentially be empty.boolean
is(Automaton.Property property)
RoundRobinState<EquivalenceClass>
onlyInitialState()
Returns the initial state.-
Methods inherited from class owl.automaton.AbstractCachedStatesAutomaton
accept, accept, accept, cache, states
-
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
accept, accept, accept, accept, name, predecessors, size, states, successor, successors, successors
-
Methods inherited from interface owl.automaton.EdgeTreeAutomatonMixin
edgeMap, edges, preferredEdgeAccess
-
-
-
-
Method Detail
-
acceptance
public GeneralizedBuchiAcceptance acceptance()
Description copied from interface:Automaton
Returns the acceptance condition of this automaton.- Returns:
- The acceptance.
-
onlyInitialState
public final RoundRobinState<EquivalenceClass> onlyInitialState()
Description copied from interface:Automaton
Returns the initial state. Throws anNoSuchElementException
if there is no andIllegalStateException
if there are multiple initial states.- Specified by:
onlyInitialState
in interfaceAutomaton<RoundRobinState<EquivalenceClass>,GeneralizedBuchiAcceptance>
- Returns:
- The unique initial state.
- See Also:
Automaton.initialStates()
-
edge
@Nonnull public final Edge<RoundRobinState<EquivalenceClass>> edge(RoundRobinState<EquivalenceClass> state, BitSet valuation)
Description copied from interface:Automaton
Returns the successor edge of the specifiedstate
under 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:
edge
in interfaceAutomaton<RoundRobinState<EquivalenceClass>,GeneralizedBuchiAcceptance>
- Parameters:
state
- The starting state of the transition.valuation
- The valuation.- Returns:
- A successor edge or
null
if none. - See Also:
Automaton.edgeMap(Object)
-
edgeTree
public final ValuationTree<Edge<RoundRobinState<EquivalenceClass>>> edgeTree(RoundRobinState<EquivalenceClass> 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 interfaceAutomaton<RoundRobinState<EquivalenceClass>,GeneralizedBuchiAcceptance>
- Parameters:
state
- The state.- Returns:
- A tree.
-
is
public final boolean is(Automaton.Property property)
- Specified by:
is
in interfaceAutomaton<RoundRobinState<EquivalenceClass>,GeneralizedBuchiAcceptance>
-
factory
public final ValuationSetFactory factory()
- Specified by:
factory
in interfaceAutomaton<S,A extends OmegaAcceptance>
-
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 interfaceAutomaton<S,A extends OmegaAcceptance>
- Returns:
- The set of initial states.
-
edges
public final Set<Edge<S>> edges(S state, BitSet valuation)
Description copied from interface:Automaton
Returns the successor edges of the specifiedstate
under the givenvaluation
.- Specified by:
edges
in interfaceAutomaton<S,A extends OmegaAcceptance>
- Specified by:
edges
in interfaceEdgeTreeAutomatonMixin<S,A extends OmegaAcceptance>
- Parameters:
state
- The starting state of the transition.valuation
- The valuation.- Returns:
- The successor edges, possibly empty.
-
-