Package owl.translations.mastertheorem

Class SymmetricEvaluatedFixpoints

java.lang.Object

owl.translations.mastertheorem.SymmetricEvaluatedFixpoints

All Implemented Interfaces:

Comparable<SymmetricEvaluatedFixpoints>, LtlLanguageExpressible

public final class SymmetricEvaluatedFixpoints
extends Object
implements Comparable<SymmetricEvaluatedFixpoints>, LtlLanguageExpressible

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	SymmetricEvaluatedFixpoints.DeterministicAutomata
static class	SymmetricEvaluatedFixpoints.NonDeterministicAutomata

Field Summary

Fields

Modifier and Type	Field	Description
Set<FOperator>	almostAlways	Corresponds to safetyAutomaton.
Fixpoints	fixpoints
Set<GOperator>	infinitelyOften	Corresponds to gfCoSafetyAutomaton.

Method Summary

Modifier and Type	Method	Description
static Set<SymmetricEvaluatedFixpoints>	build(Formula formula, Fixpoints fixpoints, Factories factories)
int	compareTo(SymmetricEvaluatedFixpoints that)
SymmetricEvaluatedFixpoints.DeterministicAutomata	deterministicAutomata(Factories factories, boolean generalized)
boolean	equals(Object o)
int	hashCode()
boolean	isEmpty()
boolean	isLiveness()
boolean	isSafety()
EquivalenceClass	language()
SymmetricEvaluatedFixpoints.NonDeterministicAutomata	nonDeterministicAutomata(Factories factories, boolean generalized)
String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

fixpoints

public final Fixpoints fixpoints

almostAlways

public final Set<FOperator> almostAlways

Corresponds to safetyAutomaton.

infinitelyOften

public final Set<GOperator> infinitelyOften

Corresponds to gfCoSafetyAutomaton.

Method Detail

build

public static Set<SymmetricEvaluatedFixpoints> build(Formula formula,
                                                     Fixpoints fixpoints,
                                                     Factories factories)

compareTo

public int compareTo(SymmetricEvaluatedFixpoints that)

Specified by:

compareTo in interface Comparable<SymmetricEvaluatedFixpoints>

equals

public boolean equals(Object o)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

isEmpty

public boolean isEmpty()

isSafety

public boolean isSafety()

isLiveness

public boolean isLiveness()

language

public EquivalenceClass language()

Specified by:

language in interface LtlLanguageExpressible

toString

public String toString()

Overrides:

toString in class Object

deterministicAutomata

public SymmetricEvaluatedFixpoints.DeterministicAutomata deterministicAutomata(Factories factories,
                                                                               boolean generalized)

nonDeterministicAutomata

public SymmetricEvaluatedFixpoints.NonDeterministicAutomata nonDeterministicAutomata(Factories factories,
                                                                                     boolean generalized)