Commit 30809215 authored by Salomon Sickert's avatar Salomon Sickert

Improve performance of BDD-based equivalence class and retain representative.

parent 01321303
......@@ -34,6 +34,10 @@ API:
* OmegaAcceptanceCast enables casting and conversion of different types of
omega-acceptance.
* EquivalenceClass always maintains the representative. This is made
possible by major performance improvements in the EquivalenceClass
implementation.
Bugfixes:
......
......@@ -3610,7 +3610,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......
......@@ -60,6 +60,11 @@ public interface EdgeTreeAutomatonMixin<S, A extends OmegaAcceptance> extends Au
return edgeTree(state).get(valuation);
}
@Override
default Set<S> successors(S state) {
return edgeTree(state).values(Edge::successor);
}
@Override
default List<PreferredEdgeAccess> preferredEdgeAccess() {
return ACCESS_MODES;
......
......@@ -24,6 +24,7 @@ import static owl.ltl.SyntacticFragment.SINGLE_STEP;
import com.google.common.primitives.ImmutableIntArray;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
......@@ -41,10 +42,9 @@ import owl.ltl.Conjunction;
import owl.ltl.Disjunction;
import owl.ltl.Formula;
import owl.ltl.GOperator;
import owl.ltl.PropositionalFormula;
import owl.ltl.Literal;
import owl.ltl.SyntacticFragment;
import owl.ltl.SyntacticFragments;
import owl.ltl.UnaryModalOperator;
import owl.ltl.XOperator;
import owl.ltl.rewriter.LiteralMapper;
import owl.ltl.rewriter.PullUpXVisitor;
......@@ -118,7 +118,7 @@ public final class DecomposedDPA {
private static boolean isSingleStep(Formula formula) {
if (formula instanceof Conjunction) {
return ((Conjunction) formula).children.stream().allMatch(DecomposedDPA::isSingleStep);
return formula.children().stream().allMatch(DecomposedDPA::isSingleStep);
}
return formula instanceof GOperator && SINGLE_STEP.contains(((GOperator) formula).operand);
......@@ -199,7 +199,8 @@ public final class DecomposedDPA {
return new LabelledTree.Leaf<>(newReference);
}
private List<LabelledTree<Tag, Reference>> createLeaves(PropositionalFormula formula) {
private List<LabelledTree<Tag, Reference>> createLeaves(
Formula.NaryPropositionalFormula formula) {
// Partition elements.
var safety = new Clusters();
var safetySingleStep = new HashMap<Integer, Clusters>();
......@@ -208,7 +209,7 @@ public final class DecomposedDPA {
var weakOrBuchiOrCoBuchi = new TreeSet<Formula>();
var parity = new TreeSet<Formula>();
for (Formula x : formula.children) {
for (Formula x : formula.children()) {
switch (annotatedTree.get(x)) {
case SAFETY:
PullUpXVisitor.XFormula rewrittenX = x.accept(PullUpXVisitor.INSTANCE);
......@@ -240,7 +241,7 @@ public final class DecomposedDPA {
// Process elements.
List<LabelledTree<Tag, Reference>> children = new ArrayList<>();
Function<Iterable<Formula>, Formula> merger = formula instanceof Conjunction
Function<Collection<Formula>, Formula> merger = formula instanceof Conjunction
? Conjunction::of
: Disjunction::of;
......@@ -274,12 +275,17 @@ public final class DecomposedDPA {
}
@Override
protected LabelledTree<Tag, Reference> visit(Formula.TemporalOperator formula) {
protected LabelledTree<Tag, Reference> visit(Formula.Temporal formula) {
return createLeaf(formula);
}
@Override
public LabelledTree<Tag, Reference> visit(Literal literal) {
return createLeaf(literal);
}
private boolean keepTreeStructureBiconditional(Formula formula) {
if (formula instanceof PropositionalFormula) {
if (formula instanceof Conjunction || formula instanceof Disjunction) {
if (formula.children().stream()
.filter(x -> annotatedTree.get(x) == Acceptance.PARITY).count() > 1) {
return false;
......@@ -290,11 +296,10 @@ public final class DecomposedDPA {
return formula.accept(new PropositionalVisitor<Boolean>() {
@Override
protected Boolean visit(Formula.TemporalOperator formula) {
protected Boolean visit(Formula.Temporal formula) {
return (SyntacticFragments.isAlmostAll(formula)
|| SyntacticFragments.isInfinitelyOften(formula))
&& SyntacticFragment.SINGLE_STEP
.contains(((UnaryModalOperator) ((UnaryModalOperator) formula).operand).operand);
&& SyntacticFragment.SINGLE_STEP.contains(formula.children().get(0).children().get(0));
}
@Override
......@@ -304,12 +309,12 @@ public final class DecomposedDPA {
@Override
public Boolean visit(Conjunction conjunction) {
return conjunction.children.stream().allMatch(this::apply);
return conjunction.children().stream().allMatch(this::apply);
}
@Override
public Boolean visit(Disjunction disjunction) {
return disjunction.children.stream().allMatch(this::apply);
return disjunction.children().stream().allMatch(this::apply);
}
});
}
......@@ -355,7 +360,7 @@ public final class DecomposedDPA {
static class Clusters {
private static final Predicate<Formula> INTERESTING_OPERATOR =
o -> o instanceof Formula.ModalOperator && !(o instanceof XOperator);
o -> o instanceof Formula.Temporal && !(o instanceof XOperator);
List<Set<Formula>> clusterList = new ArrayList<>();
......@@ -364,9 +369,11 @@ public final class DecomposedDPA {
cluster.add(formula);
clusterList.removeIf(x -> {
Set<Formula.TemporalOperator> modalOperators1 = formula.subformulas(INTERESTING_OPERATOR);
Set<Formula.TemporalOperator> modalOperators2 = x.stream()
.flatMap(y -> y.subformulas(INTERESTING_OPERATOR).stream()).collect(Collectors.toSet());
Set<Formula.Temporal> modalOperators1 = formula.subformulas(
INTERESTING_OPERATOR, Formula.Temporal.class::cast);
Set<Formula.Temporal> modalOperators2 = x.stream()
.flatMap(y -> y.subformulas(INTERESTING_OPERATOR, Formula.Temporal.class::cast).stream())
.collect(Collectors.toSet());
if (!Collections.disjoint(modalOperators1, modalOperators2)) {
cluster.addAll(x);
......@@ -384,7 +391,7 @@ public final class DecomposedDPA {
static final Annotator INSTANCE = new Annotator();
@Override
protected Map<Formula, Acceptance> visit(Formula.TemporalOperator formula) {
protected Map<Formula, Acceptance> visit(Formula.Temporal formula) {
if (SyntacticFragments.isSafety(formula)) {
return Map.of(formula, Acceptance.SAFETY);
}
......@@ -440,11 +447,16 @@ public final class DecomposedDPA {
return visitPropositional(disjunction);
}
private Map<Formula, Acceptance> visitPropositional(PropositionalFormula formula) {
@Override
public Map<Formula, Acceptance> visit(Literal literal) {
return Map.of(literal, Acceptance.WEAK);
}
private Map<Formula, Acceptance> visitPropositional(Formula.NaryPropositionalFormula formula) {
Acceptance acceptance = Acceptance.BOTTOM;
Map<Formula, Acceptance> acceptanceMap = new HashMap<>();
for (Formula child : formula.children) {
for (Formula child : formula.children()) {
Map<Formula, Acceptance> childDecisions = child.accept(this);
acceptanceMap.putAll(childDecisions);
acceptance = acceptance.lub(acceptanceMap.get(child));
......
......@@ -168,7 +168,7 @@ public final class DeterministicAutomaton<S, T> {
if (SyntacticFragments.isGCoSafety(unwrapped)) {
return new DeterministicAutomaton<>(
GenericConstructions.delay(
DeterministicConstructionsPortfolio.gCoSafety(ENV, LabelledFormula.of(unwrapped, formula.variables())),
DeterministicConstructionsPortfolio.gCoSafety(ENV, LabelledFormula.of(unwrapped, formula.atomicPropositions())),
xCount),
BUCHI, BuchiAcceptance.class,
x -> false,
......@@ -201,7 +201,7 @@ public final class DeterministicAutomaton<S, T> {
x -> x.inSet(0) ? 0.0d : 0.5d
);
}
if (SyntacticFragments.isCoSafetySafety(formula.formula())) {
return new DeterministicAutomaton<>(
DeterministicConstructionsPortfolio.coSafetySafety(ENV, formula),
......
......@@ -22,8 +22,10 @@ package owl.collections;
import com.google.common.collect.Maps;
import java.util.BitSet;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.IdentityHashMap;
import java.util.Map;
import java.util.Objects;
import java.util.Set;
......@@ -54,7 +56,15 @@ public abstract class ValuationTree<E> {
public abstract Set<E> get(BitSet valuation);
public abstract Set<E> values();
public final Set<E> values() {
return values(Function.identity());
}
public final <T> Set<T> values(Function<E, T> mapper) {
Set<T> values = new HashSet<>();
memoizedValues(values, Collections.newSetFromMap(new IdentityHashMap<>()), mapper);
return values;
}
public final Map<E, ValuationSet> inverse(ValuationSetFactory factory) {
return memoizedInverse(factory, new HashMap<>());
......@@ -73,6 +83,9 @@ public abstract class ValuationTree<E> {
ValuationSetFactory factory,
Map<ValuationTree<E>, Map<E, ValuationSet>> memoizedCalls);
protected abstract <T> void memoizedValues(
Set<T> values, Set<ValuationTree<E>> seenNodes, Function<E, T> mapper);
public static final class Leaf<E> extends ValuationTree<E> {
private static final ValuationTree<Object> EMPTY = new Leaf<>(Set.of());
......@@ -89,8 +102,11 @@ public abstract class ValuationTree<E> {
}
@Override
public Set<E> values() {
return new HashSet<>(value);
protected <T> void memoizedValues(Set<T> values,
Set<ValuationTree<E>> seenNodes, Function<E, T> mapper) {
for (E x : value) {
values.add(mapper.apply(x));
}
}
@Override
......@@ -153,10 +169,14 @@ public abstract class ValuationTree<E> {
}
@Override
public Set<E> values() {
Set<E> values = trueChild.values();
values.addAll(falseChild.values());
return values;
protected <T> void memoizedValues(Set<T> values, Set<ValuationTree<E>> seenNodes,
Function<E, T> mapper) {
if (!seenNodes.add(this)) {
return;
}
trueChild.memoizedValues(values, seenNodes, mapper);
falseChild.memoizedValues(values, seenNodes, mapper);
}
// Perfect for fork/join-parallesism
......
......@@ -19,14 +19,7 @@
package owl.factories;
import java.util.BitSet;
import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.function.Function;
import owl.collections.ValuationTree;
import owl.ltl.BooleanConstant;
import owl.ltl.EquivalenceClass;
import owl.ltl.Formula;
......@@ -35,62 +28,5 @@ import owl.ltl.Formula;
public interface EquivalenceClassFactory {
List<String> variables();
EquivalenceClass of(Formula formula);
default EquivalenceClass getFalse() {
return of(BooleanConstant.FALSE);
}
default EquivalenceClass getTrue() {
return of(BooleanConstant.TRUE);
}
/**
* Collects all literals used in the bdd and stores the corresponding atomic propositions in
* the BitSet.
*/
BitSet atomicPropositions(EquivalenceClass clazz, boolean includeNested);
/**
* Compute the support of the EquivalenceClass.
*
* @return All modal operators this equivalence class depends on.
*/
Set<Formula.ModalOperator> modalOperators(EquivalenceClass clazz);
boolean implies(EquivalenceClass clazz, EquivalenceClass other);
default EquivalenceClass conjunction(Collection<EquivalenceClass> classes) {
return conjunction(classes.iterator());
}
EquivalenceClass conjunction(Iterator<EquivalenceClass> classes);
default EquivalenceClass disjunction(Collection<EquivalenceClass> classes) {
return disjunction(classes.iterator());
}
EquivalenceClass disjunction(Iterator<EquivalenceClass> classes);
EquivalenceClass substitute(EquivalenceClass clazz,
Function<? super Formula.ModalOperator, ? extends Formula> substitution);
EquivalenceClass temporalStep(EquivalenceClass clazz, BitSet valuation);
EquivalenceClass temporalStepUnfold(EquivalenceClass clazz, BitSet valuation);
EquivalenceClass unfold(EquivalenceClass clazz);
EquivalenceClass unfoldTemporalStep(EquivalenceClass clazz, BitSet valuation);
String toString(EquivalenceClass clazz);
<T> ValuationTree<T> temporalStepTree(EquivalenceClass clazz,
Function<EquivalenceClass, Set<T>> mapper);
double trueness(EquivalenceClass clazz);
}
......@@ -26,14 +26,9 @@ public interface FactorySupplier {
EquivalenceClassFactory getEquivalenceClassFactory(List<String> alphabet);
EquivalenceClassFactory getEquivalenceClassFactory(List<String> alphabet,
boolean keepRepresentatives);
Factories getFactories(List<String> alphabet);
default Factories getFactories(List<String> alphabet, boolean keepRepresentatives) {
default Factories getFactories(List<String> alphabet) {
return new Factories(
getEquivalenceClassFactory(alphabet, keepRepresentatives),
getEquivalenceClassFactory(alphabet),
getValuationSetFactory(alphabet));
}
}
......@@ -29,17 +29,12 @@ import owl.factories.FactorySupplier;
import owl.factories.ValuationSetFactory;
public final class JBddSupplier implements FactorySupplier {
private static final JBddSupplier PLAIN = new JBddSupplier(false);
private static final JBddSupplier ANNOTATED = new JBddSupplier(true);
private static final JBddSupplier INSTANCE = new JBddSupplier();
private final boolean keepRepresentativesDefault;
private JBddSupplier() {}
private JBddSupplier(boolean keepRepresentativesDefault) {
this.keepRepresentativesDefault = keepRepresentativesDefault;
}
public static FactorySupplier async(boolean keepRepresentativesDefault) {
return keepRepresentativesDefault ? ANNOTATED : PLAIN;
public static FactorySupplier async() {
return INSTANCE;
}
private Bdd create(int size) {
......@@ -49,27 +44,23 @@ public final class JBddSupplier implements FactorySupplier {
.integrityDuplicatesMaximalSize(50)
.cacheBinaryDivider(4)
.cacheTernaryDivider(4)
.growthFactor(2)
.build();
// Do not use buildBddIterative, since 'support(...)' is broken.
return BddFactory.buildBddRecursive(size, configuration);
}
@Override
public EquivalenceClassFactory getEquivalenceClassFactory(List<String> alphabet) {
return getEquivalenceClassFactory(alphabet, keepRepresentativesDefault);
}
@Override
public EquivalenceClassFactory getEquivalenceClassFactory(List<String> alphabet,
boolean keepRepresentatives) {
Bdd eqFactoryBdd = create(1024 * (alphabet.size() + 1));
return new EquivalenceFactory(eqFactoryBdd, alphabet, keepRepresentatives);
return new EquivalenceFactory(eqFactoryBdd, alphabet);
}
@Override
public Factories getFactories(List<String> alphabet) {
return new Factories(
getEquivalenceClassFactory(alphabet, keepRepresentativesDefault),
getEquivalenceClassFactory(alphabet),
getValuationSetFactory(alphabet));
}
......
......@@ -19,8 +19,9 @@
package owl.ltl;
import java.util.BitSet;
import java.util.List;
import java.util.Objects;
import java.util.Set;
import java.util.function.Function;
import owl.ltl.visitors.BinaryVisitor;
import owl.ltl.visitors.IntVisitor;
......@@ -29,12 +30,14 @@ import owl.ltl.visitors.Visitor;
/**
* Biconditional.
*/
public final class Biconditional extends Formula.LogicalOperator {
public final class Biconditional extends Formula.Propositional {
public final Formula left;
public final Formula right;
public Biconditional(Formula leftOperand, Formula rightOperand) {
super(Objects.hash(Biconditional.class, leftOperand, rightOperand));
super(
Objects.hash(Biconditional.class, leftOperand, rightOperand),
Formulas.height(leftOperand, rightOperand) + 1);
this.left = leftOperand;
this.right = rightOperand;
}
......@@ -94,8 +97,8 @@ public final class Biconditional extends Formula.LogicalOperator {
}
@Override
public Set<Formula> children() {
return Set.of(left, right);
public List<Formula> children() {
return List.of(left, right);
}
@Override
......@@ -124,25 +127,17 @@ public final class Biconditional extends Formula.LogicalOperator {
}
@Override
public Formula substitute(Function<? super TemporalOperator, ? extends Formula> substitution) {
public Formula substitute(Function<? super Temporal, ? extends Formula> substitution) {
return Biconditional.of(left.substitute(substitution), right.substitute(substitution));
}
@Override
public String toString() {
return "(" + left + " <-> " + right + ')';
public Formula temporalStep(BitSet valuation) {
return Biconditional.of(left.temporalStep(valuation), right.temporalStep(valuation));
}
@Override
protected int compareToImpl(Formula o) {
Biconditional that = (Biconditional) o;
int comparison = left.compareTo(that.left);
return comparison == 0 ? right.compareTo(that.right) : comparison;
}
@Override
protected boolean equalsImpl(Formula o) {
Biconditional that = (Biconditional) o;
return left.equals(that.left) && right.equals(that.right);
public String toString() {
return "(" + left + " <-> " + right + ')';
}
}
/*
* Copyright (C) 2016 - 2019 (See AUTHORS)
*
* This file is part of Owl.
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package owl.ltl;
import java.util.Objects;
import java.util.Set;
public abstract class BinaryModalOperator extends Formula.ModalOperator {
public final Formula left;
public final Formula right;
BinaryModalOperator(Class<? extends BinaryModalOperator> clazz, Formula leftOperand,
Formula rightOperand) {
super(Objects.hash(clazz, leftOperand, rightOperand));
this.left = leftOperand;
this.right = rightOperand;
}
@Override
public Set<Formula> children() {
return Set.of(left, right);
}
@Override
public final boolean isPureEventual() {
return false;
}
@Override
public final boolean isPureUniversal() {
return false;
}
public abstract String operatorSymbol();
@Override
public final String toString() {
return String.format("(%s%s%s)", left, operatorSymbol(), right);
}
@Override
protected final int compareToImpl(Formula o) {
assert this.getClass() == o.getClass();
BinaryModalOperator that = (BinaryModalOperator) o;
int comparison = left.compareTo(that.left);
return comparison == 0 ? right.compareTo(that.right) : comparison;
}
@Override
protected final boolean equalsImpl(Formula o) {
assert this.getClass() == o.getClass();
BinaryModalOperator that = (BinaryModalOperator) o;
return left.equals(that.left) && right.equals(that.right);
}
}
......@@ -19,7 +19,8 @@
package owl.ltl;
import java.util.Set;
import java.util.BitSet;
import java.util.List;
import java.util.function.Function;
import javax.annotation.Nonnull;
import owl.ltl.visitors.BinaryVisitor;
......@@ -27,13 +28,13 @@ import owl.ltl.visitors.IntVisitor;
import owl.ltl.visitors.Visitor;
import owl.util.annotation.CEntryPoint;
public final class BooleanConstant extends Formula.LogicalOperator {
public final class BooleanConstant extends Formula.Propositional {
public static final BooleanConstant FALSE = new BooleanConstant(false);
public static final BooleanConstant TRUE = new BooleanConstant(true);
public final boolean value;
private BooleanConstant(boolean value) {
super(Boolean.hashCode(value));
super(Boolean.hashCode(value), 0);
this.value = value;
}
......@@ -58,8 +59,8 @@ public final class BooleanConstant extends Formula.LogicalOperator {
}
@Override
public Set<Formula> children() {
return Set.of();
public List<Formula> children() {
return List.of();
}
@Override
......@@ -84,7 +85,12 @@ public final class BooleanConstant extends Formula.LogicalOperator {
}
@Override
public Formula substitute(Function<? super TemporalOperator, ? extends Formula> substitution) {
public Formula temporalStep(BitSet valuation) {
return this;
}
@Override
public Formula substitute(Function<? super Temporal, ? extends Formula> substitution) {
return this;
}
......@@ -94,13 +100,13 @@ public final class BooleanConstant extends Formula.LogicalOperator {
}
@Override
protected int compareToImpl(Formula o) {
protected int compareValue(Formula o) {
BooleanConstant that = (BooleanConstant) o;
return Boolean.compare(value, that.value);
}
@Override
protected boolean equalsImpl(Formula o) {
protected boolean equalsValue(Formula o) {
assert o instanceof BooleanConstant;
assert this.value != ((BooleanConstant) o).value;
return false;
......