Package owl.ltl
Interface EquivalenceClass
-
- All Superinterfaces:
LtlLanguageExpressible
public interface EquivalenceClass extends LtlLanguageExpressible
A propositional equivalence class of an LTL formula.
-
-
Method Summary
-
-
-
Method Detail
-
canonicalRepresentative
default Formula canonicalRepresentative()
The canonical representative for this equivalence class, which is defined as the formula representation of thedisjunctiveNormalForm()
.- Returns:
- The canonical representative.
-
factory
EquivalenceClassFactory factory()
-
isFalse
boolean isFalse()
-
isTrue
boolean isTrue()
-
atomicPropositions
default BitSet atomicPropositions()
-
atomicPropositions
BitSet atomicPropositions(boolean includeNested)
Collects all literals used in the bdd and stores the corresponding atomic propositions in the BitSet. See alsoFormula.atomicPropositions(boolean)
.
-
temporalOperators
Set<Formula.TemporalOperator> temporalOperators()
-
implies
boolean implies(EquivalenceClass other)
-
and
EquivalenceClass and(EquivalenceClass other)
-
or
EquivalenceClass or(EquivalenceClass other)
-
accept
default EquivalenceClass accept(Visitor<? extends Formula> visitor)
-
substitute
EquivalenceClass substitute(Function<? super Formula.TemporalOperator,? extends Formula> substitution)
- Parameters:
substitution
- The substitution function. It is only called on modal / temporal operators.
-
temporalStep
EquivalenceClass temporalStep(BitSet valuation)
- Parameters:
valuation
- The assignment for the atomic propositions.
-
temporalStepTree
default ValuationTree<EquivalenceClass> temporalStepTree()
-
temporalStepTree
<T> ValuationTree<T> temporalStepTree(Function<EquivalenceClass,Set<T>> mapper)
-
unfold
EquivalenceClass unfold()
SeeFormula.unfold()
.
-
trueness
double trueness()
-
language
default EquivalenceClass language()
- Specified by:
language
in interfaceLtlLanguageExpressible
-
-