diff --git a/CHANGELOG.md b/CHANGELOG.md index 848953e38a63fbe0ba107c2e6b01a0594cd1eeae..1fd0ae7273f5a8bca4ca4fca46d692c4bba86d7a 100644 --- a/CHANGELOG.md +++ b/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: diff --git a/data/formulas/sizes/ltl2na.json b/data/formulas/sizes/ltl2na.json index b67098ae9fc97bc5b10913a9bd52957cecf86e66..230ff416560691323007f20f9a8d836f065947a0 100644 --- a/data/formulas/sizes/ltl2na.json +++ b/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, diff --git a/data/formulas/sizes/nba.symmetric.json b/data/formulas/sizes/nba.symmetric.json index a358c3d97c6c8b69c349881532770878e69dfc84..c5176d26e7a878209327db95e0e761b2c41ab46d 100644 --- a/data/formulas/sizes/nba.symmetric.json +++ b/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, diff --git a/data/formulas/sizes/nba.symmetric.portfolio.json b/data/formulas/sizes/nba.symmetric.portfolio.json index c900c61f6a7ec67ff40e29469eb703cf0db2f7db..3bdb3f00b9402556bb64f406fb71057787253a20 100644 --- a/data/formulas/sizes/nba.symmetric.portfolio.json +++ b/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, diff --git a/data/formulas/sizes/ngba.symmetric.json b/data/formulas/sizes/ngba.symmetric.json index 9972e22d8dce2c0866fd1b57a247d5708e0faa03..b82c0fdcb82d70da4f5d85f37ca56666cb7953c9 100644 --- a/data/formulas/sizes/ngba.symmetric.json +++ b/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, diff --git a/data/formulas/sizes/ngba.symmetric.portfolio.json b/data/formulas/sizes/ngba.symmetric.portfolio.json index 2fb6d8bbdc892220c5d2f9c3b21794ac38ed7183..0ef3c24ee6bbf9b6810ff8c2cc585e9e3ed08fe7 100644 --- a/data/formulas/sizes/ngba.symmetric.portfolio.json +++ b/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, diff --git a/src/main/java/owl/automaton/EdgeTreeAutomatonMixin.java b/src/main/java/owl/automaton/EdgeTreeAutomatonMixin.java index 9648261deed9613834778263f6e20911d4e67d47..fa7960d5d15ec336c2e44f33ce055b6388060255 100644 --- a/src/main/java/owl/automaton/EdgeTreeAutomatonMixin.java +++ b/src/main/java/owl/automaton/EdgeTreeAutomatonMixin.java @@ -60,6 +60,11 @@ public interface EdgeTreeAutomatonMixin extends Au return edgeTree(state).get(valuation); } + @Override + default Set successors(S state) { + return edgeTree(state).values(Edge::successor); + } + @Override default List preferredEdgeAccess() { return ACCESS_MODES; diff --git a/src/main/java/owl/cinterface/DecomposedDPA.java b/src/main/java/owl/cinterface/DecomposedDPA.java index c9c1d2727d74a19cacf5685e51df11707e17642e..40ec4b624ca16ea1e3fc7990ccbde4bfeab73090 100644 --- a/src/main/java/owl/cinterface/DecomposedDPA.java +++ b/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> createLeaves(PropositionalFormula formula) { + private List> createLeaves( + Formula.NaryPropositionalFormula formula) { // Partition elements. var safety = new Clusters(); var safetySingleStep = new HashMap(); @@ -208,7 +209,7 @@ public final class DecomposedDPA { var weakOrBuchiOrCoBuchi = new TreeSet(); var parity = new TreeSet(); - 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> children = new ArrayList<>(); - Function, Formula> merger = formula instanceof Conjunction + Function, Formula> merger = formula instanceof Conjunction ? Conjunction::of : Disjunction::of; @@ -274,12 +275,17 @@ public final class DecomposedDPA { } @Override - protected LabelledTree visit(Formula.TemporalOperator formula) { + protected LabelledTree visit(Formula.Temporal formula) { return createLeaf(formula); } + @Override + public LabelledTree 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() { @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 INTERESTING_OPERATOR = - o -> o instanceof Formula.ModalOperator && !(o instanceof XOperator); + o -> o instanceof Formula.Temporal && !(o instanceof XOperator); List> clusterList = new ArrayList<>(); @@ -364,9 +369,11 @@ public final class DecomposedDPA { cluster.add(formula); clusterList.removeIf(x -> { - Set modalOperators1 = formula.subformulas(INTERESTING_OPERATOR); - Set modalOperators2 = x.stream() - .flatMap(y -> y.subformulas(INTERESTING_OPERATOR).stream()).collect(Collectors.toSet()); + Set modalOperators1 = formula.subformulas( + INTERESTING_OPERATOR, Formula.Temporal.class::cast); + Set 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 visit(Formula.TemporalOperator formula) { + protected Map 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 visitPropositional(PropositionalFormula formula) { + @Override + public Map visit(Literal literal) { + return Map.of(literal, Acceptance.WEAK); + } + + private Map visitPropositional(Formula.NaryPropositionalFormula formula) { Acceptance acceptance = Acceptance.BOTTOM; Map acceptanceMap = new HashMap<>(); - for (Formula child : formula.children) { + for (Formula child : formula.children()) { Map childDecisions = child.accept(this); acceptanceMap.putAll(childDecisions); acceptance = acceptance.lub(acceptanceMap.get(child)); diff --git a/src/main/java/owl/cinterface/DeterministicAutomaton.java b/src/main/java/owl/cinterface/DeterministicAutomaton.java index d37b16d24ef72712520310af175a1a0ce5194ff3..50e3287df077704c8a7f7b322599d8f2f93a400e 100644 --- a/src/main/java/owl/cinterface/DeterministicAutomaton.java +++ b/src/main/java/owl/cinterface/DeterministicAutomaton.java @@ -168,7 +168,7 @@ public final class DeterministicAutomaton { 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 { x -> x.inSet(0) ? 0.0d : 0.5d ); } - + if (SyntacticFragments.isCoSafetySafety(formula.formula())) { return new DeterministicAutomaton<>( DeterministicConstructionsPortfolio.coSafetySafety(ENV, formula), diff --git a/src/main/java/owl/collections/ValuationTree.java b/src/main/java/owl/collections/ValuationTree.java index addbe36d7ed472a91cfb552f9f53fe8d742be3ba..539f7f0aad8e57b5e60d2b8a2f1b2a38883a60f9 100644 --- a/src/main/java/owl/collections/ValuationTree.java +++ b/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 { public abstract Set get(BitSet valuation); - public abstract Set values(); + public final Set values() { + return values(Function.identity()); + } + + public final Set values(Function mapper) { + Set values = new HashSet<>(); + memoizedValues(values, Collections.newSetFromMap(new IdentityHashMap<>()), mapper); + return values; + } public final Map inverse(ValuationSetFactory factory) { return memoizedInverse(factory, new HashMap<>()); @@ -73,6 +83,9 @@ public abstract class ValuationTree { ValuationSetFactory factory, Map, Map> memoizedCalls); + protected abstract void memoizedValues( + Set values, Set> seenNodes, Function mapper); + public static final class Leaf extends ValuationTree { private static final ValuationTree EMPTY = new Leaf<>(Set.of()); @@ -89,8 +102,11 @@ public abstract class ValuationTree { } @Override - public Set values() { - return new HashSet<>(value); + protected void memoizedValues(Set values, + Set> seenNodes, Function mapper) { + for (E x : value) { + values.add(mapper.apply(x)); + } } @Override @@ -153,10 +169,14 @@ public abstract class ValuationTree { } @Override - public Set values() { - Set values = trueChild.values(); - values.addAll(falseChild.values()); - return values; + protected void memoizedValues(Set values, Set> seenNodes, + Function mapper) { + if (!seenNodes.add(this)) { + return; + } + + trueChild.memoizedValues(values, seenNodes, mapper); + falseChild.memoizedValues(values, seenNodes, mapper); } // Perfect for fork/join-parallesism diff --git a/src/main/java/owl/factories/EquivalenceClassFactory.java b/src/main/java/owl/factories/EquivalenceClassFactory.java index 50bc6bc9fbd0e48affa47186d35fd5a87561ee4b..30ebb511749bfe776a4cad6c7e6a17d88933f314 100644 --- a/src/main/java/owl/factories/EquivalenceClassFactory.java +++ b/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 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 modalOperators(EquivalenceClass clazz); - - boolean implies(EquivalenceClass clazz, EquivalenceClass other); - - default EquivalenceClass conjunction(Collection classes) { - return conjunction(classes.iterator()); - } - - EquivalenceClass conjunction(Iterator classes); - - default EquivalenceClass disjunction(Collection classes) { - return disjunction(classes.iterator()); - } - - EquivalenceClass disjunction(Iterator classes); - - - EquivalenceClass substitute(EquivalenceClass clazz, - Function 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); - - ValuationTree temporalStepTree(EquivalenceClass clazz, - Function> mapper); - - double trueness(EquivalenceClass clazz); } diff --git a/src/main/java/owl/factories/FactorySupplier.java b/src/main/java/owl/factories/FactorySupplier.java index 0d0632d8fb5e23e8e348cea949adb4b93fd190df..5a55fb6ff63a7dd02b53078caaeeebc6c8951d77 100644 --- a/src/main/java/owl/factories/FactorySupplier.java +++ b/src/main/java/owl/factories/FactorySupplier.java @@ -26,14 +26,9 @@ public interface FactorySupplier { EquivalenceClassFactory getEquivalenceClassFactory(List alphabet); - EquivalenceClassFactory getEquivalenceClassFactory(List alphabet, - boolean keepRepresentatives); - - Factories getFactories(List alphabet); - - default Factories getFactories(List alphabet, boolean keepRepresentatives) { + default Factories getFactories(List alphabet) { return new Factories( - getEquivalenceClassFactory(alphabet, keepRepresentatives), + getEquivalenceClassFactory(alphabet), getValuationSetFactory(alphabet)); } } diff --git a/src/main/java/owl/factories/jbdd/EquivalenceFactory.java b/src/main/java/owl/factories/jbdd/EquivalenceFactory.java index ae5d5065a7b74da91bffdba4f14b409b46d495fd..58695d8da50969c7874fef4f53703a8ad1bc91f5 100644 --- a/src/main/java/owl/factories/jbdd/EquivalenceFactory.java +++ b/src/main/java/owl/factories/jbdd/EquivalenceFactory.java @@ -19,28 +19,21 @@ package owl.factories.jbdd; +import com.google.common.collect.Lists; import de.tum.in.jbdd.Bdd; import it.unimi.dsi.fastutil.HashCommon; import it.unimi.dsi.fastutil.objects.Object2IntMap; import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap; import java.math.BigDecimal; import java.math.RoundingMode; -import java.util.AbstractSet; -import java.util.ArrayList; import java.util.Arrays; import java.util.BitSet; -import java.util.Collection; -import java.util.ConcurrentModificationException; -import java.util.HashMap; -import java.util.Iterator; +import java.util.IdentityHashMap; import java.util.List; -import java.util.Map; +import java.util.Objects; import java.util.Set; import java.util.function.Function; -import java.util.function.IntUnaryOperator; -import java.util.function.UnaryOperator; import java.util.stream.Collectors; -import java.util.stream.Stream; import javax.annotation.Nullable; import owl.collections.ValuationTree; import owl.factories.EquivalenceClassFactory; @@ -50,498 +43,362 @@ import owl.ltl.Disjunction; import owl.ltl.EquivalenceClass; import owl.ltl.Formula; import owl.ltl.Literal; -import owl.ltl.XOperator; import owl.ltl.visitors.PrintVisitor; import owl.ltl.visitors.PropositionalIntVisitor; final class EquivalenceFactory extends GcManagedFactory implements EquivalenceClassFactory { - private final List alphabet; - private final boolean keepRepresentatives; - private final BddVisitor visitor; + private final List atomicPropositions; + private final BddEquivalenceClass falseClass; private final BddEquivalenceClass trueClass; + private final BddVisitor visitor; - private Formula.TemporalOperator[] reverseMapping; - private final Object2IntMap mapping; - - // Compose maps. - private int[] temporalStepSubstitution; - private int[] unfoldSubstitution; - - // Protect objects from the GC. - private EquivalenceClass[] temporalStepSubstitutes; - private EquivalenceClass[] unfoldSubstitutes; + private Formula.Temporal[] reverseMapping; + private final Object2IntMap mapping; - private boolean registerActive = false; + @Nullable + private Function> temporalStepTreeCachedMapper; + @Nullable + private IdentityHashMap> temporalStepTreeCache; - public EquivalenceFactory(Bdd bdd, List alphabet, boolean keepRepresentatives) { + public EquivalenceFactory(Bdd bdd, List atomicPropositions) { super(bdd); - this.alphabet = List.copyOf(alphabet); - this.keepRepresentatives = keepRepresentatives; + this.atomicPropositions = List.copyOf(atomicPropositions); - int alphabetSize = this.alphabet.size(); + int alphabetSize = this.atomicPropositions.size(); mapping = new Object2IntOpenHashMap<>(); mapping.defaultReturnValue(-1); - reverseMapping = new Formula.TemporalOperator[alphabetSize]; + reverseMapping = new Formula.Temporal[alphabetSize]; visitor = new BddVisitor(); - unfoldSubstitution = new int[alphabetSize]; - unfoldSubstitutes = new EquivalenceClass[alphabetSize]; - temporalStepSubstitution = new int[alphabetSize]; - temporalStepSubstitutes = new EquivalenceClass[alphabetSize]; - // Register literals. for (int i = 0; i < alphabetSize; i++) { - Literal literal = Literal.of(i); int node = this.bdd.createVariable(); assert this.bdd.variable(node) == i; - mapping.put(literal, i); - reverseMapping[i] = literal; } - // Literals are not unfolded. - Arrays.fill(unfoldSubstitution, -1); - trueClass = new BddEquivalenceClass(this, this.bdd.trueNode(), BooleanConstant.TRUE); falseClass = new BddEquivalenceClass(this, this.bdd.falseNode(), BooleanConstant.FALSE); } @Override public List variables() { - return alphabet; + return atomicPropositions; } @Override public EquivalenceClass of(Formula formula) { - return create(formula, toBdd(formula)); - } - - @Override - public EquivalenceClass getFalse() { - return falseClass; + return of(formula, true); } - @Override - public EquivalenceClass getTrue() { - return trueClass; - } - - - @Override - public BitSet atomicPropositions(EquivalenceClass clazz, boolean includeNested) { - if (!includeNested) { - return bdd.support(getNode(clazz), alphabet.size()); + private BddEquivalenceClass of(Formula formula, boolean scanForUnknown) { + if (scanForUnknown) { + // Scan for unknown modal operators. + var newPropositions = formula.subformulas(Formula.Temporal.class) + .stream().filter(x -> !mapping.containsKey(x)).sorted().collect(Collectors.toList()); + + if (!newPropositions.isEmpty()) { + // Create variables. + int literalOffset = atomicPropositions.size(); + int newSize = mapping.size() + newPropositions.size(); + reverseMapping = Arrays.copyOf(reverseMapping, newSize); + + for (Formula.Temporal proposition : newPropositions) { + int variable = bdd.variable(bdd.createVariable()); + mapping.put(proposition, variable); + reverseMapping[variable - literalOffset] = proposition; + } + } } - BitSet atomicPropositions = bdd.support(getNode(clazz)); + return of(formula, bdd.dereference(formula.accept(visitor))); + } - int i = atomicPropositions.nextSetBit(alphabet.size()); - for (; i >= 0; i = atomicPropositions.nextSetBit(i + 1)) { - atomicPropositions.or(reverseMapping[i].atomicPropositions(true)); + private BddEquivalenceClass of(@Nullable Formula representative, int node) { + if (node == bdd.trueNode()) { + return trueClass; } - if (atomicPropositions.length() >= alphabet.size()) { - atomicPropositions.clear(alphabet.size(), atomicPropositions.length()); + if (node == bdd.falseNode()) { + return falseClass; } - return atomicPropositions; - } + var clazz = canonicalize(new BddEquivalenceClass(this, node, representative)); - @Override - public Set modalOperators(EquivalenceClass clazz) { - BitSet support = bdd.support(getNode(clazz)); - support.clear(0, alphabet.size()); - - return new AbstractSet<>() { - @Override - public boolean contains(Object o) { - int i = mapping.getInt(o); - return i != -1 && support.get(i); - } - - @Override - public Stream stream() { - return support.stream().mapToObj(i -> (Formula.ModalOperator) reverseMapping[i]); - } - - @Override - public Iterator iterator() { - return stream().iterator(); - } - - @Override - public int size() { - return support.cardinality(); - } - }; - } - - @Override - public boolean implies(EquivalenceClass clazz, EquivalenceClass other) { - return bdd.implies(getNode(clazz), getNode(other)); - } - - @Override - public EquivalenceClass conjunction(Iterator classes) { - int resultBdd = bdd.trueNode(); - @Nullable - List representatives = new ArrayList<>(); - - while (classes.hasNext()) { - EquivalenceClass next = classes.next(); - Formula representative = next.representative(); - if (representative == null || representatives == null) { - representatives = null; - } else { - representatives.add(representative); - } - resultBdd = bdd.and(resultBdd, getNode(next)); + if (clazz.representative == null) { + clazz.representative = representative; } - return create(representatives == null ? null : Conjunction.of(representatives), resultBdd); + return clazz; } - @Override - public EquivalenceClass disjunction(Iterator classes) { - int resultBdd = bdd.falseNode(); - @Nullable - List representatives = new ArrayList<>(); + // Translates a formula into a BDD under the assumption every subformula is already registered. + private final class BddVisitor extends PropositionalIntVisitor { + @Override + public int visit(Literal literal) { + assert literal.getAtom() < atomicPropositions.size(); + int node = bdd.variableNode(literal.getAtom()); + return literal.isNegated() ? bdd.not(node) : node; + } - while (classes.hasNext()) { - EquivalenceClass next = classes.next(); - Formula representative = next.representative(); - if (representative == null || representatives == null) { - representatives = null; - } else { - representatives.add(representative); - } - resultBdd = bdd.or(resultBdd, getNode(next)); + @Override + protected int visit(Formula.Temporal formula) { + int variable = mapping.getInt(formula); + assert variable >= 0; + return bdd.variableNode(variable); } - return create(representatives == null ? null : Disjunction.of(representatives), resultBdd); - } + @Override + public int visit(BooleanConstant booleanConstant) { + return booleanConstant.value ? bdd.trueNode() : bdd.falseNode(); + } - @Override - public EquivalenceClass substitute(EquivalenceClass clazz, - Function substitution) { - BitSet support = bdd.support(getNode(clazz)); + @Override + public int visit(Conjunction conjunction) { + int x = bdd.trueNode(); - Function guardedSubstitution = x -> { - if (x instanceof Formula.ModalOperator) { - return substitution.apply((Formula.ModalOperator) x); - } else { - return x; + // Reverse list for better performance! + for (Formula child : Lists.reverse(conjunction.children())) { + int y = child.accept(this); + x = bdd.consume(bdd.and(x, y), x, y); } - }; - - int[] substitutionMap = new int[reverseMapping.length]; - Arrays.setAll(substitutionMap, - i -> support.get(i) ? toBdd(guardedSubstitution.apply(reverseMapping[i])) : -1); - - return transform(clazz, node -> bdd.compose(node, substitutionMap), - f -> f.substitute(guardedSubstitution)); - } + return x; + } - @Override - public EquivalenceClass temporalStep(EquivalenceClass clazz, BitSet valuation) { - return transform(clazz, bdd -> temporalStepBdd(bdd, valuation), f -> f.temporalStep(valuation)); - } + @Override + public int visit(Disjunction disjunction) { + int x = bdd.falseNode(); - @Override - public EquivalenceClass temporalStepUnfold(EquivalenceClass clazz, BitSet valuation) { - return transform(clazz, bdd -> unfold(temporalStepBdd(bdd, valuation)), - f -> f.temporalStepUnfold(valuation)); - } + // Reverse list for better performance! + for (Formula child : Lists.reverse(disjunction.children())) { + int y = child.accept(this); + x = bdd.consume(bdd.or(x, y), x, y); + } - private int temporalStepBdd(int node, BitSet valuation) { - // Adjust valuation literals in substitution. This is not thread-safe! - for (int i = 0; i < alphabet.size(); i++) { - temporalStepSubstitution[i] = valuation.get(i) ? bdd.trueNode() : bdd.falseNode(); + return x; } - - return bdd.compose(node, temporalStepSubstitution); - } - - @Override - public EquivalenceClass unfold(EquivalenceClass clazz) { - return transform(clazz, this::unfold, Formula::unfold); } - @Override - public EquivalenceClass unfoldTemporalStep(EquivalenceClass clazz, BitSet valuation) { - return transform(clazz, bdd -> temporalStepBdd(unfold(bdd), valuation), - f -> f.unfoldTemporalStep(valuation)); + private BddEquivalenceClass cast(EquivalenceClass clazz) { + var castedClazz = (BddEquivalenceClass) clazz; + assert equals(castedClazz.factory); + return castedClazz; } - private int unfold(int node) { - return bdd.compose(node, unfoldSubstitution); - } + static final class BddEquivalenceClass implements BddNode, EquivalenceClass { + private final EquivalenceFactory factory; + private final int node; + @Nullable + private Formula representative; - @Override - public String toString(EquivalenceClass clazz) { - int node = getNode(clazz); + @Nullable + private Set modalOperatorsCache = null; + @Nullable + private EquivalenceClass unfoldCache = null; - if (bdd.isVariable(node)) { - return PrintVisitor.toString(reverseMapping[bdd.variable(node)], alphabet, false); + private BddEquivalenceClass(EquivalenceFactory factory, int node, + @Nullable Formula representative) { + this.factory = factory; + this.node = node; + this.representative = representative; } - if (bdd.isVariableNegated(node)) { - return PrintVisitor.toString(reverseMapping[bdd.variable(node)].not(), - alphabet, false); + @Override + public Formula representative() { + return Objects.requireNonNull(representative); } - Formula representative = clazz.representative(); - return representative == null - ? String.format("%d", node) - : PrintVisitor.toString(representative, alphabet, false); - } - - @Override - public ValuationTree temporalStepTree(EquivalenceClass clazz, - Function> mapper) { - return temporalStepTree(clazz, mapper, new HashMap<>()); - } - - @Override - public double trueness(EquivalenceClass clazz) { - var satisfyingAssignments = new BigDecimal(bdd.countSatisfyingAssignments(getNode(clazz))); - var assignments = BigDecimal.valueOf(2).pow(bdd.numberOfVariables()); - return satisfyingAssignments.divide(assignments, 24, RoundingMode.HALF_DOWN).doubleValue(); - } + @Override + public boolean equals(Object obj) { + if (this == obj) { + return true; + } - private ValuationTree temporalStepTree(EquivalenceClass clazz, - Function> mapper, Map> cache) { - var tree = cache.get(clazz); + if (!(obj instanceof EquivalenceClass)) { + return false; + } - if (tree != null) { - return tree; + BddEquivalenceClass that = factory.cast((EquivalenceClass) obj); + return node == that.node; } - int node = getNode(clazz); - int pivot = bdd.isNodeRoot(node) ? alphabet.size() : bdd.variable(node); - - if (pivot >= alphabet.size()) { - Arrays.fill(temporalStepSubstitution, 0, alphabet.size(), -1); - Set value = mapper.apply(transform(clazz, - x -> bdd.compose(x, temporalStepSubstitution), - Formula::temporalStep)); - tree = ValuationTree.of(value); - } else { - int[] substitution = new int[pivot + 1]; - Arrays.fill(substitution, 0, pivot, -1); - - substitution[pivot] = bdd.trueNode(); - var trueSubTree = temporalStepTree(transform(clazz, - x -> bdd.compose(getNode(clazz), substitution), - x -> x.temporalStep(pivot, true)), mapper, cache); + @Override + public int hashCode() { + return HashCommon.mix(node); + } - substitution[pivot] = bdd.falseNode(); - var falseSubTree = temporalStepTree(transform(clazz, - x -> bdd.compose(getNode(clazz), substitution), - x -> x.temporalStep(pivot, false)), mapper, cache); + @Override + public int node() { + return node; + } - tree = ValuationTree.of(pivot, trueSubTree, falseSubTree); + @Override + public String toString() { + return representative == null + ? String.format("%d", node) + : PrintVisitor.toString(representative, factory.atomicPropositions, false); } - cache.put(clazz, tree); - return tree; - } + @Override + public EquivalenceClassFactory factory() { + return factory; + } - private BddEquivalenceClass getClass(EquivalenceClass clazz) { - assert this.equals(clazz.factory()); - return (BddEquivalenceClass) clazz; - } + @Override + public boolean isFalse() { + return factory.bdd.falseNode() == node; + } - private int getNode(EquivalenceClass clazz) { - int node = getClass(clazz).node; - assert bdd.getReferenceCount(node) == 1 || bdd.getReferenceCount(node) == -1; - return node; - } + @Override + public boolean isTrue() { + return factory.bdd.trueNode() == node; + } - private int toBdd(Formula formula) { - // Scan for unknown proper subformulas. - List newPropositions = formula.subformulas(Formula.ModalOperator.class) - .stream().filter(x -> !mapping.containsKey(x)).sorted().collect(Collectors.toList()); + @Override + public BitSet atomicPropositions() { + return atomicPropositions(false); + } - if (!newPropositions.isEmpty()) { - if (registerActive) { - throw new ConcurrentModificationException( - "Detected recursive or parallel modification of BDD data-structures."); + @Override + public BitSet atomicPropositions(boolean includeNested) { + if (!includeNested) { + return factory.bdd.support(node, factory.atomicPropositions.size()); } - registerActive = true; + BitSet atomicPropositions = factory.bdd.support(node); - checkLiteralAlphabetRange(newPropositions); - - // Create variables. - int newSize = mapping.size() + newPropositions.size(); - reverseMapping = Arrays.copyOf(reverseMapping, newSize); - - for (Formula.ModalOperator proposition : newPropositions) { - int variable = bdd.variable(bdd.createVariable()); - mapping.put(proposition, variable); - reverseMapping[variable] = proposition; - } + int literalOffset = factory.atomicPropositions.size(); + int i = atomicPropositions.nextSetBit(literalOffset); - // Compute unfolding and temporal step. - unfoldSubstitution = Arrays.copyOf(unfoldSubstitution, newSize); - unfoldSubstitutes = Arrays.copyOf(unfoldSubstitutes, newSize); - temporalStepSubstitution = Arrays.copyOf(temporalStepSubstitution, newSize); - temporalStepSubstitutes = Arrays.copyOf(temporalStepSubstitutes, newSize); - - for (Formula.ModalOperator proposition : newPropositions) { - int variable = mapping.getInt(proposition); - - if (proposition instanceof XOperator) { - Formula operand = ((XOperator) proposition).operand; - BddEquivalenceClass clazz = create(operand, toBdd(operand)); - - unfoldSubstitution[variable] = -1; - temporalStepSubstitutes[variable] = clazz; - temporalStepSubstitution[variable] = clazz.node; - } else { - Formula unfold = proposition.unfold(); - BddEquivalenceClass clazz = create(unfold, toBdd(unfold)); - - unfoldSubstitutes[variable] = clazz; - unfoldSubstitution[variable] = clazz.node; - temporalStepSubstitution[variable] = -1; - } + for (; i >= 0; i = atomicPropositions.nextSetBit(i + 1)) { + atomicPropositions.or( + factory.reverseMapping[i - literalOffset].atomicPropositions(true)); } - if (!registerActive) { - throw new ConcurrentModificationException( - "Detected recursive or parallel modification of BDD data-structures."); + if (atomicPropositions.length() >= factory.atomicPropositions.size()) { + atomicPropositions.clear(factory.atomicPropositions.size(), atomicPropositions.length()); } - registerActive = false; + return atomicPropositions; } - return bdd.dereference(formula.accept(visitor)); - } + @Override + public Set modalOperators() { + if (modalOperatorsCache == null) { + BitSet support = factory.bdd.support(node); + int literalOffset = factory.atomicPropositions.size(); + support.clear(0, literalOffset); + modalOperatorsCache = support.stream() + .mapToObj(i -> factory.reverseMapping[i - literalOffset]) + .collect(Collectors.toUnmodifiableSet()); + } - private BddEquivalenceClass create(@Nullable Formula representative, int node) { - if (node == bdd.trueNode()) { - return trueClass; + return modalOperatorsCache; } - if (node == bdd.falseNode()) { - return falseClass; + @Override + public boolean implies(EquivalenceClass other) { + return factory.bdd.implies(node, factory.cast(other).node); } - BddEquivalenceClass clazz = - new BddEquivalenceClass(this, node, keepRepresentatives ? representative : null); - return canonicalize(clazz); - } - - private BddEquivalenceClass transform(EquivalenceClass clazz, IntUnaryOperator bddTransformer, - UnaryOperator representativeTransformer) { - BddEquivalenceClass casted = getClass(clazz); - - int newBdd = bddTransformer.applyAsInt(casted.node); - - @Nullable - Formula representative = clazz.representative(); - @Nullable - Formula newRepresentative; - if (casted.node == newBdd) { - newRepresentative = representative; - } else if (representative == null) { - newRepresentative = null; - } else { - newRepresentative = representativeTransformer.apply(representative); - } - return create(newRepresentative, newBdd); - } - - // Translates a formula into a BDD under the assumption every subformula is already registered. - private final class BddVisitor extends PropositionalIntVisitor { @Override - protected int visit(Formula.TemporalOperator formula) { - if (formula instanceof Literal) { - Literal literal = (Literal) formula; - checkLiteralAlphabetRange(List.of(literal)); - int variableBdd = bdd.variableNode(literal.getAtom()); - return literal.isNegated() ? bdd.not(variableBdd) : variableBdd; - } + public EquivalenceClass and(EquivalenceClass other) { + return factory.of( + Conjunction.of(representative(), other.representative()), + factory.bdd.and(node, factory.cast(other).node)); + } - int value = mapping.getInt(formula); - assert formula instanceof Formula.ModalOperator; - assert value >= 0; - return bdd.variableNode(value); + @Override + public EquivalenceClass or(EquivalenceClass other) { + return factory.of( + Disjunction.of(representative(), other.representative()), + factory.bdd.or(node, factory.cast(other).node)); } @Override - public int visit(BooleanConstant booleanConstant) { - return booleanConstant.value ? bdd.trueNode() : bdd.falseNode(); + public EquivalenceClass substitute( + Function substitution) { + return factory.of(representative().substitute(substitution)); } @Override - public int visit(Conjunction conjunction) { - int x = bdd.trueNode(); - for (Formula child : conjunction.children) { - int y = child.accept(this); - x = bdd.consume(bdd.and(x, y), x, y); - } - return x; + public EquivalenceClass temporalStep(BitSet valuation) { + return factory.of(representative().temporalStep(valuation), false); } + @SuppressWarnings("unchecked") @Override - public int visit(Disjunction disjunction) { - int x = bdd.falseNode(); - for (Formula child : disjunction.children) { - int y = child.accept(this); - x = bdd.consume(bdd.or(x, y), x, y); + public ValuationTree temporalStepTree(Function> mapper) { + if (factory.temporalStepTreeCache == null + || !mapper.equals(factory.temporalStepTreeCachedMapper)) { + factory.temporalStepTreeCachedMapper = (Function) mapper; + factory.temporalStepTreeCache = new IdentityHashMap<>(); } - return x; + + return temporalStepTree(representative(), new BitSet(), mapper, + (IdentityHashMap) factory.temporalStepTreeCache); } - } - private void checkLiteralAlphabetRange(Collection formulas) { - for (Formula x : formulas) { - if (x instanceof Literal && ((Literal) x).getAtom() >= alphabet.size()) { - throw new IllegalArgumentException("Literal " + x + " is not within alphabet."); + private ValuationTree temporalStepTree( + Formula initialRepresentative, + BitSet pathTrace, + Function> mapper, + IdentityHashMap> cache) { + + var tree = cache.get(this); + + if (tree != null) { + return tree; } - } - } - static final class BddEquivalenceClass extends EquivalenceClass implements BddNode { - final int node; + var alphabet = factory.atomicPropositions; + var bdd = factory.bdd; - BddEquivalenceClass(EquivalenceClassFactory factory, int node, - @Nullable Formula representative) { - super(factory, representative); - this.node = node; - } + int atom = bdd.isNodeRoot(node) ? alphabet.size() : bdd.variable(node); - @Override - public boolean equals(Object obj) { - if (this == obj) { - return true; + if (atom >= alphabet.size()) { + tree = ValuationTree.of(mapper.apply( + factory.of(initialRepresentative.temporalStep(pathTrace), false))); + } else { + pathTrace.set(atom); + var trueSubTree = factory.of(null, bdd.high(node)) + .temporalStepTree(initialRepresentative, pathTrace, mapper, cache); + + pathTrace.clear(atom, pathTrace.length()); + var falseSubTree = factory.of(null, bdd.low(node)) + .temporalStepTree(initialRepresentative, pathTrace, mapper, cache); + + tree = ValuationTree.of(atom, trueSubTree, falseSubTree); } - if (obj == null || getClass() != obj.getClass()) { - return false; + cache.put(this, tree); + return tree; + } + + @Override + public EquivalenceClass unfold() { + if (unfoldCache == null) { + unfoldCache = factory.of(representative().unfold(), false); } - BddEquivalenceClass that = (BddEquivalenceClass) obj; - assert this.factory().equals(that.factory()); - return node == that.node; + return unfoldCache; } @Override - public int hashCode() { - return HashCommon.mix(node); + public double trueness() { + var satisfyingAssignments = new BigDecimal(factory.bdd.countSatisfyingAssignments(node)); + var assignments = BigDecimal.valueOf(2).pow(factory.bdd.numberOfVariables()); + return satisfyingAssignments.divide(assignments, 24, RoundingMode.HALF_DOWN).doubleValue(); } @Override - public int node() { - return node; + public EquivalenceClass language() { + return this; } } } diff --git a/src/main/java/owl/factories/jbdd/JBddSupplier.java b/src/main/java/owl/factories/jbdd/JBddSupplier.java index 6f118b34f1beb7d1a589425c6c2c2ed6ed346005..e0b3ec85deeebac229253ce3ce8ca8cf5161ea17 100644 --- a/src/main/java/owl/factories/jbdd/JBddSupplier.java +++ b/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 alphabet) { - return getEquivalenceClassFactory(alphabet, keepRepresentativesDefault); - } - - @Override - public EquivalenceClassFactory getEquivalenceClassFactory(List 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 alphabet) { return new Factories( - getEquivalenceClassFactory(alphabet, keepRepresentativesDefault), + getEquivalenceClassFactory(alphabet), getValuationSetFactory(alphabet)); } diff --git a/src/main/java/owl/ltl/Biconditional.java b/src/main/java/owl/ltl/Biconditional.java index 046a5e8af58cbb6ffa20a56ba80460998772c3e8..b8cc1f5f884920bbd340318502882a72f1e53c5a 100644 --- a/src/main/java/owl/ltl/Biconditional.java +++ b/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 children() { - return Set.of(left, right); + public List children() { + return List.of(left, right); } @Override @@ -124,25 +127,17 @@ public final class Biconditional extends Formula.LogicalOperator { } @Override - public Formula substitute(Function substitution) { + public Formula substitute(Function 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 + ')'; } } diff --git a/src/main/java/owl/ltl/BinaryModalOperator.java b/src/main/java/owl/ltl/BinaryModalOperator.java deleted file mode 100644 index 29b2e694a2816d50d62b237c70126ce6b5675a33..0000000000000000000000000000000000000000 --- a/src/main/java/owl/ltl/BinaryModalOperator.java +++ /dev/null @@ -1,72 +0,0 @@ -/* - * 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 . - */ - -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 clazz, Formula leftOperand, - Formula rightOperand) { - super(Objects.hash(clazz, leftOperand, rightOperand)); - this.left = leftOperand; - this.right = rightOperand; - } - - @Override - public Set 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); - } -} diff --git a/src/main/java/owl/ltl/BooleanConstant.java b/src/main/java/owl/ltl/BooleanConstant.java index 6abd8bfa4fbab0bfb3a528f6eb6019f8cbb6f7fb..633394597ff588ea59512d94a59f2ace012315d8 100644 --- a/src/main/java/owl/ltl/BooleanConstant.java +++ b/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 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 children() { - return Set.of(); + public List children() { + return List.of(); } @Override @@ -84,7 +85,12 @@ public final class BooleanConstant extends Formula.LogicalOperator { } @Override - public Formula substitute(Function substitution) { + public Formula temporalStep(BitSet valuation) { + return this; + } + + @Override + public Formula substitute(Function 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; diff --git a/src/main/java/owl/ltl/Conjunction.java b/src/main/java/owl/ltl/Conjunction.java index 7929d8cd683a75f0b662a7933fba89434f56cc46..222913c9d627cda05dc8f71db36417e6f7783ab0 100644 --- a/src/main/java/owl/ltl/Conjunction.java +++ b/src/main/java/owl/ltl/Conjunction.java @@ -19,77 +19,103 @@ package owl.ltl; -import java.util.Arrays; +import java.util.ArrayList; +import java.util.BitSet; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; -import java.util.Iterator; +import java.util.List; import java.util.Set; import java.util.function.Function; +import java.util.stream.Collectors; import java.util.stream.Stream; +import javax.annotation.Nullable; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; import owl.util.annotation.CEntryPoint; -public final class Conjunction extends PropositionalFormula { +public final class Conjunction extends Formula.NaryPropositionalFormula { + + public Conjunction(Formula... conjuncts) { + this(sortedList(Set.of(conjuncts)), null); + } public Conjunction(Collection conjuncts) { - super(Conjunction.class, Set.copyOf(conjuncts)); + this(sortedList(new HashSet<>(conjuncts)), null); } - public Conjunction(Formula... conjuncts) { - super(Conjunction.class, Set.of(conjuncts)); + // Internal constructor. + @SuppressWarnings("PMD.UnusedFormalParameter") + private Conjunction(List conjuncts, @Nullable Void internal) { + super(Conjunction.class, List.copyOf(conjuncts)); } @CEntryPoint - public static Formula of(Formula left, Formula right) { - return of(Arrays.asList(left, right)); + public static Formula of(Formula e1, Formula e2) { + ArrayList list = new ArrayList<>(); + list.add(e1); + list.add(e2); + return ofInternal(list); } public static Formula of(Formula... formulas) { - return of(Arrays.asList(formulas)); + ArrayList list = new ArrayList<>(formulas.length); + Collections.addAll(list, formulas); + return ofInternal(list); } - public static Formula of(Iterable iterable) { - return of(iterable.iterator()); + public static Formula of(Collection collection) { + return ofInternal(new ArrayList<>(collection)); } public static Formula of(Stream stream) { - return of(stream.iterator()); + return ofInternal(stream.collect(Collectors.toCollection(ArrayList::new))); } - public static Formula of(Iterator iterator) { - Set set = new HashSet<>(); + @SuppressWarnings("PMD.LooseCoupling") + static Formula ofInternal(ArrayList list) { + boolean sorted = false; - while (iterator.hasNext()) { - Formula child = iterator.next(); - assert child != null; + while (!sorted) { + list.sort(null); + sorted = true; - if (BooleanConstant.FALSE.equals(child)) { - return BooleanConstant.FALSE; - } + for (int i = list.size() - 1; i >= 0; i--) { + Formula child = list.get(i); - if (BooleanConstant.TRUE.equals(child)) { - continue; - } + if (BooleanConstant.FALSE.equals(child)) { + return BooleanConstant.FALSE; + } + + if (BooleanConstant.TRUE.equals(child)) { + list.remove(i); + continue; + } + + if (i > 0 && list.get(i - 1).equals(child)) { + list.remove(i); + continue; + } - if (child instanceof Conjunction) { - set.addAll(((Conjunction) child).children); - } else { - set.add(child); + if (child instanceof Conjunction) { + list.remove(i); + list.addAll(child.children()); + sorted = false; + } } } - if (set.isEmpty()) { - return BooleanConstant.TRUE; - } + switch (list.size()) { + case 0: + return BooleanConstant.TRUE; - if (set.size() == 1) { - return set.iterator().next(); - } + case 1: + return list.get(0); - // Set.copyOf is stupid if given a Set<>, hence this hack - return new Conjunction(set.toArray(Formula[]::new)); + default: + return new Conjunction(list, null); + } } @Override @@ -109,17 +135,34 @@ public final class Conjunction extends PropositionalFormula { @Override public Formula nnf() { - return Conjunction.of(map(Formula::nnf)); + return Conjunction.ofInternal(mapInternal(Formula::nnf)); } @Override public Formula not() { - return Disjunction.of(map(Formula::not)); + return Disjunction.ofInternal(mapInternal(Formula::not)); + } + + @Override + public Formula substitute(Function substitution) { + var conjunction = Conjunction.ofInternal(mapInternal(c -> c.substitute(substitution))); + + if (this.equals(conjunction)) { + return this; + } + + return conjunction; } @Override - public Formula substitute(Function substitution) { - return Conjunction.of(map(c -> c.substitute(substitution))); + public Formula temporalStep(BitSet valuation) { + var conjunction = Conjunction.ofInternal(mapInternal(c -> c.temporalStep(valuation))); + + if (this.equals(conjunction)) { + return this; + } + + return conjunction; } @Override diff --git a/src/main/java/owl/ltl/Disjunction.java b/src/main/java/owl/ltl/Disjunction.java index 785112650d00a5094991dd8af30e26c8ed222f32..6a0e6875f19e77ac496f46692e281b2f9086f3f5 100644 --- a/src/main/java/owl/ltl/Disjunction.java +++ b/src/main/java/owl/ltl/Disjunction.java @@ -19,75 +19,103 @@ package owl.ltl; -import java.util.Arrays; +import java.util.ArrayList; +import java.util.BitSet; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; -import java.util.Iterator; +import java.util.List; import java.util.Set; import java.util.function.Function; +import java.util.stream.Collectors; import java.util.stream.Stream; +import javax.annotation.Nullable; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; +import owl.util.annotation.CEntryPoint; -public final class Disjunction extends PropositionalFormula { +public final class Disjunction extends Formula.NaryPropositionalFormula { - public Disjunction(Collection conjuncts) { - super(Disjunction.class, Set.copyOf(conjuncts)); + public Disjunction(Formula... disjuncts) { + this(sortedList(Set.of(disjuncts)), null); } - public Disjunction(Formula... conjuncts) { - super(Disjunction.class, Set.of(conjuncts)); + public Disjunction(Collection disjuncts) { + this(sortedList(new HashSet<>(disjuncts)), null); } - public static Formula of(Formula left, Formula right) { - return of(Arrays.asList(left, right)); + // Internal constructor. + @SuppressWarnings("PMD.UnusedFormalParameter") + private Disjunction(List disjuncts, @Nullable Void internal) { + super(Conjunction.class, List.copyOf(disjuncts)); + } + + @CEntryPoint + public static Formula of(Formula e1, Formula e2) { + ArrayList list = new ArrayList<>(); + list.add(e1); + list.add(e2); + return ofInternal(list); } public static Formula of(Formula... formulas) { - return of(Arrays.asList(formulas)); + ArrayList list = new ArrayList<>(formulas.length); + Collections.addAll(list, formulas); + return ofInternal(list); } - public static Formula of(Iterable iterable) { - return of(iterable.iterator()); + public static Formula of(Collection collection) { + return ofInternal(new ArrayList<>(collection)); } public static Formula of(Stream stream) { - return of(stream.iterator()); + return ofInternal(stream.collect(Collectors.toCollection(ArrayList::new))); } - public static Formula of(Iterator iterator) { - Set set = new HashSet<>(); + @SuppressWarnings("PMD.LooseCoupling") + static Formula ofInternal(ArrayList list) { + boolean sorted = false; - while (iterator.hasNext()) { - Formula child = iterator.next(); - assert child != null; + while (!sorted) { + list.sort(null); + sorted = true; - if (BooleanConstant.TRUE.equals(child)) { - return BooleanConstant.TRUE; - } + for (int i = list.size() - 1; i >= 0; i--) { + Formula child = list.get(i); - if (BooleanConstant.FALSE.equals(child)) { - continue; - } + if (BooleanConstant.TRUE.equals(child)) { + return BooleanConstant.TRUE; + } + + if (BooleanConstant.FALSE.equals(child)) { + list.remove(i); + continue; + } - if (child instanceof Disjunction) { - set.addAll(((Disjunction) child).children); - } else { - set.add(child); + if (i > 0 && list.get(i - 1).equals(child)) { + list.remove(i); + continue; + } + + if (child instanceof Disjunction) { + list.remove(i); + list.addAll(child.children()); + sorted = false; + } } } - if (set.isEmpty()) { - return BooleanConstant.FALSE; - } + switch (list.size()) { + case 0: + return BooleanConstant.FALSE; - if (set.size() == 1) { - return set.iterator().next(); - } + case 1: + return list.get(0); - // Set.copyOf is stupid if given a Set<>, hence this hack - return new Disjunction(set.toArray(Formula[]::new)); + default: + return new Disjunction(list, null); + } } @Override @@ -107,17 +135,34 @@ public final class Disjunction extends PropositionalFormula { @Override public Formula nnf() { - return Disjunction.of(map(Formula::nnf)); + return Disjunction.ofInternal(mapInternal(Formula::nnf)); } @Override public Formula not() { - return Conjunction.of(map(Formula::not)); + return Conjunction.ofInternal(mapInternal(Formula::not)); } @Override - public Formula substitute(Function substitution) { - return Disjunction.of(map(c -> c.substitute(substitution))); + public Formula substitute(Function substitution) { + var disjunction = Disjunction.ofInternal(mapInternal(c -> c.substitute(substitution))); + + if (this.equals(disjunction)) { + return this; + } + + return disjunction; + } + + @Override + public Formula temporalStep(BitSet valuation) { + var disjunction = Disjunction.ofInternal(mapInternal(c -> c.temporalStep(valuation))); + + if (this.equals(disjunction)) { + return this; + } + + return disjunction; } @Override diff --git a/src/main/java/owl/ltl/EquivalenceClass.java b/src/main/java/owl/ltl/EquivalenceClass.java index 2ff7986cc23b4372b2404b30996f66ef96647d9b..be79a5d8133240a8af5f72480dbb789d55d20c81 100644 --- a/src/main/java/owl/ltl/EquivalenceClass.java +++ b/src/main/java/owl/ltl/EquivalenceClass.java @@ -19,11 +19,9 @@ package owl.ltl; -import java.util.Arrays; import java.util.BitSet; import java.util.Set; import java.util.function.Function; -import javax.annotation.Nullable; import owl.collections.ValuationTree; import owl.factories.EquivalenceClassFactory; @@ -31,139 +29,62 @@ import owl.factories.EquivalenceClassFactory; * EquivalenceClass interface. The general contract of this interface is: If two implementing * objects were created from different factories, implies and equals have to return {@code false}. */ -public class EquivalenceClass implements LtlLanguageExpressible { - private final EquivalenceClassFactory factory; - @Nullable - private final Formula representative; - - protected EquivalenceClass(EquivalenceClassFactory factory, @Nullable Formula representative) { - this.factory = factory; - this.representative = representative; - } - - @Nullable - public final Formula representative() { - return representative; - } +public interface EquivalenceClass extends LtlLanguageExpressible { + Formula representative(); - public final EquivalenceClassFactory factory() { - return factory; - } + EquivalenceClassFactory factory(); - public final boolean isFalse() { - return equals(factory.getFalse()); - } + boolean isFalse(); - public final boolean isTrue() { - return equals(factory.getTrue()); - } + boolean isTrue(); /** - * See {@link EquivalenceClassFactory#atomicPropositions(EquivalenceClass, boolean)}. + * See {@link Formula#atomicPropositions(boolean)}. */ - public final BitSet atomicPropositions() { - return factory.atomicPropositions(this, false); - } + BitSet atomicPropositions(); /** - * See {@link EquivalenceClassFactory#atomicPropositions(EquivalenceClass, boolean)}. + * Collects all literals used in the bdd and stores the corresponding atomic propositions in + * the BitSet. See also {@link Formula#atomicPropositions(boolean)}. */ - public final BitSet atomicPropositions(boolean includeNested) { - return factory.atomicPropositions(this, includeNested); - } + BitSet atomicPropositions(boolean includeNested); - // TODO: cache this field. - /** - * See {@link EquivalenceClassFactory#modalOperators(EquivalenceClass)}. - */ - public final Set modalOperators() { - return factory.modalOperators(this); - } + Set modalOperators(); - /** - * See {@link EquivalenceClassFactory#implies(EquivalenceClass, EquivalenceClass)}. - */ - public final boolean implies(EquivalenceClass other) { - return factory.implies(this, other); - } + boolean implies(EquivalenceClass other); - /** - * See {@link EquivalenceClassFactory#conjunction(java.util.Collection)}. - */ - public final EquivalenceClass and(EquivalenceClass other) { - return factory.conjunction(Arrays.asList(this, other)); - } + EquivalenceClass and(EquivalenceClass other); - /** - * See {@link EquivalenceClassFactory#disjunction(java.util.Collection)}. - */ - public final EquivalenceClass or(EquivalenceClass other) { - return factory.disjunction(Arrays.asList(this, other)); - } + EquivalenceClass or(EquivalenceClass other); /** - * See {@link EquivalenceClassFactory#substitute(EquivalenceClass, Function)}. + * See {@link Formula#substitute(Function)}. * * @param substitution The substitution function. It is only called on modal operators. */ - public final EquivalenceClass substitute( - Function substitution) { - return factory.substitute(this, substitution); - } + EquivalenceClass substitute( + Function substitution); /** - * See {@link EquivalenceClassFactory#temporalStep(EquivalenceClass, BitSet)}. + * See {@link Formula#temporalStep(BitSet)}. * * @param valuation The assignment for the atomic propositions. */ - public final EquivalenceClass temporalStep(BitSet valuation) { - return factory.temporalStep(this, valuation); - } + EquivalenceClass temporalStep(BitSet valuation); - public final ValuationTree temporalStepTree() { + default ValuationTree temporalStepTree() { return temporalStepTree(Set::of); } - public final ValuationTree temporalStepTree(Function> mapper) { - return factory.temporalStepTree(this, mapper); - } - - /** - * See {@link EquivalenceClassFactory#temporalStepUnfold(EquivalenceClass, BitSet)}. - * - * @param valuation The assignment for the atomic propositions. - */ - public final EquivalenceClass temporalStepUnfold(BitSet valuation) { - return factory.temporalStepUnfold(this, valuation); - } - - /** - * See {@link EquivalenceClassFactory#unfold(EquivalenceClass)}. - */ - public final EquivalenceClass unfold() { - return factory.unfold(this); - } + ValuationTree temporalStepTree(Function> mapper); /** - * See {@link EquivalenceClassFactory#unfoldTemporalStep(EquivalenceClass, BitSet)}. - * - * @param valuation The assignment for the atomic propositions. + * See {@link Formula#unfold()}. */ - public final EquivalenceClass unfoldTemporalStep(BitSet valuation) { - return factory.unfoldTemporalStep(this, valuation); - } + EquivalenceClass unfold(); - public final double trueness() { - return factory.trueness(this); - } + double trueness(); @Override - public EquivalenceClass language() { - return this; - } - - @Override - public final String toString() { - return factory.toString(this); - } + EquivalenceClass language(); } diff --git a/src/main/java/owl/ltl/FOperator.java b/src/main/java/owl/ltl/FOperator.java index 0fbb1abc786d63926b6b6fac202863d3fe45ce6e..557767294af2f463abc83cbc15f1d8e4a6bd7f10 100644 --- a/src/main/java/owl/ltl/FOperator.java +++ b/src/main/java/owl/ltl/FOperator.java @@ -19,7 +19,6 @@ package owl.ltl; -import java.util.BitSet; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; @@ -28,7 +27,7 @@ import owl.util.annotation.CEntryPoint; /** * Finally. */ -public final class FOperator extends UnaryModalOperator { +public final class FOperator extends Formula.UnaryTemporalOperator { public FOperator(Formula operand) { super(FOperator.class, operand); @@ -125,9 +124,4 @@ public final class FOperator extends UnaryModalOperator { public Formula unfold() { return Disjunction.of(operand.unfold(), this); } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return Disjunction.of(operand.unfoldTemporalStep(valuation), this); - } } diff --git a/src/main/java/owl/ltl/Formula.java b/src/main/java/owl/ltl/Formula.java index 9ab55bce46e37fb4bd18b40b24f86d1579c2e39d..516ff99247e2ee9a6903632c7efe53ac84db31a8 100644 --- a/src/main/java/owl/ltl/Formula.java +++ b/src/main/java/owl/ltl/Formula.java @@ -19,38 +19,36 @@ package owl.ltl; +import com.google.common.collect.Comparators; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Arrays; import java.util.BitSet; +import java.util.Comparator; +import java.util.Deque; import java.util.HashSet; import java.util.List; +import java.util.Objects; import java.util.Set; import java.util.function.Function; import java.util.function.Predicate; +import java.util.function.UnaryOperator; +import java.util.stream.Collectors; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; -import owl.ltl.visitors.PropositionalVisitor; import owl.ltl.visitors.Visitor; public abstract class Formula implements Comparable { - private static final List> ORDER = List.of( - BooleanConstant.class, - Literal.class, - Negation.class, - Conjunction.class, - Disjunction.class, - Biconditional.class, - FOperator.class, - GOperator.class, - XOperator.class, - MOperator.class, - ROperator.class, - UOperator.class, - WOperator.class); + private static final Comparator> LIST_COMPARATOR + = Comparators.lexicographical(Formula::compareTo); private final int hashCode; + private final int height; - Formula(int hashCode) { + Formula(int hashCode, int height) { this.hashCode = hashCode; + this.height = height; } public abstract int accept(IntVisitor visitor); @@ -61,8 +59,18 @@ public abstract class Formula implements Comparable { public final BitSet atomicPropositions(boolean includeNested) { BitSet atomicPropositions = new BitSet(); + Deque workQueue = new ArrayDeque<>(List.of(this)); - accept(new AtomicPropositionsVisitor(atomicPropositions, includeNested)); + while (!workQueue.isEmpty()) { + var formula = workQueue.removeLast(); + + if (formula instanceof Literal) { + atomicPropositions.set(((Literal) formula).getAtom()); + } else if (formula instanceof Propositional + || (includeNested && formula instanceof Temporal)) { + workQueue.addAll(formula.children()); + } + } return atomicPropositions; } @@ -95,11 +103,11 @@ public abstract class Formula implements Comparable { return false; } - public abstract Set children(); + public abstract List children(); @Override public final int compareTo(Formula o) { - int heightComparison = Integer.compare(height(), o.height()); + int heightComparison = Integer.compare(height, o.height); if (heightComparison != 0) { return heightComparison; @@ -111,7 +119,29 @@ public abstract class Formula implements Comparable { return classComparison; } - return compareToImpl(o); + assert getClass().equals(o.getClass()); + + int valueComparison = compareValue(o); + + if (valueComparison != 0) { + return valueComparison; + } + + var thisChildren = this.children(); + var thatChildren = o.children(); + + int lengthComparison = Integer.compare(thisChildren.size(), thatChildren.size()); + + if (lengthComparison != 0) { + return lengthComparison; + } + + return LIST_COMPARATOR.compare(thisChildren, thatChildren); + } + + @SuppressWarnings("PMD") + protected int compareValue(Formula o) { + return 0; } @Override @@ -120,12 +150,20 @@ public abstract class Formula implements Comparable { return true; } - if (o == null || !getClass().equals(o.getClass())) { + if (!(o instanceof Formula)) { return false; } Formula other = (Formula) o; - return other.hashCode == hashCode && equalsImpl(other); + return hashCode == other.hashCode + && height == other.height + && getClass().equals(other.getClass()) + && equalsValue(other) + && children().equals(other.children()); + } + + protected boolean equalsValue(Formula o) { + return true; } @Override @@ -134,7 +172,7 @@ public abstract class Formula implements Comparable { } public final int height() { - return Formulas.height(children()) + 1; + return height; } // Temporal Properties of an LTL Formula @@ -157,65 +195,34 @@ public abstract class Formula implements Comparable { */ public abstract Formula not(); - public final Set subformulas(Class clazz) { + public final Set subformulas(Class clazz) { return subformulas(clazz::isInstance, clazz::cast); } - public final Set subformulas(Predicate predicate) { + public final Set subformulas(Predicate predicate) { return subformulas(predicate, x -> x); } - public final Set subformulas( - Predicate predicate, - Function cast) { + public final Set subformulas( + Predicate predicate, Function cast) { Set subformulas = new HashSet<>(); + Deque workQueue = new ArrayDeque<>(List.of(this)); - accept(new PropositionalVisitor() { - @Override - public Void visit(Biconditional biconditional) { - biconditional.left.accept(this); - biconditional.right.accept(this); - return null; - } + while (!workQueue.isEmpty()) { + var formula = workQueue.removeLast(); - @Override - public Void visit(BooleanConstant booleanConstant) { - return null; + if (predicate.test(formula)) { + subformulas.add(cast.apply(formula)); } - @Override - public Void visit(Conjunction conjunction) { - conjunction.children.forEach(c -> c.accept(this)); - return null; - } - - @Override - public Void visit(Disjunction disjunction) { - disjunction.children.forEach(c -> c.accept(this)); - return null; - } - - @Override - protected Void visit(TemporalOperator formula) { - if (predicate.test(formula)) { - subformulas.add(cast.apply(formula)); - } - - formula.children().forEach(x -> x.accept(this)); - return null; - } - }); + workQueue.addAll(formula.children()); + } return subformulas; } - // temporal formulas public abstract Formula substitute( - Function substitution); - - public abstract Formula temporalStep(); - - public abstract Formula temporalStep(int atom, boolean valuation); + Function substitution); /** * Do a single temporal step. This means that one layer of X-operators is removed and literals are @@ -223,164 +230,209 @@ public abstract class Formula implements Comparable { */ public abstract Formula temporalStep(BitSet valuation); - /** - * Short-cut operation to avoid intermediate construction of formula ASTs. - */ - public abstract Formula temporalStepUnfold(BitSet valuation); - public abstract Formula unfold(); - /** - * Short-cut operation to avoid intermediate construction of formula ASTs. - */ - public abstract Formula unfoldTemporalStep(BitSet valuation); + public abstract static class Propositional extends Formula { + Propositional(int hashCode, int height) { + super(hashCode, height); + } - protected abstract int compareToImpl(Formula o); + @Override + public final Formula unfold() { + return substitute(Formula::unfold); + } + } - protected abstract boolean equalsImpl(Formula o); + public abstract static class Temporal extends Formula { + Temporal(int hashCode, int height) { + super(hashCode, height); + } - private static int classIndex(Formula formula) { - int index = ORDER.indexOf(formula.getClass()); - assert index >= 0; - return index; - } + public abstract String operatorSymbol(); + + @Override + public final Formula substitute( + Function substitution) { + return substitution.apply(this); + } + + @Override + public final Formula temporalStep(BitSet valuation) { + if (this instanceof XOperator) { + return ((XOperator) this).operand; + } - public abstract static class ModalOperator extends TemporalOperator { - ModalOperator(int hashCode) { - super(hashCode); + return this; + } + + @SuppressWarnings("PMD") + @Override + protected final int compareValue(Formula o) { + return 0; + } + + @Override + protected final boolean equalsValue(Formula o) { + return true; } } - public abstract static class LogicalOperator extends Formula { - LogicalOperator(int hashCode) { - super(hashCode); + public abstract static class UnaryTemporalOperator extends Temporal { + public final Formula operand; + + UnaryTemporalOperator(Class clazz, Formula operand) { + super(Objects.hash(clazz, operand), operand.height() + 1); + this.operand = operand; } @Override - public final Formula temporalStep() { - return substitute(Formula::temporalStep); + public List children() { + return List.of(operand); } @Override - public final Formula temporalStep(int atom, boolean valuation) { - return substitute(x -> x.temporalStep(atom, valuation)); + public String toString() { + return operatorSymbol() + operand; + } + } + + public abstract static class BinaryTemporalOperator extends Temporal { + public final Formula left; + public final Formula right; + + BinaryTemporalOperator(Class clazz, + Formula leftOperand, Formula rightOperand) { + super(Objects.hash(clazz, leftOperand, rightOperand), + Formulas.height(leftOperand, rightOperand) + 1); + this.left = leftOperand; + this.right = rightOperand; } @Override - public final Formula temporalStep(BitSet valuation) { - return substitute(x -> x.temporalStep(valuation)); + public List children() { + return List.of(left, right); } @Override - public final Formula temporalStepUnfold(BitSet valuation) { - return substitute(x -> x.temporalStepUnfold(valuation)); + public final boolean isPureEventual() { + return false; } @Override - public final Formula unfold() { - return substitute(Formula::unfold); + public final boolean isPureUniversal() { + return false; } @Override - public final Formula unfoldTemporalStep(BitSet valuation) { - return substitute(x -> x.unfoldTemporalStep(valuation)); + public final String toString() { + return String.format("(%s%s%s)", left, operatorSymbol(), right); } } - // TODO: Fix hierarchy naming. - public abstract static class TemporalOperator extends Formula { - TemporalOperator(int hashCode) { - super(hashCode); + public abstract static class NaryPropositionalFormula extends Propositional { + public final List children; + + NaryPropositionalFormula(Class clazz, + List children) { + super(Objects.hash(clazz, children), Formulas.height(children) + 1); + this.children = List.copyOf(children); } @Override - public final Formula substitute( - Function substitution) { - return substitution.apply(this); + public final List children() { + return children; } @Override - public final Formula temporalStep() { - return this instanceof XOperator ? ((XOperator) this).operand : this; + public final boolean isPureEventual() { + return children.stream().allMatch(Formula::isPureEventual); } @Override - public final Formula temporalStep(int atom, boolean valuation) { - if (this instanceof Literal) { - Literal literal = (Literal) this; - - if (literal.getAtom() == atom) { - return BooleanConstant.of(valuation ^ literal.isNegated()); - } - } + public final boolean isPureUniversal() { + return children.stream().allMatch(Formula::isPureUniversal); + } - return this; + public final List map(UnaryOperator mapper) { + return mapInternal(mapper); } @Override - public final Formula temporalStep(BitSet valuation) { - if (this instanceof Literal) { - Literal literal = (Literal) this; - return BooleanConstant.of(valuation.get(literal.getAtom()) ^ literal.isNegated()); - } + public final String toString() { + return children.stream() + .map(Formula::toString) + .collect(Collectors.joining(operatorSymbol(), "(", ")")); + } - return temporalStep(); + protected static List sortedList(Set children) { + Formula[] list = children.toArray(Formula[]::new); + Arrays.sort(list); + return List.of(list); } - @Override - public final Formula temporalStepUnfold(BitSet valuation) { - return temporalStep(valuation).unfold(); + @SuppressWarnings("PMD.LooseCoupling") + protected final ArrayList mapInternal(UnaryOperator mapper) { + var mappedChildren = new ArrayList<>(children); + mappedChildren.replaceAll(mapper); + return mappedChildren; } + + protected abstract String operatorSymbol(); } - private static class AtomicPropositionsVisitor extends PropositionalVisitor { - private final BitSet atomicPropositions; - private final boolean includeNested; + private static int classIndex(Formula formula) { + if (formula instanceof BooleanConstant) { + return 0; + } - public AtomicPropositionsVisitor(BitSet atomicPropositions, boolean includeNested) { - this.atomicPropositions = atomicPropositions; - this.includeNested = includeNested; + if (formula instanceof Literal) { + return 1; } - @Override - public Void visit(Biconditional biconditional) { - biconditional.left.accept(this); - biconditional.right.accept(this); - return null; + if (formula instanceof Negation) { + return 2; } - @Override - public Void visit(BooleanConstant booleanConstant) { - return null; + if (formula instanceof Conjunction) { + return 3; } - @Override - public Void visit(Conjunction conjunction) { - conjunction.children.forEach(x -> x.accept(this)); - return null; + if (formula instanceof Disjunction) { + return 4; } - @Override - public Void visit(Disjunction disjunction) { - disjunction.children.forEach(x -> x.accept(this)); - return null; + if (formula instanceof Biconditional) { + return 5; } - @Override - protected Void visit(TemporalOperator formula) { - if (formula instanceof Literal) { - atomicPropositions.set(((Literal) formula).getAtom()); - } else if (includeNested) { - formula.children().forEach(x -> x.accept(this)); - } + if (formula instanceof FOperator) { + return 6; + } - return null; + if (formula instanceof GOperator) { + return 7; } - @Override - public Void visit(Negation negation) { - negation.operand.accept(this); - return null; + if (formula instanceof XOperator) { + return 8; + } + + if (formula instanceof MOperator) { + return 9; + } + + if (formula instanceof ROperator) { + return 10; + } + + if (formula instanceof UOperator) { + return 11; } + + if (formula instanceof WOperator) { + return 12; + } + + throw new AssertionError(); } } diff --git a/src/main/java/owl/ltl/Formulas.java b/src/main/java/owl/ltl/Formulas.java index 4e1878ed7d55369b9b8f35bd664800543a66f820..6c8a8689a8c37fdcc77587508479fc954d4e95c6 100644 --- a/src/main/java/owl/ltl/Formulas.java +++ b/src/main/java/owl/ltl/Formulas.java @@ -19,45 +19,37 @@ package owl.ltl; -import com.google.common.collect.Comparators; import java.util.Collection; -import java.util.List; import java.util.Set; import owl.collections.Collections3; public final class Formulas { private Formulas() {} - public static int compare(List list1, List list2) { - int lengthComparison = Integer.compare(list1.size(), list2.size()); + public static int compare(Set set1, Set set2) { + int lengthComparison = Integer.compare(set1.size(), set2.size()); if (lengthComparison != 0) { return lengthComparison; } - int heightComparison = Integer.compare(height(list1), height(list2)); + int heightComparison = Integer.compare(height(set1), height(set2)); if (heightComparison != 0) { return heightComparison; } - return Comparators.lexicographical(Formula::compareTo).compare(list1, list2); + return Collections3.compare(set1, set2); } - public static int compare(Set set1, Set set2) { - int lengthComparison = Integer.compare(set1.size(), set2.size()); - - if (lengthComparison != 0) { - return lengthComparison; - } - - int heightComparison = Integer.compare(height(set1), height(set2)); + public static int height(Formula... formulas) { + int height = 0; - if (heightComparison != 0) { - return heightComparison; + for (var formula : formulas) { + height = Math.max(height, formula.height()); } - return Collections3.compare(set1, set2); + return height; } public static int height(Collection collection) { diff --git a/src/main/java/owl/ltl/GOperator.java b/src/main/java/owl/ltl/GOperator.java index 4628e481b307610c1f6ea92d55d89fef8b8e2a10..2306929667a29ec1beed4e8d3b2e3dbe15785bb1 100644 --- a/src/main/java/owl/ltl/GOperator.java +++ b/src/main/java/owl/ltl/GOperator.java @@ -19,7 +19,6 @@ package owl.ltl; -import java.util.BitSet; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; @@ -28,7 +27,7 @@ import owl.util.annotation.CEntryPoint; /** * Globally. */ -public final class GOperator extends UnaryModalOperator { +public final class GOperator extends Formula.UnaryTemporalOperator { public GOperator(Formula operand) { super(GOperator.class, operand); @@ -125,9 +124,4 @@ public final class GOperator extends UnaryModalOperator { public Formula unfold() { return Conjunction.of(operand.unfold(), this); } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return Conjunction.of(operand.unfoldTemporalStep(valuation), this); - } } diff --git a/src/main/java/owl/ltl/LabelledFormula.java b/src/main/java/owl/ltl/LabelledFormula.java index 9ea2e49783ec84583f84df82c3ff12befca45afc..336d933d75351492cbf464e06290e8d6880ac5c8 100644 --- a/src/main/java/owl/ltl/LabelledFormula.java +++ b/src/main/java/owl/ltl/LabelledFormula.java @@ -28,20 +28,20 @@ import owl.ltl.visitors.PrintVisitor; @AutoValue public abstract class LabelledFormula { - public abstract Formula formula(); + public abstract List atomicPropositions(); - public abstract List variables(); + public abstract Formula formula(); public static LabelledFormula of(Formula formula, List variables) { int atomicPropositionsSize = formula.atomicPropositions(true).length(); checkArgument(Collections3.isDistinct(variables)); checkArgument(atomicPropositionsSize <= variables.size()); - return new AutoValue_LabelledFormula(formula, - List.copyOf(variables.subList(0, atomicPropositionsSize))); + return new AutoValue_LabelledFormula( + List.copyOf(variables.subList(0, atomicPropositionsSize)), formula); } public LabelledFormula wrap(Formula formula) { - return of(formula, variables()); + return of(formula, atomicPropositions()); } public LabelledFormula not() { diff --git a/src/main/java/owl/ltl/Literal.java b/src/main/java/owl/ltl/Literal.java index bd1975c2ca60233e80565d38d9beb91aad63b7f1..3a31dd3e98df09554aeb868642fdaf9ab2581336 100644 --- a/src/main/java/owl/ltl/Literal.java +++ b/src/main/java/owl/ltl/Literal.java @@ -23,14 +23,15 @@ import static java.util.Objects.checkIndex; import java.util.Arrays; import java.util.BitSet; +import java.util.List; import java.util.Objects; -import java.util.Set; +import java.util.function.Function; import javax.annotation.Nonnegative; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; -public final class Literal extends Formula.TemporalOperator { +public final class Literal extends Formula.Propositional { private static final int CACHE_SIZE = 128; private static final Literal[] cache = new Literal[CACHE_SIZE]; private final int index; @@ -41,21 +42,21 @@ public final class Literal extends Formula.TemporalOperator { } private Literal(Literal other) { - super(Objects.hash(Literal.class, Integer.hashCode(-other.index))); + super(Objects.hash(Literal.class, Integer.hashCode(-other.index)), 0); this.index = -other.index; this.negation = other; assert (getAtom() == other.getAtom()) && (isNegated() ^ other.isNegated()); } private Literal(@Nonnegative int index) { - super(Objects.hash(Literal.class, Integer.hashCode(index + 1))); + super(Objects.hash(Literal.class, Integer.hashCode(index + 1)), 0); checkIndex(index, Integer.MAX_VALUE); this.index = index + 1; this.negation = new Literal(this); assert getAtom() == negation.getAtom() && (isNegated() ^ negation.isNegated()); } - + public static Literal of(@Nonnegative int index) { return of(index, false); } @@ -70,6 +71,15 @@ public final class Literal extends Formula.TemporalOperator { return negate ? literal.negation : literal; } + @Override + public Formula temporalStep(BitSet valuation) { + return BooleanConstant.of(valuation.get(getAtom()) ^ isNegated()); + } + + @Override + public Formula substitute(Function substitution) { + return this; + } @Override public int accept(IntVisitor v) { @@ -87,8 +97,8 @@ public final class Literal extends Formula.TemporalOperator { } @Override - public Set children() { - return Set.of(); + public List children() { + return List.of(); } public int getAtom() { @@ -125,17 +135,7 @@ public final class Literal extends Formula.TemporalOperator { } @Override - public Formula unfold() { - return this; - } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return temporalStep(valuation); - } - - @Override - protected int compareToImpl(Formula o) { + protected int compareValue(Formula o) { Literal that = (Literal) o; int comparison = Integer.compare(getAtom(), that.getAtom()); @@ -147,7 +147,7 @@ public final class Literal extends Formula.TemporalOperator { } @Override - protected boolean equalsImpl(Formula o) { + protected boolean equalsValue(Formula o) { Literal that = (Literal) o; return index == that.index; } diff --git a/src/main/java/owl/ltl/MOperator.java b/src/main/java/owl/ltl/MOperator.java index e32b93501be5f174bc72dd1d4c0045b6503a043d..d112f4e0046bfc206080f9c683ba25aaf328be51 100644 --- a/src/main/java/owl/ltl/MOperator.java +++ b/src/main/java/owl/ltl/MOperator.java @@ -19,7 +19,6 @@ package owl.ltl; -import java.util.BitSet; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; @@ -28,7 +27,7 @@ import owl.util.annotation.CEntryPoint; /** * Strong Release. */ -public final class MOperator extends BinaryModalOperator { +public final class MOperator extends Formula.BinaryTemporalOperator { public MOperator(Formula leftOperand, Formula rightOperand) { super(MOperator.class, leftOperand, rightOperand); @@ -100,10 +99,4 @@ public final class MOperator extends BinaryModalOperator { public Formula unfold() { return Conjunction.of(right.unfold(), Disjunction.of(left.unfold(), this)); } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return Conjunction.of(right.unfoldTemporalStep(valuation), - Disjunction.of(left.unfoldTemporalStep(valuation), this)); - } } diff --git a/src/main/java/owl/ltl/Negation.java b/src/main/java/owl/ltl/Negation.java index 669ae0abfe42caeb14cacc4f1bf04fa8aafa18b9..1aac0da2a61bb14682177f4db163be4f019812a2 100644 --- a/src/main/java/owl/ltl/Negation.java +++ b/src/main/java/owl/ltl/Negation.java @@ -19,19 +19,19 @@ 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; import owl.ltl.visitors.Visitor; -public class Negation extends Formula.LogicalOperator { +public class Negation extends Formula.Propositional { public final Formula operand; public Negation(Formula operand) { - super(Objects.hash(Negation.class, operand)); + super(Objects.hash(Negation.class, operand), operand.height() + 1); this.operand = operand; } @@ -51,20 +51,8 @@ public class Negation extends Formula.LogicalOperator { } @Override - public Set children() { - return Set.of(operand); - } - - @Override - protected int compareToImpl(Formula o) { - Negation that = (Negation) o; - return operand.compareTo(that.operand); - } - - @Override - protected boolean equalsImpl(Formula o) { - Negation that = (Negation) o; - return operand.equals(that.operand); + public List children() { + return List.of(operand); } @Override @@ -88,7 +76,12 @@ public class Negation extends Formula.LogicalOperator { } @Override - public Formula substitute(Function substitution) { + public Formula temporalStep(BitSet valuation) { + return new Negation(operand.temporalStep(valuation)); + } + + @Override + public Formula substitute(Function substitution) { throw new UnsupportedOperationException("this is not supported"); } } diff --git a/src/main/java/owl/ltl/PropositionalFormula.java b/src/main/java/owl/ltl/PropositionalFormula.java deleted file mode 100644 index 9c07e66a02a9cbad60e05077b340767a104bcfd9..0000000000000000000000000000000000000000 --- a/src/main/java/owl/ltl/PropositionalFormula.java +++ /dev/null @@ -1,207 +0,0 @@ -/* - * 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 . - */ - -package owl.ltl; - -import static java.util.Spliterator.DISTINCT; -import static java.util.Spliterator.IMMUTABLE; -import static java.util.Spliterator.NONNULL; -import static java.util.Spliterator.ORDERED; -import static java.util.Spliterator.SIZED; -import static java.util.Spliterator.SORTED; - -import com.google.common.collect.Comparators; -import java.util.AbstractSet; -import java.util.ArrayList; -import java.util.Collections; -import java.util.Comparator; -import java.util.Iterator; -import java.util.List; -import java.util.Objects; -import java.util.Set; -import java.util.SortedSet; -import java.util.Spliterator; -import java.util.Spliterators; -import java.util.function.Consumer; -import java.util.function.Function; -import java.util.stream.Collectors; -import java.util.stream.Stream; -import owl.collections.Collections3; - -public abstract class PropositionalFormula extends Formula.LogicalOperator { - - public final SortedSet children; - private final List childrenDistinctSortedList; - - PropositionalFormula(Class clazz, Set children) { - super(Objects.hash(clazz, children)); - var sortedList = new ArrayList<>(children); - sortedList.sort(Formula::compareTo); - this.childrenDistinctSortedList = List.copyOf(sortedList); - this.children = new DistinctListAsSortedSet(childrenDistinctSortedList); - } - - public static Formula shortCircuit(Formula formula) { - if (formula instanceof Conjunction) { - Conjunction conjunction = (Conjunction) formula; - - if (conjunction.children.stream().anyMatch(x -> conjunction.children.contains(x.not()))) { - return BooleanConstant.FALSE; - } - } - - if (formula instanceof Disjunction) { - Disjunction disjunction = (Disjunction) formula; - - if (disjunction.children.stream().anyMatch(x -> disjunction.children.contains(x.not()))) { - return BooleanConstant.TRUE; - } - } - - return formula; - } - - @Override - public SortedSet children() { - return children; - } - - @Override - public boolean isPureEventual() { - return children.stream().allMatch(Formula::isPureEventual); - } - - @Override - public boolean isPureUniversal() { - return children.stream().allMatch(Formula::isPureUniversal); - } - - public Stream map(Function mapper) { - return children.stream().map(mapper); - } - - @Override - public String toString() { - return children.stream() - .map(Formula::toString) - .collect(Collectors.joining(operatorSymbol(), "(", ")")); - } - - @Override - protected final int compareToImpl(Formula o) { - assert this.getClass().equals(o.getClass()); - PropositionalFormula that = (PropositionalFormula) o; - return Formulas.compare(this.childrenDistinctSortedList, that.childrenDistinctSortedList); - } - - @Override - protected final boolean equalsImpl(Formula o) { - assert this.getClass().equals(o.getClass()); - PropositionalFormula that = (PropositionalFormula) o; - return childrenDistinctSortedList.equals(that.childrenDistinctSortedList); - } - - protected abstract String operatorSymbol(); - - private static class DistinctListAsSortedSet - extends AbstractSet implements SortedSet { - private final List distinctList; - - private DistinctListAsSortedSet(List distinctList) { - this.distinctList = List.copyOf(distinctList); - assert Collections3.isDistinct(this.distinctList); - assert Comparators.isInStrictOrder(this.distinctList, Comparator.naturalOrder()); - } - - @Override - public Comparator comparator() { - return Formula::compareTo; - } - - @Override - public boolean contains(Object element) { - if (element instanceof Formula) { - int index = index((Formula) element); - return 0 <= index && index < size(); - } - - return false; - } - - @Override - public Object[] toArray() { - return distinctList.toArray(); - } - - @Override - public T[] toArray(T[] array) { - return distinctList.toArray(array); - } - - @Override - public void forEach(Consumer action) { - distinctList.forEach(action); - } - - @Override - public SortedSet subSet(Formula fromElement, Formula toElement) { - throw new UnsupportedOperationException("Not yet implemented."); - } - - @Override - public SortedSet headSet(Formula toElement) { - throw new UnsupportedOperationException("Not yet implemented."); - } - - @Override - public SortedSet tailSet(Formula fromElement) { - throw new UnsupportedOperationException("Not yet implemented."); - } - - @Override - public Formula first() { - return distinctList.get(0); - } - - @Override - public Formula last() { - return distinctList.get(size() - 1); - } - - @Override - public Spliterator spliterator() { - return Spliterators.spliterator(distinctList.iterator(), size(), - SIZED | DISTINCT | SORTED | ORDERED | NONNULL | IMMUTABLE); - } - - @Override - public Iterator iterator() { - return distinctList.iterator(); - } - - @Override - public int size() { - return distinctList.size(); - } - - private int index(Formula formula) { - return Collections.binarySearch(distinctList, formula); - } - } -} diff --git a/src/main/java/owl/ltl/ROperator.java b/src/main/java/owl/ltl/ROperator.java index dd56d3668ca20b3efef22d630bb568e8138bdbbe..257559745858e31d0a60bbbb711a69ebfd5c84a7 100644 --- a/src/main/java/owl/ltl/ROperator.java +++ b/src/main/java/owl/ltl/ROperator.java @@ -19,7 +19,6 @@ package owl.ltl; -import java.util.BitSet; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; @@ -28,7 +27,7 @@ import owl.util.annotation.CEntryPoint; /** * Weak Release. */ -public final class ROperator extends BinaryModalOperator { +public final class ROperator extends Formula.BinaryTemporalOperator { public ROperator(Formula leftOperand, Formula rightOperand) { super(ROperator.class, leftOperand, rightOperand); @@ -99,10 +98,4 @@ public final class ROperator extends BinaryModalOperator { public Formula unfold() { return Conjunction.of(right.unfold(), Disjunction.of(left.unfold(), this)); } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return Conjunction.of(right.unfoldTemporalStep(valuation), - Disjunction.of(left.unfoldTemporalStep(valuation), this)); - } } diff --git a/src/main/java/owl/ltl/UOperator.java b/src/main/java/owl/ltl/UOperator.java index 0801211efd638451b49042354d96f9a800f20811..95ce9926f9a7e69db9d6a729165441d6b6b95f19 100644 --- a/src/main/java/owl/ltl/UOperator.java +++ b/src/main/java/owl/ltl/UOperator.java @@ -19,7 +19,6 @@ package owl.ltl; -import java.util.BitSet; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; @@ -28,7 +27,7 @@ import owl.util.annotation.CEntryPoint; /** * Strong Until. */ -public final class UOperator extends BinaryModalOperator { +public final class UOperator extends Formula.BinaryTemporalOperator { public UOperator(Formula leftOperand, Formula rightOperand) { super(UOperator.class, leftOperand, rightOperand); @@ -99,10 +98,4 @@ public final class UOperator extends BinaryModalOperator { public Formula unfold() { return Disjunction.of(right.unfold(), Conjunction.of(left.unfold(), this)); } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return Disjunction.of(right.unfoldTemporalStep(valuation), - Conjunction.of(left.unfoldTemporalStep(valuation), this)); - } } diff --git a/src/main/java/owl/ltl/UnaryModalOperator.java b/src/main/java/owl/ltl/UnaryModalOperator.java deleted file mode 100644 index 25d45ee2f4c569cb49b5060f283d02413846941b..0000000000000000000000000000000000000000 --- a/src/main/java/owl/ltl/UnaryModalOperator.java +++ /dev/null @@ -1,58 +0,0 @@ -/* - * 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 . - */ - -package owl.ltl; - -import java.util.Objects; -import java.util.Set; - -public abstract class UnaryModalOperator extends Formula.ModalOperator { - public final Formula operand; - - UnaryModalOperator(Class clazz, Formula operand) { - super(Objects.hash(clazz, operand)); - this.operand = operand; - } - - @Override - public Set children() { - return Set.of(operand); - } - - public abstract String operatorSymbol(); - - @Override - public String toString() { - return operatorSymbol() + operand; - } - - @Override - protected int compareToImpl(Formula o) { - assert this.getClass() == o.getClass(); - UnaryModalOperator that = (UnaryModalOperator) o; - return operand.compareTo(that.operand); - } - - @Override - protected boolean equalsImpl(Formula o) { - assert this.getClass() == o.getClass(); - UnaryModalOperator that = (UnaryModalOperator) o; - return operand.equals(that.operand); - } -} diff --git a/src/main/java/owl/ltl/WOperator.java b/src/main/java/owl/ltl/WOperator.java index 926d464682251dca7e32e8ad59789b4fb1fb3114..135539aac5aada5ef73b12c9a182be72f018de0a 100644 --- a/src/main/java/owl/ltl/WOperator.java +++ b/src/main/java/owl/ltl/WOperator.java @@ -19,7 +19,6 @@ package owl.ltl; -import java.util.BitSet; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; @@ -28,7 +27,7 @@ import owl.util.annotation.CEntryPoint; /** * Weak Until. */ -public final class WOperator extends BinaryModalOperator { +public final class WOperator extends Formula.BinaryTemporalOperator { public WOperator(Formula leftOperand, Formula rightOperand) { super(WOperator.class, leftOperand, rightOperand); @@ -99,10 +98,4 @@ public final class WOperator extends BinaryModalOperator { public Formula unfold() { return Disjunction.of(right.unfold(), Conjunction.of(left.unfold(), this)); } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return Disjunction.of(right.unfoldTemporalStep(valuation), - Conjunction.of(left.unfoldTemporalStep(valuation), this)); - } } diff --git a/src/main/java/owl/ltl/XOperator.java b/src/main/java/owl/ltl/XOperator.java index a82f66918f6362720e0fc35c2565e5eca7b827d4..34410a5808cca1265b0da76019b43467b27a21d5 100644 --- a/src/main/java/owl/ltl/XOperator.java +++ b/src/main/java/owl/ltl/XOperator.java @@ -20,7 +20,6 @@ package owl.ltl; import com.google.common.base.Preconditions; -import java.util.BitSet; import owl.ltl.visitors.BinaryVisitor; import owl.ltl.visitors.IntVisitor; import owl.ltl.visitors.Visitor; @@ -29,7 +28,7 @@ import owl.util.annotation.CEntryPoint; /** * Next. */ -public final class XOperator extends UnaryModalOperator { +public final class XOperator extends Formula.UnaryTemporalOperator { public XOperator(Formula operand) { super(XOperator.class, operand); @@ -119,9 +118,4 @@ public final class XOperator extends UnaryModalOperator { public Formula unfold() { return this; } - - @Override - public Formula unfoldTemporalStep(BitSet valuation) { - return temporalStep(valuation); - } } diff --git a/src/main/java/owl/ltl/algorithms/LanguageAnalysis.java b/src/main/java/owl/ltl/algorithms/LanguageAnalysis.java index 056e1cf6a9ea8ba818f802b3b54c313e6acb1c0e..0f82ad1a6ccc5cecc6c36149f326d40761cfeb18 100644 --- a/src/main/java/owl/ltl/algorithms/LanguageAnalysis.java +++ b/src/main/java/owl/ltl/algorithms/LanguageAnalysis.java @@ -35,7 +35,7 @@ public final class LanguageAnalysis { public static boolean isSatisfiable(Formula formula) { if (formula instanceof Disjunction) { - return ((Disjunction) formula).children.stream().anyMatch(LanguageAnalysis::isSatisfiable); + return formula.children().stream().anyMatch(LanguageAnalysis::isSatisfiable); } var labelledFormula = attachDummyAlphabet(formula); diff --git a/src/main/java/owl/ltl/ltlf/LtlfToLtlTranslator.java b/src/main/java/owl/ltl/ltlf/LtlfToLtlTranslator.java index 3520f28fde1fc2eff5c5f764258eb23edd163053..d612840bd21b288d89c6d80009ea9bf8a531d7f6 100644 --- a/src/main/java/owl/ltl/ltlf/LtlfToLtlTranslator.java +++ b/src/main/java/owl/ltl/ltlf/LtlfToLtlTranslator.java @@ -65,12 +65,12 @@ public final class LtlfToLtlTranslator { @Override public Formula visit(Conjunction conjunction) { - return Conjunction.of(conjunction.children.stream().map(x -> x.accept(this))); + return Conjunction.of(conjunction.map(x -> x.accept(this))); } @Override public Formula visit(Disjunction disjunction) { - return Disjunction.of(disjunction.children.stream().map(x -> x.accept(this))); + return Disjunction.of(disjunction.map(x -> x.accept(this))); } @Override diff --git a/src/main/java/owl/ltl/ltlf/PreprocessorVisitor.java b/src/main/java/owl/ltl/ltlf/PreprocessorVisitor.java index 768cd41cbfb3e9ef82ce07be2ebfd5fdc474e68e..8c755a64c9aafea9d37005a1279c5b601345c55e 100644 --- a/src/main/java/owl/ltl/ltlf/PreprocessorVisitor.java +++ b/src/main/java/owl/ltl/ltlf/PreprocessorVisitor.java @@ -1,6 +1,5 @@ package owl.ltl.ltlf; -import owl.collections.Collections3; import owl.ltl.Biconditional; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; @@ -42,14 +41,12 @@ public class PreprocessorVisitor implements Visitor { @Override public Formula visit(Conjunction conjunction) { - return new Conjunction( - Collections3.transformSet(conjunction.children(), x -> x.accept(this))); + return new Conjunction(conjunction.map(x -> x.accept(this))); } @Override public Formula visit(Disjunction disjunction) { - return new Disjunction( - Collections3.transformSet(disjunction.children(), x -> x.accept(this))); + return new Disjunction(disjunction.map(x -> x.accept(this))); } @Override diff --git a/src/main/java/owl/ltl/rewriter/DeduplicationRewriter.java b/src/main/java/owl/ltl/rewriter/DeduplicationRewriter.java index c21a2e26490902c4b228efcb02f1c6a03e32ab04..1d42b96aa15e29672f6d1917bfb0e14dccecb410 100644 --- a/src/main/java/owl/ltl/rewriter/DeduplicationRewriter.java +++ b/src/main/java/owl/ltl/rewriter/DeduplicationRewriter.java @@ -22,6 +22,7 @@ package owl.ltl.rewriter; import java.util.HashMap; import java.util.Map; import java.util.function.Supplier; +import java.util.function.UnaryOperator; import owl.ltl.Biconditional; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; @@ -37,7 +38,7 @@ import owl.ltl.WOperator; import owl.ltl.XOperator; import owl.ltl.visitors.Visitor; -public final class DeduplicationRewriter implements Visitor { +public final class DeduplicationRewriter implements Visitor, UnaryOperator { // TODO Static + Concurrent / Cache? private final Map map = new HashMap<>(); diff --git a/src/main/java/owl/ltl/rewriter/NormalForms.java b/src/main/java/owl/ltl/rewriter/NormalForms.java index 7f691cb765cacb345e890e43cb55e896434058a3..d441821ea08b4e0578871f7c43a55d5ad49ea0b3 100644 --- a/src/main/java/owl/ltl/rewriter/NormalForms.java +++ b/src/main/java/owl/ltl/rewriter/NormalForms.java @@ -39,16 +39,18 @@ import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; import owl.ltl.Formula; -import owl.ltl.PropositionalFormula; +import owl.ltl.Literal; import owl.ltl.SyntacticFragments; import owl.ltl.visitors.PropositionalVisitor; public final class NormalForms { - public static final Function> SYNTHETIC_CO_SAFETY_LITERAL = - x -> x.children.stream().filter(SyntacticFragments::isCoSafety).collect(toSet()); + public static final Function> + SYNTHETIC_CO_SAFETY_LITERAL = + x -> x.children.stream().filter(SyntacticFragments::isCoSafety).collect(toSet()); - public static final Function> SYNTHETIC_SAFETY_LITERAL = - x -> x.children.stream().filter(SyntacticFragments::isSafety).collect(toSet()); + public static final Function> + SYNTHETIC_SAFETY_LITERAL = + x -> x.children.stream().filter(SyntacticFragments::isSafety).collect(toSet()); private NormalForms() {} @@ -63,7 +65,8 @@ public final class NormalForms { } public static Set> toCnf(Formula formula, - Function> syntheticLiteralFactory) { + Function> syntheticLiteralFactory) { var visitor = new ConjunctiveNormalFormVisitor(syntheticLiteralFactory); var cnf = formula.accept(visitor).representatives(); return new ClausesView(cnf, visitor.literals()); @@ -80,7 +83,8 @@ public final class NormalForms { } public static Set> toDnf(Formula formula, - Function> syntheticLiteralFactory) { + Function> syntheticLiteralFactory) { var visitor = new DisjunctiveNormalFormVisitor(syntheticLiteralFactory); var dnf = formula.accept(visitor).representatives(); return new ClausesView(dnf, visitor.literals()); @@ -89,11 +93,11 @@ public final class NormalForms { private abstract static class AbstractNormalFormVisitor extends PropositionalVisitor { - final Function> + final Function> syntheticLiteralFactory; private final Map literals; - private AbstractNormalFormVisitor(Function> syntheticLiteralFactory) { this.literals = new LinkedHashMap<>(); this.syntheticLiteralFactory = syntheticLiteralFactory; @@ -110,14 +114,19 @@ public final class NormalForms { } @Override - protected UpwardClosedSet visit(Formula.TemporalOperator literal) { + public UpwardClosedSet visit(Literal literal) { return singleton(literal); } + + @Override + protected UpwardClosedSet visit(Formula.Temporal temporalOperator) { + return singleton(temporalOperator); + } } private static final class ConjunctiveNormalFormVisitor extends AbstractNormalFormVisitor { - private ConjunctiveNormalFormVisitor(Function> syntheticLiteralFactory) { super(syntheticLiteralFactory); } @@ -166,7 +175,7 @@ public final class NormalForms { private static final class DisjunctiveNormalFormVisitor extends AbstractNormalFormVisitor { - private DisjunctiveNormalFormVisitor(Function> syntheticLiteralFactory) { super(syntheticLiteralFactory); } diff --git a/src/main/java/owl/ltl/rewriter/PullUpXVisitor.java b/src/main/java/owl/ltl/rewriter/PullUpXVisitor.java index 71c3b2029e2f1a999ed75df61ad992a6ebe258e6..19b4ae5a07d0014b18614b7c439dfb14aed28fd1 100644 --- a/src/main/java/owl/ltl/rewriter/PullUpXVisitor.java +++ b/src/main/java/owl/ltl/rewriter/PullUpXVisitor.java @@ -19,13 +19,11 @@ package owl.ltl.rewriter; -import java.util.List; import java.util.function.BiFunction; import java.util.function.Function; import java.util.function.UnaryOperator; import java.util.stream.Collectors; import owl.ltl.Biconditional; -import owl.ltl.BinaryModalOperator; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; @@ -36,7 +34,6 @@ import owl.ltl.Literal; import owl.ltl.MOperator; import owl.ltl.ROperator; import owl.ltl.UOperator; -import owl.ltl.UnaryModalOperator; import owl.ltl.WOperator; import owl.ltl.XOperator; import owl.ltl.visitors.Visitor; @@ -62,14 +59,16 @@ public final class PullUpXVisitor implements Visitor { @Override public XFormula visit(Conjunction conjunction) { - List children = conjunction.map(c -> c.accept(this)).collect(Collectors.toList()); + var children = conjunction.children().stream() + .map(c -> c.accept(this)).collect(Collectors.toList()); int depth = children.stream().mapToInt(c -> c.depth).min().orElse(0); return new XFormula(depth, Conjunction.of(children.stream().map(c -> c.toFormula(depth)))); } @Override public XFormula visit(Disjunction disjunction) { - List children = disjunction.map(c -> c.accept(this)).collect(Collectors.toList()); + var children = disjunction.children().stream() + .map(c -> c.accept(this)).collect(Collectors.toList()); int depth = children.stream().mapToInt(c -> c.depth).min().orElse(0); return new XFormula(depth, Disjunction.of(children.stream().map(c -> c.toFormula(depth)))); } @@ -116,7 +115,7 @@ public final class PullUpXVisitor implements Visitor { return r; } - private XFormula visit(BinaryModalOperator operator, + private XFormula visit(Formula.BinaryTemporalOperator operator, BiFunction constructor) { XFormula right = operator.right.accept(this); XFormula left = operator.left.accept(this); @@ -125,7 +124,8 @@ public final class PullUpXVisitor implements Visitor { return left; } - private XFormula visit(UnaryModalOperator operator, Function constructor) { + private XFormula visit(Formula.UnaryTemporalOperator operator, + Function constructor) { XFormula formula = operator.operand.accept(this); formula.formula = constructor.apply(formula.formula); return formula; diff --git a/src/main/java/owl/ltl/rewriter/SyntacticFairnessSimplifier.java b/src/main/java/owl/ltl/rewriter/SyntacticFairnessSimplifier.java index f395dd341fe04d721105cb71e3a3e20301fca9a9..f5ebb55bb5ad41d171bc5b4aa519ca856a05c7b0 100644 --- a/src/main/java/owl/ltl/rewriter/SyntacticFairnessSimplifier.java +++ b/src/main/java/owl/ltl/rewriter/SyntacticFairnessSimplifier.java @@ -19,10 +19,9 @@ package owl.ltl.rewriter; -import com.google.common.collect.Sets; +import com.google.common.collect.Lists; import java.util.ArrayList; import java.util.List; -import java.util.Set; import java.util.function.Predicate; import java.util.function.UnaryOperator; import javax.annotation.Nullable; @@ -34,7 +33,6 @@ import owl.ltl.Formula; import owl.ltl.GOperator; import owl.ltl.Literal; import owl.ltl.MOperator; -import owl.ltl.PropositionalFormula; import owl.ltl.ROperator; import owl.ltl.SyntacticFragment; import owl.ltl.UOperator; @@ -130,6 +128,26 @@ class SyntacticFairnessSimplifier implements UnaryOperator { throw new AssertionError("Unreachable"); } + private static Formula shortCircuit(Formula formula) { + if (formula instanceof Conjunction) { + Conjunction conjunction = (Conjunction) formula; + + if (conjunction.children.stream().anyMatch(x -> conjunction.children.contains(x.not()))) { + return BooleanConstant.FALSE; + } + } + + if (formula instanceof Disjunction) { + Disjunction disjunction = (Disjunction) formula; + + if (disjunction.children.stream().anyMatch(x -> disjunction.children.contains(x.not()))) { + return BooleanConstant.TRUE; + } + } + + return formula; + } + private static final class AlmostAllVisitor implements Visitor { private static Formula wrap(Formula formula) { @@ -148,22 +166,22 @@ class SyntacticFairnessSimplifier implements UnaryOperator { @Override public Formula visit(Conjunction conjunction) { if (SyntacticFragment.FINITE.contains(conjunction)) { - return wrap(PropositionalFormula.shortCircuit(conjunction)); + return wrap(shortCircuit(conjunction)); } - return PropositionalFormula.shortCircuit( + return shortCircuit( Conjunction.of(conjunction.map(x -> x.accept(this)))); } @Override public Formula visit(Disjunction disjunction) { if (SyntacticFragment.FINITE.contains(disjunction)) { - return wrap(PropositionalFormula.shortCircuit(disjunction)); + return wrap(shortCircuit(disjunction)); } List disjuncts = new ArrayList<>(); List xFragment = new ArrayList<>(); - List> conjuncts = new ArrayList<>(); + List> conjuncts = new ArrayList<>(); disjunction.children.forEach(child -> { if (child instanceof FOperator) { @@ -174,16 +192,16 @@ class SyntacticFairnessSimplifier implements UnaryOperator { xFragment.add(child); } else { assert child instanceof Conjunction; - conjuncts.add(((PropositionalFormula) child).children); + conjuncts.add(child.children()); } }); - conjuncts.add(Set.of(Disjunction.of(xFragment))); - Formula conjunction = Conjunction.of(Sets.cartesianProduct(conjuncts).stream() + conjuncts.add(List.of(Disjunction.of(xFragment))); + Formula conjunction = Conjunction.of(Lists.cartesianProduct(conjuncts).stream() .map(Disjunction::of)); disjuncts.add(conjunction.accept(this)); - return PropositionalFormula.shortCircuit(Disjunction.of(disjuncts)); + return shortCircuit(Disjunction.of(disjuncts)); } @Override @@ -225,12 +243,12 @@ class SyntacticFairnessSimplifier implements UnaryOperator { @Override public Formula visit(Conjunction conjunction) { if (SyntacticFragment.FINITE.contains(conjunction)) { - return wrap(PropositionalFormula.shortCircuit(conjunction)); + return wrap(shortCircuit(conjunction)); } List conjuncts = new ArrayList<>(); List xFragment = new ArrayList<>(); - List> disjuncts = new ArrayList<>(); + List> disjuncts = new ArrayList<>(); conjunction.children.forEach(child -> { if (child instanceof FOperator) { @@ -241,25 +259,25 @@ class SyntacticFairnessSimplifier implements UnaryOperator { xFragment.add(child); } else { assert child instanceof Disjunction; - disjuncts.add(((PropositionalFormula) child).children); + disjuncts.add(child.children()); } }); - disjuncts.add(Set.of(Conjunction.of(xFragment))); + disjuncts.add(List.of(Conjunction.of(xFragment))); Formula disjunction = Disjunction.of( - Sets.cartesianProduct(disjuncts).stream().map(Conjunction::of)); + Lists.cartesianProduct(disjuncts).stream().map(Conjunction::of)); conjuncts.add(disjunction.accept(this)); - return PropositionalFormula.shortCircuit(Conjunction.of(conjuncts)); + return shortCircuit(Conjunction.of(conjuncts)); } @Override public Formula visit(Disjunction disjunction) { if (SyntacticFragment.FINITE.contains(disjunction)) { - return wrap(PropositionalFormula.shortCircuit(disjunction)); + return wrap(shortCircuit(disjunction)); } - return PropositionalFormula.shortCircuit( + return shortCircuit( Disjunction.of(disjunction.map(x -> x.accept(this)))); } diff --git a/src/main/java/owl/ltl/rewriter/SyntacticSimplifier.java b/src/main/java/owl/ltl/rewriter/SyntacticSimplifier.java index e7ef795fc68246cd1334ef8d7f104b75d04be35c..6cf249f022b90ff8350f0b84e3fa30f4865986e3 100644 --- a/src/main/java/owl/ltl/rewriter/SyntacticSimplifier.java +++ b/src/main/java/owl/ltl/rewriter/SyntacticSimplifier.java @@ -28,7 +28,6 @@ import java.util.function.UnaryOperator; import java.util.stream.Collectors; import owl.collections.Collections3; import owl.ltl.Biconditional; -import owl.ltl.BinaryModalOperator; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; @@ -37,7 +36,6 @@ import owl.ltl.Formula; import owl.ltl.GOperator; import owl.ltl.Literal; import owl.ltl.MOperator; -import owl.ltl.PropositionalFormula; import owl.ltl.ROperator; import owl.ltl.UOperator; import owl.ltl.WOperator; @@ -73,7 +71,7 @@ final class SyntacticSimplifier implements Visitor, UnaryOperator newConjunction = conjunction.map(x -> x.accept(this)).collect(Collectors.toSet()); + Set newConjunction = new HashSet<>(conjunction.map(x -> x.accept(this))); // Short-circuit conjunction if it contains x and !x. if (newConjunction.stream().anyMatch(x -> newConjunction.contains(x.not()))) { @@ -109,14 +107,16 @@ final class SyntacticSimplifier implements Visitor, UnaryOperator x instanceof UOperator || x instanceof WOperator)) { if (newConjunction.contains(operator.right)) { newConjunction.remove(operator); } } - for (BinaryModalOperator operator : filter(newConjunction, BinaryModalOperator.class, + for (Formula.BinaryTemporalOperator operator + : filter(newConjunction, Formula.BinaryTemporalOperator.class, x -> x instanceof MOperator || x instanceof ROperator)) { if (newConjunction.contains(operator.left)) { newConjunction.remove(operator); @@ -137,7 +137,7 @@ final class SyntacticSimplifier implements Visitor, UnaryOperator newDisjunction = disjunction.map(x -> x.accept(this)).collect(Collectors.toSet()); + Set newDisjunction = new HashSet<>(disjunction.map(x -> x.accept(this))); // Short-circuit disjunction if it contains x and !x. if (newDisjunction.stream().anyMatch(x -> newDisjunction.contains(x.not()))) { @@ -173,15 +173,17 @@ final class SyntacticSimplifier implements Visitor, UnaryOperator x instanceof MOperator || x instanceof ROperator)) { + for (Formula.BinaryTemporalOperator operator : + filter(newDisjunction, Formula.BinaryTemporalOperator.class, + x -> x instanceof MOperator || x instanceof ROperator)) { if (newDisjunction.contains(operator.right)) { newDisjunction.remove(operator); } } - for (BinaryModalOperator operator : filter(newDisjunction, BinaryModalOperator.class, - x -> x instanceof UOperator || x instanceof WOperator)) { + for (Formula.BinaryTemporalOperator operator : + filter(newDisjunction, Formula.BinaryTemporalOperator.class, + x -> x instanceof UOperator || x instanceof WOperator)) { if (newDisjunction.contains(operator.left)) { newDisjunction.remove(operator); newDisjunction.add(operator.right); @@ -488,10 +490,10 @@ final class SyntacticSimplifier implements Visitor, UnaryOperator suspendable = ((PropositionalFormula) operand).children.stream().filter( - Formula::isSuspendable).collect(Collectors.toSet()); - Set others = Sets.difference(((PropositionalFormula) operand).children, suspendable); + if (operand instanceof Formula.NaryPropositionalFormula) { + Set suspendable = operand.children() + .stream().filter(Formula::isSuspendable).collect(Collectors.toSet()); + Set others = Sets.difference(new HashSet<>(operand.children()), suspendable); if (!suspendable.isEmpty()) { if (operand instanceof Conjunction) { @@ -517,13 +519,12 @@ final class SyntacticSimplifier implements Visitor, UnaryOperator true); } - @SuppressWarnings("unchecked") private static Set filter(Collection iterator, Class clazz, Predicate predicate) { Set operators = new HashSet<>(); iterator.forEach(x -> { - if (clazz.isInstance(x) && predicate.test((T) x)) { - operators.add((T) x); + if (clazz.isInstance(x) && predicate.test(clazz.cast(x))) { + operators.add(clazz.cast(x)); } }); diff --git a/src/main/java/owl/ltl/util/FormulaIsomorphism.java b/src/main/java/owl/ltl/util/FormulaIsomorphism.java index 82a280ac8e81427203ec4e5dc19205eb50f1ae2d..d4dd8314ef9efe6694d799624a354323709d7f5c 100644 --- a/src/main/java/owl/ltl/util/FormulaIsomorphism.java +++ b/src/main/java/owl/ltl/util/FormulaIsomorphism.java @@ -20,7 +20,6 @@ package owl.ltl.util; import com.google.common.collect.Collections2; -import java.util.ArrayList; import java.util.Arrays; import java.util.BitSet; import java.util.List; @@ -28,7 +27,6 @@ import java.util.stream.Collectors; import javax.annotation.Nullable; import owl.collections.Collections3; import owl.ltl.Biconditional; -import owl.ltl.BinaryModalOperator; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; @@ -37,10 +35,8 @@ import owl.ltl.Formula; import owl.ltl.GOperator; import owl.ltl.Literal; import owl.ltl.MOperator; -import owl.ltl.PropositionalFormula; import owl.ltl.ROperator; import owl.ltl.UOperator; -import owl.ltl.UnaryModalOperator; import owl.ltl.WOperator; import owl.ltl.XOperator; import owl.ltl.visitors.BinaryVisitor; @@ -116,22 +112,22 @@ public final class FormulaIsomorphism { @Override public Boolean visit(Conjunction conjunction, Formula formula) { - return visitPropositionalOperator(conjunction, formula); + return visitNaryPropositionalOperator(conjunction, formula); } @Override public Boolean visit(Disjunction disjunction, Formula formula) { - return visitPropositionalOperator(disjunction, formula); + return visitNaryPropositionalOperator(disjunction, formula); } @Override public Boolean visit(FOperator fOperator, Formula formula) { - return visitUnaryOperator(fOperator, formula); + return visitTemporal(fOperator, formula); } @Override public Boolean visit(GOperator gOperator, Formula formula) { - return visitUnaryOperator(gOperator, formula); + return visitTemporal(gOperator, formula); } @Override @@ -151,60 +147,67 @@ public final class FormulaIsomorphism { @Override public Boolean visit(MOperator mOperator, Formula formula) { - return visitBinaryOperator(mOperator, formula); + return visitTemporal(mOperator, formula); } @Override public Boolean visit(UOperator uOperator, Formula formula) { - return visitBinaryOperator(uOperator, formula); + return visitTemporal(uOperator, formula); } @Override public Boolean visit(ROperator rOperator, Formula formula) { - return visitBinaryOperator(rOperator, formula); + return visitTemporal(rOperator, formula); } @Override public Boolean visit(WOperator wOperator, Formula formula) { - return visitBinaryOperator(wOperator, formula); + return visitTemporal(wOperator, formula); } @Override public Boolean visit(XOperator xOperator, Formula formula) { - return visitUnaryOperator(xOperator, formula); + return visitTemporal(xOperator, formula); } - private Boolean visitUnaryOperator(UnaryModalOperator operator, Formula formula) { - if (!operator.getClass().isInstance(formula)) { + private Boolean visitTemporal(Formula.Temporal formula1, Formula formula2) { + if (!formula1.getClass().isInstance(formula2)) { return Boolean.FALSE; } - return operator.operand.accept(this, ((UnaryModalOperator) formula).operand); - } - - private Boolean visitBinaryOperator(BinaryModalOperator operator, Formula formula) { - if (!operator.getClass().isInstance(formula)) { + if (formula1.height() != formula2.height()) { return Boolean.FALSE; } - return operator.left.accept(this, ((BinaryModalOperator) formula).left) - && operator.right.accept(this, ((BinaryModalOperator) formula).right); + List children1 = formula1.children(); + List children2 = formula2.children(); + + assert children1.size() == children2.size(); + + for (int i = 0; i < children1.size(); i++) { + if (!children1.get(i).accept(this, children2.get(i))) { + return false; + } + } + + return true; } - private Boolean visitPropositionalOperator(PropositionalFormula formula1, Formula formula2) { + private Boolean visitNaryPropositionalOperator(Formula formula1, Formula formula2) { if (!formula1.getClass().isInstance(formula2)) { return Boolean.FALSE; } - PropositionalFormula formula2Casted = (PropositionalFormula) formula2; - - if (formula1.children.size() != formula2Casted.children.size()) { + if (formula1.height() != formula2.height()) { return Boolean.FALSE; } - // TODO, check height. - List children1 = new ArrayList<>(formula1.children); - List children2 = new ArrayList<>(formula2Casted.children); + List children1 = formula1.children(); + List children2 = formula2.children(); + + if (children1.size() != children2.size()) { + return Boolean.FALSE; + } for (List children2Permutation : Collections2.permutations(children2)) { int i = 0; diff --git a/src/main/java/owl/ltl/visitors/LatexPrintVisitor.java b/src/main/java/owl/ltl/visitors/LatexPrintVisitor.java index 80670bfd2925124dea998cdf09ccf46b821ff69b..8f5e8f87c1214f6ba6d402603fb356fc9081d637 100644 --- a/src/main/java/owl/ltl/visitors/LatexPrintVisitor.java +++ b/src/main/java/owl/ltl/visitors/LatexPrintVisitor.java @@ -19,11 +19,11 @@ package owl.ltl.visitors; +import com.google.common.collect.Comparators; +import java.util.Comparator; import java.util.List; -import java.util.Spliterator; import java.util.stream.Collectors; import java.util.stream.Stream; -import owl.ltl.BinaryModalOperator; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; @@ -32,10 +32,8 @@ import owl.ltl.Formula; import owl.ltl.GOperator; import owl.ltl.Literal; import owl.ltl.MOperator; -import owl.ltl.PropositionalFormula; import owl.ltl.ROperator; import owl.ltl.UOperator; -import owl.ltl.UnaryModalOperator; import owl.ltl.WOperator; import owl.ltl.XOperator; @@ -64,12 +62,12 @@ public class LatexPrintVisitor implements Visitor { @Override public String visit(FOperator fOperator) { - return visit((UnaryModalOperator) fOperator); + return visit((Formula.UnaryTemporalOperator) fOperator); } @Override public String visit(GOperator gOperator) { - return visit((UnaryModalOperator) gOperator); + return visit((Formula.UnaryTemporalOperator) gOperator); } @Override @@ -80,38 +78,39 @@ public class LatexPrintVisitor implements Visitor { @Override public String visit(MOperator mOperator) { - return visit((BinaryModalOperator) mOperator); + return visit((Formula.BinaryTemporalOperator) mOperator); } @Override public String visit(ROperator rOperator) { - return visit((BinaryModalOperator) rOperator); + return visit((Formula.BinaryTemporalOperator) rOperator); } @Override public String visit(UOperator uOperator) { - return visit((BinaryModalOperator) uOperator); + return visit((Formula.BinaryTemporalOperator) uOperator); } @Override public String visit(WOperator wOperator) { - return visit((BinaryModalOperator) wOperator); + return visit((Formula.BinaryTemporalOperator) wOperator); } @Override public String visit(XOperator xOperator) { - return visit((UnaryModalOperator) xOperator); + return visit((Formula.UnaryTemporalOperator) xOperator); } - private String visit(UnaryModalOperator operator) { - if (operator.operand instanceof UnaryModalOperator || operator.operand instanceof Literal) { + private String visit(Formula.UnaryTemporalOperator operator) { + if (operator.operand instanceof Formula.UnaryTemporalOperator + || operator.operand instanceof Literal) { return '\\' + operator.operatorSymbol() + ' ' + operator.operand.accept(this); } return '\\' + operator.operatorSymbol() + " (" + operator.operand.accept(this) + ')'; } - private String visit(BinaryModalOperator operator) { + private String visit(Formula.BinaryTemporalOperator operator) { return Stream.of(operator.left, operator.right) .map(x -> { if (x instanceof Literal) { @@ -123,11 +122,12 @@ public class LatexPrintVisitor implements Visitor { .collect(Collectors.joining(" \\" + operator.operatorSymbol() + ' ')); } - private String visit(PropositionalFormula propositionalFormula, String latexString) { // NOPMD - assert propositionalFormula.children.spliterator().hasCharacteristics(Spliterator.SORTED); - return propositionalFormula.children.stream() + private String visit(Formula.NaryPropositionalFormula propositionalFormula, String latexString) { + // NOPMD + assert Comparators.isInStrictOrder(propositionalFormula.children(), Comparator.naturalOrder()); + return propositionalFormula.children().stream() .map(x -> { - if (x instanceof Formula.LogicalOperator && !(x instanceof BooleanConstant)) { + if (x instanceof Formula.Propositional && !(x instanceof BooleanConstant)) { return '(' + x.accept(this) + ')'; } else { return x.accept(this); diff --git a/src/main/java/owl/ltl/visitors/PrintVisitor.java b/src/main/java/owl/ltl/visitors/PrintVisitor.java index ec117fdd79ddb2c93bfdc9a62b597b6c1a178522..f9fcae90cc6c6ededba4e6ccd66ec94e7012f837 100644 --- a/src/main/java/owl/ltl/visitors/PrintVisitor.java +++ b/src/main/java/owl/ltl/visitors/PrintVisitor.java @@ -19,13 +19,12 @@ package owl.ltl.visitors; +import com.google.common.collect.Comparators; +import java.util.Comparator; import java.util.List; -import java.util.Spliterator; import java.util.stream.Collectors; import javax.annotation.Nullable; - import owl.ltl.Biconditional; -import owl.ltl.BinaryModalOperator; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; @@ -38,32 +37,33 @@ import owl.ltl.MOperator; import owl.ltl.Negation; import owl.ltl.ROperator; import owl.ltl.UOperator; -import owl.ltl.UnaryModalOperator; import owl.ltl.WOperator; import owl.ltl.XOperator; public final class PrintVisitor implements Visitor { private final boolean parenthesize; @Nullable - private final List variableMapping; + private final List atomicPropositions; - private PrintVisitor(boolean parenthesize, @Nullable List variableMapping) { - this.variableMapping = variableMapping; + private PrintVisitor(boolean parenthesize, @Nullable List atomicPropositions) { + this.atomicPropositions = atomicPropositions == null + ? atomicPropositions + : List.copyOf(atomicPropositions); this.parenthesize = parenthesize; } - public static String toString(Formula formula, @Nullable List variableMapping) { - return toString(formula, variableMapping, false); + public static String toString(Formula formula, @Nullable List atomicPropositions) { + return toString(formula, atomicPropositions, false); } - public static String toString(Formula formula, @Nullable List variableMapping, + public static String toString(Formula formula, @Nullable List atomicPropositions, boolean parenthesize) { - PrintVisitor visitor = new PrintVisitor(parenthesize, variableMapping); + PrintVisitor visitor = new PrintVisitor(parenthesize, atomicPropositions); return formula.accept(visitor); } public static String toString(LabelledFormula formula, boolean parenthesize) { - PrintVisitor visitor = new PrintVisitor(parenthesize, formula.variables()); + PrintVisitor visitor = new PrintVisitor(parenthesize, formula.atomicPropositions()); return formula.formula().accept(visitor); } @@ -80,7 +80,7 @@ public final class PrintVisitor implements Visitor { @Override public String visit(Conjunction conjunction) { - assert conjunction.children.spliterator().hasCharacteristics(Spliterator.SORTED); + assert Comparators.isInStrictOrder(conjunction.children(), Comparator.naturalOrder()); return '(' + conjunction.children.stream() .map(this::visitParenthesized) .collect(Collectors.joining(" & ")) + ')'; @@ -88,7 +88,7 @@ public final class PrintVisitor implements Visitor { @Override public String visit(Disjunction disjunction) { - assert disjunction.children.spliterator().hasCharacteristics(Spliterator.SORTED); + assert Comparators.isInStrictOrder(disjunction.children(), Comparator.naturalOrder()); return '(' + disjunction.children.stream() .map(this::visitParenthesized) .collect(Collectors.joining(" | ")) + ')'; @@ -96,12 +96,12 @@ public final class PrintVisitor implements Visitor { @Override public String visit(FOperator fOperator) { - return visit((UnaryModalOperator) fOperator); + return visit((Formula.UnaryTemporalOperator) fOperator); } @Override public String visit(GOperator gOperator) { - return visit((UnaryModalOperator) gOperator); + return visit((Formula.UnaryTemporalOperator) gOperator); } @Override @@ -111,42 +111,42 @@ public final class PrintVisitor implements Visitor { @Override public String visit(Literal literal) { - String name = variableMapping == null + String name = atomicPropositions == null ? "p" + literal.getAtom() - : variableMapping.get(literal.getAtom()); + : atomicPropositions.get(literal.getAtom()); return literal.isNegated() ? '!' + name : name; } @Override public String visit(MOperator mOperator) { - return visit((BinaryModalOperator) mOperator); + return visit((Formula.BinaryTemporalOperator) mOperator); } @Override public String visit(ROperator rOperator) { - return visit((BinaryModalOperator) rOperator); + return visit((Formula.BinaryTemporalOperator) rOperator); } @Override public String visit(UOperator uOperator) { - return visit((BinaryModalOperator) uOperator); + return visit((Formula.BinaryTemporalOperator) uOperator); } @Override public String visit(WOperator wOperator) { - return visit((BinaryModalOperator) wOperator); + return visit((Formula.BinaryTemporalOperator) wOperator); } @Override public String visit(XOperator xOperator) { - return visit((UnaryModalOperator) xOperator); + return visit((Formula.UnaryTemporalOperator) xOperator); } - private String visit(UnaryModalOperator operator) { + private String visit(Formula.UnaryTemporalOperator operator) { return operator.operatorSymbol() + visitParenthesized(operator.operand); } - private String visit(BinaryModalOperator operator) { + private String visit(Formula.BinaryTemporalOperator operator) { return "((" + operator.left.accept(this) + ") " + operator.operatorSymbol() + " (" + operator.right.accept(this) + "))"; diff --git a/src/main/java/owl/ltl/visitors/PropositionalIntVisitor.java b/src/main/java/owl/ltl/visitors/PropositionalIntVisitor.java index 479984506af8d41775526806261011371228e97e..5c8e6b9dd720818916c39607a8252213bad51617 100644 --- a/src/main/java/owl/ltl/visitors/PropositionalIntVisitor.java +++ b/src/main/java/owl/ltl/visitors/PropositionalIntVisitor.java @@ -22,7 +22,6 @@ package owl.ltl.visitors; import owl.ltl.FOperator; import owl.ltl.Formula; import owl.ltl.GOperator; -import owl.ltl.Literal; import owl.ltl.MOperator; import owl.ltl.ROperator; import owl.ltl.UOperator; @@ -35,46 +34,41 @@ import owl.ltl.XOperator; */ public abstract class PropositionalIntVisitor implements IntVisitor { - protected abstract int visit(Formula.TemporalOperator formula); + protected abstract int visit(Formula.Temporal formula); @Override public final int visit(FOperator fOperator) { - return this.visit((Formula.TemporalOperator) fOperator); + return this.visit((Formula.Temporal) fOperator); } @Override public final int visit(GOperator gOperator) { - return this.visit((Formula.TemporalOperator) gOperator); - } - - @Override - public final int visit(Literal literal) { - return this.visit((Formula.TemporalOperator) literal); + return this.visit((Formula.Temporal) gOperator); } @Override public final int visit(MOperator mOperator) { - return this.visit((Formula.TemporalOperator) mOperator); + return this.visit((Formula.Temporal) mOperator); } @Override public final int visit(ROperator rOperator) { - return this.visit((Formula.TemporalOperator) rOperator); + return this.visit((Formula.Temporal) rOperator); } @Override public final int visit(UOperator uOperator) { - return this.visit((Formula.TemporalOperator) uOperator); + return this.visit((Formula.Temporal) uOperator); } @Override public final int visit(WOperator wOperator) { - return this.visit((Formula.TemporalOperator) wOperator); + return this.visit((Formula.Temporal) wOperator); } @Override public final int visit(XOperator xOperator) { - return this.visit((Formula.TemporalOperator) xOperator); + return this.visit((Formula.Temporal) xOperator); } } diff --git a/src/main/java/owl/ltl/visitors/PropositionalVisitor.java b/src/main/java/owl/ltl/visitors/PropositionalVisitor.java index ef34f49b971a149198843cd04d111bbb467e3cbc..e595dc4bff2ee5065cc3ac7a98979549a7510a56 100644 --- a/src/main/java/owl/ltl/visitors/PropositionalVisitor.java +++ b/src/main/java/owl/ltl/visitors/PropositionalVisitor.java @@ -22,7 +22,6 @@ package owl.ltl.visitors; import owl.ltl.FOperator; import owl.ltl.Formula; import owl.ltl.GOperator; -import owl.ltl.Literal; import owl.ltl.MOperator; import owl.ltl.ROperator; import owl.ltl.UOperator; @@ -35,45 +34,40 @@ import owl.ltl.XOperator; */ public abstract class PropositionalVisitor implements Visitor { - protected abstract T visit(Formula.TemporalOperator formula); + protected abstract T visit(Formula.Temporal formula); @Override public final T visit(FOperator fOperator) { - return this.visit((Formula.TemporalOperator) fOperator); + return this.visit((Formula.Temporal) fOperator); } @Override public final T visit(GOperator gOperator) { - return this.visit((Formula.TemporalOperator) gOperator); - } - - @Override - public final T visit(Literal literal) { - return this.visit((Formula.TemporalOperator) literal); + return this.visit((Formula.Temporal) gOperator); } @Override public final T visit(MOperator mOperator) { - return this.visit((Formula.TemporalOperator) mOperator); + return this.visit((Formula.Temporal) mOperator); } @Override public final T visit(ROperator rOperator) { - return this.visit((Formula.TemporalOperator) rOperator); + return this.visit((Formula.Temporal) rOperator); } @Override public final T visit(UOperator uOperator) { - return this.visit((Formula.TemporalOperator) uOperator); + return this.visit((Formula.Temporal) uOperator); } @Override public final T visit(WOperator wOperator) { - return this.visit((Formula.TemporalOperator) wOperator); + return this.visit((Formula.Temporal) wOperator); } @Override public final T visit(XOperator xOperator) { - return this.visit((Formula.TemporalOperator) xOperator); + return this.visit((Formula.Temporal) xOperator); } } diff --git a/src/main/java/owl/ltl/visitors/XDepthVisitor.java b/src/main/java/owl/ltl/visitors/XDepthVisitor.java index 7cd603cb71a5a581a5d3a9a0fa94e83854eab6fe..b3605d6705d50ff593616bd469245c3c856d29fa 100644 --- a/src/main/java/owl/ltl/visitors/XDepthVisitor.java +++ b/src/main/java/owl/ltl/visitors/XDepthVisitor.java @@ -29,7 +29,6 @@ import owl.ltl.FOperator; import owl.ltl.Formula; import owl.ltl.GOperator; import owl.ltl.Literal; -import owl.ltl.PropositionalFormula; import owl.ltl.XOperator; public class XDepthVisitor implements IntVisitor { @@ -67,13 +66,13 @@ public class XDepthVisitor implements IntVisitor { @Nonnegative @Override public int visit(Conjunction conjunction) { - return visit((PropositionalFormula) conjunction); + return visit((Formula.NaryPropositionalFormula) conjunction); } @Nonnegative @Override public int visit(Disjunction disjunction) { - return visit((PropositionalFormula) disjunction); + return visit((Formula.NaryPropositionalFormula) disjunction); } @Nonnegative @@ -89,7 +88,7 @@ public class XDepthVisitor implements IntVisitor { } @Nonnegative - private int visit(PropositionalFormula formula) { + private int visit(Formula.NaryPropositionalFormula formula) { int max = 0; for (Formula child : formula.children) { diff --git a/src/main/java/owl/run/Environment.java b/src/main/java/owl/run/Environment.java index e89bc01688f634206b137dcb773fe7bd92c9161a..4a8b0e83fb5b966546cbd89c2bc6fa51c0c1da8e 100644 --- a/src/main/java/owl/run/Environment.java +++ b/src/main/java/owl/run/Environment.java @@ -33,7 +33,7 @@ public abstract class Environment { public abstract boolean annotations(); public FactorySupplier factorySupplier() { - return JBddSupplier.async(annotations()); + return JBddSupplier.async(); } public static Environment of(boolean annotated) { diff --git a/src/main/java/owl/translations/BlockingElements.java b/src/main/java/owl/translations/BlockingElements.java index 4accbcdfc4172030f1282c826f999e274c2dbbbd..5bc5a1d922fa77340b1db0da29357314bcc3598e 100644 --- a/src/main/java/owl/translations/BlockingElements.java +++ b/src/main/java/owl/translations/BlockingElements.java @@ -14,8 +14,8 @@ import owl.translations.mastertheorem.Predicates; public class BlockingElements { private final BitSet atomicPropositions; - private final Set blockingCoSafety; - private final Set blockingSafety; + private final Set blockingCoSafety; + private final Set blockingSafety; public BlockingElements(Formula formula) { this.atomicPropositions = formula.atomicPropositions(true); @@ -26,10 +26,10 @@ public class BlockingElements { var greatestFixpoints = formula.subformulas(Predicates.IS_GREATEST_FIXPOINT); blockingCoSafety = formula.children() .stream() - .filter(x -> x instanceof Formula.ModalOperator + .filter(x -> x instanceof Formula.Temporal && SyntacticFragments.isCoSafety(x) && greatestFixpoints.stream().noneMatch(y -> y.anyMatch(x::equals))) - .map(Formula.ModalOperator.class::cast) + .map(Formula.Temporal.class::cast) .collect(Collectors.toUnmodifiableSet()); } else { blockingCoSafety = Set.of(); @@ -45,10 +45,10 @@ public class BlockingElements { blockingSafety = formula.children() .stream() - .filter(x -> x instanceof Formula.ModalOperator + .filter(x -> x instanceof Formula.Temporal && SyntacticFragments.isSafety(x) && fixpoints.stream().noneMatch(y -> y.anyMatch(x::equals))) - .map(Formula.ModalOperator.class::cast) + .map(Formula.Temporal.class::cast) .collect(Collectors.toUnmodifiableSet()); } else { blockingSafety = Set.of(); @@ -56,17 +56,13 @@ public class BlockingElements { } public boolean isBlockedByCoSafety(EquivalenceClass clazz) { - var modalOperators = clazz.modalOperators(); - - return SyntacticFragments.isCoSafety(modalOperators) + return SyntacticFragments.isCoSafety(clazz.modalOperators()) || clazz.atomicPropositions(true).intersects(atomicPropositions) - || !Collections.disjoint(blockingCoSafety, modalOperators); + || !Collections.disjoint(blockingCoSafety, clazz.modalOperators()); } public boolean isBlockedBySafety(EquivalenceClass clazz) { - var modalOperators = clazz.modalOperators(); - - return SyntacticFragments.isSafety(modalOperators) - || !Collections.disjoint(blockingSafety, modalOperators); + return SyntacticFragments.isSafety(clazz.modalOperators()) + || !Collections.disjoint(blockingSafety, clazz.modalOperators()); } } diff --git a/src/main/java/owl/translations/ExternalTranslator.java b/src/main/java/owl/translations/ExternalTranslator.java index 9b801d958e81449f169c12a8f94e5978ed7ad832..1567e128ab7267b92ab8542153c6aa79aae9e2d9 100644 --- a/src/main/java/owl/translations/ExternalTranslator.java +++ b/src/main/java/owl/translations/ExternalTranslator.java @@ -141,7 +141,8 @@ public class ExternalTranslator try (Reader reader = new BufferedReader( new InputStreamReader(process.getInputStream(), Charset.defaultCharset()))) { FactorySupplier factorySupplier = env.factorySupplier(); - ValuationSetFactory vsFactory = factorySupplier.getValuationSetFactory(formula.variables()); + ValuationSetFactory vsFactory = factorySupplier.getValuationSetFactory( + formula.atomicPropositions()); Automaton automaton = AutomatonReader.readHoa(reader, x -> { checkArgument(vsFactory.alphabet().containsAll(x)); diff --git a/src/main/java/owl/translations/canonical/DeterministicConstructions.java b/src/main/java/owl/translations/canonical/DeterministicConstructions.java index 6af3bdadad1c48e739b5644e95bca3850df7cfaa..2ae5b0a3317c9e9da8b430c3f457267eb22350bf 100644 --- a/src/main/java/owl/translations/canonical/DeterministicConstructions.java +++ b/src/main/java/owl/translations/canonical/DeterministicConstructions.java @@ -118,8 +118,8 @@ public final class DeterministicConstructions { EquivalenceClass successorInternal(EquivalenceClass clazz, BitSet valuation) { return eagerUnfold - ? clazz.temporalStepUnfold(valuation) - : clazz.unfoldTemporalStep(valuation); + ? clazz.temporalStep(valuation).unfold() + : clazz.unfold().temporalStep(valuation); } ValuationTree successorTreeInternal(EquivalenceClass clazz) { @@ -140,6 +140,9 @@ public final class DeterministicConstructions { extends Base { private final EquivalenceClass initialState; + private final Function>> + edgeMapper = x -> Collections3.ofNullable(this.buildEdge(x.unfold())); + private Terminal(Factories factories, boolean eagerUnfold, Formula formula) { super(factories, eagerUnfold); this.initialState = initialStateInternal(factory.of(formula)); @@ -158,7 +161,9 @@ public final class DeterministicConstructions { @Override public final ValuationTree> edgeTree(EquivalenceClass clazz) { - return super.successorTreeInternal(clazz, x -> Collections3.ofNullable(this.buildEdge(x))); + return eagerUnfold + ? clazz.temporalStepTree(edgeMapper) + : clazz.unfold().temporalStepTree(x -> Collections3.ofNullable(this.buildEdge(x))); } @Nullable @@ -394,7 +399,7 @@ public final class DeterministicConstructions { @Override public BreakpointState onlyInitialState() { - return BreakpointState.of(initialState, factory.getTrue()); + return BreakpointState.of(initialState, factory.of(BooleanConstant.TRUE)); } @Override @@ -422,10 +427,10 @@ public final class DeterministicConstructions { EquivalenceClass newNext = next; if (current.implies(next)) { - newNext = factory.getTrue(); + newNext = factory.of(BooleanConstant.TRUE); } else if (next.modalOperators().stream().allMatch(SyntacticFragment.FINITE::contains)) { newCurrent = current.and(next); - newNext = factory.getTrue(); + newNext = factory.of(BooleanConstant.TRUE); if (current.modalOperators().stream().allMatch(SyntacticFragment.FINITE::contains)) { accepting = true; @@ -475,7 +480,7 @@ public final class DeterministicConstructions { && !SyntacticFragments.isCoSafety(formula) && !SyntacticFragments.isSafety(formula) && (!(formula instanceof Disjunction) - || !((Disjunction) formula).children.stream().allMatch(SyntacticFragments::isFgSafety))); + || !formula.children().stream().allMatch(SyntacticFragments::isFgSafety))); this.initialState = initialStateInternal(factory.of(formula)); } @@ -526,11 +531,11 @@ public final class DeterministicConstructions { } if (language.isTrue() || SyntacticFragments.isSafety(language.modalOperators())) { - return Edge.of(BreakpointState.of(language, factory.getTrue())); + return Edge.of(BreakpointState.of(language, factory.of(BooleanConstant.TRUE))); } if (SyntacticFragments.isCoSafety(language.modalOperators())) { - return Edge.of(BreakpointState.of(language, factory.getTrue()), 0); + return Edge.of(BreakpointState.of(language, factory.of(BooleanConstant.TRUE)), 0); } if (safety.isFalse()) { @@ -538,7 +543,8 @@ public final class DeterministicConstructions { } if (safety.isTrue()) { - return Edge.of(BreakpointState.of(factory.getTrue(), factory.getTrue())); + return Edge.of(BreakpointState.of(factory.of(BooleanConstant.TRUE), + factory.of(BooleanConstant.TRUE))); } return Edge.of(BreakpointState.of(language, safety)); diff --git a/src/main/java/owl/translations/canonical/DeterministicConstructionsPortfolio.java b/src/main/java/owl/translations/canonical/DeterministicConstructionsPortfolio.java index 199ab0941f5af098d167af98dc6687ec253b930e..ac1ffec3ebb2ff8675e681d2f90e545659e6964e 100644 --- a/src/main/java/owl/translations/canonical/DeterministicConstructionsPortfolio.java +++ b/src/main/java/owl/translations/canonical/DeterministicConstructionsPortfolio.java @@ -29,6 +29,7 @@ import owl.automaton.acceptance.CoBuchiAcceptance; import owl.automaton.acceptance.GeneralizedBuchiAcceptance; import owl.automaton.acceptance.GeneralizedCoBuchiAcceptance; import owl.automaton.acceptance.OmegaAcceptance; +import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; import owl.ltl.EquivalenceClass; @@ -100,13 +101,13 @@ public final class DeterministicConstructionsPortfolio safety( Environment environment, LabelledFormula formula) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); return new DeterministicConstructions.Safety(factories, true, formula.formula()); } public static Automaton coSafety( Environment environment, LabelledFormula formula) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); return new DeterministicConstructions.CoSafety(factories, true, formula.formula()); } public static Automaton, GeneralizedBuchiAcceptance> gfCoSafety(Environment environment, LabelledFormula formula, boolean generalized) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); var formulas = formula.formula() instanceof Conjunction - ? formula.formula().children() + ? Set.copyOf(formula.formula().children()) : Set.of(formula.formula()); return new DeterministicConstructions.GfCoSafety(factories, true, formulas, generalized); } @@ -143,13 +144,13 @@ public final class DeterministicConstructionsPortfolio, BuchiAcceptance> gCoSafety( Environment environment, LabelledFormula formula) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); return new DeterministicConstructions.GCoSafety(factories, true, formula.formula()); } public static Automaton, CoBuchiAcceptance> coSafetySafety( Environment environment, LabelledFormula formula) { - var factories = environment.factorySupplier().getFactories(formula.variables(), true); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); return new DeterministicConstructions.CoSafetySafety(factories, formula.formula()); } @@ -158,8 +159,9 @@ public final class DeterministicConstructionsPortfolio !x.current().isTrue() || !x.next().isTrue()); } diff --git a/src/main/java/owl/translations/canonical/LegacyFactory.java b/src/main/java/owl/translations/canonical/LegacyFactory.java index 19cae95aa66361adbe4c1bc4af347b6c6773de98..09cc00c75c221365e07d116932057b0a85db58c3 100644 --- a/src/main/java/owl/translations/canonical/LegacyFactory.java +++ b/src/main/java/owl/translations/canonical/LegacyFactory.java @@ -26,6 +26,7 @@ import owl.automaton.acceptance.AllAcceptance; import owl.automaton.edge.Edge; import owl.collections.ValuationTree; import owl.factories.Factories; +import owl.ltl.BooleanConstant; import owl.ltl.EquivalenceClass; /** @@ -64,7 +65,7 @@ public final class LegacyFactory public EquivalenceClass successor(EquivalenceClass clazz, BitSet valuation, EquivalenceClass environment) { EquivalenceClass state = successorInternal(clazz, valuation); - return environment.implies(state) ? factory.getTrue() : state; + return environment.implies(state) ? factory.of(BooleanConstant.TRUE) : state; } @Override @@ -77,6 +78,6 @@ public final class LegacyFactory public EquivalenceClass initialStateInternal(EquivalenceClass clazz, EquivalenceClass environment) { EquivalenceClass state = initialStateInternal(clazz); - return environment.implies(state) ? factory.getTrue() : state; + return environment.implies(state) ? factory.of(BooleanConstant.TRUE) : state; } } diff --git a/src/main/java/owl/translations/canonical/NonDeterministicConstructions.java b/src/main/java/owl/translations/canonical/NonDeterministicConstructions.java index 9f8864493c1705dce153106c56369fdd8d70bb00..22ceed693067f540de980521bbb66b2be3bc0461 100644 --- a/src/main/java/owl/translations/canonical/NonDeterministicConstructions.java +++ b/src/main/java/owl/translations/canonical/NonDeterministicConstructions.java @@ -26,7 +26,6 @@ import com.google.common.base.Preconditions; import com.google.common.collect.Sets; import java.util.ArrayList; import java.util.BitSet; -import java.util.Comparator; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -55,7 +54,6 @@ import owl.ltl.Formula; import owl.ltl.GOperator; import owl.ltl.Literal; import owl.ltl.MOperator; -import owl.ltl.PropositionalFormula; import owl.ltl.ROperator; import owl.ltl.SyntacticFragment; import owl.ltl.SyntacticFragments; @@ -109,27 +107,13 @@ public final class NonDeterministicConstructions { ValuationTree successorTreeInternal(Formula state, Function, ? extends Set> mapper) { - return successorTreeInternalRecursive(unfoldWithSuspension(state), mapper); - } - - private ValuationTree successorTreeInternalRecursive(Formula clause, - Function, ? extends Set> mapper) { - int nextVariable = clause.atomicPropositions(false).nextSetBit(0); - - if (nextVariable == -1) { - return ValuationTree.of(mapper.apply(toCompactDnf(clause.temporalStep()))); - } else { - var trueChild = successorTreeInternalRecursive( - clause.temporalStep(nextVariable, true), mapper); - var falseChild = successorTreeInternalRecursive( - clause.temporalStep(nextVariable, false), mapper); - return ValuationTree.of(nextVariable, trueChild, falseChild); - } + var clazz = factory.of(unfoldWithSuspension(state)); + return clazz.temporalStepTree(x -> mapper.apply(toCompactDnf(x.representative()))); } Set toCompactDnf(Formula formula) { if (formula instanceof Disjunction) { - var dnf = ((Disjunction) formula).children.stream() + var dnf = formula.children().stream() .flatMap(x -> toCompactDnf(x).stream()).collect(Collectors.toSet()); var finiteLtl = new HashSet(); @@ -157,7 +141,7 @@ public final class NonDeterministicConstructions { return dnf; } - Function> syntheticLiteralFactory = x -> { + Function> syntheticLiteralFactory = x -> { if (x instanceof Conjunction) { return Set.of(); } @@ -165,7 +149,7 @@ public final class NonDeterministicConstructions { var finiteLtl = new HashSet(); // NOPMD var nonFiniteLtl = new HashSet(); // NOPMD - x.children.forEach(y -> { + x.children().forEach(y -> { if (IsLiteralOrXVisitor.INSTANCE.apply(x)) { finiteLtl.add(y); } else { @@ -175,7 +159,7 @@ public final class NonDeterministicConstructions { for (Formula finiteFormula : finiteLtl) { if (nonFiniteLtl.stream().noneMatch(z -> z.anyMatch(finiteFormula::equals))) { - return x.children; + return Set.copyOf(x.children()); } } @@ -216,7 +200,7 @@ public final class NonDeterministicConstructions { .collect(Collectors.toSet()); EquivalenceClass temporalOperatorsClazz = factory.of(Conjunction.of( - clause2.stream().filter(Formula.TemporalOperator.class::isInstance))); + clause2.stream().filter(Formula.Temporal.class::isInstance))); Set retainedFacts = new HashSet<>(); @@ -225,7 +209,7 @@ public final class NonDeterministicConstructions { return Stream.empty(); } - if (literal instanceof Formula.TemporalOperator) { + if (literal instanceof Formula.Temporal) { retainedFacts.add(literal); } else if (temporalOperatorsClazz.implies(factory.of(literal))) { assert literal instanceof Disjunction; @@ -260,8 +244,13 @@ public final class NonDeterministicConstructions { } @Override - protected Boolean visit(Formula.TemporalOperator formula) { - return formula instanceof XOperator || formula instanceof Literal; + public Boolean visit(Literal literal) { + return true; + } + + @Override + protected Boolean visit(Formula.Temporal formula) { + return formula instanceof XOperator; } } @@ -492,13 +481,13 @@ public final class NonDeterministicConstructions { } } - singletonAutomata.sort(Comparator.naturalOrder()); + singletonAutomata.sort(null); // Ensure that there is at least one automaton. if (automata.isEmpty()) { automata.add(new FOperator(singletonAutomata.remove(0))); } else { - automata.sort(Comparator.naturalOrder()); + automata.sort(null); } // Iteratively build common edge-tree. diff --git a/src/main/java/owl/translations/canonical/NonDeterministicConstructionsPortfolio.java b/src/main/java/owl/translations/canonical/NonDeterministicConstructionsPortfolio.java index 1e5f2e3a42465679a178b79c8fca8fabeef14711..83ec97c8c4f90de72355f1aaa76fc4eb373383aa 100644 --- a/src/main/java/owl/translations/canonical/NonDeterministicConstructionsPortfolio.java +++ b/src/main/java/owl/translations/canonical/NonDeterministicConstructionsPortfolio.java @@ -90,28 +90,28 @@ public final class NonDeterministicConstructionsPortfolio coSafety( Environment environment, LabelledFormula formula) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); return new NonDeterministicConstructions.CoSafety(factories, formula.formula()); } public static Automaton safety( Environment environment, LabelledFormula formula) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); return new NonDeterministicConstructions.Safety(factories, formula.formula()); } public static Automaton, GeneralizedBuchiAcceptance> gfCoSafety( Environment environment, LabelledFormula formula, boolean generalized) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); var formulas = formula.formula() instanceof Conjunction - ? formula.formula().children() + ? Set.copyOf(formula.formula().children()) : Set.of(formula.formula()); return new NonDeterministicConstructions.GfCoSafety(factories, formulas, generalized); } public static Automaton fgSafety( Environment environment, LabelledFormula formula) { - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); return new NonDeterministicConstructions.FgSafety(factories, formula.formula()); } } diff --git a/src/main/java/owl/translations/canonical/Util.java b/src/main/java/owl/translations/canonical/Util.java index cd087b8ca0e4e72a194d4a77a211073f229cb73a..1d8d84ddd46cf255f413672c0eba6f318903ff44 100644 --- a/src/main/java/owl/translations/canonical/Util.java +++ b/src/main/java/owl/translations/canonical/Util.java @@ -29,7 +29,7 @@ import java.util.Set; import owl.collections.ValuationTree; import owl.ltl.BooleanConstant; import owl.ltl.Formula; -import owl.ltl.UnaryModalOperator; +import owl.ltl.Literal; class Util { @@ -72,8 +72,12 @@ class Util { Formula[] trueSingleSteps = new Formula[singleSteps.size()]; Formula[] falseSingleSteps = new Formula[singleSteps.size()]; - Arrays.setAll(trueSingleSteps, i -> singleSteps.get(i).temporalStep(variable, true)); - Arrays.setAll(falseSingleSteps, i -> singleSteps.get(i).temporalStep(variable, false)); + + + Arrays.setAll(trueSingleSteps, + i -> singleSteps.get(i).substitute(x -> temporalStep(x, variable, true))); + Arrays.setAll(falseSingleSteps, + i -> singleSteps.get(i).substitute(x -> temporalStep(x, variable, false))); var trueChild = singleStepTreeRecursive(Arrays.asList(trueSingleSteps), cache); var falseChild = singleStepTreeRecursive(Arrays.asList(falseSingleSteps), cache); @@ -86,7 +90,19 @@ class Util { } static Formula unwrap(Formula formula) { - return ((UnaryModalOperator) formula).operand; + return ((Formula.UnaryTemporalOperator) formula).operand; + } + + private static Formula temporalStep(Formula formula, int atom, boolean valuation) { + if (formula instanceof Literal) { + Literal literal = (Literal) formula; + + if (literal.getAtom() == atom) { + return BooleanConstant.of(valuation ^ literal.isNegated()); + } + } + + return formula; } @AutoValue diff --git a/src/main/java/owl/translations/delag/DelagBuilder.java b/src/main/java/owl/translations/delag/DelagBuilder.java index 2950fa5ee447cbd166e56708f94a8ef171f0d27b..44342eec51b80ca648d602dd2ea8181ff983b00a 100644 --- a/src/main/java/owl/translations/delag/DelagBuilder.java +++ b/src/main/java/owl/translations/delag/DelagBuilder.java @@ -98,7 +98,7 @@ public class DelagBuilder @Override public Automaton, EmersonLeiAcceptance> apply(LabelledFormula inputFormula) { LabelledFormula formula = inputFormula.nnf(); - Factories factories = environment.factorySupplier().getFactories(formula.variables()); + Factories factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); if (formula.formula().equals(BooleanConstant.FALSE)) { return AutomatonFactory.empty(factories.vsFactory, diff --git a/src/main/java/owl/translations/delag/DependencyTree.java b/src/main/java/owl/translations/delag/DependencyTree.java index 490e88fb5814b5d67676dec688936e710ab1aa74..06f6a5796b74e8fdcefe26a47070e1125bf81954 100644 --- a/src/main/java/owl/translations/delag/DependencyTree.java +++ b/src/main/java/owl/translations/delag/DependencyTree.java @@ -35,7 +35,6 @@ import owl.automaton.Automaton.Property; import owl.ltl.Formula; import owl.ltl.SyntacticFragment; import owl.ltl.SyntacticFragments; -import owl.ltl.UnaryModalOperator; import owl.ltl.visitors.PrintVisitor; import owl.ltl.visitors.XDepthVisitor; import owl.translations.delag.ProductState.Builder; @@ -106,7 +105,8 @@ abstract class DependencyTree { } static Formula unwrap(Formula formula) { - return ((UnaryModalOperator) ((UnaryModalOperator) formula).operand).operand; + return ((Formula.UnaryTemporalOperator) + ((Formula.UnaryTemporalOperator) formula).operand).operand; } @Nullable @@ -274,7 +274,7 @@ abstract class DependencyTree { } if (type == Type.SAFETY || type == Type.CO_SAFETY) { - var successor = state.productState.safety().get(formula).temporalStepUnfold(valuation); + var successor = state.productState.safety().get(formula).temporalStep(valuation).unfold(); if (successor.isFalse()) { builder.addFinished(this, Boolean.FALSE); diff --git a/src/main/java/owl/translations/delag/DependencyTreeFactory.java b/src/main/java/owl/translations/delag/DependencyTreeFactory.java index f6745ddb102c6adcf46aad7906c5a0dbcb3a1b96..59c63d4fce44098bca54a9535114c88b9bee016d 100644 --- a/src/main/java/owl/translations/delag/DependencyTreeFactory.java +++ b/src/main/java/owl/translations/delag/DependencyTreeFactory.java @@ -67,7 +67,7 @@ class DependencyTreeFactory extends PropositionalVisitor> { } @Override - protected DependencyTree visit(Formula.TemporalOperator formula) { + protected DependencyTree visit(Formula.Temporal formula) { return defaultAction(formula, null); } diff --git a/src/main/java/owl/translations/ltl2dpa/AsymmetricDPAConstruction.java b/src/main/java/owl/translations/ltl2dpa/AsymmetricDPAConstruction.java index 400a57c39b9d0ed063da2cddc945de75fb543075..02c0b3df75f5b352c02410e321e4c89c458d4d5e 100644 --- a/src/main/java/owl/translations/ltl2dpa/AsymmetricDPAConstruction.java +++ b/src/main/java/owl/translations/ltl2dpa/AsymmetricDPAConstruction.java @@ -39,6 +39,7 @@ import owl.automaton.acceptance.ParityAcceptance.Parity; import owl.automaton.algorithms.SccDecomposition; import owl.automaton.edge.Edge; import owl.factories.EquivalenceClassFactory; +import owl.ltl.BooleanConstant; import owl.ltl.EquivalenceClass; import owl.ltl.Formula; import owl.ltl.LabelledFormula; @@ -133,7 +134,7 @@ final class AsymmetricDPAConstruction { // Compute successors of existing ranking. List ranking = new ArrayList<>(previousRanking.size()); int rankingColor = 2 * previousRanking.size(); // Default rejecting color. - var rankingLanguage = factory.getFalse(); + var rankingLanguage = factory.of(BooleanConstant.FALSE); { var iterator = previousRanking.iterator(); @@ -173,7 +174,7 @@ final class AsymmetricDPAConstruction { if (!iterator.hasNext() && partitionedFixpoints.get(3).containsKey(rankingSuccessor.evaluatedFixpoints) && ldba.annotation().headSet(fixpoints).size() == previousSafetyProgress) { - rankingLanguage = factory.getTrue(); + rankingLanguage = factory.of(BooleanConstant.TRUE); } } } diff --git a/src/main/java/owl/translations/ltl2dpa/LTL2DPAFunction.java b/src/main/java/owl/translations/ltl2dpa/LTL2DPAFunction.java index e8ca460a7a5e631d350a80cd86d47f4315c19bd4..4e7a82cf713e0809214ee25c54fd8de2988d614e 100644 --- a/src/main/java/owl/translations/ltl2dpa/LTL2DPAFunction.java +++ b/src/main/java/owl/translations/ltl2dpa/LTL2DPAFunction.java @@ -43,6 +43,7 @@ import owl.automaton.acceptance.ParityAcceptance; import owl.automaton.acceptance.optimizations.ParityAcceptanceOptimizations; import owl.automaton.transformations.ParityUtil; import owl.automaton.util.AnnotatedStateOptimisation; +import owl.ltl.BooleanConstant; import owl.ltl.LabelledFormula; import owl.run.Environment; import owl.translations.mastertheorem.Selector; @@ -198,14 +199,15 @@ public class LTL2DPAFunction implements Function(optimisedDpa, - AsymmetricRankingState.of(factory.getFalse()), + AsymmetricRankingState.of(factory.of(BooleanConstant.FALSE)), configuration.contains(COMPRESS_COLOURS)); } return new Result<>(optimisedDpa, - AsymmetricRankingState.of(dpa.onlyInitialState().state().factory().getFalse()), + AsymmetricRankingState.of(dpa.onlyInitialState().state().factory().of(BooleanConstant.FALSE)), configuration.contains(COMPRESS_COLOURS)); } diff --git a/src/main/java/owl/translations/ltl2ldba/AsymmetricLDBAConstruction.java b/src/main/java/owl/translations/ltl2ldba/AsymmetricLDBAConstruction.java index 4cd455dcf503a76f6b5160bc2211b5de9635eb97..72ccbc22d9a1d4ed8c4e92de26088c69b395aa4a 100644 --- a/src/main/java/owl/translations/ltl2ldba/AsymmetricLDBAConstruction.java +++ b/src/main/java/owl/translations/ltl2ldba/AsymmetricLDBAConstruction.java @@ -89,10 +89,10 @@ public final class AsymmetricLDBAConstruction blockingModalOperators; + Set blockingModalOperators; int acceptanceSets = 1; var knownFixpoints = new TreeSet(); @@ -144,7 +144,7 @@ public final class AsymmetricLDBAConstruction> jumps = new HashMap<>(); Consumer jumpGenerator = x -> { - Set operators = x.modalOperators(); + Set operators = x.modalOperators(); // The state is a simple safety or cosafety condition. We don't need to use reasoning about // the infinite behaviour and simply build the left-derivative of the formula. @@ -156,9 +156,9 @@ public final class AsymmetricLDBAConstruction productStates = new ArrayList<>(); - Set allModalOperators = new HashSet<>(); + Set allModalOperators = new HashSet<>(); operators.forEach(y -> allModalOperators.addAll(y.subformulas(Predicates.IS_GREATEST_FIXPOINT, - Formula.ModalOperator.class::cast))); + Formula.Temporal.class::cast))); for (Fixpoints fixpoints : knownFixpoints) { if (fixpoints.allFixpointsPresent(allModalOperators)) { @@ -175,7 +175,8 @@ public final class AsymmetricLDBAConstruction> { + extends PropositionalVisitor> { private static final BlockingModalOperatorsVisitor INSTANCE = new BlockingModalOperatorsVisitor(); @@ -456,26 +457,26 @@ public final class AsymmetricLDBAConstruction visit(Formula.TemporalOperator formula) { + protected Set visit(Formula.Temporal formula) { if (SyntacticFragment.FINITE.contains(formula)) { return Set.of(); } if (SyntacticFragments.isCoSafety(formula)) { - return Set.of((Formula.ModalOperator) formula); + return Set.of(formula); } return Set.of(); } @Override - public Set visit(BooleanConstant booleanConstant) { + public Set visit(BooleanConstant booleanConstant) { return Set.of(); } @Override - public Set visit(Conjunction conjunction) { - Set blockingOperators = new HashSet<>(); + public Set visit(Conjunction conjunction) { + Set blockingOperators = new HashSet<>(); for (Formula child : conjunction.children) { // Only consider non-finite LTL formulas. @@ -488,8 +489,8 @@ public final class AsymmetricLDBAConstruction visit(Disjunction disjunction) { - Set blockingOperators = null; + public Set visit(Disjunction disjunction) { + Set blockingOperators = null; for (Formula child : disjunction.children) { // Only consider non-finite LTL formulas. diff --git a/src/main/java/owl/translations/ltl2ldba/SymmetricLDBAConstruction.java b/src/main/java/owl/translations/ltl2ldba/SymmetricLDBAConstruction.java index b2f1081cdbc802421491739a56162d4759e1bc39..e36f07fb330677e798b9f3ad44950f18a7a50a03 100644 --- a/src/main/java/owl/translations/ltl2ldba/SymmetricLDBAConstruction.java +++ b/src/main/java/owl/translations/ltl2ldba/SymmetricLDBAConstruction.java @@ -97,7 +97,7 @@ public final class SymmetricLDBAConstruction, BiFunction>> apply(LabelledFormula input) { var formula = input.nnf(); - var factories = environment.factorySupplier().getFactories(formula.variables(), true); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); // Declare components of LDBA @@ -123,7 +123,7 @@ public final class SymmetricLDBAConstruction initialFormulas.add(Disjunction.of(x))); - initialFormulas.sort(Formula::compareTo); + initialFormulas.sort(null); for (Formula initialFormula : initialFormulas) { var sets = Selector.selectSymmetric(initialFormula, false); @@ -216,7 +216,7 @@ public final class SymmetricLDBAConstruction x.subformulas(Formula.ModalOperator.class).stream()) + .flatMap(x -> x.subformulas(Formula.Temporal.class).stream()) .collect(Collectors.toUnmodifiableSet()); var availableFixpoints = knownFixpoints.get(entry.getKey()).stream() @@ -360,7 +360,7 @@ public final class SymmetricLDBAConstruction modalOperators = clazz.modalOperators(); + Set modalOperators = clazz.modalOperators(); if (modalOperators.isEmpty()) { return true; diff --git a/src/main/java/owl/translations/ltl2nba/SymmetricNBAConstruction.java b/src/main/java/owl/translations/ltl2nba/SymmetricNBAConstruction.java index b797ae8da62a9735d584403785abdbdd58d8fadf..ac9bd82c94240b672ff1d9fbd7441a5b567a483a 100644 --- a/src/main/java/owl/translations/ltl2nba/SymmetricNBAConstruction.java +++ b/src/main/java/owl/translations/ltl2nba/SymmetricNBAConstruction.java @@ -80,7 +80,7 @@ public final class SymmetricNBAConstruction, B> apply(LabelledFormula input) { var formula = input.nnf(); - var factories = environment.factorySupplier().getFactories(formula.variables(), false); + var factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); var automaton = new SymmetricNBA(factories, formula); var mutableAutomaton = MutableAutomatonFactory.copy(automaton); AcceptanceOptimizations.removeDeadStates(mutableAutomaton); @@ -255,7 +255,7 @@ public final class SymmetricNBAConstruction x.allFixpointsPresent(allModalOperators)) @@ -264,7 +264,7 @@ public final class SymmetricNBAConstruction y.subformulas(Formula.ModalOperator.class).contains(x))) { + .noneMatch(y -> y.subformulas(Formula.Temporal.class).contains(x))) { return Set.of(); } } diff --git a/src/main/java/owl/translations/mastertheorem/AsymmetricEvaluatedFixpoints.java b/src/main/java/owl/translations/mastertheorem/AsymmetricEvaluatedFixpoints.java index b89f54a2ef38af3f0e3d0aa37335b17a7e8118f8..bc78b859d5b2218f5b4df6befe209a7e88af3b27 100644 --- a/src/main/java/owl/translations/mastertheorem/AsymmetricEvaluatedFixpoints.java +++ b/src/main/java/owl/translations/mastertheorem/AsymmetricEvaluatedFixpoints.java @@ -80,7 +80,7 @@ public final class AsymmetricEvaluatedFixpoints Rewriter.ToCoSafety toCoSafety = new Rewriter.ToCoSafety(fixpoints.greatestFixpoints()); Set gOperatorsRewritten = new HashSet<>(); - for (Formula.ModalOperator greatestFixpoint : fixpoints.greatestFixpoints()) { + for (Formula.Temporal greatestFixpoint : fixpoints.greatestFixpoints()) { GOperator gOperator = (GOperator) greatestFixpoint; Formula operand = gOperator.operand.substitute(toCoSafety); diff --git a/src/main/java/owl/translations/mastertheorem/ExtendedRewriter.java b/src/main/java/owl/translations/mastertheorem/ExtendedRewriter.java index f63b92ca0d6051d1fb157f961718888e4e00b08c..7a202d05f32d3907ffe3bb20383728217e4d9c70 100644 --- a/src/main/java/owl/translations/mastertheorem/ExtendedRewriter.java +++ b/src/main/java/owl/translations/mastertheorem/ExtendedRewriter.java @@ -19,10 +19,11 @@ package owl.translations.mastertheorem; +import com.google.common.collect.Comparators; +import java.util.Comparator; import java.util.HashSet; import java.util.Optional; import java.util.Set; -import java.util.Spliterator; import java.util.function.Consumer; import javax.annotation.Nullable; import owl.ltl.BooleanConstant; @@ -53,7 +54,7 @@ class ExtendedRewriter { // variables are created. We only propagate constants and try to minimise the context-dependent // creation of new variables. private static class AdviceFunction - implements BinaryVisitor, Formula> { + implements BinaryVisitor, Formula> { // Least Fixed-Points private final Set fOperators; @@ -70,13 +71,13 @@ class ExtendedRewriter { private final boolean insideAlmostAll; // Usage Detector - private final Consumer consumer; + private final Consumer consumer; private final @Nullable AdviceFunction prerunAdviceFunction; private AdviceFunction(Mode mode, - Iterable x, - Iterable y, - Consumer consumer, + Iterable x, + Iterable y, + Consumer consumer, boolean insideAlmostAll) { this.insideAlmostAll = insideAlmostAll; @@ -138,7 +139,7 @@ class ExtendedRewriter { Set fOperators, Set mOperators, Set uOperators, - Consumer consumer, + Consumer consumer, Set gOperators, Set rOperators, Set wOperators, @@ -155,12 +156,12 @@ class ExtendedRewriter { this.prerunAdviceFunction = null; } - public Formula apply(Formula.ModalOperator formula) { + public Formula apply(Formula.Temporal formula) { return apply(formula, Optional.of(formula)); } @Override - public Formula apply(Formula formula, Optional scope) { + public Formula apply(Formula formula, Optional scope) { // Avoid marking elements falsely as used by pre-running the advice-function and checking for // trivial results. if (prerunAdviceFunction != null @@ -178,33 +179,59 @@ class ExtendedRewriter { // Simple Cases @Override - public Formula visit(BooleanConstant booleanConstant, Optional scope) { + public Formula visit(BooleanConstant booleanConstant, Optional scope) { return booleanConstant; } @Override - public Formula visit(Literal literal, Optional scope) { + public Formula visit(Literal literal, Optional scope) { return literal; } @Override - public Formula visit(Conjunction conjunction, Optional scope) { + public Formula visit(Conjunction conjunction, Optional scope) { + Set children = new HashSet<>(); + // Stable iteration order to ensure deterministic results. - assert conjunction.children.spliterator().hasCharacteristics(Spliterator.SORTED); - return Conjunction.of( - conjunction.children.stream().map(x -> x.accept(this, Optional.empty()))); + assert Comparators.isInStrictOrder(conjunction.children(), Comparator.naturalOrder()); + + for (Formula child : conjunction.children()) { + var visitedChild = child.accept(this, Optional.empty()); + + // Short-circuit to ensure correct update of "unused operators" + if (visitedChild.equals(BooleanConstant.FALSE)) { + return BooleanConstant.FALSE; + } + + children.add(visitedChild); + } + + return Conjunction.of(children); } @Override - public Formula visit(Disjunction disjunction, Optional scope) { + public Formula visit(Disjunction disjunction, Optional scope) { + Set children = new HashSet<>(); + // Stable iteration order to ensure deterministic results. - assert disjunction.children.spliterator().hasCharacteristics(Spliterator.SORTED); - return Disjunction.of( - disjunction.children.stream().map(x -> x.accept(this, Optional.empty()))); + assert Comparators.isInStrictOrder(disjunction.children(), Comparator.naturalOrder()); + + for (Formula child : disjunction.children()) { + var visitedChild = child.accept(this, Optional.empty()); + + // Short-circuit to ensure correct update of "unused operators" + if (visitedChild.equals(BooleanConstant.TRUE)) { + return BooleanConstant.TRUE; + } + + children.add(visitedChild); + } + + return Disjunction.of(children); } @Override - public Formula visit(XOperator xOperator, Optional scope) { + public Formula visit(XOperator xOperator, Optional scope) { var operand = xOperator.operand.accept(this, Optional.empty()); return operand instanceof BooleanConstant ? operand : new XOperator(operand); } @@ -212,7 +239,7 @@ class ExtendedRewriter { // Least Fixed-points @Override - public Formula visit(FOperator fOperator, Optional scope) { + public Formula visit(FOperator fOperator, Optional scope) { if (scope.isPresent() && fOperator.equals(scope.get())) { assert mode == Mode.STRONG; return fOperator(fOperator.operand.accept(this, Optional.empty())); @@ -223,7 +250,7 @@ class ExtendedRewriter { } @Override - public Formula visit(MOperator mOperator, Optional scope) { + public Formula visit(MOperator mOperator, Optional scope) { if (scope.isPresent() && mOperator.equals(scope.get())) { assert mode == Mode.STRONG; return mOperator( @@ -246,7 +273,7 @@ class ExtendedRewriter { } @Override - public Formula visit(UOperator uOperator, Optional scope) { + public Formula visit(UOperator uOperator, Optional scope) { if (scope.isPresent() && uOperator.equals(scope.get())) { assert mode == Mode.STRONG; return uOperator( @@ -271,7 +298,7 @@ class ExtendedRewriter { // Greatest Fixed-points @Override - public Formula visit(GOperator gOperator, Optional scope) { + public Formula visit(GOperator gOperator, Optional scope) { if (scope.isPresent() && gOperator.equals(scope.get())) { assert mode == Mode.WEAK; return gOperator(gOperator.operand.accept(this, Optional.empty())); @@ -288,7 +315,7 @@ class ExtendedRewriter { } @Override - public Formula visit(ROperator rOperator, Optional scope) { + public Formula visit(ROperator rOperator, Optional scope) { if (scope.isPresent() && rOperator.equals(scope.get())) { assert mode == Mode.WEAK; return rOperator( @@ -312,7 +339,7 @@ class ExtendedRewriter { } @Override - public Formula visit(WOperator wOperator, Optional scope) { + public Formula visit(WOperator wOperator, Optional scope) { if (scope.isPresent() && wOperator.equals(scope.get())) { assert mode == Mode.WEAK; return wOperator( @@ -423,18 +450,18 @@ class ExtendedRewriter { } static final class ToSafety extends AdviceFunction { - ToSafety(Fixpoints fixpoints, Consumer consumer) { + ToSafety(Fixpoints fixpoints, Consumer consumer) { super(Mode.WEAK, fixpoints.leastFixpoints(), fixpoints.greatestFixpoints(), consumer, true); } - ToSafety(Iterable x, - Consumer consumer) { + ToSafety(Iterable x, + Consumer consumer) { super(Mode.WEAK, x, Set.of(), consumer, false); } } static final class ToCoSafety extends AdviceFunction { - ToCoSafety(Fixpoints fixpoints, Consumer consumer) { + ToCoSafety(Fixpoints fixpoints, Consumer consumer) { super(Mode.STRONG, fixpoints.leastFixpoints(), fixpoints.greatestFixpoints(), consumer, true); } } diff --git a/src/main/java/owl/translations/mastertheorem/Fixpoints.java b/src/main/java/owl/translations/mastertheorem/Fixpoints.java index 816d38599d6caa8b4b3273c42b47937bbf2f6e4c..cdf3990e54d991102edb1c13e2026450d1571ca1 100644 --- a/src/main/java/owl/translations/mastertheorem/Fixpoints.java +++ b/src/main/java/owl/translations/mastertheorem/Fixpoints.java @@ -39,14 +39,14 @@ import owl.ltl.WOperator; @AutoValue public abstract class Fixpoints implements Comparable { - public abstract Set leastFixpoints(); + public abstract Set leastFixpoints(); - public abstract Set greatestFixpoints(); + public abstract Set greatestFixpoints(); - public static Fixpoints of(Collection leastFixpoints, - Collection greatestFixpoints) { - Set leastFixpointsCopy = Set.copyOf(leastFixpoints); - Set greatestFixpointsCopy = Set.copyOf(greatestFixpoints); + public static Fixpoints of(Collection leastFixpoints, + Collection greatestFixpoints) { + Set leastFixpointsCopy = Set.copyOf(leastFixpoints); + Set greatestFixpointsCopy = Set.copyOf(greatestFixpoints); checkArgument(leastFixpointsCopy.stream().allMatch(Predicates.IS_LEAST_FIXPOINT)); checkArgument(greatestFixpointsCopy.stream().allMatch(Predicates.IS_GREATEST_FIXPOINT)); @@ -54,11 +54,11 @@ public abstract class Fixpoints implements Comparable { return new AutoValue_Fixpoints(leastFixpointsCopy, greatestFixpointsCopy); } - public static Fixpoints of(Collection fixpoints) { - Set leastFixpoints = new HashSet<>(); - Set greatestFixpoints = new HashSet<>(); + public static Fixpoints of(Collection fixpoints) { + Set leastFixpoints = new HashSet<>(); + Set greatestFixpoints = new HashSet<>(); - for (Formula.ModalOperator fixpoint : fixpoints) { + for (Formula.Temporal fixpoint : fixpoints) { if (Predicates.IS_LEAST_FIXPOINT.test(fixpoint)) { leastFixpoints.add(fixpoint); } else { @@ -67,12 +67,12 @@ public abstract class Fixpoints implements Comparable { } } - return of(Set.of(leastFixpoints.toArray(Formula.ModalOperator[]::new)), - Set.of(greatestFixpoints.toArray(Formula.ModalOperator[]::new))); + return of(Set.of(leastFixpoints.toArray(Formula.Temporal[]::new)), + Set.of(greatestFixpoints.toArray(Formula.Temporal[]::new))); } public boolean allFixpointsPresent( - Collection formulas) { + Collection formulas) { Set waitingFixpoints = new HashSet<>(leastFixpoints()); waitingFixpoints.addAll(greatestFixpoints()); waitingFixpoints.removeAll(formulas); @@ -88,7 +88,7 @@ public abstract class Fixpoints implements Comparable { public abstract boolean equals(Object o); @Memoized - public Set fixpoints() { + public Set fixpoints() { return Set.copyOf(Sets.union(leastFixpoints(), greatestFixpoints())); } diff --git a/src/main/java/owl/translations/mastertheorem/Rewriter.java b/src/main/java/owl/translations/mastertheorem/Rewriter.java index 70baf6e448047d5a945458abf657882c13622da7..ea546a12f8374cd970f1a6a53d18bb3a0ff18781 100644 --- a/src/main/java/owl/translations/mastertheorem/Rewriter.java +++ b/src/main/java/owl/translations/mastertheorem/Rewriter.java @@ -78,7 +78,7 @@ public class Rewriter { this(fixpoints.greatestFixpoints()); } - public ToCoSafety(Iterable y) { + public ToCoSafety(Iterable y) { Set gOperators = new HashSet<>(); Set rOperators = new HashSet<>(); Set wOperators = new HashSet<>(); @@ -198,7 +198,7 @@ public class Rewriter { this(fixpoints.leastFixpoints()); } - public ToSafety(Iterable x) { + public ToSafety(Iterable x) { Set fOperators = new HashSet<>(); Set mOperators = new HashSet<>(); Set uOperators = new HashSet<>(); diff --git a/src/main/java/owl/translations/mastertheorem/Selector.java b/src/main/java/owl/translations/mastertheorem/Selector.java index 9189bd03a1519220eef0e0012c717207a3f0ffd5..4a4f5961dbeec96396e2aed9b6c0868fd2c85703 100644 --- a/src/main/java/owl/translations/mastertheorem/Selector.java +++ b/src/main/java/owl/translations/mastertheorem/Selector.java @@ -27,7 +27,6 @@ import java.util.HashSet; import java.util.List; import java.util.Set; import java.util.stream.Stream; -import owl.ltl.BinaryModalOperator; import owl.ltl.Conjunction; import owl.ltl.Disjunction; import owl.ltl.FOperator; @@ -38,7 +37,6 @@ import owl.ltl.MOperator; import owl.ltl.ROperator; import owl.ltl.SyntacticFragments; import owl.ltl.UOperator; -import owl.ltl.UnaryModalOperator; import owl.ltl.WOperator; import owl.ltl.XOperator; import owl.ltl.rewriter.NormalForms; @@ -79,7 +77,7 @@ public final class Selector { } private static Stream selectAsymmetricFromClause(Set clause) { - List>> elementSets = new ArrayList<>(); + List>> elementSets = new ArrayList<>(); for (Formula element : clause) { assert isClauseElement(element); @@ -93,8 +91,8 @@ public final class Selector { List fixpointsList = new ArrayList<>(); - for (List> combination : Sets.cartesianProduct(elementSets)) { - Set union = new HashSet<>(); + for (List> combination : Sets.cartesianProduct(elementSets)) { + Set union = new HashSet<>(); combination.forEach(union::addAll); fixpointsList.add(Fixpoints.of(Set.of(), union)); } @@ -104,7 +102,7 @@ public final class Selector { private static Stream selectSymmetricFromClause(Set clause) { List fixpointsList = new ArrayList<>(); - List>> elementSets = new ArrayList<>(); + List>> elementSets = new ArrayList<>(); for (Formula element : clause) { assert isClauseElement(element); @@ -113,14 +111,14 @@ public final class Selector { continue; } - Set fixpoints = new HashSet<>(); + Set fixpoints = new HashSet<>(); UnscopedVisitor visitor = new UnscopedVisitor(fixpoints); element.accept(visitor); elementSets.add(Sets.powerSet(fixpoints)); } - for (List> combination : Sets.cartesianProduct(elementSets)) { - Set union = new HashSet<>(); + for (List> combination : Sets.cartesianProduct(elementSets)) { + Set union = new HashSet<>(); combination.forEach(union::addAll); fixpointsList.add(Fixpoints.of(union)); } @@ -131,20 +129,20 @@ public final class Selector { private static boolean isClauseElement(Formula formula) { return SyntacticFragments.isCoSafety(formula) || formula instanceof Literal - || formula instanceof UnaryModalOperator - || formula instanceof BinaryModalOperator; + || formula instanceof Formula.UnaryTemporalOperator + || formula instanceof Formula.BinaryTemporalOperator; } - private static Set selectAllFixpoints( + private static Set selectAllFixpoints( Formula formula) { return formula.subformulas(Predicates.IS_FIXPOINT, - Formula.ModalOperator.class::cast); + Formula.Temporal.class::cast); } - private static Set selectGreatestFixpoints( + private static Set selectGreatestFixpoints( Formula formula) { return formula.subformulas(Predicates.IS_GREATEST_FIXPOINT, - Formula.ModalOperator.class::cast); + Formula.Temporal.class::cast); } private abstract static class AbstractSymmetricVisitor implements Visitor { @@ -175,7 +173,7 @@ public final class Selector { private static final class UnscopedVisitor extends AbstractSymmetricVisitor { private final GScopedVisitor gScopedVisitor; - private UnscopedVisitor(Set fixpoints) { + private UnscopedVisitor(Set fixpoints) { gScopedVisitor = new GScopedVisitor(fixpoints); } @@ -219,9 +217,9 @@ public final class Selector { } private static class GScopedVisitor extends AbstractSymmetricVisitor { - private final Set fixpoints; + private final Set fixpoints; - private GScopedVisitor(Set fixpoints) { + private GScopedVisitor(Set fixpoints) { this.fixpoints = fixpoints; } diff --git a/src/main/java/owl/translations/mastertheorem/SymmetricEvaluatedFixpoints.java b/src/main/java/owl/translations/mastertheorem/SymmetricEvaluatedFixpoints.java index cf710a55d87a346dbcd7e6ea2fb3f396ab38cfe1..9b53f0fa2732432766b5a65620aa55bac05f5733 100644 --- a/src/main/java/owl/translations/mastertheorem/SymmetricEvaluatedFixpoints.java +++ b/src/main/java/owl/translations/mastertheorem/SymmetricEvaluatedFixpoints.java @@ -85,7 +85,7 @@ public final class SymmetricEvaluatedFixpoints Set infinitelyOftenFormulas = new HashSet<>(); - for (Formula.ModalOperator leastFixpoint : fixpoints.leastFixpoints()) { + for (Formula.Temporal leastFixpoint : fixpoints.leastFixpoints()) { Formula infinitelyOften = unwrapX(SimplifierFactory.apply( GOperator.of(FOperator.of(toCoSafety.apply(leastFixpoint))), Mode.SYNTACTIC_FIXPOINT, Mode.PULL_UP_X)); @@ -140,7 +140,7 @@ public final class SymmetricEvaluatedFixpoints List> almostAlwaysFormulasAlternatives = new ArrayList<>(); - for (Formula.ModalOperator greatestFixpoint : fixpoints.greatestFixpoints()) { + for (Formula.Temporal greatestFixpoint : fixpoints.greatestFixpoints()) { Formula almostAlways = unwrapX(SimplifierFactory.apply( FOperator.of(GOperator.of(toSafety.apply(greatestFixpoint))), Mode.SYNTACTIC_FIXPOINT, Mode.PULL_UP_X)); @@ -173,8 +173,8 @@ public final class SymmetricEvaluatedFixpoints var toSafetyWithoutGreatestFixpoints = new ExtendedRewriter.ToSafety(fixpoints.leastFixpoints(), unusedFixpoints::remove); - for (Formula.ModalOperator modalOperator - : formula.subformulas(Predicates.IS_GREATEST_FIXPOINT, Formula.ModalOperator.class::cast)) { + for (Formula.Temporal modalOperator + : formula.subformulas(Predicates.IS_GREATEST_FIXPOINT, Formula.Temporal.class::cast)) { toSafetyWithoutGreatestFixpoints.apply(modalOperator); } diff --git a/src/main/java/owl/translations/rabinizer/MonitorBuilder.java b/src/main/java/owl/translations/rabinizer/MonitorBuilder.java index 16c00d80e72e41d0b03c32a53f54ad17203035a5..1dd61bf2178c27e7ba92520e8afd413f3eae90c9 100644 --- a/src/main/java/owl/translations/rabinizer/MonitorBuilder.java +++ b/src/main/java/owl/translations/rabinizer/MonitorBuilder.java @@ -72,7 +72,7 @@ final class MonitorBuilder { this.gOperator = gOperator; this.vsFactory = vsFactory; - Set modalOperators = operand.modalOperators(); + Set modalOperators = operand.modalOperators(); boolean isCoSafety = modalOperators.stream().allMatch(SyntacticFragments::isCoSafety); if (isCoSafety && gOperator.operand instanceof FOperator) { diff --git a/src/main/java/owl/translations/rabinizer/RabinizerBuilder.java b/src/main/java/owl/translations/rabinizer/RabinizerBuilder.java index 087264afbd4f73d5ceecbd78456f95fb7a65d848..2320c0feee98ff56a80e216f2dadc17698f3dd0f 100644 --- a/src/main/java/owl/translations/rabinizer/RabinizerBuilder.java +++ b/src/main/java/owl/translations/rabinizer/RabinizerBuilder.java @@ -66,7 +66,6 @@ import owl.collections.ValuationSet; import owl.factories.EquivalenceClassFactory; import owl.factories.Factories; import owl.factories.ValuationSetFactory; -import owl.ltl.BinaryModalOperator; import owl.ltl.BooleanConstant; import owl.ltl.Conjunction; import owl.ltl.Disjunction; @@ -81,7 +80,6 @@ import owl.ltl.ROperator; import owl.ltl.SyntacticFragment; import owl.ltl.SyntacticFragments; import owl.ltl.UOperator; -import owl.ltl.UnaryModalOperator; import owl.ltl.WOperator; import owl.ltl.XOperator; import owl.ltl.visitors.Converter; @@ -206,7 +204,7 @@ public final class RabinizerBuilder { public static MutableAutomaton build( LabelledFormula formula, Environment environment, RabinizerConfiguration configuration) { - Factories factories = environment.factorySupplier().getFactories(formula.variables()); + Factories factories = environment.factorySupplier().getFactories(formula.atomicPropositions()); Formula phiNormalized = formula.formula().nnf().accept( new UnabbreviateVisitor(WOperator.class, ROperator.class)); // TODO Check if the formula only has a single G @@ -529,7 +527,7 @@ public final class RabinizerBuilder { // Handle the |G| = {} case // TODO: Piggyback on an existing RabinPair. - RabinizerState trueState = RabinizerState.of(eqFactory.getTrue(), List.of()); + RabinizerState trueState = RabinizerState.of(eqFactory.of(BooleanConstant.TRUE), List.of()); if (rabinizerAutomaton.states().contains(trueState)) { assert Objects.equals(Iterables.getOnlyElement(rabinizerAutomaton.successors(trueState)), trueState); @@ -776,14 +774,14 @@ public final class RabinizerBuilder { // TODO Can we optimize for eager? - for (Formula.ModalOperator temporalOperator : equivalenceClass.modalOperators()) { + for (Formula.Temporal temporalOperator : equivalenceClass.modalOperators()) { if (temporalOperator instanceof GOperator) { gOperators.add((GOperator) temporalOperator); } else { Formula unwrapped = temporalOperator; - while (unwrapped instanceof UnaryModalOperator) { - unwrapped = ((UnaryModalOperator) unwrapped).operand; + while (unwrapped instanceof Formula.UnaryTemporalOperator) { + unwrapped = ((Formula.UnaryTemporalOperator) unwrapped).operand; if (unwrapped instanceof GOperator) { break; @@ -794,8 +792,8 @@ public final class RabinizerBuilder { if (unwrapped instanceof GOperator) { gOperators.add((GOperator) unwrapped); - } else if (unwrapped instanceof BinaryModalOperator) { - BinaryModalOperator binaryOperator = (BinaryModalOperator) unwrapped; + } else if (unwrapped instanceof Formula.BinaryTemporalOperator) { + var binaryOperator = (Formula.BinaryTemporalOperator) unwrapped; findSupportingSubFormulas(factory.of(binaryOperator.left), gOperators); findSupportingSubFormulas(factory.of(binaryOperator.right), gOperators); } else { @@ -973,7 +971,8 @@ public final class RabinizerBuilder { // consequent (i.e. the master state). We can omit the conjunction of the active operators // for the antecedent, since we will inject it anyway - AtomicReference antecedent = new AtomicReference<>(eqFactory.getTrue()); + AtomicReference antecedent = new AtomicReference<>( + eqFactory.of(BooleanConstant.TRUE)); int relevantIndex2 = -1; int activeIndex2 = -1; for (int gIndex1 = 0; gIndex1 < activeFormulas.length; gIndex1++) { diff --git a/src/main/java/owl/translations/rabinizer/RabinizerStateFactory.java b/src/main/java/owl/translations/rabinizer/RabinizerStateFactory.java index 5a985f59fa61d12a3b135635232dbc39f308bfd8..b66004fac0fce871595aaae9fc7561f0accc2338 100644 --- a/src/main/java/owl/translations/rabinizer/RabinizerStateFactory.java +++ b/src/main/java/owl/translations/rabinizer/RabinizerStateFactory.java @@ -87,10 +87,10 @@ class RabinizerStateFactory { if (fairnessFragment) { successor = state; } else { - successor = state.temporalStepUnfold(valuation); + successor = state.temporalStep(valuation).unfold(); } } else { - successor = state.unfoldTemporalStep(valuation); + successor = state.unfold().temporalStep(valuation); } // If the master moves into false, there is no way of accepting, since the finite prefix @@ -129,8 +129,8 @@ class RabinizerStateFactory { EquivalenceClass getRankSuccessor(EquivalenceClass equivalenceClass, BitSet valuation) { if (noSubFormula) { return eager - ? equivalenceClass.temporalStepUnfold(valuation) - : equivalenceClass.unfoldTemporalStep(valuation); + ? equivalenceClass.temporalStep(valuation).unfold() + : equivalenceClass.unfold().temporalStep(valuation); } return eager diff --git a/src/test/java/owl/cinterface/DecomposedDPATest.java b/src/test/java/owl/cinterface/DecomposedDPATest.java index 4a5d3caba576bfaeca52a68ca03b7b07815958db..1e0142468bfccfcc18e1216a710dc3efdd103026 100644 --- a/src/test/java/owl/cinterface/DecomposedDPATest.java +++ b/src/test/java/owl/cinterface/DecomposedDPATest.java @@ -235,7 +235,7 @@ class DecomposedDPATest { @Test void testPerformanceComplementConstructionHeuristic() { // Computing the automaton without COMPLEMENT_CONSTRUCTION_HEURISTIC takes minutes. - assertTimeout(Duration.ofSeconds(6), () -> { + assertTimeout(Duration.ofSeconds(2), () -> { var formula = LtlParser.syntax( "((FGp2|GFp1)&(FGp3|GFp2)&(FGp4|GFp3)&(FGp5|GFp4)&(FGp6|GFp5))"); of(formula, true, false, 0); @@ -244,7 +244,7 @@ class DecomposedDPATest { @Test void testPerformanceAmbaDecomposedLock12() { - assertTimeout(Duration.ofSeconds(10), () -> { + assertTimeout(Duration.ofSeconds(2), () -> { var ambaDecomposedLockLiterals = new ArrayList(); ambaDecomposedLockLiterals.add("decide"); IntStream.range(0, 12).mapToObj(x -> "hlock_" + x).forEach(ambaDecomposedLockLiterals::add); diff --git a/src/test/java/owl/cinterface/DeterministicAutomatonTest.java b/src/test/java/owl/cinterface/DeterministicAutomatonTest.java index 885958cac17b0cde8916fb7b3fb3062b8656dd01..97b6d0a4d201ccfb74a872a493d57a70525bcd96 100644 --- a/src/test/java/owl/cinterface/DeterministicAutomatonTest.java +++ b/src/test/java/owl/cinterface/DeterministicAutomatonTest.java @@ -76,7 +76,7 @@ class DeterministicAutomatonTest { assertTimeout(Duration.ofMillis(100), () -> { var formula = LtlParser.parse("(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v)" + "& X G (w | x | y)"); - assertEquals(25, formula.variables().size()); + assertEquals(25, formula.atomicPropositions().size()); var instance1 = DeterministicAutomaton.of(formula); var instance2 = DeterministicAutomaton.of(formula.not()); diff --git a/src/test/java/owl/ltl/BddEquivalenceClassTest.java b/src/test/java/owl/ltl/BddEquivalenceClassTest.java index 4125357701403ef5138ea0e3fb135339a49a2537..06a621b6d662aeccc8ba2b3828ccdd437beecff9 100644 --- a/src/test/java/owl/ltl/BddEquivalenceClassTest.java +++ b/src/test/java/owl/ltl/BddEquivalenceClassTest.java @@ -26,6 +26,6 @@ public class BddEquivalenceClassTest extends EquivalenceClassTest { @Override protected EquivalenceClassFactory obtainFactory(LabelledFormula domain) { return Environment.annotated().factorySupplier() - .getEquivalenceClassFactory(domain.variables(), false); + .getEquivalenceClassFactory(domain.atomicPropositions()); } } \ No newline at end of file diff --git a/src/test/java/owl/ltl/EquivalenceClassTest.java b/src/test/java/owl/ltl/EquivalenceClassTest.java index 1fb76fc9af8214a2e90fccfe23517b8013f8c6d7..4211aa7bfca12f2d450f15261aed4480b55b13c2 100644 --- a/src/test/java/owl/ltl/EquivalenceClassTest.java +++ b/src/test/java/owl/ltl/EquivalenceClassTest.java @@ -25,6 +25,7 @@ import static org.junit.jupiter.api.Assertions.assertNotNull; import static org.junit.jupiter.api.Assertions.assertTrue; import static owl.util.Assertions.assertThat; +import de.tum.in.naturals.bitset.BitSets; import java.util.BitSet; import java.util.List; import java.util.Set; @@ -77,7 +78,7 @@ abstract class EquivalenceClassTest { @Test void testEquivalent() { - EquivalenceClass equivalenceClass = factory.getFalse(); + EquivalenceClass equivalenceClass = factory.of(BooleanConstant.FALSE); assertEquals(equivalenceClass, equivalenceClass); assertEquals(equivalenceClass, factory.of(SimplifierFactory @@ -235,6 +236,28 @@ abstract class EquivalenceClassTest { factory.of(LtlParser.syntax("X a")).temporalStep(stepSet)); } + @Test + void testTemporalStepTree() { + var formula = LtlParser.parse("G (a | b | X c)"); + var factory = obtainFactory(formula); + var clazz = factory.of(formula.formula()); + + var formula1 = formula.formula(); + var tree1 = clazz.temporalStepTree(); + + var formula2 = formula1.unfold(); + var tree2 = clazz.unfold().temporalStepTree(); + + var formula3 = formula2.temporalStep(new BitSet()).unfold(); + var tree3 = tree2.get(new BitSet()).iterator().next().unfold().temporalStepTree(); + + for (BitSet set : BitSets.powerSet(4)) { + assertEquals(Set.of(factory.of(formula1.temporalStep(set))), tree1.get(set)); + assertEquals(Set.of(factory.of(formula2.temporalStep(set))), tree2.get(set)); + assertEquals(Set.of(factory.of(formula3.temporalStep(set))), tree3.get(set)); + } + } + @Test void testUnfoldUnfold() { for (LabelledFormula formula : formulas) { @@ -249,10 +272,10 @@ abstract class EquivalenceClassTest { @Test void testTruthness() { double precision = 0.000_000_01d; - assertEquals(1.0d, factory.getTrue().trueness(), precision); + assertEquals(1.0d, factory.of(BooleanConstant.TRUE).trueness(), precision); assertEquals(0.75d, factory.of(LtlParser.syntax("a | b")).trueness(), precision); assertEquals(0.5d, factory.of(LtlParser.syntax("a")).trueness(), precision); assertEquals(0.25d, factory.of(LtlParser.syntax("a & b")).trueness(), precision); - assertEquals(0.0d, factory.getFalse().trueness(), precision); + assertEquals(0.0d, factory.of(BooleanConstant.FALSE).trueness(), precision); } } diff --git a/src/test/java/owl/ltl/FormulaTest.java b/src/test/java/owl/ltl/FormulaTest.java index a533a9b479aff26e572e1033c66698b77256e921..57b39e9e2a380b38d33e9e49a5dbbe352e7c8830 100644 --- a/src/test/java/owl/ltl/FormulaTest.java +++ b/src/test/java/owl/ltl/FormulaTest.java @@ -25,7 +25,6 @@ import static org.junit.jupiter.api.Assertions.assertTrue; import com.google.common.collect.Lists; import java.util.Arrays; -import java.util.BitSet; import java.util.Comparator; import java.util.List; import java.util.Set; @@ -36,7 +35,6 @@ import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; import owl.ltl.parser.LtlParser; -@SuppressWarnings("PMD.UnusedPrivateMethod") public class FormulaTest { private static final List FORMULAS = List.of( @@ -69,21 +67,6 @@ public class FormulaTest { LtlParser.syntax("G (X (a <-> b))"), LtlParser.syntax("G (X (a xor b))")); - - private static final BitSet ONE = new BitSet(); - - private static final BitSet THREE = new BitSet(); - - private static final BitSet TWO = new BitSet(); - - private static final BitSet ZERO = new BitSet(); - - static { - ONE.set(0); - TWO.set(1); - THREE.set(0, 2); - } - public static List formulaProvider() { return FORMULAS; } @@ -93,23 +76,18 @@ public class FormulaTest { .stream().map(x -> Arguments.of(x.get(0), x.get(1))); } - private static Stream temporalStepCartesianProductProvider() { - return Lists.cartesianProduct(FORMULAS, List.of(ZERO, ONE, TWO, THREE)) - .stream().map(x -> Arguments.of(x.toArray())); - } - @ParameterizedTest @MethodSource("formulaProvider") void allMatch(Formula formula) { - Set subformulas = formula.subformulas(Formula.TemporalOperator.class); + Set subformulas = formula.subformulas(Formula.Temporal.class); assertTrue(formula.allMatch( - x -> x instanceof Formula.LogicalOperator || subformulas.contains(x))); + x -> x instanceof Formula.Propositional || subformulas.contains(x))); } @ParameterizedTest @MethodSource("formulaProvider") void anyMatch(Formula formula) { - for (Formula x : formula.subformulas(Formula.TemporalOperator.class)) { + for (Formula x : formula.subformulas(Formula.Temporal.class)) { assertTrue(formula.anyMatch(x::equals)); } } @@ -158,16 +136,4 @@ public class FormulaTest { assertEquals(formula, formula.not().not()); assertEquals(formula.not(), formula.not().not().not()); } - - @ParameterizedTest - @MethodSource("temporalStepCartesianProductProvider") - void temporalStepUnfold(Formula formula, BitSet bitSet) { - assertEquals(formula.temporalStep(bitSet).unfold(), formula.temporalStepUnfold(bitSet)); - } - - @ParameterizedTest - @MethodSource("temporalStepCartesianProductProvider") - void unfoldTemporalStep(Formula formula, BitSet bitSet) { - assertEquals(formula.unfold().temporalStep(bitSet), formula.unfoldTemporalStep(bitSet)); - } } diff --git a/src/test/java/owl/ltl/LabelledFormulaTest.java b/src/test/java/owl/ltl/LabelledFormulaTest.java index 229ea0f5d6ae19c9e5e8864701fc88389c06b5fc..a9966231e921637b4d119986ee0533eb8139f4e0 100644 --- a/src/test/java/owl/ltl/LabelledFormulaTest.java +++ b/src/test/java/owl/ltl/LabelledFormulaTest.java @@ -11,7 +11,7 @@ class LabelledFormulaTest { @Test void ofReduced() { var formula = LabelledFormula.of(LtlParser.syntax("a"), List.of("a", "b", "c")); - assertEquals(List.of("a"), formula.variables()); + assertEquals(List.of("a"), formula.atomicPropositions()); } @Test diff --git a/src/test/java/owl/ltl/parser/LtlParserTest.java b/src/test/java/owl/ltl/parser/LtlParserTest.java index a9336869ab107f48474a213ff6710cbc5379221d..fab33efed69237e49f6782352b09229ea679f331 100644 --- a/src/test/java/owl/ltl/parser/LtlParserTest.java +++ b/src/test/java/owl/ltl/parser/LtlParserTest.java @@ -74,14 +74,14 @@ class LtlParserTest { @Test void testSingleQuotedLiteralParsing() { LabelledFormula formula = LtlParser.parse("'a b c'"); - assertEquals(List.of("a b c"), formula.variables()); + assertEquals(List.of("a b c"), formula.atomicPropositions()); assertEquals(Literal.of(0), formula.formula()); } @Test void testDoubleQuotedLiteralParsing() { LabelledFormula formula = LtlParser.parse("\"a b c\""); - assertEquals(List.of("a b c"), formula.variables()); + assertEquals(List.of("a b c"), formula.atomicPropositions()); assertEquals(Literal.of(0), formula.formula()); } diff --git a/src/test/java/owl/ltl/rewriter/NormalFormsTest.java b/src/test/java/owl/ltl/rewriter/NormalFormsTest.java index bdd47212326331bc0fdd07322526d9c948932d11..8f4b614466d8d15c1739f77fa09e8d8e19335a61 100644 --- a/src/test/java/owl/ltl/rewriter/NormalFormsTest.java +++ b/src/test/java/owl/ltl/rewriter/NormalFormsTest.java @@ -135,7 +135,7 @@ class NormalFormsTest { @MethodSource("labelledFormulaProvider") void testCorrectness(LabelledFormula formula) { var factory = Environment.of(false) - .factorySupplier().getEquivalenceClassFactory(formula.variables()); + .factorySupplier().getEquivalenceClassFactory(formula.atomicPropositions()); assertEquals(factory.of(formula.formula()), factory.of(NormalForms.toDnfFormula(formula.formula()))); @@ -153,8 +153,8 @@ class NormalFormsTest { @Test void testSyntheticLiteralFeature() { var labelledFormula = LtlParser.parse("(a | b | X c)", List.of("a", "b", "c")); - var clause1 = Set.of(LtlParser.syntax("a | b", labelledFormula.variables())); - var clause2 = Set.of(LtlParser.syntax("X c", labelledFormula.variables())); + var clause1 = Set.of(LtlParser.syntax("a | b", labelledFormula.atomicPropositions())); + var clause2 = Set.of(LtlParser.syntax("X c", labelledFormula.atomicPropositions())); assertEquals(Set.of(clause1, clause2), NormalForms.toDnf(labelledFormula.formula(), x -> x.children().stream().filter(Literal.class::isInstance).collect(Collectors.toSet()))); diff --git a/src/test/java/owl/ltl/util/FormulaIsomorphismTest.java b/src/test/java/owl/ltl/util/FormulaIsomorphismTest.java index 5519f23be080033429d12f06abc403899c2e2e32..c1a42f1f841a3275f39c77b7a6d51f9d1571428f 100644 --- a/src/test/java/owl/ltl/util/FormulaIsomorphismTest.java +++ b/src/test/java/owl/ltl/util/FormulaIsomorphismTest.java @@ -85,7 +85,7 @@ class FormulaIsomorphismTest { + "&& (((r_2) && (X (r_5))) -> (X ((g_2) && (g_5))))\n" + "&& (((r_3) && (X (r_4))) -> (X ((g_3) && (g_4))))\n" + "&& (((r_3) && (X (r_5))) -> (X ((g_3) && (g_5))))\n" - + "&& (((r_4) && (X (r_5))) -> (X ((g_4) && (g_5))))", formula1.variables()); + + "&& (((r_4) && (X (r_5))) -> (X ((g_4) && (g_5))))", formula1.atomicPropositions()); assertTimeout(Duration.ofMillis(500), () -> assertNull(FormulaIsomorphism.compute(formula1.formula(), formula2.formula()))); diff --git a/src/test/java/owl/translations/LTL2DAModuleFunctionTest.java b/src/test/java/owl/translations/LTL2DAModuleFunctionTest.java index 058c701877dee78eec2627aa4cafc29cd11197fc..8fd176b6a24a284c8fdc4d0a264a8e4d982e6fe2 100644 --- a/src/test/java/owl/translations/LTL2DAModuleFunctionTest.java +++ b/src/test/java/owl/translations/LTL2DAModuleFunctionTest.java @@ -31,6 +31,7 @@ import owl.automaton.Automaton; import owl.automaton.acceptance.ParityAcceptance; import owl.automaton.algorithms.LanguageEmptiness; import owl.automaton.edge.Edge; +import owl.ltl.BooleanConstant; import owl.ltl.EquivalenceClass; import owl.ltl.parser.LtlParser; import owl.run.Environment; @@ -57,7 +58,7 @@ class LTL2DAModuleFunctionTest { @Test void performanceSafety() { var formula = LtlParser.parse(LARGE); - assertEquals(29, formula.variables().size()); + assertEquals(29, formula.atomicPropositions().size()); var automaton = (Automaton) TRANSLATOR.apply(formula); var state = automaton.onlyInitialState(); @@ -71,10 +72,10 @@ class LTL2DAModuleFunctionTest { @Test void performanceCosafety() { var formula = LtlParser.parse(LARGE).not(); - assertEquals(29, formula.variables().size()); + assertEquals(29, formula.atomicPropositions().size()); var automaton = (Automaton) TRANSLATOR.apply(formula); - var state = automaton.onlyInitialState().factory().getTrue(); + var state = automaton.onlyInitialState().factory().of(BooleanConstant.TRUE); var edge = Edge.of(state, 0); // Check true sink. diff --git a/src/test/java/owl/translations/canonical/DeterministicConstructionsPortfolioTest.java b/src/test/java/owl/translations/canonical/DeterministicConstructionsPortfolioTest.java index f162690fe04b88f091543dc4316ece9f85664aa2..8dbd45d405d93574a6c86ffb91ca1530554ea9f4 100644 --- a/src/test/java/owl/translations/canonical/DeterministicConstructionsPortfolioTest.java +++ b/src/test/java/owl/translations/canonical/DeterministicConstructionsPortfolioTest.java @@ -31,18 +31,29 @@ import static owl.util.Assertions.assertThat; import de.tum.in.naturals.bitset.BitSets; import java.util.List; +import java.util.stream.Collectors; +import java.util.stream.IntStream; +import org.junit.jupiter.api.Disabled; import org.junit.jupiter.api.Nested; import org.junit.jupiter.api.Test; import org.junit.jupiter.api.TestInstance; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; +import org.junit.jupiter.params.provider.ValueSource; import owl.automaton.Automaton; import owl.automaton.acceptance.AllAcceptance; import owl.automaton.acceptance.BuchiAcceptance; import owl.automaton.acceptance.CoBuchiAcceptance; import owl.automaton.output.HoaPrinter; +import owl.ltl.Conjunction; +import owl.ltl.Disjunction; import owl.ltl.EquivalenceClass; +import owl.ltl.GOperator; +import owl.ltl.LabelledFormula; +import owl.ltl.Literal; +import owl.ltl.UOperator; +import owl.ltl.XOperator; import owl.ltl.parser.LtlParser; import owl.run.Environment; @@ -234,4 +245,61 @@ class DeterministicConstructionsPortfolioTest { } } } + + @Disabled + @ParameterizedTest + @ValueSource( + ints = {8, 10, 12, 14, 16}) + void coSafetyDeepNesting(int k) { + var formula = LabelledFormula.of( + leftNestedU(k), + IntStream.range(0, k + 1).mapToObj(i -> "a" + i).collect(Collectors.toUnmodifiableList())); + var automaton = coSafety(Environment.annotated(), formula); + automaton.states(); + } + + @Disabled + @ParameterizedTest + @ValueSource( + ints = {8, 16, 32, 64}) + void safetyLargeAlphabet(int k) { + var automaton = safety(Environment.standard(), largeAlphabetSafety(k)); + automaton.edgeTree(automaton.onlyInitialState()); + } + + @Disabled + @ParameterizedTest + @ValueSource( + ints = {8, 10, 12, 14, 16}) + void safetyLargeStateSpace(int k) { + var automaton = safety(Environment.standard(), largeStateSpaceSafety(k)); + automaton.states(); + } + + LabelledFormula largeAlphabetSafety(int k) { + var conjunction = Conjunction.of( + IntStream.range(0, k) + .mapToObj(x -> Disjunction.of(Literal.of(2 * x), Literal.of(2 * x + 1)))); + return LabelledFormula.of( + GOperator.of(conjunction), + IntStream.range(0, 2 * k).mapToObj(i -> "a" + i).collect(Collectors.toUnmodifiableList())); + } + + LabelledFormula largeStateSpaceSafety(int k) { + var disjunction = Disjunction.of( + IntStream.range(0, k) + .mapToObj(x -> Conjunction.of(Literal.of(2 * x), XOperator.of(Literal.of(2 * x + 1))))); + return LabelledFormula.of( + new GOperator(disjunction), + IntStream.range(0, 2 * k) + .mapToObj(i -> "a" + i).collect(Collectors.toUnmodifiableList())); + } + + UOperator leftNestedU(int i) { + if (i <= 1) { + return new UOperator(Literal.of(0), Literal.of(1)); + } + + return new UOperator(leftNestedU(i - 1), Literal.of(i)); + } } \ No newline at end of file