aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kristof@marussy.com>2023-12-06 23:52:07 +0100
committerLibravatar Kristóf Marussy <kristof@marussy.com>2023-12-08 21:48:48 +0100
commitd40ec70132ebb324873cb8c3868eb65309f46f8c (patch)
tree31c9ca6e5454f61868b4123574b723b33ecc704e
parentchore: upgrade to Eclipse 2023-12 (diff)
downloadrefinery-d40ec70132ebb324873cb8c3868eb65309f46f8c.tar.gz
refinery-d40ec70132ebb324873cb8c3868eb65309f46f8c.tar.zst
refinery-d40ec70132ebb324873cb8c3868eb65309f46f8c.zip
feat: state-based store for cross references
Efficiently store cross references even if default ref(*, *): false. Uses propagation rules instead of view queries to reason about type constraints and multiplicity.
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java64
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java4
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java2
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java5
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java4
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java7
-rw-r--r--subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java10
-rw-r--r--subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java15
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java8
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java2
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java4
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInitializer.java52
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java104
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java3
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java84
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java95
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java54
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java6
-rw-r--r--subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java84
-rw-r--r--subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java34
-rw-r--r--subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java30
21 files changed, 512 insertions, 159 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
index ecaa7e0d..38bf5a61 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
@@ -27,9 +27,7 @@ import tools.refinery.store.reasoning.seed.ModelSeed;
27import tools.refinery.store.reasoning.seed.Seed; 27import tools.refinery.store.reasoning.seed.Seed;
28import tools.refinery.store.reasoning.translator.TranslationException; 28import tools.refinery.store.reasoning.translator.TranslationException;
29import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; 29import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
30import tools.refinery.store.reasoning.translator.metamodel.Metamodel; 30import tools.refinery.store.reasoning.translator.metamodel.*;
31import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder;
32import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
33import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; 31import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
34import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; 32import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
35import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; 33import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
@@ -73,6 +71,10 @@ public class ModelInitializer {
73 71
74 private ScopePropagator scopePropagator; 72 private ScopePropagator scopePropagator;
75 73
74 private int nodeCount;
75
76 private ModelSeed.Builder modelSeedBuilder;
77
76 private ModelSeed modelSeed; 78 private ModelSeed modelSeed;
77 79
78 public void readProblem(Problem problem) { 80 public void readProblem(Problem problem) {
@@ -101,13 +103,17 @@ public class ModelInitializer {
101 TruthValue.FALSE)); 103 TruthValue.FALSE));
102 collectNodes(); 104 collectNodes();
103 collectPartialSymbols(); 105 collectPartialSymbols();
106 nodeCount = problemTrace.getNodeTrace().size();
107 modelSeedBuilder = ModelSeed.builder(nodeCount);
108 collectAssertions();
104 collectMetamodel(); 109 collectMetamodel();
105 metamodel = metamodelBuilder.build(); 110 metamodel = metamodelBuilder.build();
106 problemTrace.setMetamodel(metamodel); 111 problemTrace.setMetamodel(metamodel);
107 collectAssertions(); 112 fixClassDeclarationAssertions();
108 int nodeCount = problemTrace.getNodeTrace().size();
109 var modelSeedBuilder = ModelSeed.builder(nodeCount);
110 for (var entry : relationInfoMap.entrySet()) { 113 for (var entry : relationInfoMap.entrySet()) {
114 if (entry.getKey() instanceof ReferenceDeclaration) {
115 continue;
116 }
111 var info = entry.getValue(); 117 var info = entry.getValue();
112 var partialRelation = info.partialRelation(); 118 var partialRelation = info.partialRelation();
113 modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); 119 modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
@@ -296,7 +302,20 @@ public class ModelInitializer {
296 } 302 }
297 var multiplicity = getMultiplicityConstraint(referenceDeclaration); 303 var multiplicity = getMultiplicityConstraint(referenceDeclaration);
298 try { 304 try {
299 metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation); 305 var seed = relationInfoMap.get(referenceDeclaration).toSeed(nodeCount);
306 var defaultValue = seed.majorityValue();
307 if (defaultValue.must()) {
308 defaultValue = TruthValue.FALSE;
309 }
310 modelSeedBuilder.seed(relation, seed);
311 metamodelBuilder.reference(relation, ReferenceInfo.builder()
312 .containment(containment)
313 .source(source)
314 .multiplicity(multiplicity)
315 .target(target)
316 .opposite(oppositeRelation)
317 .defaultValue(defaultValue)
318 .build());
300 } catch (RuntimeException e) { 319 } catch (RuntimeException e) {
301 throw TracedException.addTrace(classDeclaration, e); 320 throw TracedException.addTrace(classDeclaration, e);
302 } 321 }
@@ -355,10 +374,6 @@ public class ModelInitializer {
355 collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN); 374 collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN);
356 var tuple = Tuple.of(newNodeId); 375 var tuple = Tuple.of(newNodeId);
357 mergeValue(classDeclaration, tuple, TruthValue.TRUE); 376 mergeValue(classDeclaration, tuple, TruthValue.TRUE);
358 var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
359 for (var subType : typeInfo.getDirectSubtypes()) {
360 partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
361 }
362 } 377 }
363 378
364 private void collectEnumAssertions(EnumDeclaration enumDeclaration) { 379 private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
@@ -399,6 +414,27 @@ public class ModelInitializer {
399 } 414 }
400 } 415 }
401 416
417 private void fixClassDeclarationAssertions() {
418 for (var statement : problem.getStatements()) {
419 if (statement instanceof ClassDeclaration classDeclaration) {
420 fixClassDeclarationAssertions(classDeclaration);
421 }
422 }
423 }
424
425 private void fixClassDeclarationAssertions(ClassDeclaration classDeclaration) {
426 var newNode = classDeclaration.getNewNode();
427 if (newNode == null) {
428 return;
429 }
430 var newNodeId = getNodeId(newNode);
431 var tuple = Tuple.of(newNodeId);
432 var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
433 for (var subType : typeInfo.getDirectSubtypes()) {
434 partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
435 }
436 }
437
402 private void mergeValue(Relation relation, Tuple key, TruthValue value) { 438 private void mergeValue(Relation relation, Tuple key, TruthValue value) {
403 getRelationInfo(relation).assertions().mergeValue(key, value); 439 getRelationInfo(relation).assertions().mergeValue(key, value);
404 } 440 }
@@ -482,7 +518,7 @@ public class ModelInitializer {
482 defaultValue = TruthValue.FALSE; 518 defaultValue = TruthValue.FALSE;
483 } else { 519 } else {
484 var seed = modelSeed.getSeed(partialRelation); 520 var seed = modelSeed.getSeed(partialRelation);
485 defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN; 521 defaultValue = seed.majorityValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
486 var cursor = seed.getCursor(defaultValue, problemTrace.getNodeTrace().size()); 522 var cursor = seed.getCursor(defaultValue, problemTrace.getNodeTrace().size());
487 // The symbol should be mutable if there is at least one non-default entry in the seed. 523 // The symbol should be mutable if there is at least one non-default entry in the seed.
488 mutable = mutable || cursor.move(); 524 mutable = mutable || cursor.move();
@@ -495,7 +531,7 @@ public class ModelInitializer {
495 var problemParameters = predicateDefinition.getParameters(); 531 var problemParameters = predicateDefinition.getParameters();
496 int arity = problemParameters.size(); 532 int arity = problemParameters.size();
497 var parameters = new NodeVariable[arity]; 533 var parameters = new NodeVariable[arity];
498 var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity); 534 var parameterMap = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(arity);
499 var commonLiterals = new ArrayList<Literal>(); 535 var commonLiterals = new ArrayList<Literal>();
500 for (int i = 0; i < arity; i++) { 536 for (int i = 0; i < arity; i++) {
501 var problemParameter = problemParameters.get(i); 537 var problemParameter = problemParameters.get(i);
@@ -532,7 +568,7 @@ public class ModelInitializer {
532 return existing; 568 return existing;
533 } 569 }
534 int localScopeSize = existing.size() + newVariables.size(); 570 int localScopeSize = existing.size() + newVariables.size();
535 var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize); 571 var localScope = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(localScopeSize);
536 localScope.putAll(existing); 572 localScope.putAll(existing);
537 for (var newVariable : newVariables) { 573 for (var newVariable : newVariables) {
538 localScope.put(newVariable, Variable.of(newVariable.getName())); 574 localScope.put(newVariable, Variable.of(newVariable.getName()));
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
index c732f784..5d25f148 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
@@ -40,8 +40,8 @@ class DecisionTree implements MutableSeed<TruthValue> {
40 } 40 }
41 41
42 @Override 42 @Override
43 public TruthValue reducedValue() { 43 public TruthValue majorityValue() {
44 return root.getOtherwiseReducedValue().getTruthValue(); 44 return root.getMajorityValue().getTruthValueOrElse(TruthValue.FALSE);
45 } 45 }
46 46
47 @Override 47 @Override
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
index ebca2634..31d6fc78 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
@@ -100,6 +100,8 @@ abstract class DecisionTreeNode {
100 100
101 protected abstract LazyIntIterable getChildKeys(); 101 protected abstract LazyIntIterable getChildKeys();
102 102
103 public abstract DecisionTreeValue getMajorityValue();
104
103 protected abstract boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, 105 protected abstract boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex,
104 int[] sortedChildren); 106 int[] sortedChildren);
105 107
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
index 0e2f5d18..2ad216ce 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
@@ -130,6 +130,11 @@ final class IntermediateNode extends DecisionTreeNode {
130 return children.keysView(); 130 return children.keysView();
131 } 131 }
132 132
133 @Override
134 public DecisionTreeValue getMajorityValue() {
135 return otherwise.getMajorityValue();
136 }
137
133 protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) { 138 protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
134 for (int i = startIndex; i < sortedChildren.length; i++) { 139 for (int i = startIndex; i < sortedChildren.length; i++) {
135 var key = sortedChildren[i]; 140 var key = sortedChildren[i];
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
index 7a72c656..f100c5a6 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
@@ -29,14 +29,14 @@ class NullaryMutableSeed implements MutableSeed<TruthValue> {
29 } 29 }
30 30
31 @Override 31 @Override
32 public TruthValue reducedValue() { 32 public TruthValue majorityValue() {
33 return value.getTruthValue(); 33 return value.getTruthValue();
34 } 34 }
35 35
36 @Override 36 @Override
37 public TruthValue get(Tuple key) { 37 public TruthValue get(Tuple key) {
38 validateKey(key); 38 validateKey(key);
39 return reducedValue(); 39 return majorityValue();
40 } 40 }
41 41
42 private static void validateKey(Tuple key) { 42 private static void validateKey(Tuple key) {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
index d3dd757c..dc501479 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
@@ -115,7 +115,7 @@ class TerminalNode extends DecisionTreeNode {
115 115
116 @Override 116 @Override
117 protected DecisionTreeValue getOtherwiseReducedValue() { 117 protected DecisionTreeValue getOtherwiseReducedValue() {
118 return otherwise; 118 return getMajorityValue();
119 } 119 }
120 120
121 @Override 121 @Override
@@ -124,6 +124,11 @@ class TerminalNode extends DecisionTreeNode {
124 } 124 }
125 125
126 @Override 126 @Override
127 public DecisionTreeValue getMajorityValue() {
128 return otherwise;
129 }
130
131 @Override
127 protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) { 132 protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
128 if (startIndex >= sortedChildren.length) { 133 if (startIndex >= sortedChildren.length) {
129 return false; 134 return false;
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
index 2320de2c..61ce850f 100644
--- a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
@@ -276,6 +276,16 @@ class DecisionTreeTests {
276 assertThat(sut.getReducedValue(), is(TruthValue.TRUE)); 276 assertThat(sut.getReducedValue(), is(TruthValue.TRUE));
277 } 277 }
278 278
279 @Test
280 void overwriteWildcardAllTest() {
281 var first = new DecisionTree(2, TruthValue.UNKNOWN);
282 first.mergeValue(Tuple.of(-1, -1), TruthValue.FALSE);
283 var second = new DecisionTree(2, null);
284 second.mergeValue(Tuple.of(1, -1), TruthValue.TRUE);
285 first.overwriteValues(second);
286 assertThat(first.majorityValue(), is(TruthValue.FALSE));
287 }
288
279 private Map<Tuple, TruthValue> iterateAll(DecisionTree sut, TruthValue defaultValue, int nodeCount) { 289 private Map<Tuple, TruthValue> iterateAll(DecisionTree sut, TruthValue defaultValue, int nodeCount) {
280 var cursor = sut.getCursor(defaultValue, nodeCount); 290 var cursor = sut.getCursor(defaultValue, nodeCount);
281 var map = new LinkedHashMap<Tuple, TruthValue>(); 291 var map = new LinkedHashMap<Tuple, TruthValue>();
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 a2c56a6b..5ee97ce1 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
@@ -27,7 +27,6 @@ import tools.refinery.store.reasoning.translator.containment.ContainmentHierarch
27import tools.refinery.store.reasoning.translator.metamodel.Metamodel; 27import tools.refinery.store.reasoning.translator.metamodel.Metamodel;
28import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator; 28import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
29import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; 29import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
30import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
31import tools.refinery.store.representation.TruthValue; 30import tools.refinery.store.representation.TruthValue;
32import tools.refinery.store.representation.cardinality.CardinalityIntervals; 31import tools.refinery.store.representation.cardinality.CardinalityIntervals;
33import tools.refinery.store.statecoding.StateCoderAdapter; 32import tools.refinery.store.statecoding.StateCoderAdapter;
@@ -109,10 +108,16 @@ class PredicateScopeTest {
109 private ModelStore createStore() { 108 private ModelStore createStore() {
110 var metamodel = Metamodel.builder() 109 var metamodel = Metamodel.builder()
111 .type(index) 110 .type(index)
112 .reference(next, index, false, 111 .reference(next, builder -> builder
113 ConstrainedMultiplicity.of(CardinalityIntervals.LONE, nextInvalidMultiplicity), index, prev) 112 .source(index)
114 .reference(prev, index, false, 113 .target(index)
115 ConstrainedMultiplicity.of(CardinalityIntervals.LONE, prevInvalidMultiplicity), index, next) 114 .multiplicity(CardinalityIntervals.LONE, nextInvalidMultiplicity)
115 .opposite(prev))
116 .reference(prev, builder -> builder
117 .source(index)
118 .target(index)
119 .multiplicity(CardinalityIntervals.LONE, prevInvalidMultiplicity)
120 .opposite(next))
116 .build(); 121 .build();
117 return ModelStore.builder() 122 return ModelStore.builder()
118 .with(QueryInterpreterAdapter.builder()) 123 .with(QueryInterpreterAdapter.builder())
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
index 8b1c3bb3..3b78db02 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
@@ -12,19 +12,19 @@ import tools.refinery.store.tuple.Tuple;
12import java.util.Map; 12import java.util.Map;
13import java.util.Objects; 13import java.util.Objects;
14 14
15record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, T> map) implements Seed<T> { 15record MapBasedSeed<T>(int arity, Class<T> valueType, T majorityValue, Map<Tuple, T> map) implements Seed<T> {
16 @Override 16 @Override
17 public T get(Tuple key) { 17 public T get(Tuple key) {
18 var value = map.get(key); 18 var value = map.get(key);
19 return value == null ? reducedValue : value; 19 return value == null ? majorityValue : value;
20 } 20 }
21 21
22 @Override 22 @Override
23 public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) { 23 public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) {
24 if (Objects.equals(defaultValue, reducedValue)) { 24 if (Objects.equals(defaultValue, majorityValue)) {
25 return Cursors.of(map); 25 return Cursors.of(map);
26 } 26 }
27 return new CartesianProductCursor<>(arity, nodeCount, reducedValue, defaultValue, map); 27 return new CartesianProductCursor<>(arity, nodeCount, majorityValue, defaultValue, map);
28 } 28 }
29 29
30 private static class CartesianProductCursor<T> implements Cursor<Tuple, T> { 30 private static class CartesianProductCursor<T> implements Cursor<Tuple, T> {
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
index 732efbcc..d9bad866 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
@@ -19,7 +19,7 @@ public interface Seed<T> {
19 19
20 Class<T> valueType(); 20 Class<T> valueType();
21 21
22 T reducedValue(); 22 T majorityValue();
23 23
24 T get(Tuple key); 24 T get(Tuple key);
25 25
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 d8c6a5ea..7241b032 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
@@ -7,9 +7,11 @@ package tools.refinery.store.reasoning.translator.crossreference;
7 7
8import tools.refinery.store.reasoning.representation.PartialRelation; 8import tools.refinery.store.reasoning.representation.PartialRelation;
9import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; 9import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
10import tools.refinery.store.representation.TruthValue;
10 11
11public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity, 12public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity,
12 PartialRelation targetType, Multiplicity targetMultiplicity) { 13 PartialRelation targetType, Multiplicity targetMultiplicity,
14 TruthValue defaultValue) {
13 public boolean isConstrained() { 15 public boolean isConstrained() {
14 return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained(); 16 return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained();
15 } 17 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInitializer.java
new file mode 100644
index 00000000..9347e91e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInitializer.java
@@ -0,0 +1,52 @@
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.crossreference;
7
8import tools.refinery.store.model.Model;
9import tools.refinery.store.reasoning.ReasoningAdapter;
10import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
11import tools.refinery.store.reasoning.representation.PartialRelation;
12import tools.refinery.store.reasoning.seed.ModelSeed;
13import tools.refinery.store.representation.Symbol;
14import tools.refinery.store.representation.TruthValue;
15import tools.refinery.store.tuple.Tuple;
16
17class DirectedCrossReferenceInitializer implements PartialModelInitializer {
18 private final PartialRelation linkType;
19 private final PartialRelation sourceType;
20 private final PartialRelation targetType;
21 private final Symbol<TruthValue> symbol;
22
23 public DirectedCrossReferenceInitializer(PartialRelation linkType, PartialRelation sourceType,
24 PartialRelation targetType, Symbol<TruthValue> symbol) {
25 this.linkType = linkType;
26 this.sourceType = sourceType;
27 this.targetType = targetType;
28 this.symbol = symbol;
29 }
30
31 @Override
32 public void initialize(Model model, ModelSeed modelSeed) {
33 var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
34 var sourceRefiner = reasoningAdapter.getRefiner(sourceType);
35 var targetRefiner = reasoningAdapter.getRefiner(targetType);
36 var interpretation = model.getInterpretation(symbol);
37 var cursor = modelSeed.getCursor(linkType, symbol.defaultValue());
38 while (cursor.move()) {
39 var key = cursor.getKey();
40 var value = cursor.getValue();
41 interpretation.put(key, value);
42 if (value.must()) {
43 boolean merged = sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) &&
44 targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
45 if (!merged) {
46 throw new IllegalArgumentException("Failed to merge end types of reference %s for key %s"
47 .formatted(linkType, key));
48 }
49 }
50 }
51 }
52}
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 9028337c..fc7477f1 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
@@ -5,6 +5,7 @@
5 */ 5 */
6package tools.refinery.store.reasoning.translator.crossreference; 6package tools.refinery.store.reasoning.translator.crossreference;
7 7
8import tools.refinery.store.dse.propagation.PropagationBuilder;
8import tools.refinery.store.dse.transition.Rule; 9import tools.refinery.store.dse.transition.Rule;
9import tools.refinery.store.model.ModelStoreBuilder; 10import tools.refinery.store.model.ModelStoreBuilder;
10import tools.refinery.store.model.ModelStoreConfiguration; 11import tools.refinery.store.model.ModelStoreConfiguration;
@@ -14,9 +15,9 @@ import tools.refinery.store.query.view.ForbiddenView;
14import tools.refinery.store.reasoning.lifting.DnfLifter; 15import tools.refinery.store.reasoning.lifting.DnfLifter;
15import tools.refinery.store.reasoning.literal.Concreteness; 16import tools.refinery.store.reasoning.literal.Concreteness;
16import tools.refinery.store.reasoning.literal.Modality; 17import tools.refinery.store.reasoning.literal.Modality;
17import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
18import tools.refinery.store.reasoning.representation.PartialRelation; 18import tools.refinery.store.reasoning.representation.PartialRelation;
19import tools.refinery.store.reasoning.translator.PartialRelationTranslator; 19import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
20import tools.refinery.store.reasoning.translator.TranslationException;
20import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; 21import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
21import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; 22import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
22import tools.refinery.store.representation.Symbol; 23import tools.refinery.store.representation.Symbol;
@@ -24,6 +25,7 @@ import tools.refinery.store.representation.TruthValue;
24 25
25import static tools.refinery.store.query.literal.Literals.not; 26import static tools.refinery.store.query.literal.Literals.not;
26import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; 27import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
28import static tools.refinery.store.reasoning.actions.PartialActionLiterals.merge;
27import static tools.refinery.store.reasoning.literal.PartialLiterals.*; 29import static tools.refinery.store.reasoning.literal.PartialLiterals.*;
28import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; 30import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
29 31
@@ -35,7 +37,7 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
35 public DirectedCrossReferenceTranslator(PartialRelation linkType, DirectedCrossReferenceInfo info) { 37 public DirectedCrossReferenceTranslator(PartialRelation linkType, DirectedCrossReferenceInfo info) {
36 this.linkType = linkType; 38 this.linkType = linkType;
37 this.info = info; 39 this.info = info;
38 symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN); 40 symbol = Symbol.of(linkType.name(), 2, TruthValue.class, info.defaultValue());
39 } 41 }
40 42
41 @Override 43 @Override
@@ -45,41 +47,77 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
45 var targetType = info.targetType(); 47 var targetType = info.targetType();
46 var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); 48 var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false);
47 var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); 49 var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true);
48 var forbiddenView = new ForbiddenView(symbol);
49 var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); 50 var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL);
50 51
51 storeBuilder.with(PartialRelationTranslator.of(linkType) 52 var defaultValue = info.defaultValue();
52 .symbol(symbol) 53 if (defaultValue.must()) {
53 .may(Query.of(mayName, (builder, source, target) -> { 54 throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s"
55 .formatted(defaultValue, linkType));
56 }
57
58 var translator = PartialRelationTranslator.of(linkType);
59 translator.symbol(symbol);
60 if (defaultValue.may()) {
61 var forbiddenView = new ForbiddenView(symbol);
62 translator.may(Query.of(mayName, (builder, source, target) -> {
63 builder.clause(
64 mayNewSource.call(source),
65 mayNewTarget.call(target),
66 not(forbiddenView.call(source, target))
67 );
68 if (info.isConstrained()) {
69 // Violation of monotonicity:
70 // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the
71 // corresponding error pattern will already mark the node as invalid.
72 builder.clause(
73 must(linkType.call(source, target)),
74 not(forbiddenView.call(source, target)),
75 may(sourceType.call(source)),
76 may(targetType.call(target))
77 );
78 }
79 }));
80 } else {
81 var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class);
82 propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
83 builder.clause(
84 may(linkType.call(p1, p2)),
85 not(may(sourceType.call(p1)))
86 );
87 builder.clause(
88 may(linkType.call(p1, p2)),
89 not(may(targetType.call(p2)))
90 );
91 if (info.isConstrained()) {
92 builder.clause(
93 may(linkType.call(p1, p2)),
94 not(must(linkType.call(p1, p2))),
95 not(mayNewSource.call(p1))
96 );
54 builder.clause( 97 builder.clause(
55 mayNewSource.call(source), 98 may(linkType.call(p1, p2)),
56 mayNewTarget.call(target), 99 not(must(linkType.call(p1, p2))),
57 not(forbiddenView.call(source, target)) 100 not(mayNewTarget.call(p2))
58 ); 101 );
59 if (info.isConstrained()) { 102 }
60 // Violation of monotonicity: 103 builder.action(
61 // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the 104 merge(linkType, TruthValue.FALSE, p1, p2)
62 // corresponding error pattern will already mark the node as invalid. 105 );
63 builder.clause( 106 }));
64 must(linkType.call(source, target)), 107 }
65 not(forbiddenView.call(source, target)), 108 translator.refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType));
66 may(sourceType.call(source)), 109 translator.initializer(new DirectedCrossReferenceInitializer(linkType, sourceType, targetType, symbol));
67 may(targetType.call(target)) 110 translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder
68 ); 111 .clause(
69 } 112 may(linkType.call(source, target)),
70 })) 113 not(candidateMust(linkType.call(source, target))),
71 .refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)) 114 not(MULTI_VIEW.call(source)),
72 .initializer(new RefinementBasedInitializer<>(linkType)) 115 not(MULTI_VIEW.call(target))
73 .decision(Rule.of(linkType.name(), (builder, source, target) -> builder 116 )
74 .clause( 117 .action(
75 may(linkType.call(source, target)), 118 add(linkType, source, target)
76 not(candidateMust(linkType.call(source, target))), 119 )));
77 not(MULTI_VIEW.call(source)), 120 storeBuilder.with(translator);
78 not(MULTI_VIEW.call(target))
79 )
80 .action(
81 add(linkType, source, target)
82 ))));
83 121
84 storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, 122 storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false,
85 info.sourceMultiplicity())); 123 info.sourceMultiplicity()));
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 fe99bc54..34e9032a 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
@@ -7,8 +7,9 @@ package tools.refinery.store.reasoning.translator.crossreference;
7 7
8import tools.refinery.store.reasoning.representation.PartialRelation; 8import tools.refinery.store.reasoning.representation.PartialRelation;
9import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; 9import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
10import tools.refinery.store.representation.TruthValue;
10 11
11public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity) { 12public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity, TruthValue defaultValue) {
12 public boolean isConstrained() { 13 public boolean isConstrained() {
13 return multiplicity.isConstrained(); 14 return multiplicity.isConstrained();
14 } 15 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java
new file mode 100644
index 00000000..77339aa0
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java
@@ -0,0 +1,84 @@
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.crossreference;
7
8import org.jetbrains.annotations.NotNull;
9import tools.refinery.store.model.Model;
10import tools.refinery.store.reasoning.ReasoningAdapter;
11import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
12import tools.refinery.store.reasoning.representation.PartialRelation;
13import tools.refinery.store.reasoning.seed.ModelSeed;
14import tools.refinery.store.reasoning.translator.TranslationException;
15import tools.refinery.store.representation.Symbol;
16import tools.refinery.store.representation.TruthValue;
17import tools.refinery.store.tuple.Tuple;
18
19import java.util.LinkedHashMap;
20
21class UndirectedCrossReferenceInitializer implements PartialModelInitializer {
22 private final PartialRelation linkType;
23 private final PartialRelation sourceType;
24 private final Symbol<TruthValue> symbol;
25
26 UndirectedCrossReferenceInitializer(PartialRelation linkType, PartialRelation sourceType,
27 Symbol<TruthValue> symbol) {
28 this.linkType = linkType;
29 this.sourceType = sourceType;
30 this.symbol = symbol;
31 }
32
33 @Override
34 public void initialize(Model model, ModelSeed modelSeed) {
35 var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
36 var mergedMap = getMergedMap(modelSeed);
37 var sourceRefiner = reasoningAdapter.getRefiner(sourceType);
38 var interpretation = model.getInterpretation(symbol);
39 for (var entry : mergedMap.entrySet()) {
40 var key = entry.getKey();
41 var value = entry.getValue();
42 interpretation.put(key, value);
43 if (value.must()) {
44 boolean merged = sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) &&
45 sourceRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
46 if (!merged) {
47 throw new IllegalArgumentException("Failed to merge end types of reference %s for key %s"
48 .formatted(linkType, key));
49 }
50 }
51 }
52 }
53
54 @NotNull
55 private LinkedHashMap<Tuple, TruthValue> getMergedMap(ModelSeed modelSeed) {
56 var defaultValue = symbol.defaultValue();
57 var originalMap = new LinkedHashMap<Tuple, TruthValue>();
58 var cursor = modelSeed.getCursor(linkType, defaultValue);
59 while (cursor.move()) {
60 if (originalMap.put(cursor.getKey(), cursor.getValue()) != null) {
61 throw new TranslationException(linkType, "Duplicate value for key " + cursor.getKey());
62 }
63 }
64 var mergedMap = LinkedHashMap.<Tuple, TruthValue>newLinkedHashMap(originalMap.size());
65 for (var entry : originalMap.entrySet()) {
66 var key = entry.getKey();
67 var value = entry.getValue();
68 int first = key.get(0);
69 int second = key.get(1);
70 var oppositeKey = Tuple.of(second, first);
71 var oppositeValue = originalMap.get(oppositeKey);
72 if (oppositeValue != null && second < first) {
73 // Already processed entry.
74 continue;
75 }
76 var mergedValue = value.merge(oppositeValue == null ? defaultValue : oppositeValue);
77 mergedMap.put(key, mergedValue);
78 if (first != second) {
79 mergedMap.put(oppositeKey, mergedValue);
80 }
81 }
82 return mergedMap;
83 }
84}
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 c554e2a4..b76838b3 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
@@ -5,6 +5,7 @@
5 */ 5 */
6package tools.refinery.store.reasoning.translator.crossreference; 6package tools.refinery.store.reasoning.translator.crossreference;
7 7
8import tools.refinery.store.dse.propagation.PropagationBuilder;
8import tools.refinery.store.dse.transition.Rule; 9import tools.refinery.store.dse.transition.Rule;
9import tools.refinery.store.model.ModelStoreBuilder; 10import tools.refinery.store.model.ModelStoreBuilder;
10import tools.refinery.store.model.ModelStoreConfiguration; 11import tools.refinery.store.model.ModelStoreConfiguration;
@@ -13,15 +14,16 @@ import tools.refinery.store.query.view.ForbiddenView;
13import tools.refinery.store.reasoning.lifting.DnfLifter; 14import tools.refinery.store.reasoning.lifting.DnfLifter;
14import tools.refinery.store.reasoning.literal.Concreteness; 15import tools.refinery.store.reasoning.literal.Concreteness;
15import tools.refinery.store.reasoning.literal.Modality; 16import tools.refinery.store.reasoning.literal.Modality;
16import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
17import tools.refinery.store.reasoning.representation.PartialRelation; 17import tools.refinery.store.reasoning.representation.PartialRelation;
18import tools.refinery.store.reasoning.translator.PartialRelationTranslator; 18import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
19import tools.refinery.store.reasoning.translator.TranslationException;
19import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; 20import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
20import tools.refinery.store.representation.Symbol; 21import tools.refinery.store.representation.Symbol;
21import tools.refinery.store.representation.TruthValue; 22import tools.refinery.store.representation.TruthValue;
22 23
23import static tools.refinery.store.query.literal.Literals.not; 24import static tools.refinery.store.query.literal.Literals.not;
24import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; 25import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
26import static tools.refinery.store.reasoning.actions.PartialActionLiterals.merge;
25import static tools.refinery.store.reasoning.literal.PartialLiterals.*; 27import static tools.refinery.store.reasoning.literal.PartialLiterals.*;
26import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; 28import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
27 29
@@ -33,50 +35,77 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati
33 public UndirectedCrossReferenceTranslator(PartialRelation linkType, UndirectedCrossReferenceInfo info) { 35 public UndirectedCrossReferenceTranslator(PartialRelation linkType, UndirectedCrossReferenceInfo info) {
34 this.linkType = linkType; 36 this.linkType = linkType;
35 this.info = info; 37 this.info = info;
36 symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN); 38 symbol = Symbol.of(linkType.name(), 2, TruthValue.class, info.defaultValue());
37 } 39 }
38 40
39 @Override 41 @Override
40 public void apply(ModelStoreBuilder storeBuilder) { 42 public void apply(ModelStoreBuilder storeBuilder) {
41 var name = linkType.name(); 43 var name = linkType.name();
42 var type = info.type(); 44 var type = info.type();
43 var forbiddenView = new ForbiddenView(symbol);
44 var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); 45 var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL);
45 46
47 var defaultValue = info.defaultValue();
48 if (defaultValue.must()) {
49 throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s"
50 .formatted(defaultValue, linkType));
51 }
52
46 var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false); 53 var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false);
47 54
48 storeBuilder.with(PartialRelationTranslator.of(linkType) 55 var translator = PartialRelationTranslator.of(linkType);
49 .symbol(symbol) 56 translator.symbol(symbol);
50 .may(Query.of(mayName, (builder, source, target) -> { 57 if (defaultValue.may()) {
58 var forbiddenView = new ForbiddenView(symbol);
59 translator.may(Query.of(mayName, (builder, source, target) -> {
60 builder.clause(
61 mayNewSource.call(source),
62 mayNewSource.call(target),
63 not(forbiddenView.call(source, target))
64 );
65 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(
70 must(linkType.call(source, target)),
71 not(forbiddenView.call(source, target)),
72 may(type.call(source)),
73 may(type.call(target))
74 );
75 }
76 }));
77 } else {
78 var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class);
79 propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
80 builder.clause(
81 may(linkType.call(p1, p2)),
82 not(may(type.call(p1)))
83 );
84 if (info.isConstrained()) {
51 builder.clause( 85 builder.clause(
52 mayNewSource.call(source), 86 may(linkType.call(p1, p2)),
53 mayNewSource.call(target), 87 not(must(linkType.call(p1, p2))),
54 not(forbiddenView.call(source, target)) 88 not(mayNewSource.call(p1))
55 ); 89 );
56 if (info.isConstrained()) { 90 }
57 // Violation of monotonicity: 91 builder.action(
58 // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the 92 merge(linkType, TruthValue.FALSE, p1, p2)
59 // corresponding error pattern will already mark the node as invalid. 93 );
60 builder.clause( 94 }));
61 must(linkType.call(source, target)), 95 }
62 not(forbiddenView.call(source, target)), 96 translator.refiner(UndirectedCrossReferenceRefiner.of(symbol, type));
63 may(type.call(source)), 97 translator.initializer(new UndirectedCrossReferenceInitializer(linkType, type, symbol));
64 may(type.call(target)) 98 translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder
65 ); 99 .clause(
66 } 100 may(linkType.call(source, target)),
67 })) 101 not(candidateMust(linkType.call(source, target))),
68 .refiner(UndirectedCrossReferenceRefiner.of(symbol, type)) 102 not(MULTI_VIEW.call(source)),
69 .initializer(new RefinementBasedInitializer<>(linkType)) 103 not(MULTI_VIEW.call(target))
70 .decision(Rule.of(linkType.name(), (builder, source, target) -> builder 104 )
71 .clause( 105 .action(
72 may(linkType.call(source, target)), 106 add(linkType, source, target)
73 not(candidateMust(linkType.call(source, target))), 107 )));
74 not(MULTI_VIEW.call(source)), 108 storeBuilder.with(translator);
75 not(MULTI_VIEW.call(target))
76 )
77 .action(
78 add(linkType, source, target)
79 ))));
80 109
81 storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); 110 storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity()));
82 } 111 }
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 74022fc6..a5047768 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
@@ -16,6 +16,7 @@ import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMulti
16import tools.refinery.store.reasoning.translator.typehierarchy.TypeInfo; 16import tools.refinery.store.reasoning.translator.typehierarchy.TypeInfo;
17 17
18import java.util.*; 18import java.util.*;
19import java.util.function.Consumer;
19 20
20public class MetamodelBuilder { 21public class MetamodelBuilder {
21 private final ContainedTypeHierarchyBuilder typeHierarchyBuilder = new ContainedTypeHierarchyBuilder(); 22 private final ContainedTypeHierarchyBuilder typeHierarchyBuilder = new ContainedTypeHierarchyBuilder();
@@ -68,6 +69,12 @@ public class MetamodelBuilder {
68 return this; 69 return this;
69 } 70 }
70 71
72 public MetamodelBuilder reference(PartialRelation linkType, Consumer<ReferenceInfoBuilder> callback) {
73 var builder = ReferenceInfo.builder();
74 callback.accept(builder);
75 return reference(linkType, builder.build());
76 }
77
71 public MetamodelBuilder reference(PartialRelation linkType, ReferenceInfo info) { 78 public MetamodelBuilder reference(PartialRelation linkType, ReferenceInfo info) {
72 if (linkType.arity() != 2) { 79 if (linkType.arity() != 2) {
73 throw new TranslationException(linkType, 80 throw new TranslationException(linkType,
@@ -81,47 +88,6 @@ public class MetamodelBuilder {
81 return this; 88 return this;
82 } 89 }
83 90
84 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
85 Multiplicity multiplicity, PartialRelation targetType,
86 PartialRelation opposite) {
87 return reference(linkType, new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite));
88 }
89
90 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity,
91 PartialRelation targetType, PartialRelation opposite) {
92 return reference(linkType, sourceType, false, multiplicity, targetType, opposite);
93 }
94
95 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType,
96 boolean containment, PartialRelation targetType, PartialRelation opposite) {
97 return reference(linkType, sourceType, containment, UnconstrainedMultiplicity.INSTANCE, targetType, opposite);
98 }
99
100 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, PartialRelation targetType,
101 PartialRelation opposite) {
102 return reference(linkType, sourceType, UnconstrainedMultiplicity.INSTANCE, targetType, opposite);
103 }
104
105 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
106 Multiplicity multiplicity, PartialRelation targetType) {
107 return reference(linkType, sourceType, containment, multiplicity, targetType, null);
108 }
109
110 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity,
111 PartialRelation targetType) {
112 return reference(linkType, sourceType, multiplicity, targetType, null);
113 }
114
115 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
116 PartialRelation targetType) {
117 return reference(linkType, sourceType, containment, targetType, null);
118 }
119
120 public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType,
121 PartialRelation targetType) {
122 return reference(linkType, sourceType, targetType, null);
123 }
124
125 public MetamodelBuilder references(Collection<Map.Entry<PartialRelation, ReferenceInfo>> entries) { 91 public MetamodelBuilder references(Collection<Map.Entry<PartialRelation, ReferenceInfo>> entries) {
126 for (var entry : entries) { 92 for (var entry : entries) {
127 reference(entry.getKey(), entry.getValue()); 93 reference(entry.getKey(), entry.getValue());
@@ -160,10 +126,12 @@ public class MetamodelBuilder {
160 var targetType = info.targetType(); 126 var targetType = info.targetType();
161 var opposite = info.opposite(); 127 var opposite = info.opposite();
162 Multiplicity targetMultiplicity = UnconstrainedMultiplicity.INSTANCE; 128 Multiplicity targetMultiplicity = UnconstrainedMultiplicity.INSTANCE;
129 var defaultValue = info.defaultValue();
163 if (opposite != null) { 130 if (opposite != null) {
164 var oppositeInfo = referenceInfoMap.get(opposite); 131 var oppositeInfo = referenceInfoMap.get(opposite);
165 validateOpposite(linkType, info, opposite, oppositeInfo); 132 validateOpposite(linkType, info, opposite, oppositeInfo);
166 targetMultiplicity = oppositeInfo.multiplicity(); 133 targetMultiplicity = oppositeInfo.multiplicity();
134 defaultValue = defaultValue.merge(oppositeInfo.defaultValue());
167 if (oppositeInfo.containment()) { 135 if (oppositeInfo.containment()) {
168 // Skip processing this reference and process it once we encounter its containment opposite. 136 // Skip processing this reference and process it once we encounter its containment opposite.
169 return; 137 return;
@@ -175,7 +143,7 @@ public class MetamodelBuilder {
175 targetType, linkType, sourceType)); 143 targetType, linkType, sourceType));
176 } 144 }
177 undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType, 145 undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType,
178 info.multiplicity())); 146 info.multiplicity(), defaultValue));
179 return; 147 return;
180 } 148 }
181 oppositeReferences.put(opposite, linkType); 149 oppositeReferences.put(opposite, linkType);
@@ -185,7 +153,7 @@ public class MetamodelBuilder {
185 return; 153 return;
186 } 154 }
187 directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(), 155 directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(),
188 targetType, targetMultiplicity)); 156 targetType, targetMultiplicity, defaultValue));
189 } 157 }
190 158
191 private void processContainmentInfo(PartialRelation linkType, ReferenceInfo info, 159 private void processContainmentInfo(PartialRelation linkType, ReferenceInfo info,
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 9a6b4012..9d7fc9c3 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
@@ -7,7 +7,11 @@ package tools.refinery.store.reasoning.translator.metamodel;
7 7
8import tools.refinery.store.reasoning.representation.PartialRelation; 8import tools.refinery.store.reasoning.representation.PartialRelation;
9import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; 9import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
10import tools.refinery.store.representation.TruthValue;
10 11
11public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity, 12public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity,
12 PartialRelation targetType, PartialRelation opposite) { 13 PartialRelation targetType, PartialRelation opposite, TruthValue defaultValue) {
14 public static ReferenceInfoBuilder builder() {
15 return new ReferenceInfoBuilder();
16 }
13} 17}
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
new file mode 100644
index 00000000..43d01503
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java
@@ -0,0 +1,84 @@
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.metamodel;
7
8import org.jetbrains.annotations.NotNull;
9import org.jetbrains.annotations.Nullable;
10import tools.refinery.store.reasoning.representation.PartialRelation;
11import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
12import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
13import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity;
14import tools.refinery.store.representation.TruthValue;
15import tools.refinery.store.representation.cardinality.CardinalityInterval;
16
17public final class ReferenceInfoBuilder {
18 private boolean containment;
19 private PartialRelation sourceType;
20 private Multiplicity multiplicity = UnconstrainedMultiplicity.INSTANCE;
21 private PartialRelation targetType;
22 private PartialRelation opposite;
23 private TruthValue defaultValue = TruthValue.UNKNOWN;
24
25 ReferenceInfoBuilder() {
26 }
27
28 public ReferenceInfoBuilder source(@NotNull PartialRelation sourceType) {
29 if (sourceType.arity() != 1) {
30 throw new IllegalArgumentException("Source type %s must be of arity 1".formatted(sourceType));
31 }
32 this.sourceType = sourceType;
33 return this;
34 }
35
36 public ReferenceInfoBuilder target(@NotNull PartialRelation targetType) {
37 if (targetType.arity() != 1) {
38 throw new IllegalArgumentException("Target type %s must be of arity 1".formatted(targetType));
39 }
40 this.targetType = targetType;
41 return this;
42 }
43
44 public ReferenceInfoBuilder containment(boolean containment) {
45 this.containment = containment;
46 return this;
47 }
48
49 public ReferenceInfoBuilder multiplicity(@NotNull Multiplicity multiplicity) {
50 this.multiplicity = multiplicity;
51 return this;
52 }
53
54 public ReferenceInfoBuilder multiplicity(@NotNull CardinalityInterval multiplicityInterval,
55 @NotNull PartialRelation errorSymbol) {
56 return multiplicity(ConstrainedMultiplicity.of(multiplicityInterval, errorSymbol));
57 }
58
59 public ReferenceInfoBuilder opposite(@Nullable PartialRelation opposite) {
60 if (opposite != null && opposite.arity() != 2) {
61 throw new IllegalArgumentException("Opposite %s must be of arity 2".formatted(targetType));
62 }
63 this.opposite = opposite;
64 return this;
65 }
66
67 public ReferenceInfoBuilder defaultValue(@NotNull TruthValue defaultValue) {
68 if (defaultValue.must()) {
69 throw new IllegalArgumentException("Unsupported default value");
70 }
71 this.defaultValue = defaultValue;
72 return this;
73 }
74
75 public ReferenceInfo build() {
76 if (sourceType == null) {
77 throw new IllegalStateException("Source type is required");
78 }
79 if (targetType == null) {
80 throw new IllegalStateException("Target type is required");
81 }
82 return new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite, defaultValue);
83 }
84}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java
index 0f1a1006..ba6ba6da 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java
@@ -8,7 +8,6 @@ package tools.refinery.store.reasoning.translator.metamodel;
8import org.junit.jupiter.api.Test; 8import org.junit.jupiter.api.Test;
9import tools.refinery.store.reasoning.representation.PartialRelation; 9import tools.refinery.store.reasoning.representation.PartialRelation;
10import tools.refinery.store.reasoning.translator.TranslationException; 10import tools.refinery.store.reasoning.translator.TranslationException;
11import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
12import tools.refinery.store.representation.cardinality.CardinalityIntervals; 11import tools.refinery.store.representation.cardinality.CardinalityIntervals;
13 12
14import static org.junit.jupiter.api.Assertions.assertThrows; 13import static org.junit.jupiter.api.Assertions.assertThrows;
@@ -24,8 +23,13 @@ class MetamodelBuilderTest {
24 var builder = Metamodel.builder() 23 var builder = Metamodel.builder()
25 .type(university) 24 .type(university)
26 .type(course) 25 .type(course)
27 .reference(courses, university, course, location) 26 .reference(courses, referenceBuilder -> referenceBuilder
28 .reference(location, course, university); 27 .source(university)
28 .target(course)
29 .opposite(location))
30 .reference(location, referenceBuilder -> referenceBuilder
31 .source(course)
32 .target(university));
29 33
30 assertThrows(TranslationException.class, builder::build); 34 assertThrows(TranslationException.class, builder::build);
31 } 35 }
@@ -35,8 +39,14 @@ class MetamodelBuilderTest {
35 var builder = Metamodel.builder() 39 var builder = Metamodel.builder()
36 .type(university) 40 .type(university)
37 .type(course) 41 .type(course)
38 .reference(courses, university, course, location) 42 .reference(courses, referenceBuilder -> referenceBuilder
39 .reference(location, course, course, courses); 43 .source(university)
44 .target(course)
45 .opposite(location))
46 .reference(location, referenceBuilder -> referenceBuilder
47 .source(course)
48 .target(course)
49 .opposite(courses));
40 50
41 assertThrows(TranslationException.class, builder::build); 51 assertThrows(TranslationException.class, builder::build);
42 } 52 }
@@ -48,10 +58,16 @@ class MetamodelBuilderTest {
48 var builder = Metamodel.builder() 58 var builder = Metamodel.builder()
49 .type(university) 59 .type(university)
50 .type(course) 60 .type(course)
51 .reference(courses, university, true, course, location) 61 .reference(courses, referenceBuilder -> referenceBuilder
52 .reference(location, course, 62 .containment(true)
53 ConstrainedMultiplicity.of(CardinalityIntervals.atLeast(2), invalidMultiplicity), 63 .source(university)
54 university, courses); 64 .target(course)
65 .opposite(location))
66 .reference(location, referenceBuilder -> referenceBuilder
67 .source(course)
68 .multiplicity(CardinalityIntervals.atLeast(2), invalidMultiplicity)
69 .target(university)
70 .opposite(courses));
55 71
56 assertThrows(TranslationException.class, builder::build); 72 assertThrows(TranslationException.class, builder::build);
57 } 73 }
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java
index 6c2f55af..88e6a4d7 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java
@@ -16,7 +16,6 @@ import tools.refinery.store.reasoning.representation.PartialRelation;
16import tools.refinery.store.reasoning.seed.ModelSeed; 16import tools.refinery.store.reasoning.seed.ModelSeed;
17import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; 17import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
18import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; 18import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
19import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
20import tools.refinery.store.representation.TruthValue; 19import tools.refinery.store.representation.TruthValue;
21import tools.refinery.store.representation.cardinality.CardinalityIntervals; 20import tools.refinery.store.representation.cardinality.CardinalityIntervals;
22import tools.refinery.store.tuple.Tuple; 21import tools.refinery.store.tuple.Tuple;
@@ -45,12 +44,23 @@ class MetamodelTest {
45 .type(teacher, person) 44 .type(teacher, person)
46 .type(university) 45 .type(university)
47 .type(course) 46 .type(course)
48 .reference(courses, university, true, course, location) 47 .reference(courses, builder -> builder
49 .reference(location, course, university, courses) 48 .containment(true)
50 .reference(lecturer, course, 49 .source(university)
51 ConstrainedMultiplicity.of(CardinalityIntervals.ONE, invalidLecturerCount), teacher) 50 .target(course)
52 .reference(enrolledStudents, course, 51 .opposite(location))
53 ConstrainedMultiplicity.of(CardinalityIntervals.SOME, invalidStudentCount), student) 52 .reference(location, builder -> builder
53 .source(course)
54 .target(university)
55 .opposite(courses))
56 .reference(lecturer, builder -> builder
57 .source(course)
58 .multiplicity(CardinalityIntervals.ONE, invalidLecturerCount)
59 .target(teacher))
60 .reference(enrolledStudents, builder -> builder
61 .source(course)
62 .multiplicity(CardinalityIntervals.SOME, invalidStudentCount)
63 .target(student))
54 .build(); 64 .build();
55 65
56 var seed = ModelSeed.builder(5) 66 var seed = ModelSeed.builder(5)
@@ -105,10 +115,12 @@ class MetamodelTest {
105 var metamodel = Metamodel.builder() 115 var metamodel = Metamodel.builder()
106 .type(university) 116 .type(university)
107 .type(course) 117 .type(course)
108 .reference(courses, university, true, course) 118 .reference(courses, builder -> builder
119 .containment(true)
120 .source(university)
121 .target(course))
109 .build(); 122 .build();
110 123
111
112 var seed = ModelSeed.builder(4) 124 var seed = ModelSeed.builder(4)
113 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder 125 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
114 .reducedValue(CardinalityIntervals.ONE) 126 .reducedValue(CardinalityIntervals.ONE)