Package owl.ltl

Class Formula

java.lang.Object

owl.ltl.Formula

All Implemented Interfaces:

Comparable<Formula>

Direct Known Subclasses:

Formula.PropositionalOperator, Formula.TemporalOperator

public abstract class Formula
extends Object
implements Comparable<Formula>

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Formula.BinaryTemporalOperator
static class	Formula.NaryPropositionalOperator
static class	Formula.PropositionalOperator
static class	Formula.TemporalOperator
static class	Formula.UnaryTemporalOperator

Field Summary

Fields

Modifier and Type	Field	Description
List<Formula>	operands

Method Summary

Modifier and Type	Method	Description
abstract <R,P> R	accept(BinaryVisitor<P,R> visitor, P parameter)
abstract int	accept(IntVisitor visitor)
abstract <R> R	accept(Visitor<R> visitor)
boolean	allMatch(Predicate<Formula> predicate)
boolean	anyMatch(Predicate<Formula> predicate)
BitSet	atomicPropositions(boolean includeNested)
int	compareTo(Formula that)
protected int	compareValue(Formula o)
boolean	equals(Object o)
protected boolean	equalsValue(Formula o)
int	hashCode()
int	height()
abstract boolean	isPureEventual()
abstract boolean	isPureUniversal()
boolean	isSuspendable()
abstract Formula	nnf()
abstract Formula	not()	Syntactically negate this formula.
<E extends Formula> Set<E>	subformulas(Class<? extends E> clazz)
Set<Formula>	subformulas(Predicate<? super Formula> predicate)
<E extends Formula> Set<E>	subformulas(Predicate<? super Formula> predicate, Function<? super Formula,E> cast)
abstract Formula	substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
abstract Formula	temporalStep(BitSet valuation)	Do a single temporal step.
abstract Formula	unfold()

Methods inherited from class java.lang.Object

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

Field Detail

operands

public final List<Formula> operands

Method Detail

accept

public abstract int accept(IntVisitor visitor)

accept

public abstract <R> R accept(Visitor<R> visitor)

accept

public abstract <R,P> R accept(BinaryVisitor<P,R> visitor,
                                     P parameter)

atomicPropositions

public final BitSet atomicPropositions(boolean includeNested)

allMatch

public final boolean allMatch(Predicate<Formula> predicate)

anyMatch

public final boolean anyMatch(Predicate<Formula> predicate)

compareTo

public final int compareTo(Formula that)

Specified by:

compareTo in interface Comparable<Formula>

compareValue

protected int compareValue(Formula o)

equals

public final boolean equals(Object o)

Overrides:

equals in class Object

equalsValue

protected boolean equalsValue(Formula o)

hashCode

public final int hashCode()

Overrides:

hashCode in class Object

height

public final int height()

isPureEventual

public abstract boolean isPureEventual()

isPureUniversal

public abstract boolean isPureUniversal()

isSuspendable

public final boolean isSuspendable()

nnf

public abstract Formula nnf()

not

public abstract Formula not()

Syntactically negate this formula.

If this formula is in NNF, the returned negation will also be in NNF.

Returns:

the negation of this formula.

subformulas

public final <E extends Formula> Set<E> subformulas(Class<? extends E> clazz)

subformulas

public final Set<Formula> subformulas(Predicate<? super Formula> predicate)

subformulas

public final <E extends Formula> Set<E> subformulas(Predicate<? super Formula> predicate,
                                                    Function<? super Formula,E> cast)

substitute

public abstract Formula substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)

temporalStep

public abstract Formula temporalStep(BitSet valuation)

Do a single temporal step. This means that one layer of X-operators is removed and literals are replaced by their valuations.

unfold

public abstract Formula unfold()