Package owl.bdd

Interface EquivalenceClassFactory

public interface EquivalenceClassFactory

A factory for creating propositional equivalence classes for LTL formulas.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static class	EquivalenceClassFactory.Encoding

Method Summary

Modifier and Type	Method	Description
EquivalenceClass	and(Collection<? extends EquivalenceClass> classes)
List<String>	atomicPropositions()	The atomic propositions associated with this factory.
void	clearCaches()
EquivalenceClassFactory.Encoding	defaultEncoding()
default EquivalenceClass	of(boolean value)
EquivalenceClass	of(Formula formula)	Create or retrieve a (propositional) equivalence class for a LTL formula.
EquivalenceClass	or(Collection<? extends EquivalenceClass> classes)
EquivalenceClassFactory	withDefaultEncoding(EquivalenceClassFactory.Encoding encoding)

Method Detail

atomicPropositions

List<String> atomicPropositions()

The atomic propositions associated with this factory.

Returns:

the list of atomic propositions for all formulas.

of

EquivalenceClass of(Formula formula)

Create or retrieve a (propositional) equivalence class for a LTL formula.

Parameters:

formula - The LTL formula. It is expected to be negation normal form.

Returns:

the corresponding equivalence class.

of

default EquivalenceClass of(boolean value)

and

EquivalenceClass and(Collection<? extends EquivalenceClass> classes)

or

EquivalenceClass or(Collection<? extends EquivalenceClass> classes)

defaultEncoding

EquivalenceClassFactory.Encoding defaultEncoding()

withDefaultEncoding

EquivalenceClassFactory withDefaultEncoding(EquivalenceClassFactory.Encoding encoding)

clearCaches

void clearCaches()