From 2e0bceb2f25989713f1baf6311d3787c3003d794 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 6 Nov 2023 00:38:12 +0100 Subject: feat: predicates as reference types Now unary predicates may be used as types for cross-references. This might create circular references between predicate, but no differently than when the user manually creates predicates with circular references. The reference types of containment and container references still have to be classes, because we use the class hierarchy to encode contained types. --- .../DirectedCrossReferenceRefiner.java | 10 ++++++-- .../translator/metamodel/MetamodelBuilder.java | 30 ++++++++++++++-------- 2 files changed, 27 insertions(+), 13 deletions(-) (limited to 'subprojects/store-reasoning/src') diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java index 0700f9f7..2e804b44 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java @@ -15,15 +15,17 @@ import tools.refinery.store.representation.TruthValue; import tools.refinery.store.tuple.Tuple; class DirectedCrossReferenceRefiner extends ConcreteSymbolRefiner { + private final PartialRelation targetType; private final PartialInterpretationRefiner sourceRefiner; - private final PartialInterpretationRefiner targetRefiner; + private PartialInterpretationRefiner targetRefiner; public DirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, Symbol concreteSymbol, PartialRelation sourceType, PartialRelation targetType) { super(adapter, partialSymbol, concreteSymbol); + this.targetType = targetType; + // Source is always a class, so we can rely on the fact that it is always constructed before this refiner. sourceRefiner = adapter.getRefiner(sourceType); - targetRefiner = adapter.getRefiner(targetType); } @Override @@ -32,6 +34,10 @@ class DirectedCrossReferenceRefiner extends ConcreteSymbolRefiner Date: Wed, 15 Nov 2023 23:34:41 +0100 Subject: fix: contains assertions --- .../ProblemCrossrefProposalProvider.java | 6 -- .../store/reasoning/scope/PredicateScopeTest.java | 2 + .../ContainmentHierarchyTranslator.java | 38 +++++++----- .../containment/ContainmentLinkRefiner.java | 4 +- .../translator/containment/ContainsRefiner.java | 71 ++++++++++++++++++++++ .../containment/InferredContainment.java | 2 +- .../containment/MustAnyContainmentLinkView.java | 21 +++++++ 7 files changed, 120 insertions(+), 24 deletions(-) create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustAnyContainmentLinkView.java (limited to 'subprojects/store-reasoning/src') diff --git a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java index 27e936a1..166b4400 100644 --- a/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java +++ b/subprojects/language-ide/src/main/java/tools/refinery/language/ide/contentassist/ProblemCrossrefProposalProvider.java @@ -169,12 +169,6 @@ public class ProblemCrossrefProposalProvider extends IdeCrossrefProposalProvider return supertypeShouldBeVisible(candidate, context, builtinSymbols, candidateEObjectOrProxy); } - if (eReference.equals(ProblemPackage.Literals.ASSERTION__RELATION)) { - // Currently, we don't support assertions on the {@code contains} relation. - return !builtinSymbols.contains().equals(candidateEObjectOrProxy) && - !builtinSymbols.contained().equals(candidateEObjectOrProxy); - } - return true; } diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java index d21bd12e..a2c56a6b 100644 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java @@ -84,6 +84,8 @@ class PredicateScopeTest { .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) .seed(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, + builder -> builder.reducedValue(TruthValue.UNKNOWN)) .seed(index, builder -> builder.reducedValue(TruthValue.TRUE)) .seed(next, builder -> builder .reducedValue(TruthValue.UNKNOWN) diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java index 61037be3..c85bd8b7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java @@ -52,9 +52,10 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { private final Symbol containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class, InferredContainment.UNKNOWN); + private final AnySymbolView mustAnyContainmentLinkView = new MustAnyContainmentLinkView(containsStorage); private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage); private final RelationalQuery containsMayNewTargetHelper; - private final RelationalQuery containsMayExistingHelper; + private final RelationalQuery containsWithoutLink; private final RelationalQuery weakComponents; private final RelationalQuery strongComponents; private final Map containmentInfoMap; @@ -67,18 +68,15 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder .clause(Integer.class, existingContainers -> List.of( may(CONTAINED_SYMBOL.call(child)), - new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, List.of(Variable.of(), child)), + new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, + List.of(Variable.of(), child)), check(less(existingContainers, constant(1))) ))); - containsMayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder - .clause(Integer.class, existingContainers -> List.of( - must(CONTAINS_SYMBOL.call(parent, child)), - not(forbiddenContainsView.call(parent, child)) - // Violation of monotonicity: - // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the - // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid. - ))); + containsWithoutLink = Query.of(name + "#withoutLink", (builder, parent, child) -> builder.clause( + must(CONTAINS_SYMBOL.call(parent, child)), + not(mustAnyContainmentLinkView.call(parent, child)) + )); var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause( must(CONTAINS_SYMBOL.call(parent, child)), @@ -139,13 +137,21 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause( mayNewSourceHelper.call(parent), mayNewTargetHelper.call(child), - not(must(CONTAINS_SYMBOL.call(parent, child))), + not(mustAnyContainmentLinkView.call(parent, child)), not(forbiddenLinkView.call(parent, child)) )); + var existingContainsLink = Query.of(name + "#existingContaints", (builder, parent, child) -> builder + .clause( + must(linkType.call(parent, child)) + ) + .clause( + containsWithoutLink.call(parent, child) + )); + var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause( - must(linkType.call(parent, child)), - containsMayExistingHelper.call(parent, child), + existingContainsLink.call(parent, child), + not(forbiddenContainsView.call(parent, child)), may(sourceType.call(parent)), may(targetType.call(child)), not(forbiddenLinkView.call(parent, child)) @@ -224,7 +230,9 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { })) .must(Query.of(mustName, (builder, parent, child) -> builder.clause( new MustContainsView(containsStorage).call(parent, child) - )))); + ))) + .refiner(ContainsRefiner.of(containsStorage)) + .initializer(new RefinementBasedInitializer<>(CONTAINS_SYMBOL))); } private void translateInvalidContainer(ModelStoreBuilder storeBuilder) { @@ -245,7 +253,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { ) .clause(container -> List.of( MultiObjectTranslator.MULTI_VIEW.call(multi), - must(CONTAINS_SYMBOL.call(container, multi)), + mustAnyContainmentLinkView.call(container, multi), not(MultiObjectTranslator.MULTI_VIEW.call(container)) )) .action( diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java index 497ed98f..e44fcffd 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java @@ -24,8 +24,8 @@ class ContainmentLinkRefiner extends AbstractPartialInterpretationRefiner sourceRefiner; private final PartialInterpretationRefiner targetRefiner; - public ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, - Factory factory) { + private ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + Factory factory) { super(adapter, partialSymbol); this.factory = factory; interpretation = adapter.getModel().getInterpretation(factory.symbol); diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java new file mode 100644 index 00000000..a7196a1c --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java @@ -0,0 +1,71 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; +import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; +import tools.refinery.store.reasoning.representation.PartialSymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.Set; + +class ContainsRefiner extends AbstractPartialInterpretationRefiner { + private static final Map EMPTY_VALUES; + + static { + var values = TruthValue.values(); + EMPTY_VALUES = new LinkedHashMap<>(values.length); + for (var value : values) { + EMPTY_VALUES.put(value, new InferredContainment(value, Set.of(), Set.of())); + } + } + + private final Interpretation interpretation; + private final PartialInterpretationRefiner containedRefiner; + + private ContainsRefiner(ReasoningAdapter adapter, PartialSymbol partialSymbol, + Symbol containsStorage) { + super(adapter, partialSymbol); + interpretation = adapter.getModel().getInterpretation(containsStorage); + containedRefiner = adapter.getRefiner(ContainmentHierarchyTranslator.CONTAINED_SYMBOL); + } + + @Override + public boolean merge(Tuple key, TruthValue value) { + var oldValue = interpretation.get(key); + var newValue = mergeLink(oldValue, value); + if (oldValue != newValue) { + interpretation.put(key, newValue); + } + if (value.must()) { + return containedRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); + } + return true; + } + + public InferredContainment mergeLink(InferredContainment oldValue, TruthValue toMerge) { + var newContains = oldValue.contains().merge(toMerge); + if (newContains.equals(oldValue.contains())) { + return oldValue; + } + var mustLinks = oldValue.mustLinks(); + var forbiddenLinks = oldValue.forbiddenLinks(); + if (mustLinks.isEmpty() && forbiddenLinks.isEmpty()) { + return EMPTY_VALUES.get(newContains); + } + return new InferredContainment(newContains, mustLinks, forbiddenLinks); + } + + public static PartialInterpretationRefiner.Factory of(Symbol symbol) { + return (adapter, partialSymbol) -> new ContainsRefiner(adapter, partialSymbol, symbol); + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java index 8df23d9a..8a757ed2 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java @@ -24,7 +24,7 @@ final class InferredContainment { this.contains = adjustContains(contains, mustLinks, forbiddenLinks); this.mustLinks = mustLinks; this.forbiddenLinks = forbiddenLinks; - hashCode = Objects.hash(contains, mustLinks, forbiddenLinks); + hashCode = Objects.hash(this.contains, mustLinks, forbiddenLinks); } private static TruthValue adjustContains(TruthValue contains, Set mustLinks, diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustAnyContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustAnyContainmentLinkView.java new file mode 100644 index 00000000..1cc537c6 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustAnyContainmentLinkView.java @@ -0,0 +1,21 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.containment; + +import tools.refinery.store.query.view.TuplePreservingView; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +class MustAnyContainmentLinkView extends TuplePreservingView { + public MustAnyContainmentLinkView(Symbol symbol) { + super(symbol, "contains#mustAnyLink"); + } + + @Override + protected boolean doFilter(Tuple key, InferredContainment value) { + return !value.mustLinks().isEmpty(); + } +} -- cgit v1.2.3-54-g00ecf