diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-11-15 23:34:41 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-11-17 14:53:26 +0100 |
commit | caae5494ef22e31eb5f135f7f877b89b7155ce1e (patch) | |
tree | 4e9c259ca2ca23013267fd676cd179ca4abee1bb /subprojects | |
parent | feat(language): opposite reference validation (diff) | |
download | refinery-caae5494ef22e31eb5f135f7f877b89b7155ce1e.tar.gz refinery-caae5494ef22e31eb5f135f7f877b89b7155ce1e.tar.zst refinery-caae5494ef22e31eb5f135f7f877b89b7155ce1e.zip |
fix: contains assertions
Diffstat (limited to 'subprojects')
7 files changed, 120 insertions, 24 deletions
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 | |||
169 | return supertypeShouldBeVisible(candidate, context, builtinSymbols, candidateEObjectOrProxy); | 169 | return supertypeShouldBeVisible(candidate, context, builtinSymbols, candidateEObjectOrProxy); |
170 | } | 170 | } |
171 | 171 | ||
172 | if (eReference.equals(ProblemPackage.Literals.ASSERTION__RELATION)) { | ||
173 | // Currently, we don't support assertions on the {@code contains} relation. | ||
174 | return !builtinSymbols.contains().equals(candidateEObjectOrProxy) && | ||
175 | !builtinSymbols.contained().equals(candidateEObjectOrProxy); | ||
176 | } | ||
177 | |||
178 | return true; | 172 | return true; |
179 | } | 173 | } |
180 | 174 | ||
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 { | |||
84 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) | 84 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) |
85 | .seed(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, | 85 | .seed(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, |
86 | builder -> builder.reducedValue(TruthValue.UNKNOWN)) | 86 | builder -> builder.reducedValue(TruthValue.UNKNOWN)) |
87 | .seed(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, | ||
88 | builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
87 | .seed(index, builder -> builder.reducedValue(TruthValue.TRUE)) | 89 | .seed(index, builder -> builder.reducedValue(TruthValue.TRUE)) |
88 | .seed(next, builder -> builder | 90 | .seed(next, builder -> builder |
89 | .reducedValue(TruthValue.UNKNOWN) | 91 | .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 { | |||
52 | 52 | ||
53 | private final Symbol<InferredContainment> containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class, | 53 | private final Symbol<InferredContainment> containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class, |
54 | InferredContainment.UNKNOWN); | 54 | InferredContainment.UNKNOWN); |
55 | private final AnySymbolView mustAnyContainmentLinkView = new MustAnyContainmentLinkView(containsStorage); | ||
55 | private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage); | 56 | private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage); |
56 | private final RelationalQuery containsMayNewTargetHelper; | 57 | private final RelationalQuery containsMayNewTargetHelper; |
57 | private final RelationalQuery containsMayExistingHelper; | 58 | private final RelationalQuery containsWithoutLink; |
58 | private final RelationalQuery weakComponents; | 59 | private final RelationalQuery weakComponents; |
59 | private final RelationalQuery strongComponents; | 60 | private final RelationalQuery strongComponents; |
60 | private final Map<PartialRelation, ContainmentInfo> containmentInfoMap; | 61 | private final Map<PartialRelation, ContainmentInfo> containmentInfoMap; |
@@ -67,18 +68,15 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
67 | containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder | 68 | containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder |
68 | .clause(Integer.class, existingContainers -> List.of( | 69 | .clause(Integer.class, existingContainers -> List.of( |
69 | may(CONTAINED_SYMBOL.call(child)), | 70 | may(CONTAINED_SYMBOL.call(child)), |
70 | new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, List.of(Variable.of(), child)), | 71 | new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, |
72 | List.of(Variable.of(), child)), | ||
71 | check(less(existingContainers, constant(1))) | 73 | check(less(existingContainers, constant(1))) |
72 | ))); | 74 | ))); |
73 | 75 | ||
74 | containsMayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder | 76 | containsWithoutLink = Query.of(name + "#withoutLink", (builder, parent, child) -> builder.clause( |
75 | .clause(Integer.class, existingContainers -> List.of( | 77 | must(CONTAINS_SYMBOL.call(parent, child)), |
76 | must(CONTAINS_SYMBOL.call(parent, child)), | 78 | not(mustAnyContainmentLinkView.call(parent, child)) |
77 | not(forbiddenContainsView.call(parent, child)) | 79 | )); |
78 | // Violation of monotonicity: | ||
79 | // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
80 | // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid. | ||
81 | ))); | ||
82 | 80 | ||
83 | var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause( | 81 | var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause( |
84 | must(CONTAINS_SYMBOL.call(parent, child)), | 82 | must(CONTAINS_SYMBOL.call(parent, child)), |
@@ -139,13 +137,21 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
139 | var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause( | 137 | var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause( |
140 | mayNewSourceHelper.call(parent), | 138 | mayNewSourceHelper.call(parent), |
141 | mayNewTargetHelper.call(child), | 139 | mayNewTargetHelper.call(child), |
142 | not(must(CONTAINS_SYMBOL.call(parent, child))), | 140 | not(mustAnyContainmentLinkView.call(parent, child)), |
143 | not(forbiddenLinkView.call(parent, child)) | 141 | not(forbiddenLinkView.call(parent, child)) |
144 | )); | 142 | )); |
145 | 143 | ||
144 | var existingContainsLink = Query.of(name + "#existingContaints", (builder, parent, child) -> builder | ||
145 | .clause( | ||
146 | must(linkType.call(parent, child)) | ||
147 | ) | ||
148 | .clause( | ||
149 | containsWithoutLink.call(parent, child) | ||
150 | )); | ||
151 | |||
146 | var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause( | 152 | var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause( |
147 | must(linkType.call(parent, child)), | 153 | existingContainsLink.call(parent, child), |
148 | containsMayExistingHelper.call(parent, child), | 154 | not(forbiddenContainsView.call(parent, child)), |
149 | may(sourceType.call(parent)), | 155 | may(sourceType.call(parent)), |
150 | may(targetType.call(child)), | 156 | may(targetType.call(child)), |
151 | not(forbiddenLinkView.call(parent, child)) | 157 | not(forbiddenLinkView.call(parent, child)) |
@@ -224,7 +230,9 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
224 | })) | 230 | })) |
225 | .must(Query.of(mustName, (builder, parent, child) -> builder.clause( | 231 | .must(Query.of(mustName, (builder, parent, child) -> builder.clause( |
226 | new MustContainsView(containsStorage).call(parent, child) | 232 | new MustContainsView(containsStorage).call(parent, child) |
227 | )))); | 233 | ))) |
234 | .refiner(ContainsRefiner.of(containsStorage)) | ||
235 | .initializer(new RefinementBasedInitializer<>(CONTAINS_SYMBOL))); | ||
228 | } | 236 | } |
229 | 237 | ||
230 | private void translateInvalidContainer(ModelStoreBuilder storeBuilder) { | 238 | private void translateInvalidContainer(ModelStoreBuilder storeBuilder) { |
@@ -245,7 +253,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
245 | ) | 253 | ) |
246 | .clause(container -> List.of( | 254 | .clause(container -> List.of( |
247 | MultiObjectTranslator.MULTI_VIEW.call(multi), | 255 | MultiObjectTranslator.MULTI_VIEW.call(multi), |
248 | must(CONTAINS_SYMBOL.call(container, multi)), | 256 | mustAnyContainmentLinkView.call(container, multi), |
249 | not(MultiObjectTranslator.MULTI_VIEW.call(container)) | 257 | not(MultiObjectTranslator.MULTI_VIEW.call(container)) |
250 | )) | 258 | )) |
251 | .action( | 259 | .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<TruthV | |||
24 | private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner; | 24 | private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner; |
25 | private final PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner; | 25 | private final PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner; |
26 | 26 | ||
27 | public ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | 27 | private ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, |
28 | Factory factory) { | 28 | Factory factory) { |
29 | super(adapter, partialSymbol); | 29 | super(adapter, partialSymbol); |
30 | this.factory = factory; | 30 | this.factory = factory; |
31 | interpretation = adapter.getModel().getInterpretation(factory.symbol); | 31 | 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 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
10 | import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner; | ||
11 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | ||
12 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | import tools.refinery.store.representation.TruthValue; | ||
15 | import tools.refinery.store.tuple.Tuple; | ||
16 | |||
17 | import java.util.LinkedHashMap; | ||
18 | import java.util.Map; | ||
19 | import java.util.Set; | ||
20 | |||
21 | class ContainsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> { | ||
22 | private static final Map<TruthValue, InferredContainment> EMPTY_VALUES; | ||
23 | |||
24 | static { | ||
25 | var values = TruthValue.values(); | ||
26 | EMPTY_VALUES = new LinkedHashMap<>(values.length); | ||
27 | for (var value : values) { | ||
28 | EMPTY_VALUES.put(value, new InferredContainment(value, Set.of(), Set.of())); | ||
29 | } | ||
30 | } | ||
31 | |||
32 | private final Interpretation<InferredContainment> interpretation; | ||
33 | private final PartialInterpretationRefiner<TruthValue, Boolean> containedRefiner; | ||
34 | |||
35 | private ContainsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol, | ||
36 | Symbol<InferredContainment> containsStorage) { | ||
37 | super(adapter, partialSymbol); | ||
38 | interpretation = adapter.getModel().getInterpretation(containsStorage); | ||
39 | containedRefiner = adapter.getRefiner(ContainmentHierarchyTranslator.CONTAINED_SYMBOL); | ||
40 | } | ||
41 | |||
42 | @Override | ||
43 | public boolean merge(Tuple key, TruthValue value) { | ||
44 | var oldValue = interpretation.get(key); | ||
45 | var newValue = mergeLink(oldValue, value); | ||
46 | if (oldValue != newValue) { | ||
47 | interpretation.put(key, newValue); | ||
48 | } | ||
49 | if (value.must()) { | ||
50 | return containedRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE); | ||
51 | } | ||
52 | return true; | ||
53 | } | ||
54 | |||
55 | public InferredContainment mergeLink(InferredContainment oldValue, TruthValue toMerge) { | ||
56 | var newContains = oldValue.contains().merge(toMerge); | ||
57 | if (newContains.equals(oldValue.contains())) { | ||
58 | return oldValue; | ||
59 | } | ||
60 | var mustLinks = oldValue.mustLinks(); | ||
61 | var forbiddenLinks = oldValue.forbiddenLinks(); | ||
62 | if (mustLinks.isEmpty() && forbiddenLinks.isEmpty()) { | ||
63 | return EMPTY_VALUES.get(newContains); | ||
64 | } | ||
65 | return new InferredContainment(newContains, mustLinks, forbiddenLinks); | ||
66 | } | ||
67 | |||
68 | public static PartialInterpretationRefiner.Factory<TruthValue, Boolean> of(Symbol<InferredContainment> symbol) { | ||
69 | return (adapter, partialSymbol) -> new ContainsRefiner(adapter, partialSymbol, symbol); | ||
70 | } | ||
71 | } | ||
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 { | |||
24 | this.contains = adjustContains(contains, mustLinks, forbiddenLinks); | 24 | this.contains = adjustContains(contains, mustLinks, forbiddenLinks); |
25 | this.mustLinks = mustLinks; | 25 | this.mustLinks = mustLinks; |
26 | this.forbiddenLinks = forbiddenLinks; | 26 | this.forbiddenLinks = forbiddenLinks; |
27 | hashCode = Objects.hash(contains, mustLinks, forbiddenLinks); | 27 | hashCode = Objects.hash(this.contains, mustLinks, forbiddenLinks); |
28 | } | 28 | } |
29 | 29 | ||
30 | private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks, | 30 | private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> 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 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.containment; | ||
7 | |||
8 | import tools.refinery.store.query.view.TuplePreservingView; | ||
9 | import tools.refinery.store.representation.Symbol; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | class MustAnyContainmentLinkView extends TuplePreservingView<InferredContainment> { | ||
13 | public MustAnyContainmentLinkView(Symbol<InferredContainment> symbol) { | ||
14 | super(symbol, "contains#mustAnyLink"); | ||
15 | } | ||
16 | |||
17 | @Override | ||
18 | protected boolean doFilter(Tuple key, InferredContainment value) { | ||
19 | return !value.mustLinks().isEmpty(); | ||
20 | } | ||
21 | } | ||