aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
diff options
context:
space:
mode:
Diffstat (limited to 'subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java')
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java255
1 files changed, 255 insertions, 0 deletions
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
new file mode 100644
index 00000000..61037be3
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
@@ -0,0 +1,255 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.store.reasoning.translator.containment;
7
8import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder;
9import tools.refinery.store.dse.transition.Rule;
10import tools.refinery.store.model.ModelStoreBuilder;
11import tools.refinery.store.model.ModelStoreConfiguration;
12import tools.refinery.store.query.dnf.Query;
13import tools.refinery.store.query.dnf.RelationalQuery;
14import tools.refinery.store.query.literal.Connectivity;
15import tools.refinery.store.query.literal.Literal;
16import tools.refinery.store.query.literal.RepresentativeElectionLiteral;
17import tools.refinery.store.query.term.Variable;
18import tools.refinery.store.query.view.AnySymbolView;
19import tools.refinery.store.reasoning.lifting.DnfLifter;
20import tools.refinery.store.reasoning.literal.Concreteness;
21import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral;
22import tools.refinery.store.reasoning.literal.Modality;
23import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
24import tools.refinery.store.reasoning.representation.PartialRelation;
25import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
26import tools.refinery.store.reasoning.translator.RoundingMode;
27import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
28import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
29import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
30import tools.refinery.store.representation.Symbol;
31import tools.refinery.store.representation.cardinality.CardinalityIntervals;
32import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
33
34import java.util.ArrayList;
35import java.util.List;
36import java.util.Map;
37
38import static tools.refinery.store.query.literal.Literals.check;
39import static tools.refinery.store.query.literal.Literals.not;
40import static tools.refinery.store.query.term.int_.IntTerms.constant;
41import static tools.refinery.store.query.term.int_.IntTerms.less;
42import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL;
43import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
44import static tools.refinery.store.reasoning.actions.PartialActionLiterals.focus;
45import static tools.refinery.store.reasoning.literal.PartialLiterals.*;
46
47public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
48 public static final PartialRelation CONTAINED_SYMBOL = new PartialRelation("contained", 1);
49 public static final PartialRelation INVALID_CONTAINER = new PartialRelation("invalidContainer",
50 1);
51 public static final PartialRelation CONTAINS_SYMBOL = new PartialRelation("contains", 2);
52
53 private final Symbol<InferredContainment> containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class,
54 InferredContainment.UNKNOWN);
55 private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage);
56 private final RelationalQuery containsMayNewTargetHelper;
57 private final RelationalQuery containsMayExistingHelper;
58 private final RelationalQuery weakComponents;
59 private final RelationalQuery strongComponents;
60 private final Map<PartialRelation, ContainmentInfo> containmentInfoMap;
61
62 public ContainmentHierarchyTranslator(Map<PartialRelation, ContainmentInfo> containmentInfoMap) {
63 this.containmentInfoMap = containmentInfoMap;
64
65 var name = CONTAINS_SYMBOL.name();
66
67 containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder
68 .clause(Integer.class, existingContainers -> List.of(
69 may(CONTAINED_SYMBOL.call(child)),
70 new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, List.of(Variable.of(), child)),
71 check(less(existingContainers, constant(1)))
72 )));
73
74 containsMayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder
75 .clause(Integer.class, existingContainers -> List.of(
76 must(CONTAINS_SYMBOL.call(parent, child)),
77 not(forbiddenContainsView.call(parent, child))
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
83 var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause(
84 must(CONTAINS_SYMBOL.call(parent, child)),
85 must(EXISTS_SYMBOL.call(parent)),
86 must(EXISTS_SYMBOL.call(child))
87 ));
88
89 weakComponents = Query.of(name + "#weakComponents", (builder, node, representative) -> builder.clause(
90 new RepresentativeElectionLiteral(Connectivity.WEAK, mustExistBothContains.getDnf(), node,
91 representative)
92 ));
93
94 strongComponents = Query.of(name + "#strongComponents", (builder, node, representative) -> builder.clause(
95 new RepresentativeElectionLiteral(Connectivity.STRONG, mustExistBothContains.getDnf(), node,
96 representative)
97 ));
98 }
99
100 @Override
101 public void apply(ModelStoreBuilder storeBuilder) {
102 storeBuilder.symbol(containsStorage);
103 translateContains(storeBuilder);
104 translateInvalidContainer(storeBuilder);
105 for (var entry : containmentInfoMap.entrySet()) {
106 var linkType = entry.getKey();
107 var info = entry.getValue();
108 translateContainmentLinkType(storeBuilder, linkType, info);
109 translateInvalidMultiplicity(storeBuilder, linkType, info);
110 }
111 translateFocusNotContained(storeBuilder);
112 }
113
114 private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType,
115 ContainmentInfo info) {
116 var name = linkType.name();
117 var sourceType = info.sourceType();
118 var targetType = info.targetType();
119 var upperCardinality = info.multiplicity().multiplicity().upperBound();
120
121 var mayNewSourceHelper = Query.of(name + "#mayNewSourceHelper", (builder, parent) -> {
122 var literals = new ArrayList<Literal>();
123 literals.add(may(sourceType.call(parent)));
124 if (upperCardinality instanceof FiniteUpperCardinality finiteUpperCardinality) {
125 var existingCount = Variable.of("existingCount", Integer.class);
126 literals.add(new CountLowerBoundLiteral(existingCount, linkType, List.of(parent, Variable.of())));
127 literals.add(check(less(existingCount, constant(finiteUpperCardinality.finiteUpperBound()))));
128 }
129 builder.clause(literals);
130 });
131
132 var mayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder.clause(
133 containsMayNewTargetHelper.call(child),
134 may(targetType.call(child))
135 ));
136
137 var forbiddenLinkView = new ForbiddenContainmentLinkView(containsStorage, linkType);
138
139 var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause(
140 mayNewSourceHelper.call(parent),
141 mayNewTargetHelper.call(child),
142 not(must(CONTAINS_SYMBOL.call(parent, child))),
143 not(forbiddenLinkView.call(parent, child))
144 ));
145
146 var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause(
147 must(linkType.call(parent, child)),
148 containsMayExistingHelper.call(parent, child),
149 may(sourceType.call(parent)),
150 may(targetType.call(child)),
151 not(forbiddenLinkView.call(parent, child))
152 // Violation of monotonicity:
153 // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the
154 // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid.
155 ));
156
157 var may = Query.of(name + "#may", (builder, parent, child) -> builder
158 .clause(
159 mayNewHelper.call(parent, child),
160 not(weakComponents.call(parent, Variable.of()))
161 )
162 .clause(representative -> List.of(
163 mayNewHelper.call(parent, child),
164 weakComponents.call(parent, representative),
165 // Violation of para-consistency:
166 // If there is a surely existing node with at least two containers, its (transitive) containers
167 // will end up in the same weakly connected component, and we will spuriously mark the
168 // containment edge between the (transitive) containers as {@code FALSE}. However, such
169 // models can never be finished.
170 //
171 // Violation of monotonicity:
172 // if the a {@code TRUE} value is added to the representation in the previous situation,
173 // we'll check strongly connected components instead of weakly connected ones. Therefore, the
174 // view for the partial symbol will change from {@code FALSE} to {@code TRUE}. This doesn't
175 // affect the overall inconsistency of the partial model (due to the surely existing node
176 // with multiple containers).
177 not(weakComponents.call(child, representative))
178 ))
179 .clause(
180 mayExistingHelper.call(parent, child),
181 not(strongComponents.call(parent, Variable.of()))
182 )
183 .clause(representative -> List.of(
184 mayExistingHelper.call(parent, child),
185 strongComponents.call(parent, representative),
186 not(strongComponents.call(child, representative))
187 )));
188
189 storeBuilder.with(PartialRelationTranslator.of(linkType)
190 .may(may)
191 .must(Query.of(name + "#must", (builder, parent, child) -> builder.clause(
192 new MustContainmentLinkView(containsStorage, linkType).call(parent, child)
193 )))
194 .roundingMode(RoundingMode.PREFER_FALSE)
195 .refiner(ContainmentLinkRefiner.of(linkType, containsStorage, info.sourceType(), info.targetType()))
196 .initializer(new RefinementBasedInitializer<>(linkType))
197 .decision(Rule.of(linkType.name(), (builder, source, target) -> builder
198 .clause(
199 may(linkType.call(source, target)),
200 not(candidateMust(linkType.call(source, target))),
201 not(MultiObjectTranslator.MULTI_VIEW.call(source))
202 )
203 .action(focusedTarget -> List.of(
204 focus(target, focusedTarget),
205 add(linkType, source, focusedTarget)
206 )))));
207 }
208
209 private void translateInvalidMultiplicity(ModelStoreBuilder storeBuilder, PartialRelation linkType,
210 ContainmentInfo info) {
211 storeBuilder.with(new InvalidMultiplicityErrorTranslator(info.sourceType(), linkType, false,
212 info.multiplicity()));
213 }
214
215 private void translateContains(ModelStoreBuilder storeBuilder) {
216 var name = CONTAINS_SYMBOL.name();
217 var mustName = DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL);
218
219 storeBuilder.with(PartialRelationTranslator.of(CONTAINS_SYMBOL)
220 .query(Query.of(name, (builder, parent, child) -> {
221 for (var linkType : containmentInfoMap.keySet()) {
222 builder.clause(linkType.call(parent, child));
223 }
224 }))
225 .must(Query.of(mustName, (builder, parent, child) -> builder.clause(
226 new MustContainsView(containsStorage).call(parent, child)
227 ))));
228 }
229
230 private void translateInvalidContainer(ModelStoreBuilder storeBuilder) {
231 storeBuilder.with(new InvalidMultiplicityErrorTranslator(CONTAINED_SYMBOL, CONTAINS_SYMBOL, true,
232 ConstrainedMultiplicity.of(CardinalityIntervals.ONE, INVALID_CONTAINER)));
233 }
234
235 private void translateFocusNotContained(ModelStoreBuilder storeBuilder) {
236 var dseBuilderOption = storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class);
237 if (dseBuilderOption.isEmpty()) {
238 return;
239 }
240 var dseBuilder = dseBuilderOption.get();
241 dseBuilder.transformation(Rule.of("NOT_CONTAINED", (builder, multi) -> builder
242 .clause(
243 MultiObjectTranslator.MULTI_VIEW.call(multi),
244 not(may(CONTAINED_SYMBOL.call(multi)))
245 )
246 .clause(container -> List.of(
247 MultiObjectTranslator.MULTI_VIEW.call(multi),
248 must(CONTAINS_SYMBOL.call(container, multi)),
249 not(MultiObjectTranslator.MULTI_VIEW.call(container))
250 ))
251 .action(
252 focus(multi, Variable.of())
253 )));
254 }
255}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 19:05:47 +0000