diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-06-01 18:37:20 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-06-01 20:17:47 +0200 |
commit | 07b4048828d9ef8126282c4626dd3f0729213d91 (patch) | |
tree | 4523d01e7802585ae3a3c7ec622d1b0a1e3dfa91 /subprojects/store-reasoning/src/main | |
parent | fix(reasoning): candidate count literal rewriting (diff) | |
download | refinery-07b4048828d9ef8126282c4626dd3f0729213d91.tar.gz refinery-07b4048828d9ef8126282c4626dd3f0729213d91.tar.zst refinery-07b4048828d9ef8126282c4626dd3f0729213d91.zip |
feat: partial references
References marked as partial are not concretized during model generation. The
should be managed by the user manually using propagation rules instead.
Diffstat (limited to 'subprojects/store-reasoning/src/main')
9 files changed, 251 insertions, 134 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java index 26449df5..56c9d682 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java | |||
@@ -1,16 +1,18 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.crossreference; | 6 | package tools.refinery.store.reasoning.translator.crossreference; |
7 | 7 | ||
8 | import tools.refinery.logic.dnf.Query; | 8 | import tools.refinery.logic.dnf.Query; |
9 | import tools.refinery.logic.dnf.QueryBuilder; | ||
9 | import tools.refinery.logic.dnf.RelationalQuery; | 10 | import tools.refinery.logic.dnf.RelationalQuery; |
10 | import tools.refinery.logic.literal.Literal; | 11 | import tools.refinery.logic.literal.Literal; |
11 | import tools.refinery.logic.term.NodeVariable; | 12 | import tools.refinery.logic.term.NodeVariable; |
12 | import tools.refinery.logic.term.Variable; | 13 | import tools.refinery.logic.term.Variable; |
13 | import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality; | 14 | import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality; |
15 | import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; | ||
14 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; | 16 | import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; |
15 | import tools.refinery.store.reasoning.representation.PartialRelation; | 17 | import tools.refinery.store.reasoning.representation.PartialRelation; |
16 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | 18 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; |
@@ -21,6 +23,7 @@ import java.util.List; | |||
21 | import static tools.refinery.logic.literal.Literals.check; | 23 | import static tools.refinery.logic.literal.Literals.check; |
22 | import static tools.refinery.logic.term.int_.IntTerms.constant; | 24 | import static tools.refinery.logic.term.int_.IntTerms.constant; |
23 | import static tools.refinery.logic.term.int_.IntTerms.less; | 25 | import static tools.refinery.logic.term.int_.IntTerms.less; |
26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMay; | ||
24 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | 27 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; |
25 | 28 | ||
26 | class CrossReferenceUtils { | 29 | class CrossReferenceUtils { |
@@ -30,6 +33,34 @@ class CrossReferenceUtils { | |||
30 | 33 | ||
31 | public static RelationalQuery createMayHelper(PartialRelation linkType, PartialRelation type, | 34 | public static RelationalQuery createMayHelper(PartialRelation linkType, PartialRelation type, |
32 | Multiplicity multiplicity, boolean inverse) { | 35 | Multiplicity multiplicity, boolean inverse) { |
36 | var preparedBuilder = prepareBuilder(linkType, inverse); | ||
37 | var literals = new ArrayList<Literal>(); | ||
38 | literals.add(may(type.call(preparedBuilder.variable()))); | ||
39 | if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality(var finiteUpperBound)) { | ||
40 | var existingLinks = Variable.of("existingLinks", Integer.class); | ||
41 | literals.add(new CountLowerBoundLiteral(existingLinks, linkType, preparedBuilder.arguments())); | ||
42 | literals.add(check(less(existingLinks, constant(finiteUpperBound)))); | ||
43 | } | ||
44 | return preparedBuilder.builder().clause(literals).build(); | ||
45 | } | ||
46 | |||
47 | public static RelationalQuery createCandidateMayHelper(PartialRelation linkType, PartialRelation type, | ||
48 | Multiplicity multiplicity, boolean inverse) { | ||
49 | var preparedBuilder = prepareBuilder(linkType, inverse); | ||
50 | var literals = new ArrayList<Literal>(); | ||
51 | literals.add(candidateMay(type.call(preparedBuilder.variable()))); | ||
52 | if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality(var finiteUpperBound)) { | ||
53 | var existingLinks = Variable.of("existingLinks", Integer.class); | ||
54 | literals.add(new CountCandidateLowerBoundLiteral(existingLinks, linkType, preparedBuilder.arguments())); | ||
55 | literals.add(check(less(existingLinks, constant(finiteUpperBound)))); | ||
56 | } | ||
57 | return preparedBuilder.builder().clause(literals).build(); | ||
58 | } | ||
59 | |||
60 | private record PreparedBuilder(QueryBuilder builder, NodeVariable variable, List<Variable> arguments) { | ||
61 | } | ||
62 | |||
63 | private static PreparedBuilder prepareBuilder(PartialRelation linkType, boolean inverse) { | ||
33 | String name; | 64 | String name; |
34 | NodeVariable variable; | 65 | NodeVariable variable; |
35 | List<Variable> arguments; | 66 | List<Variable> arguments; |
@@ -44,14 +75,6 @@ class CrossReferenceUtils { | |||
44 | } | 75 | } |
45 | var builder = Query.builder(linkType.name() + "#mayNew" + name); | 76 | var builder = Query.builder(linkType.name() + "#mayNew" + name); |
46 | builder.parameter(variable); | 77 | builder.parameter(variable); |
47 | var literals = new ArrayList<Literal>(); | 78 | return new PreparedBuilder(builder, variable, arguments); |
48 | literals.add(may(type.call(variable))); | ||
49 | if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { | ||
50 | var existingLinks = Variable.of("existingLinks", Integer.class); | ||
51 | literals.add(new CountLowerBoundLiteral(existingLinks, linkType, arguments)); | ||
52 | literals.add(check(less(existingLinks, constant(finiteUpperCardinality.finiteUpperBound())))); | ||
53 | } | ||
54 | builder.clause(literals); | ||
55 | return builder.build(); | ||
56 | } | 79 | } |
57 | } | 80 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java index 982f835f..ef5bcebb 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -11,7 +11,7 @@ import tools.refinery.logic.term.truthvalue.TruthValue; | |||
11 | 11 | ||
12 | public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity, | 12 | public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity, |
13 | PartialRelation targetType, Multiplicity targetMultiplicity, | 13 | PartialRelation targetType, Multiplicity targetMultiplicity, |
14 | TruthValue defaultValue) { | 14 | TruthValue defaultValue, boolean partial) { |
15 | public boolean isConstrained() { | 15 | public boolean isConstrained() { |
16 | return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained(); | 16 | return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained(); |
17 | } | 17 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java index 5bf1f5ab..1985a43f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -18,6 +18,7 @@ import tools.refinery.store.reasoning.literal.Concreteness; | |||
18 | import tools.refinery.store.reasoning.literal.Modality; | 18 | import tools.refinery.store.reasoning.literal.Modality; |
19 | import tools.refinery.store.reasoning.representation.PartialRelation; | 19 | import tools.refinery.store.reasoning.representation.PartialRelation; |
20 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 20 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
21 | import tools.refinery.store.reasoning.translator.RoundingMode; | ||
21 | import tools.refinery.store.reasoning.translator.TranslationException; | 22 | import tools.refinery.store.reasoning.translator.TranslationException; |
22 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; | 23 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; |
23 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | 24 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; |
@@ -42,27 +43,77 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration | |||
42 | 43 | ||
43 | @Override | 44 | @Override |
44 | public void apply(ModelStoreBuilder storeBuilder) { | 45 | public void apply(ModelStoreBuilder storeBuilder) { |
45 | var name = linkType.name(); | ||
46 | var sourceType = info.sourceType(); | 46 | var sourceType = info.sourceType(); |
47 | var targetType = info.targetType(); | 47 | var targetType = info.targetType(); |
48 | var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); | ||
49 | var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); | ||
50 | var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); | ||
51 | |||
52 | var defaultValue = info.defaultValue(); | 48 | var defaultValue = info.defaultValue(); |
53 | if (defaultValue.must()) { | 49 | if (defaultValue.must()) { |
54 | throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s" | 50 | throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s" |
55 | .formatted(defaultValue, linkType)); | 51 | .formatted(defaultValue, linkType)); |
56 | } | 52 | } |
57 | |||
58 | var translator = PartialRelationTranslator.of(linkType); | 53 | var translator = PartialRelationTranslator.of(linkType); |
59 | translator.symbol(symbol); | 54 | translator.symbol(symbol); |
60 | if (defaultValue.may()) { | 55 | if (defaultValue.may()) { |
61 | var forbiddenView = new ForbiddenView(symbol); | 56 | configureWithDefaultUnknown(translator); |
62 | translator.may(Query.of(mayName, (builder, source, target) -> { | 57 | } else { |
58 | configureWithDefaultFalse(storeBuilder); | ||
59 | } | ||
60 | translator.refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)); | ||
61 | translator.initializer(new DirectedCrossReferenceInitializer(linkType, sourceType, targetType, symbol)); | ||
62 | if (info.partial()) { | ||
63 | translator.roundingMode(RoundingMode.NONE); | ||
64 | } else { | ||
65 | translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder | ||
66 | .clause( | ||
67 | may(linkType.call(source, target)), | ||
68 | not(candidateMust(linkType.call(source, target))), | ||
69 | not(MULTI_VIEW.call(source)), | ||
70 | not(MULTI_VIEW.call(target)) | ||
71 | ) | ||
72 | .action( | ||
73 | add(linkType, source, target) | ||
74 | ))); | ||
75 | } | ||
76 | storeBuilder.with(translator); | ||
77 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, | ||
78 | info.sourceMultiplicity())); | ||
79 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true, | ||
80 | info.targetMultiplicity())); | ||
81 | } | ||
82 | |||
83 | private void configureWithDefaultUnknown(PartialRelationTranslator translator) { | ||
84 | var name = linkType.name(); | ||
85 | var sourceType = info.sourceType(); | ||
86 | var targetType = info.targetType(); | ||
87 | var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); | ||
88 | var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); | ||
89 | var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); | ||
90 | var forbiddenView = new ForbiddenView(symbol); | ||
91 | translator.may(Query.of(mayName, (builder, source, target) -> { | ||
92 | builder.clause( | ||
93 | mayNewSource.call(source), | ||
94 | mayNewTarget.call(target), | ||
95 | not(forbiddenView.call(source, target)) | ||
96 | ); | ||
97 | if (info.isConstrained()) { | ||
98 | // Violation of monotonicity: | ||
99 | // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
100 | // corresponding error pattern will already mark the node as invalid. | ||
101 | builder.clause( | ||
102 | must(linkType.call(source, target)), | ||
103 | not(forbiddenView.call(source, target)), | ||
104 | may(sourceType.call(source)), | ||
105 | may(targetType.call(target)) | ||
106 | ); | ||
107 | } | ||
108 | })); | ||
109 | if (info.partial()) { | ||
110 | var candidateMayNewSource = createCandidateMayHelper(sourceType, info.sourceMultiplicity(), false); | ||
111 | var candidateMayNewTarget = createCandidateMayHelper(targetType, info.targetMultiplicity(), true); | ||
112 | var candidateMayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.CANDIDATE); | ||
113 | translator.candidateMay(Query.of(candidateMayName, (builder, source, target) -> { | ||
63 | builder.clause( | 114 | builder.clause( |
64 | mayNewSource.call(source), | 115 | candidateMayNewSource.call(source), |
65 | mayNewTarget.call(target), | 116 | candidateMayNewTarget.call(target), |
66 | not(forbiddenView.call(source, target)) | 117 | not(forbiddenView.call(source, target)) |
67 | ); | 118 | ); |
68 | if (info.isConstrained()) { | 119 | if (info.isConstrained()) { |
@@ -70,63 +121,56 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration | |||
70 | // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the | 121 | // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the |
71 | // corresponding error pattern will already mark the node as invalid. | 122 | // corresponding error pattern will already mark the node as invalid. |
72 | builder.clause( | 123 | builder.clause( |
73 | must(linkType.call(source, target)), | 124 | candidateMust(linkType.call(source, target)), |
74 | not(forbiddenView.call(source, target)), | 125 | not(forbiddenView.call(source, target)), |
75 | may(sourceType.call(source)), | 126 | candidateMay(sourceType.call(source)), |
76 | may(targetType.call(target)) | 127 | candidateMay(targetType.call(target)) |
77 | ); | 128 | ); |
78 | } | 129 | } |
79 | })); | 130 | })); |
80 | } else { | 131 | } |
81 | var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); | 132 | } |
82 | propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { | 133 | |
134 | private RelationalQuery createMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { | ||
135 | return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse); | ||
136 | } | ||
137 | |||
138 | private RelationalQuery createCandidateMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { | ||
139 | return CrossReferenceUtils.createCandidateMayHelper(linkType, type, multiplicity, inverse); | ||
140 | } | ||
141 | |||
142 | private void configureWithDefaultFalse(ModelStoreBuilder storeBuilder) { | ||
143 | var name = linkType.name(); | ||
144 | var sourceType = info.sourceType(); | ||
145 | var targetType = info.targetType(); | ||
146 | var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); | ||
147 | var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); | ||
148 | var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); | ||
149 | propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { | ||
150 | builder.clause( | ||
151 | may(linkType.call(p1, p2)), | ||
152 | not(may(sourceType.call(p1))) | ||
153 | ); | ||
154 | builder.clause( | ||
155 | may(linkType.call(p1, p2)), | ||
156 | not(may(targetType.call(p2))) | ||
157 | ); | ||
158 | if (info.isConstrained()) { | ||
83 | builder.clause( | 159 | builder.clause( |
84 | may(linkType.call(p1, p2)), | 160 | may(linkType.call(p1, p2)), |
85 | not(may(sourceType.call(p1))) | 161 | not(must(linkType.call(p1, p2))), |
162 | not(mayNewSource.call(p1)) | ||
86 | ); | 163 | ); |
87 | builder.clause( | 164 | builder.clause( |
88 | may(linkType.call(p1, p2)), | 165 | may(linkType.call(p1, p2)), |
89 | not(may(targetType.call(p2))) | 166 | not(must(linkType.call(p1, p2))), |
167 | not(mayNewTarget.call(p2)) | ||
90 | ); | 168 | ); |
91 | if (info.isConstrained()) { | 169 | } |
92 | builder.clause( | 170 | builder.action( |
93 | may(linkType.call(p1, p2)), | 171 | merge(linkType, TruthValue.FALSE, p1, p2) |
94 | not(must(linkType.call(p1, p2))), | 172 | ); |
95 | not(mayNewSource.call(p1)) | 173 | })); |
96 | ); | ||
97 | builder.clause( | ||
98 | may(linkType.call(p1, p2)), | ||
99 | not(must(linkType.call(p1, p2))), | ||
100 | not(mayNewTarget.call(p2)) | ||
101 | ); | ||
102 | } | ||
103 | builder.action( | ||
104 | merge(linkType, TruthValue.FALSE, p1, p2) | ||
105 | ); | ||
106 | })); | ||
107 | } | ||
108 | translator.refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)); | ||
109 | translator.initializer(new DirectedCrossReferenceInitializer(linkType, sourceType, targetType, symbol)); | ||
110 | translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder | ||
111 | .clause( | ||
112 | may(linkType.call(source, target)), | ||
113 | not(candidateMust(linkType.call(source, target))), | ||
114 | not(MULTI_VIEW.call(source)), | ||
115 | not(MULTI_VIEW.call(target)) | ||
116 | ) | ||
117 | .action( | ||
118 | add(linkType, source, target) | ||
119 | ))); | ||
120 | storeBuilder.with(translator); | ||
121 | |||
122 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, | ||
123 | info.sourceMultiplicity())); | ||
124 | |||
125 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true, | ||
126 | info.targetMultiplicity())); | ||
127 | } | 174 | } |
128 | 175 | ||
129 | private RelationalQuery createMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { | ||
130 | return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse); | ||
131 | } | ||
132 | } | 176 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java index 560eb04a..78b9cd86 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -9,7 +9,8 @@ import tools.refinery.store.reasoning.representation.PartialRelation; | |||
9 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | 9 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; |
10 | import tools.refinery.logic.term.truthvalue.TruthValue; | 10 | import tools.refinery.logic.term.truthvalue.TruthValue; |
11 | 11 | ||
12 | public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity, TruthValue defaultValue) { | 12 | public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity, TruthValue defaultValue, |
13 | boolean partial) { | ||
13 | public boolean isConstrained() { | 14 | public boolean isConstrained() { |
14 | return multiplicity.isConstrained(); | 15 | return multiplicity.isConstrained(); |
15 | } | 16 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java index 97c0b800..af0ddd2e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java | |||
@@ -1,25 +1,26 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.crossreference; | 6 | package tools.refinery.store.reasoning.translator.crossreference; |
7 | 7 | ||
8 | import tools.refinery.logic.dnf.Query; | ||
9 | import tools.refinery.logic.term.truthvalue.TruthValue; | ||
8 | import tools.refinery.store.dse.propagation.PropagationBuilder; | 10 | import tools.refinery.store.dse.propagation.PropagationBuilder; |
9 | import tools.refinery.store.dse.transition.Rule; | 11 | import tools.refinery.store.dse.transition.Rule; |
10 | import tools.refinery.store.model.ModelStoreBuilder; | 12 | import tools.refinery.store.model.ModelStoreBuilder; |
11 | import tools.refinery.store.model.ModelStoreConfiguration; | 13 | import tools.refinery.store.model.ModelStoreConfiguration; |
12 | import tools.refinery.logic.dnf.Query; | ||
13 | import tools.refinery.store.query.view.ForbiddenView; | 14 | import tools.refinery.store.query.view.ForbiddenView; |
14 | import tools.refinery.store.reasoning.lifting.DnfLifter; | 15 | import tools.refinery.store.reasoning.lifting.DnfLifter; |
15 | import tools.refinery.store.reasoning.literal.Concreteness; | 16 | import tools.refinery.store.reasoning.literal.Concreteness; |
16 | import tools.refinery.store.reasoning.literal.Modality; | 17 | import tools.refinery.store.reasoning.literal.Modality; |
17 | import tools.refinery.store.reasoning.representation.PartialRelation; | 18 | import tools.refinery.store.reasoning.representation.PartialRelation; |
18 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 19 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
20 | import tools.refinery.store.reasoning.translator.RoundingMode; | ||
19 | import tools.refinery.store.reasoning.translator.TranslationException; | 21 | import tools.refinery.store.reasoning.translator.TranslationException; |
20 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; | 22 | import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; |
21 | import tools.refinery.store.representation.Symbol; | 23 | import tools.refinery.store.representation.Symbol; |
22 | import tools.refinery.logic.term.truthvalue.TruthValue; | ||
23 | 24 | ||
24 | import static tools.refinery.logic.literal.Literals.not; | 25 | import static tools.refinery.logic.literal.Literals.not; |
25 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; | 26 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; |
@@ -40,73 +41,106 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati | |||
40 | 41 | ||
41 | @Override | 42 | @Override |
42 | public void apply(ModelStoreBuilder storeBuilder) { | 43 | public void apply(ModelStoreBuilder storeBuilder) { |
43 | var name = linkType.name(); | ||
44 | var type = info.type(); | 44 | var type = info.type(); |
45 | var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); | ||
46 | |||
47 | var defaultValue = info.defaultValue(); | 45 | var defaultValue = info.defaultValue(); |
48 | if (defaultValue.must()) { | 46 | if (defaultValue.must()) { |
49 | throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s" | 47 | throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s" |
50 | .formatted(defaultValue, linkType)); | 48 | .formatted(defaultValue, linkType)); |
51 | } | 49 | } |
52 | |||
53 | var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false); | ||
54 | |||
55 | var translator = PartialRelationTranslator.of(linkType); | 50 | var translator = PartialRelationTranslator.of(linkType); |
56 | translator.symbol(symbol); | 51 | translator.symbol(symbol); |
57 | if (defaultValue.may()) { | 52 | if (defaultValue.may()) { |
58 | var forbiddenView = new ForbiddenView(symbol); | 53 | configureWithDefaultUnknown(translator); |
59 | translator.may(Query.of(mayName, (builder, source, target) -> { | 54 | } else { |
55 | configureWithDefaultFalse(storeBuilder); | ||
56 | } | ||
57 | translator.refiner(UndirectedCrossReferenceRefiner.of(symbol, type)); | ||
58 | translator.initializer(new UndirectedCrossReferenceInitializer(linkType, type, symbol)); | ||
59 | if (info.partial()) { | ||
60 | translator.roundingMode(RoundingMode.NONE); | ||
61 | } else { | ||
62 | translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder | ||
63 | .clause( | ||
64 | may(linkType.call(source, target)), | ||
65 | not(candidateMust(linkType.call(source, target))), | ||
66 | not(MULTI_VIEW.call(source)), | ||
67 | not(MULTI_VIEW.call(target)) | ||
68 | ) | ||
69 | .action( | ||
70 | add(linkType, source, target) | ||
71 | ))); | ||
72 | } | ||
73 | storeBuilder.with(translator); | ||
74 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); | ||
75 | } | ||
76 | |||
77 | private void configureWithDefaultUnknown(PartialRelationTranslator translator) { | ||
78 | var name = linkType.name(); | ||
79 | var type = info.type(); | ||
80 | var multiplicity = info.multiplicity(); | ||
81 | var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); | ||
82 | var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, false); | ||
83 | var forbiddenView = new ForbiddenView(symbol); | ||
84 | translator.may(Query.of(mayName, (builder, source, target) -> { | ||
85 | builder.clause( | ||
86 | mayNewSource.call(source), | ||
87 | mayNewSource.call(target), | ||
88 | not(forbiddenView.call(source, target)) | ||
89 | ); | ||
90 | if (info.isConstrained()) { | ||
91 | // Violation of monotonicity: | ||
92 | // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
93 | // corresponding error pattern will already mark the node as invalid. | ||
94 | builder.clause( | ||
95 | must(linkType.call(source, target)), | ||
96 | not(forbiddenView.call(source, target)), | ||
97 | may(type.call(source)), | ||
98 | may(type.call(target)) | ||
99 | ); | ||
100 | } | ||
101 | })); | ||
102 | if (info.partial()) { | ||
103 | var candidateMayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.CANDIDATE); | ||
104 | var candidateMayNewSource = CrossReferenceUtils.createCandidateMayHelper(linkType, type, multiplicity, | ||
105 | false); | ||
106 | translator.candidateMay(Query.of(candidateMayName, (builder, source, target) -> { | ||
60 | builder.clause( | 107 | builder.clause( |
61 | mayNewSource.call(source), | 108 | candidateMayNewSource.call(source), |
62 | mayNewSource.call(target), | 109 | candidateMayNewSource.call(target), |
63 | not(forbiddenView.call(source, target)) | 110 | not(forbiddenView.call(source, target)) |
64 | ); | 111 | ); |
65 | if (info.isConstrained()) { | 112 | if (info.isConstrained()) { |
66 | // Violation of monotonicity: | ||
67 | // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the | ||
68 | // corresponding error pattern will already mark the node as invalid. | ||
69 | builder.clause( | 113 | builder.clause( |
70 | must(linkType.call(source, target)), | 114 | candidateMust(linkType.call(source, target)), |
71 | not(forbiddenView.call(source, target)), | 115 | not(forbiddenView.call(source, target)), |
72 | may(type.call(source)), | 116 | candidateMay(type.call(source)), |
73 | may(type.call(target)) | 117 | candidateMay(type.call(target)) |
74 | ); | 118 | ); |
75 | } | 119 | } |
76 | })); | 120 | })); |
77 | } else { | 121 | } |
78 | var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); | 122 | } |
79 | propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { | 123 | |
124 | private void configureWithDefaultFalse(ModelStoreBuilder storeBuilder) { | ||
125 | var name = linkType.name(); | ||
126 | var type = info.type(); | ||
127 | var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false); | ||
128 | var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); | ||
129 | propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { | ||
130 | builder.clause( | ||
131 | may(linkType.call(p1, p2)), | ||
132 | not(may(type.call(p1))) | ||
133 | ); | ||
134 | if (info.isConstrained()) { | ||
80 | builder.clause( | 135 | builder.clause( |
81 | may(linkType.call(p1, p2)), | 136 | may(linkType.call(p1, p2)), |
82 | not(may(type.call(p1))) | 137 | not(must(linkType.call(p1, p2))), |
83 | ); | 138 | not(mayNewSource.call(p1)) |
84 | if (info.isConstrained()) { | ||
85 | builder.clause( | ||
86 | may(linkType.call(p1, p2)), | ||
87 | not(must(linkType.call(p1, p2))), | ||
88 | not(mayNewSource.call(p1)) | ||
89 | ); | ||
90 | } | ||
91 | builder.action( | ||
92 | merge(linkType, TruthValue.FALSE, p1, p2) | ||
93 | ); | 139 | ); |
94 | })); | 140 | } |
95 | } | 141 | builder.action( |
96 | translator.refiner(UndirectedCrossReferenceRefiner.of(symbol, type)); | 142 | merge(linkType, TruthValue.FALSE, p1, p2) |
97 | translator.initializer(new UndirectedCrossReferenceInitializer(linkType, type, symbol)); | 143 | ); |
98 | translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder | 144 | })); |
99 | .clause( | ||
100 | may(linkType.call(source, target)), | ||
101 | not(candidateMust(linkType.call(source, target))), | ||
102 | not(MULTI_VIEW.call(source)), | ||
103 | not(MULTI_VIEW.call(target)) | ||
104 | ) | ||
105 | .action( | ||
106 | add(linkType, source, target) | ||
107 | ))); | ||
108 | storeBuilder.with(translator); | ||
109 | |||
110 | storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); | ||
111 | } | 145 | } |
112 | } | 146 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java index d1979b8c..94bf1c5d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -143,7 +143,7 @@ public class MetamodelBuilder { | |||
143 | targetType, linkType, sourceType)); | 143 | targetType, linkType, sourceType)); |
144 | } | 144 | } |
145 | undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType, | 145 | undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType, |
146 | info.multiplicity(), defaultValue)); | 146 | info.multiplicity(), defaultValue, info.partial())); |
147 | return; | 147 | return; |
148 | } | 148 | } |
149 | oppositeReferences.put(opposite, linkType); | 149 | oppositeReferences.put(opposite, linkType); |
@@ -153,7 +153,7 @@ public class MetamodelBuilder { | |||
153 | return; | 153 | return; |
154 | } | 154 | } |
155 | directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(), | 155 | directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(), |
156 | targetType, targetMultiplicity, defaultValue)); | 156 | targetType, targetMultiplicity, defaultValue, info.partial())); |
157 | } | 157 | } |
158 | 158 | ||
159 | private void processContainmentInfo(PartialRelation linkType, ReferenceInfo info, | 159 | private void processContainmentInfo(PartialRelation linkType, ReferenceInfo info, |
@@ -197,5 +197,9 @@ public class MetamodelBuilder { | |||
197 | throw new TranslationException(opposite, "Opposite %s of containment %s cannot be containment" | 197 | throw new TranslationException(opposite, "Opposite %s of containment %s cannot be containment" |
198 | .formatted(opposite, linkType)); | 198 | .formatted(opposite, linkType)); |
199 | } | 199 | } |
200 | if (info.partial() != oppositeInfo.partial()) { | ||
201 | throw new TranslationException(opposite, "Either both %s and %s have to be partial or neither of them" | ||
202 | .formatted(opposite, linkType)); | ||
203 | } | ||
200 | } | 204 | } |
201 | } | 205 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java index 47a2e95f..94050dc0 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java | |||
@@ -10,7 +10,14 @@ import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | |||
10 | import tools.refinery.logic.term.truthvalue.TruthValue; | 10 | import tools.refinery.logic.term.truthvalue.TruthValue; |
11 | 11 | ||
12 | public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity, | 12 | public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity, |
13 | PartialRelation targetType, PartialRelation opposite, TruthValue defaultValue) { | 13 | PartialRelation targetType, PartialRelation opposite, TruthValue defaultValue, |
14 | boolean partial) { | ||
15 | public ReferenceInfo { | ||
16 | if (containment && partial) { | ||
17 | throw new IllegalArgumentException("Containment references cannot be partial"); | ||
18 | } | ||
19 | } | ||
20 | |||
14 | public static ReferenceInfoBuilder builder() { | 21 | public static ReferenceInfoBuilder builder() { |
15 | return new ReferenceInfoBuilder(); | 22 | return new ReferenceInfoBuilder(); |
16 | } | 23 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java index 39240d6b..90fb22b5 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java | |||
@@ -21,6 +21,7 @@ public final class ReferenceInfoBuilder { | |||
21 | private PartialRelation targetType; | 21 | private PartialRelation targetType; |
22 | private PartialRelation opposite; | 22 | private PartialRelation opposite; |
23 | private TruthValue defaultValue = TruthValue.UNKNOWN; | 23 | private TruthValue defaultValue = TruthValue.UNKNOWN; |
24 | private boolean partial; | ||
24 | 25 | ||
25 | ReferenceInfoBuilder() { | 26 | ReferenceInfoBuilder() { |
26 | } | 27 | } |
@@ -72,6 +73,11 @@ public final class ReferenceInfoBuilder { | |||
72 | return this; | 73 | return this; |
73 | } | 74 | } |
74 | 75 | ||
76 | public ReferenceInfoBuilder partial(boolean partial) { | ||
77 | this.partial = partial; | ||
78 | return this; | ||
79 | } | ||
80 | |||
75 | public ReferenceInfo build() { | 81 | public ReferenceInfo build() { |
76 | if (sourceType == null) { | 82 | if (sourceType == null) { |
77 | throw new IllegalStateException("Source type is required"); | 83 | throw new IllegalStateException("Source type is required"); |
@@ -79,6 +85,6 @@ public final class ReferenceInfoBuilder { | |||
79 | if (targetType == null) { | 85 | if (targetType == null) { |
80 | throw new IllegalStateException("Target type is required"); | 86 | throw new IllegalStateException("Target type is required"); |
81 | } | 87 | } |
82 | return new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite, defaultValue); | 88 | return new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite, defaultValue, partial); |
83 | } | 89 | } |
84 | } | 90 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java index 0ca6eac2..e2eff921 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 20232-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -52,12 +52,11 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati | |||
52 | 52 | ||
53 | @Override | 53 | @Override |
54 | public void apply(ModelStoreBuilder storeBuilder) { | 54 | public void apply(ModelStoreBuilder storeBuilder) { |
55 | if (!(multiplicity instanceof ConstrainedMultiplicity constrainedMultiplicity)) { | 55 | if (!(multiplicity instanceof ConstrainedMultiplicity(var cardinalityInterval, var errorSymbol))) { |
56 | return; | 56 | return; |
57 | } | 57 | } |
58 | 58 | ||
59 | var name = constrainedMultiplicity.errorSymbol().name(); | 59 | var name = errorSymbol.name(); |
60 | var cardinalityInterval = constrainedMultiplicity.multiplicity(); | ||
61 | var node = Variable.of("node"); | 60 | var node = Variable.of("node"); |
62 | var other = Variable.of("other"); | 61 | var other = Variable.of("other"); |
63 | List<Variable> arguments = inverse ? List.of(other, node) : List.of(node, other); | 62 | List<Variable> arguments = inverse ? List.of(other, node) : List.of(node, other); |
@@ -98,8 +97,7 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati | |||
98 | )); | 97 | )); |
99 | } | 98 | } |
100 | 99 | ||
101 | if (cardinalityInterval.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { | 100 | if (cardinalityInterval.upperBound() instanceof FiniteUpperCardinality(int upperBound)) { |
102 | int upperBound = finiteUpperCardinality.finiteUpperBound(); | ||
103 | mustBuilder.clause(Integer.class, existingContents -> List.of( | 101 | mustBuilder.clause(Integer.class, existingContents -> List.of( |
104 | must(nodeType.call(node)), | 102 | must(nodeType.call(node)), |
105 | new CountLowerBoundLiteral(existingContents, linkType, arguments), | 103 | new CountLowerBoundLiteral(existingContents, linkType, arguments), |
@@ -128,7 +126,7 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati | |||
128 | output.assign(missingBuilder.build().aggregate(INT_SUM, Variable.of())) | 126 | output.assign(missingBuilder.build().aggregate(INT_SUM, Variable.of())) |
129 | )); | 127 | )); |
130 | 128 | ||
131 | storeBuilder.with(PartialRelationTranslator.of(constrainedMultiplicity.errorSymbol()) | 129 | storeBuilder.with(PartialRelationTranslator.of(errorSymbol) |
132 | .mayNever() | 130 | .mayNever() |
133 | .must(mustBuilder.build()) | 131 | .must(mustBuilder.build()) |
134 | .candidateMay(candidateMayBuilder.build()) | 132 | .candidateMay(candidateMayBuilder.build()) |