Package owl.translations.canonical

Class DeterministicConstructions.SafetyCoSafety

java.lang.Object

owl.automaton.AbstractMemoizingAutomaton<S,A>

owl.automaton.AbstractMemoizingAutomaton.EdgeTreeImplementation<S,A>

owl.translations.canonical.DeterministicConstructions.SafetyCoSafety

All Implemented Interfaces:

Automaton<DeterministicConstructions.BreakpointStateRejecting,BuchiAcceptance>

Enclosing class:

DeterministicConstructions

public static final class DeterministicConstructions.SafetyCoSafety
extends AbstractMemoizingAutomaton.EdgeTreeImplementation<S,A>

Nested Class Summary

Nested classes/interfaces inherited from class owl.automaton.AbstractMemoizingAutomaton

AbstractMemoizingAutomaton.EdgeImplementation<S,A extends EmersonLeiAcceptance>, AbstractMemoizingAutomaton.EdgeMapImplementation<S,A extends EmersonLeiAcceptance>, AbstractMemoizingAutomaton.EdgesImplementation<S,A extends EmersonLeiAcceptance>, AbstractMemoizingAutomaton.EdgeTreeImplementation<S,A extends EmersonLeiAcceptance>, AbstractMemoizingAutomaton.PartitionedEdgeTreeImplementation<A,B,C extends EmersonLeiAcceptance>

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

Automaton.Property

Field Summary

Fields

Modifier and Type	Field	Description
DeterministicConstructions.SuspensionCheck	suspensionCheck

Fields inherited from class owl.automaton.AbstractMemoizingAutomaton

acceptance, atomicPropositions, initialStates

Method Summary

Modifier and Type	Method	Description
MtBdd<Edge<DeterministicConstructions.BreakpointStateRejecting>>	edgeTreeImpl(DeterministicConstructions.BreakpointStateRejecting state)
DeterministicConstructions.BreakpointStateRejecting	initialState(Formula formula)
boolean	is(Automaton.Property property)
static DeterministicConstructions.SafetyCoSafety	of(Factories factories, Formula formula)
static DeterministicConstructions.SafetyCoSafety	of(Factories factories, Formula formula, boolean complete, boolean deactivateSuspensionCheckOnInitialFormula)
static DeterministicConstructions.SafetyCoSafety	of(LabelledFormula formula)

Methods inherited from class owl.automaton.AbstractMemoizingAutomaton

acceptance, atomicPropositions, edge, edgeMap, edges, edges, edgeTree, explorationCompleted, factory, initialState, initialStates, memoizingAutomaton, states, successor, successors, successors

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

suspensionCheck

public final DeterministicConstructions.SuspensionCheck suspensionCheck

Method Detail

of

public static DeterministicConstructions.SafetyCoSafety of(LabelledFormula formula)

of

public static DeterministicConstructions.SafetyCoSafety of(Factories factories,
                                                           Formula formula)

of

public static DeterministicConstructions.SafetyCoSafety of(Factories factories,
                                                           Formula formula,
                                                           boolean complete,
                                                           boolean deactivateSuspensionCheckOnInitialFormula)

initialState

public DeterministicConstructions.BreakpointStateRejecting initialState(Formula formula)

edgeTreeImpl

public MtBdd<Edge<DeterministicConstructions.BreakpointStateRejecting>> edgeTreeImpl(DeterministicConstructions.BreakpointStateRejecting state)

Specified by:

edgeTreeImpl in class AbstractMemoizingAutomaton<DeterministicConstructions.BreakpointStateRejecting,BuchiAcceptance>

is

public boolean is(Automaton.Property property)

Specified by:

is in interface Automaton<S,A extends EmersonLeiAcceptance>

Overrides:

is in class AbstractMemoizingAutomaton<S,A extends EmersonLeiAcceptance>