All Superinterfaces:

LtlLanguageExpressible
```
public interface EquivalenceClass
extends LtlLanguageExpressible
```
A propositional equivalence class of an LTL formula.

Method Summary

All Methods Instance Methods Abstract Methods Default Methods
Modifier and Type	Method	Description
`EquivalenceClass`	`and(EquivalenceClass other)`
`default BitSet`	`atomicPropositions(boolean includeNested)`	Collects all literals used in the bdd and stores the corresponding atomic propositions in the BitSet.
`default Formula`	`canonicalRepresentativeCnf()`	The canonical representative for this equivalence class, which is defined as the formula representation of the `conjunctiveNormalForm()`.
`default Formula`	`canonicalRepresentativeDnf()`	The canonical representative for this equivalence class, which is defined as the formula representation of the `disjunctiveNormalForm()`.
`Set<Set<Formula>>`	`conjunctiveNormalForm()`
`Set<Set<Formula>>`	`disjunctiveNormalForm()`
`EquivalenceClass`	`encode(EquivalenceClassFactory.Encoding encoding)`
`EquivalenceClassFactory.Encoding`	`encoding()`
`EquivalenceClassFactory`	`factory()`
`boolean`	`implies(EquivalenceClass other)`
`boolean`	`isFalse()`
`boolean`	`isTrue()`
`default EquivalenceClass`	`language()`
`EquivalenceClass`	`not()`
`EquivalenceClass`	`or(EquivalenceClass other)`
`EquivalenceClass`	`substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)`	See `Formula.substitute(Function)`.
`List<Formula>`	`support(boolean includeNested)`	A sorted, distinct list of formula objects (`Literal` and `Formula.TemporalOperator`) that are used as propositions in the support of the backing BDD.
`default Set<Formula.TemporalOperator>`	`temporalOperators()`
`default Set<Formula.TemporalOperator>`	`temporalOperators(boolean includeNested)`
`default EquivalenceClass`	`temporalStep(BitSet valuation)`	See `Formula.temporalStep(BitSet)`.
`MtBdd<EquivalenceClass>`	`temporalStepTree()`
`double`	`trueness()`
`EquivalenceClass`	`unfold()`	See `Formula.unfold()`.

- Method Detail
  - atomicPropositions
```
default BitSet atomicPropositions(boolean includeNested)
```
    Collects all literals used in the bdd and stores the corresponding atomic propositions in the BitSet. See also Formula.atomicPropositions(boolean).
  - canonicalRepresentativeCnf
```
default Formula canonicalRepresentativeCnf()
```
    The canonical representative for this equivalence class, which is defined as the formula representation of the conjunctiveNormalForm().
    
    Returns:
    
    The canonical representative.
  - canonicalRepresentativeDnf
```
default Formula canonicalRepresentativeDnf()
```
    The canonical representative for this equivalence class, which is defined as the formula representation of the disjunctiveNormalForm().
    
    Returns:
    
    The canonical representative.
  - conjunctiveNormalForm
```
Set<Set<Formula>> conjunctiveNormalForm()
```
  - disjunctiveNormalForm
```
Set<Set<Formula>> disjunctiveNormalForm()
```
  - factory
```
EquivalenceClassFactory factory()
```
  - isFalse
```
boolean isFalse()
```
  - isTrue
```
boolean isTrue()
```
  - support
```
List<Formula> support(boolean includeNested)
```
    A sorted, distinct list of formula objects (Literal and Formula.TemporalOperator) that are used as propositions in the support of the backing BDD.
    
    Parameters:
    
    includeNested - include also nested subformulas.
    
    Returns:
    
    sorted, distinct, and unmodifiable list.
  - temporalOperators
```
default Set<Formula.TemporalOperator> temporalOperators()
```
  - temporalOperators
```
default Set<Formula.TemporalOperator> temporalOperators(boolean includeNested)
```
  - implies
```
boolean implies(EquivalenceClass other)
```
  - and
```
EquivalenceClass and(EquivalenceClass other)
```
  - or
```
EquivalenceClass or(EquivalenceClass other)
```
  - substitute
```
EquivalenceClass substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
```
    See Formula.substitute(Function).
    
    Parameters:
    
    substitution - The substitution function. It is only called on modal / temporal operators.
  - temporalStep
```
default EquivalenceClass temporalStep(BitSet valuation)
```
    See Formula.temporalStep(BitSet).
    
    Parameters:
    
    valuation - The assignment for the atomic propositions.
  - temporalStepTree
```
MtBdd<EquivalenceClass> temporalStepTree()
```
  - unfold
```
EquivalenceClass unfold()
```
    See Formula.unfold().
  - trueness
```
double trueness()
```
  - not
```
EquivalenceClass not()
```
  - encoding
```
EquivalenceClassFactory.Encoding encoding()
```
  - encode
```
EquivalenceClass encode(EquivalenceClassFactory.Encoding encoding)
```
  - language
```
default EquivalenceClass language()
```
    Specified by:
    
    language in interface LtlLanguageExpressible

Interface EquivalenceClass

Method Summary

Method Detail

atomicPropositions

canonicalRepresentativeCnf

canonicalRepresentativeDnf

conjunctiveNormalForm

disjunctiveNormalForm

factory

isFalse

isTrue

support

temporalOperators

temporalOperators

implies

and

or

substitute

temporalStep

temporalStepTree

unfold

trueness

not

encoding

encode

language