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

CHANGELOG.md

@@ -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:
 

data/formulas/sizes/ltl2na.json

@@ -3610,7 +3610,7 @@
   {
     "formula": "G(a | ((!a) U (Xa)))",
     "properties": {
-      "size": 7,
+      "size": 8,
       "initialStatesSize": 1,
       "acceptanceName": "BuchiAcceptance",
       "acceptanceSets": 1,

data/formulas/sizes/nba.symmetric.json

@@ -3951,7 +3951,7 @@
   {
     "formula": "G(a | ((!a) U (Xa)))",
     "properties": {
-      "size": 7,
+      "size": 8,
       "initialStatesSize": 1,
       "acceptanceName": "BuchiAcceptance",
       "acceptanceSets": 1,

data/formulas/sizes/nba.symmetric.portfolio.json

@@ -3951,7 +3951,7 @@
   {
     "formula": "G(a | ((!a) U (Xa)))",
     "properties": {
-      "size": 7,
+      "size": 8,
       "initialStatesSize": 1,
       "acceptanceName": "BuchiAcceptance",
       "acceptanceSets": 1,

data/formulas/sizes/ngba.symmetric.json

@@ -3951,7 +3951,7 @@
   {
     "formula": "G(a | ((!a) U (Xa)))",
     "properties": {
-      "size": 7,
+      "size": 8,
       "initialStatesSize": 1,
       "acceptanceName": "BuchiAcceptance",
       "acceptanceSets": 1,

data/formulas/sizes/ngba.symmetric.portfolio.json

@@ -3951,7 +3951,7 @@
   {
     "formula": "G(a | ((!a) U (Xa)))",
     "properties": {
-      "size": 7,
+      "size": 8,
       "initialStatesSize": 1,
       "acceptanceName": "BuchiAcceptance",
       "acceptanceSets": 1,

src/main/java/owl/automaton/EdgeTreeAutomatonMixin.java

@@ -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;

src/main/java/owl/cinterface/DecomposedDPA.java

@@ -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,15 @@ 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
+        public Boolean visit(Literal literal) {
+          return false;
         }
 
         @Override
@@ -304,12 +314,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 +365,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 +374,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 +396,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 +452,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));

src/main/java/owl/cinterface/DeterministicAutomaton.java

@@ -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),

src/main/java/owl/collections/ValuationTree.java

@@ -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

src/main/java/owl/factories/EquivalenceClassFactory.java

@@ -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);
 }

src/main/java/owl/factories/FactorySupplier.java

@@ -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));
   }
 }

src/main/java/owl/factories/jbdd/JBddSupplier.java

@@ -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));
   }
 

src/main/java/owl/ltl/Biconditional.java

@@ -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 + ')';
   }
 }

src/main/java/owl/ltl/BinaryModalOperator.java

-/*
- * 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);
-  }
-}

src/main/java/owl/ltl/BooleanConstant.java

@@ -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