aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/language-semantics
diff options
context:
space:
mode:
Diffstat (limited to 'subprojects/language-semantics')
-rw-r--r--subprojects/language-semantics/build.gradle.kts9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java10
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java16
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java12
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java200
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java12
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java16
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java16
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java10
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java674
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java31
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java51
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java32
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java9
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java28
-rw-r--r--subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java83
-rw-r--r--subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java79
-rw-r--r--subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java339
-rw-r--r--subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/internal/DecisionTreeTests.java (renamed from subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/tests/DecisionTreeTests.java)14
22 files changed, 1616 insertions, 52 deletions
diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts
index 38cd9e0d..338ae345 100644
--- a/subprojects/language-semantics/build.gradle.kts
+++ b/subprojects/language-semantics/build.gradle.kts
@@ -9,9 +9,14 @@ plugins {
9} 9}
10 10
11dependencies { 11dependencies {
12 implementation(libs.eclipseCollections) 12 api(libs.eclipseCollections.api)
13 implementation(libs.eclipseCollections.api)
14 api(project(":refinery-language")) 13 api(project(":refinery-language"))
15 api(project(":refinery-store")) 14 api(project(":refinery-store"))
15 api(project(":refinery-store-query"))
16 api(project(":refinery-store-reasoning"))
17 implementation(project(":refinery-store-reasoning-scope"))
18 runtimeOnly(libs.eclipseCollections)
19 testImplementation(project(":refinery-store-dse-visualization"))
20 testImplementation(project(":refinery-store-query-viatra"))
16 testImplementation(testFixtures(project(":refinery-language"))) 21 testImplementation(testFixtures(project(":refinery-language")))
17} 22}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java
new file mode 100644
index 00000000..6f706069
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/BuiltInDetail.java
@@ -0,0 +1,10 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record BuiltInDetail() implements RelationDetail {
9 public static final BuiltInDetail INSTANCE = new BuiltInDetail();
10}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java
new file mode 100644
index 00000000..1d3190f5
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ClassDetail.java
@@ -0,0 +1,16 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record ClassDetail(boolean abstractClass) implements RelationDetail {
9 public static final ClassDetail CONCRETE_CLASS = new ClassDetail(false);
10
11 public static final ClassDetail ABSTRACT_CLASS = new ClassDetail(true);
12
13 public static ClassDetail ofAbstractClass(boolean abstractClass) {
14 return abstractClass ? ABSTRACT_CLASS : CONCRETE_CLASS;
15 }
16}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java
new file mode 100644
index 00000000..d2dcb43a
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/Metadata.java
@@ -0,0 +1,12 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public sealed interface Metadata permits NodeMetadata, RelationMetadata {
9 String name();
10
11 String simpleName();
12}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java
new file mode 100644
index 00000000..cc262129
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/MetadataCreator.java
@@ -0,0 +1,200 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8import com.google.inject.Inject;
9import org.eclipse.emf.ecore.EObject;
10import org.eclipse.xtext.naming.IQualifiedNameConverter;
11import org.eclipse.xtext.naming.IQualifiedNameProvider;
12import org.eclipse.xtext.naming.QualifiedName;
13import org.eclipse.xtext.scoping.IScope;
14import org.eclipse.xtext.scoping.IScopeProvider;
15import tools.refinery.language.model.problem.*;
16import tools.refinery.language.semantics.model.ModelInitializer;
17import tools.refinery.language.semantics.model.TracedException;
18import tools.refinery.language.utils.ProblemUtil;
19import tools.refinery.store.reasoning.representation.PartialRelation;
20
21import java.util.*;
22
23public class MetadataCreator {
24 @Inject
25 private IScopeProvider scopeProvider;
26
27 @Inject
28 private IQualifiedNameProvider qualifiedNameProvider;
29
30 @Inject
31 private IQualifiedNameConverter qualifiedNameConverter;
32
33 private ModelInitializer initializer;
34
35 private IScope nodeScope;
36
37 private IScope relationScope;
38
39 public void setInitializer(ModelInitializer initializer) {
40 if (initializer == null) {
41 throw new IllegalArgumentException("Initializer was already set");
42 }
43 this.initializer = initializer;
44 var problem = initializer.getProblem();
45 nodeScope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
46 relationScope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION);
47 }
48
49 public static String unnamedNode(int nodeId) {
50 return "::" + nodeId;
51 }
52
53 public List<NodeMetadata> getNodesMetadata() {
54 return getNodesMetadata(initializer.getNodeCount(), true);
55 }
56
57 public List<NodeMetadata> getNodesMetadata(int nodeCount, boolean preserveNewNodes) {
58 var nodes = new NodeMetadata[Math.max(initializer.getNodeCount(), nodeCount)];
59 for (var entry : initializer.getNodeTrace().keyValuesView()) {
60 var node = entry.getOne();
61 var id = entry.getTwo();
62 nodes[id] = getNodeMetadata(id, node, preserveNewNodes);
63 }
64 for (int i = 0; i < nodes.length; i++) {
65 if (nodes[i] == null) {
66 var nodeName = unnamedNode(i);
67 nodes[i] = new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT);
68 }
69 }
70 return List.of(nodes);
71 }
72
73 private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes) {
74 var kind = getNodeKind(node);
75 if (!preserveNewNodes && kind == NodeKind.NEW) {
76 var nodeName = unnamedNode(nodeId);
77 return new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT);
78 }
79 var qualifiedName = getQualifiedName(node);
80 var simpleName = getSimpleName(node, qualifiedName, nodeScope);
81 return new NodeMetadata(qualifiedNameConverter.toString(qualifiedName),
82 qualifiedNameConverter.toString(simpleName), getNodeKind(node));
83 }
84
85 private NodeKind getNodeKind(Node node) {
86 if (ProblemUtil.isImplicitNode(node)) {
87 return NodeKind.IMPLICIT;
88 } else if (ProblemUtil.isIndividualNode(node)) {
89 return NodeKind.INDIVIDUAL;
90 } else if (ProblemUtil.isNewNode(node)) {
91 return NodeKind.NEW;
92 } else {
93 throw new TracedException(node, "Unknown node type");
94 }
95 }
96
97 public List<RelationMetadata> getRelationsMetadata() {
98 var relationTrace = initializer.getRelationTrace();
99 var relations = new ArrayList<RelationMetadata>(relationTrace.size());
100 for (var entry : relationTrace.entrySet()) {
101 var relation = entry.getKey();
102 var partialRelation = entry.getValue();
103 var metadata = getRelationMetadata(relation, partialRelation);
104 relations.add(metadata);
105 }
106 return Collections.unmodifiableList(relations);
107 }
108
109 private RelationMetadata getRelationMetadata(Relation relation, PartialRelation partialRelation) {
110 var qualifiedName = getQualifiedName(relation);
111 var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
112 var simpleName = getSimpleName(relation, qualifiedName, relationScope);
113 var simpleNameString = qualifiedNameConverter.toString(simpleName);
114 var arity = partialRelation.arity();
115 var detail = getRelationDetail(relation, partialRelation);
116 return new RelationMetadata(qualifiedNameString, simpleNameString, arity, detail);
117 }
118
119 private RelationDetail getRelationDetail(Relation relation, PartialRelation partialRelation) {
120 if (ProblemUtil.isBuiltIn(relation) && !ProblemUtil.isError(relation)) {
121 return getBuiltInDetail();
122 }
123 if (relation instanceof ClassDeclaration classDeclaration) {
124 return getClassDetail(classDeclaration);
125 } else if (relation instanceof ReferenceDeclaration) {
126 return getReferenceDetail(partialRelation);
127 } else if (relation instanceof EnumDeclaration) {
128 return getEnumDetail();
129 } else if (relation instanceof PredicateDefinition predicateDefinition) {
130 return getPredicateDetail(predicateDefinition);
131 } else {
132 throw new TracedException(relation, "Unknown relation");
133 }
134 }
135
136 private RelationDetail getBuiltInDetail() {
137 return BuiltInDetail.INSTANCE;
138 }
139
140 private RelationDetail getClassDetail(ClassDeclaration classDeclaration) {
141 return ClassDetail.ofAbstractClass(classDeclaration.isAbstract());
142 }
143
144 private RelationDetail getReferenceDetail(PartialRelation partialRelation) {
145 var metamodel = initializer.getMetamodel();
146 var opposite = metamodel.oppositeReferences().get(partialRelation);
147 if (opposite == null) {
148 boolean isContainment = metamodel.containmentHierarchy().containsKey(partialRelation);
149 return ReferenceDetail.ofContainment(isContainment);
150 } else {
151 boolean isContainer = metamodel.containmentHierarchy().containsKey(opposite);
152 return new OppositeReferenceDetail(isContainer, opposite.name());
153 }
154 }
155
156 private RelationDetail getEnumDetail() {
157 return ClassDetail.CONCRETE_CLASS;
158 }
159
160 private RelationDetail getPredicateDetail(PredicateDefinition predicate) {
161 return PredicateDetail.ofError(predicate.isError());
162 }
163
164 private QualifiedName getQualifiedName(EObject eObject) {
165 var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
166 if (qualifiedName == null) {
167 throw new TracedException(eObject, "Unknown qualified name");
168 }
169 return qualifiedName;
170 }
171
172 private QualifiedName getSimpleName(EObject eObject, QualifiedName qualifiedName, IScope scope) {
173 var descriptions = scope.getElements(eObject);
174 var names = new HashSet<QualifiedName>();
175 for (var description : descriptions) {
176 // {@code getQualifiedName()} will refer to the full name for objects that are loaded from the global
177 // scope, but {@code getName()} returns the qualified name that we set in
178 // {@code ProblemResourceDescriptionStrategy}.
179 names.add(description.getName());
180 }
181 var iterator = names.stream().sorted(Comparator.comparingInt(QualifiedName::getSegmentCount)).iterator();
182 while (iterator.hasNext()) {
183 var simpleName = iterator.next();
184 if (names.contains(simpleName) && isUnique(scope, simpleName)) {
185 return simpleName;
186 }
187 }
188 throw new TracedException(eObject, "Ambiguous qualified name: " +
189 qualifiedNameConverter.toString(qualifiedName));
190 }
191
192 private boolean isUnique(IScope scope, QualifiedName name) {
193 var iterator = scope.getElements(name).iterator();
194 if (!iterator.hasNext()) {
195 return false;
196 }
197 iterator.next();
198 return !iterator.hasNext();
199 }
200}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java
new file mode 100644
index 00000000..01f0cd09
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeKind.java
@@ -0,0 +1,12 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public enum NodeKind {
9 IMPLICIT,
10 INDIVIDUAL,
11 NEW
12}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java
new file mode 100644
index 00000000..812952c0
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/NodeMetadata.java
@@ -0,0 +1,9 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record NodeMetadata(String name, String simpleName, NodeKind kind) implements Metadata {
9}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java
new file mode 100644
index 00000000..26d7461c
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/OppositeReferenceDetail.java
@@ -0,0 +1,9 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record OppositeReferenceDetail(boolean container, String opposite) implements RelationDetail {
9}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java
new file mode 100644
index 00000000..ca397eca
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/PredicateDetail.java
@@ -0,0 +1,16 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record PredicateDetail(boolean error) implements RelationDetail {
9 public static final PredicateDetail PREDICATE = new PredicateDetail(false);
10
11 public static final PredicateDetail ERROR_PREDICATE = new PredicateDetail(true);
12
13 public static PredicateDetail ofError(boolean error) {
14 return error ? ERROR_PREDICATE : PREDICATE;
15 }
16}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java
new file mode 100644
index 00000000..36771566
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/ReferenceDetail.java
@@ -0,0 +1,16 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record ReferenceDetail(boolean containment) implements RelationDetail {
9 public static final ReferenceDetail CROSS_REFERENCE = new ReferenceDetail(false);
10
11 public static final ReferenceDetail CONTAINMENT_REFERENCE = new ReferenceDetail(true);
12
13 public static ReferenceDetail ofContainment(boolean containment) {
14 return containment ? CONTAINMENT_REFERENCE : CROSS_REFERENCE;
15 }
16}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java
new file mode 100644
index 00000000..105179fd
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationDetail.java
@@ -0,0 +1,10 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public sealed interface RelationDetail permits ClassDetail, ReferenceDetail, PredicateDetail, OppositeReferenceDetail,
9 BuiltInDetail {
10}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java
new file mode 100644
index 00000000..5abcc253
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/metadata/RelationMetadata.java
@@ -0,0 +1,9 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.metadata;
7
8public record RelationMetadata(String name, String simpleName, int arity, RelationDetail detail) implements Metadata {
9}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
index 06b8ad77..85c8d701 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
@@ -9,67 +9,408 @@ import com.google.inject.Inject;
9import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; 9import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
10import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; 10import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
11import tools.refinery.language.model.problem.*; 11import tools.refinery.language.model.problem.*;
12import tools.refinery.language.semantics.model.internal.DecisionTree; 12import tools.refinery.language.semantics.model.internal.MutableSeed;
13import tools.refinery.language.utils.BuiltinSymbols;
13import tools.refinery.language.utils.ProblemDesugarer; 14import tools.refinery.language.utils.ProblemDesugarer;
14import tools.refinery.language.utils.RelationInfo; 15import tools.refinery.language.utils.ProblemUtil;
15import tools.refinery.store.representation.Symbol; 16import tools.refinery.store.dse.propagation.PropagationBuilder;
17import tools.refinery.store.model.ModelStoreBuilder;
18import tools.refinery.store.query.Constraint;
19import tools.refinery.store.query.dnf.InvalidClauseException;
20import tools.refinery.store.query.dnf.Query;
21import tools.refinery.store.query.dnf.RelationalQuery;
22import tools.refinery.store.query.literal.*;
23import tools.refinery.store.query.term.NodeVariable;
24import tools.refinery.store.query.term.Variable;
25import tools.refinery.store.reasoning.ReasoningAdapter;
26import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
27import tools.refinery.store.reasoning.representation.PartialRelation;
28import tools.refinery.store.reasoning.scope.ScopePropagator;
29import tools.refinery.store.reasoning.seed.ModelSeed;
30import tools.refinery.store.reasoning.seed.Seed;
31import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
32import tools.refinery.store.reasoning.translator.metamodel.Metamodel;
33import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder;
34import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
35import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
36import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
37import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
38import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity;
39import tools.refinery.store.reasoning.translator.predicate.PredicateTranslator;
16import tools.refinery.store.representation.TruthValue; 40import tools.refinery.store.representation.TruthValue;
41import tools.refinery.store.representation.cardinality.CardinalityInterval;
42import tools.refinery.store.representation.cardinality.CardinalityIntervals;
43import tools.refinery.store.representation.cardinality.UpperCardinalities;
17import tools.refinery.store.tuple.Tuple; 44import tools.refinery.store.tuple.Tuple;
18 45
19import java.util.HashMap; 46import java.util.*;
20import java.util.Map;
21 47
22public class ModelInitializer { 48public class ModelInitializer {
23 @Inject 49 @Inject
24 private ProblemDesugarer desugarer; 50 private ProblemDesugarer desugarer;
25 51
52 @Inject
53 private SemanticsUtils semanticsUtils;
54
55 private Problem problem;
56
57 private ModelStoreBuilder storeBuilder;
58
59 private BuiltinSymbols builtinSymbols;
60
61 private PartialRelation nodeRelation;
62
26 private final MutableObjectIntMap<Node> nodeTrace = ObjectIntMaps.mutable.empty(); 63 private final MutableObjectIntMap<Node> nodeTrace = ObjectIntMaps.mutable.empty();
27 64
28 private final Map<tools.refinery.language.model.problem.Relation, Symbol<TruthValue>> relationTrace = 65 private final Map<Relation, RelationInfo> relationInfoMap = new LinkedHashMap<>();
29 new HashMap<>(); 66
67 private final Map<PartialRelation, RelationInfo> partialRelationInfoMap = new HashMap<>();
68
69 private final Map<AnyPartialSymbol, Relation> inverseTrace = new HashMap<>();
70
71 private Map<Relation, PartialRelation> relationTrace;
72
73 private final MetamodelBuilder metamodelBuilder = Metamodel.builder();
74
75 private Metamodel metamodel;
76
77 private final Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>();
78
79 private ScopePropagator scopePropagator;
80
81 private ModelSeed modelSeed;
82
83 public Problem getProblem() {
84 return problem;
85 }
86
87 public int getNodeCount() {
88 return nodeTrace.size();
89 }
90
91 public MutableObjectIntMap<Node> getNodeTrace() {
92 return nodeTrace;
93 }
94
95 public Map<Relation, PartialRelation> getRelationTrace() {
96 return relationTrace;
97 }
30 98
31 private int nodeCount = 0; 99 public Relation getInverseTrace(AnyPartialSymbol partialRelation) {
100 return inverseTrace.get(partialRelation);
101 }
102
103 public Metamodel getMetamodel() {
104 return metamodel;
105 }
32 106
33 public void createModel(Problem problem) { 107 public ModelSeed createModel(Problem problem, ModelStoreBuilder storeBuilder) {
34 var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( 108 this.problem = problem;
109 this.storeBuilder = storeBuilder;
110 builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException(
35 "Problem has no builtin library")); 111 "Problem has no builtin library"));
36 var collectedSymbols = desugarer.collectSymbols(problem); 112 var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE);
37 for (var node : collectedSymbols.nodes().keySet()) { 113 nodeRelation = nodeInfo.partialRelation();
38 nodeTrace.put(node, nodeCount); 114 metamodelBuilder.type(nodeRelation);
39 nodeCount += 1; 115 putRelationInfo(builtinSymbols.exists(), new RelationInfo(ReasoningAdapter.EXISTS_SYMBOL, null,
40 } 116 TruthValue.TRUE));
41 for (var pair : collectedSymbols.relations().entrySet()) { 117 putRelationInfo(builtinSymbols.equals(), new RelationInfo(ReasoningAdapter.EQUALS_SYMBOL,
42 var relation = pair.getKey(); 118 (TruthValue) null,
43 var relationInfo = pair.getValue(); 119 null));
44 var isEqualsRelation = relation == builtinSymbols.equals(); 120 putRelationInfo(builtinSymbols.contained(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINED_SYMBOL,
45 var decisionTree = mergeAssertions(relationInfo, isEqualsRelation); 121 null, TruthValue.UNKNOWN));
46 var defaultValue = isEqualsRelation ? TruthValue.FALSE : TruthValue.UNKNOWN; 122 putRelationInfo(builtinSymbols.contains(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINS_SYMBOL,
47 relationTrace.put(relation, Symbol.of( 123 null, TruthValue.UNKNOWN));
48 relationInfo.name(), relationInfo.arity(), TruthValue.class, defaultValue)); 124 putRelationInfo(builtinSymbols.invalidContainer(),
49 } 125 new RelationInfo(ContainmentHierarchyTranslator.INVALID_CONTAINER, TruthValue.FALSE,
50 } 126 TruthValue.FALSE));
51 127 collectNodes();
52 private DecisionTree mergeAssertions(RelationInfo relationInfo, boolean isEqualsRelation) { 128 collectPartialSymbols();
53 var arity = relationInfo.arity(); 129 collectMetamodel();
54 var defaultAssertions = new DecisionTree(arity, isEqualsRelation ? null : TruthValue.UNKNOWN); 130 metamodel = metamodelBuilder.build();
55 var assertions = new DecisionTree(arity); 131 collectAssertions();
56 for (var assertion : relationInfo.assertions()) { 132 storeBuilder.with(new MultiObjectTranslator());
57 var tuple = getTuple(assertion); 133 storeBuilder.with(new MetamodelTranslator(metamodel));
58 var value = getTruthValue(assertion.getValue()); 134 relationTrace = new LinkedHashMap<>(relationInfoMap.size());
59 if (assertion.isDefault()) { 135 int nodeCount = getNodeCount();
60 defaultAssertions.mergeValue(tuple, value); 136 var modelSeedBuilder = ModelSeed.builder(nodeCount);
137 for (var entry : relationInfoMap.entrySet()) {
138 var relation = entry.getKey();
139 var info = entry.getValue();
140 var partialRelation = info.partialRelation();
141 relationTrace.put(relation, partialRelation);
142 modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
143 }
144 collectScopes();
145 if (scopePropagator != null) {
146 if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) {
147 throw new TracedException(problem, "Type scopes require a PropagationBuilder");
148 }
149 storeBuilder.with(scopePropagator);
150 }
151 modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
152 .reducedValue(CardinalityIntervals.SET)
153 .putAll(countSeed));
154 modelSeed = modelSeedBuilder.build();
155 collectPredicates();
156 return modelSeed;
157 }
158
159 private void collectNodes() {
160 for (var statement : problem.getStatements()) {
161 if (statement instanceof IndividualDeclaration individualDeclaration) {
162 for (var individual : individualDeclaration.getNodes()) {
163 collectNode(individual);
164 }
165 } else if (statement instanceof ClassDeclaration classDeclaration) {
166 var newNode = classDeclaration.getNewNode();
167 if (newNode != null) {
168 collectNode(newNode);
169 }
170 } else if (statement instanceof EnumDeclaration enumDeclaration) {
171 for (var literal : enumDeclaration.getLiterals()) {
172 collectNode(literal);
173 }
174 }
175 }
176 for (var node : problem.getNodes()) {
177 collectNode(node);
178 }
179 }
180
181 private void collectNode(Node node) {
182 nodeTrace.getIfAbsentPut(node, this::getNodeCount);
183 }
184
185 private void collectPartialSymbols() {
186 for (var statement : problem.getStatements()) {
187 if (statement instanceof ClassDeclaration classDeclaration) {
188 collectClassDeclarationSymbols(classDeclaration);
189 } else if (statement instanceof EnumDeclaration enumDeclaration) {
190 collectPartialRelation(enumDeclaration, 1, TruthValue.FALSE, TruthValue.FALSE);
191 } else if (statement instanceof PredicateDefinition predicateDefinition) {
192 collectPredicateDefinitionSymbol(predicateDefinition);
193 }
194 }
195 }
196
197 private void collectClassDeclarationSymbols(ClassDeclaration classDeclaration) {
198 collectPartialRelation(classDeclaration, 1, null, TruthValue.UNKNOWN);
199 for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
200 if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
201 collectPartialRelation(referenceDeclaration, 2, null, TruthValue.UNKNOWN);
202 var invalidMultiplicityConstraint = referenceDeclaration.getInvalidMultiplicity();
203 if (invalidMultiplicityConstraint != null) {
204 collectPartialRelation(invalidMultiplicityConstraint, 1, TruthValue.FALSE, TruthValue.FALSE);
205 }
61 } else { 206 } else {
62 assertions.mergeValue(tuple, value); 207 throw new TracedException(featureDeclaration, "Unknown feature declaration");
208 }
209 }
210 }
211
212 private void collectPredicateDefinitionSymbol(PredicateDefinition predicateDefinition) {
213 int arity = predicateDefinition.getParameters().size();
214 if (predicateDefinition.isError()) {
215 collectPartialRelation(predicateDefinition, arity, TruthValue.FALSE, TruthValue.FALSE);
216 } else {
217 collectPartialRelation(predicateDefinition, arity, null, TruthValue.UNKNOWN);
218 }
219 }
220
221 private void putRelationInfo(Relation relation, RelationInfo info) {
222 relationInfoMap.put(relation, info);
223 partialRelationInfoMap.put(info.partialRelation(), info);
224 inverseTrace.put(info.partialRelation(), relation);
225 }
226
227 private RelationInfo collectPartialRelation(Relation relation, int arity, TruthValue value,
228 TruthValue defaultValue) {
229 return relationInfoMap.computeIfAbsent(relation, key -> {
230 var name = getName(relation);
231 var info = new RelationInfo(name, arity, value, defaultValue);
232 partialRelationInfoMap.put(info.partialRelation(), info);
233 inverseTrace.put(info.partialRelation(), relation);
234 return info;
235 });
236 }
237
238 private String getName(Relation relation) {
239 return semanticsUtils.getName(relation).orElseGet(() -> "::" + relationInfoMap.size());
240 }
241
242 private void collectMetamodel() {
243 for (var statement : problem.getStatements()) {
244 if (statement instanceof ClassDeclaration classDeclaration) {
245 collectClassDeclarationMetamodel(classDeclaration);
246 } else if (statement instanceof EnumDeclaration enumDeclaration) {
247 collectEnumMetamodel(enumDeclaration);
248 }
249 }
250 }
251
252 private void collectEnumMetamodel(EnumDeclaration enumDeclaration) {
253 try {
254 metamodelBuilder.type(getPartialRelation(enumDeclaration), nodeRelation);
255 } catch (RuntimeException e) {
256 throw TracedException.addTrace(enumDeclaration, e);
257 }
258 }
259
260 private void collectClassDeclarationMetamodel(ClassDeclaration classDeclaration) {
261 var superTypes = classDeclaration.getSuperTypes();
262 var partialSuperTypes = new ArrayList<PartialRelation>(superTypes.size() + 1);
263 partialSuperTypes.add(nodeRelation);
264 for (var superType : superTypes) {
265 partialSuperTypes.add(getPartialRelation(superType));
266 }
267 try {
268 metamodelBuilder.type(getPartialRelation(classDeclaration), classDeclaration.isAbstract(),
269 partialSuperTypes);
270 } catch (RuntimeException e) {
271 throw TracedException.addTrace(classDeclaration, e);
272 }
273 for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
274 if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) {
275 collectReferenceDeclarationMetamodel(classDeclaration, referenceDeclaration);
63 } 276 }
64 } 277 }
65 defaultAssertions.overwriteValues(assertions); 278 }
66 if (isEqualsRelation) { 279
67 for (int i = 0; i < nodeCount; i++) { 280 private void collectReferenceDeclarationMetamodel(ClassDeclaration classDeclaration,
68 defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE); 281 ReferenceDeclaration referenceDeclaration) {
282 var relation = getPartialRelation(referenceDeclaration);
283 var source = getPartialRelation(classDeclaration);
284 var target = getPartialRelation(referenceDeclaration.getReferenceType());
285 boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT;
286 var opposite = referenceDeclaration.getOpposite();
287 PartialRelation oppositeRelation = null;
288 if (opposite != null) {
289 oppositeRelation = getPartialRelation(opposite);
290 }
291 var multiplicity = getMultiplicityConstraint(referenceDeclaration);
292 try {
293 metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation);
294 } catch (RuntimeException e) {
295 throw TracedException.addTrace(classDeclaration, e);
296 }
297 }
298
299 private Multiplicity getMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) {
300 if (!ProblemUtil.hasMultiplicityConstraint(referenceDeclaration)) {
301 return UnconstrainedMultiplicity.INSTANCE;
302 }
303 var problemMultiplicity = referenceDeclaration.getMultiplicity();
304 CardinalityInterval interval;
305 if (problemMultiplicity == null) {
306 interval = CardinalityIntervals.LONE;
307 } else {
308 interval = getCardinalityInterval(problemMultiplicity);
309 }
310 var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation();
311 return ConstrainedMultiplicity.of(interval, constraint);
312 }
313
314 private static CardinalityInterval getCardinalityInterval(
315 tools.refinery.language.model.problem.Multiplicity problemMultiplicity) {
316 if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) {
317 return CardinalityIntervals.exactly(exactMultiplicity.getExactValue());
318 } else if (problemMultiplicity instanceof RangeMultiplicity rangeMultiplicity) {
319 var upperBound = rangeMultiplicity.getUpperBound();
320 return CardinalityIntervals.between(rangeMultiplicity.getLowerBound(),
321 upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound));
322 } else {
323 throw new TracedException(problemMultiplicity, "Unknown multiplicity");
324 }
325 }
326
327 private void collectAssertions() {
328 for (var statement : problem.getStatements()) {
329 if (statement instanceof ClassDeclaration classDeclaration) {
330 collectClassDeclarationAssertions(classDeclaration);
331 } else if (statement instanceof EnumDeclaration enumDeclaration) {
332 collectEnumAssertions(enumDeclaration);
333 } else if (statement instanceof IndividualDeclaration individualDeclaration) {
334 for (var individual : individualDeclaration.getNodes()) {
335 collectIndividualAssertions(individual);
336 }
337 } else if (statement instanceof Assertion assertion) {
338 collectAssertion(assertion);
69 } 339 }
70 defaultAssertions.setAllMissing(TruthValue.FALSE);
71 } 340 }
72 return defaultAssertions; 341 }
342
343 private void collectClassDeclarationAssertions(ClassDeclaration classDeclaration) {
344 var newNode = classDeclaration.getNewNode();
345 if (newNode == null) {
346 return;
347 }
348 var newNodeId = getNodeId(newNode);
349 collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN);
350 var tuple = Tuple.of(newNodeId);
351 mergeValue(classDeclaration, tuple, TruthValue.TRUE);
352 var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
353 for (var subType : typeInfo.getDirectSubtypes()) {
354 partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
355 }
356 }
357
358 private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
359 var overlay = MutableSeed.of(1, null);
360 for (var literal : enumDeclaration.getLiterals()) {
361 collectIndividualAssertions(literal);
362 var nodeId = getNodeId(literal);
363 overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE);
364 }
365 var info = getRelationInfo(enumDeclaration);
366 info.assertions().overwriteValues(overlay);
367 }
368
369 private void collectIndividualAssertions(Node node) {
370 var nodeId = getNodeId(node);
371 collectCardinalityAssertions(nodeId, TruthValue.TRUE);
372 }
373
374 private void collectCardinalityAssertions(int nodeId, TruthValue value) {
375 mergeValue(builtinSymbols.exists(), Tuple.of(nodeId), value);
376 mergeValue(builtinSymbols.equals(), Tuple.of(nodeId, nodeId), value);
377 }
378
379 private void collectAssertion(Assertion assertion) {
380 var tuple = getTuple(assertion);
381 var value = getTruthValue(assertion.getValue());
382 var relation = assertion.getRelation();
383 var info = getRelationInfo(relation);
384 var partialRelation = info.partialRelation();
385 if (partialRelation.arity() != tuple.getSize()) {
386 throw new TracedException(assertion, "Expected %d arguments for %s, got %d instead"
387 .formatted(partialRelation.arity(), partialRelation, tuple.getSize()));
388 }
389 if (assertion.isDefault()) {
390 info.defaultAssertions().mergeValue(tuple, value);
391 } else {
392 info.assertions().mergeValue(tuple, value);
393 }
394 }
395
396 private void mergeValue(Relation relation, Tuple key, TruthValue value) {
397 getRelationInfo(relation).assertions().mergeValue(key, value);
398 }
399
400 private RelationInfo getRelationInfo(Relation relation) {
401 var info = relationInfoMap.get(relation);
402 if (info == null) {
403 throw new IllegalArgumentException("Unknown relation: " + relation);
404 }
405 return info;
406 }
407
408 private PartialRelation getPartialRelation(Relation relation) {
409 return getRelationInfo(relation).partialRelation();
410 }
411
412 private int getNodeId(Node node) {
413 return nodeTrace.getOrThrow(node);
73 } 414 }
74 415
75 private Tuple getTuple(Assertion assertion) { 416 private Tuple getTuple(Assertion assertion) {
@@ -79,11 +420,11 @@ public class ModelInitializer {
79 for (int i = 0; i < arity; i++) { 420 for (int i = 0; i < arity; i++) {
80 var argument = arguments.get(i); 421 var argument = arguments.get(i);
81 if (argument instanceof NodeAssertionArgument nodeArgument) { 422 if (argument instanceof NodeAssertionArgument nodeArgument) {
82 nodes[i] = nodeTrace.getOrThrow(nodeArgument.getNode()); 423 nodes[i] = getNodeId(nodeArgument.getNode());
83 } else if (argument instanceof WildcardAssertionArgument) { 424 } else if (argument instanceof WildcardAssertionArgument) {
84 nodes[i] = -1; 425 nodes[i] = -1;
85 } else { 426 } else {
86 throw new IllegalArgumentException("Unknown assertion argument: " + argument); 427 throw new TracedException(argument, "Unsupported assertion argument");
87 } 428 }
88 } 429 }
89 return Tuple.of(nodes); 430 return Tuple.of(nodes);
@@ -100,4 +441,249 @@ public class ModelInitializer {
100 case ERROR -> TruthValue.ERROR; 441 case ERROR -> TruthValue.ERROR;
101 }; 442 };
102 } 443 }
444
445 private void collectPredicates() {
446 for (var statement : problem.getStatements()) {
447 if (statement instanceof PredicateDefinition predicateDefinition) {
448 collectPredicateDefinitionTraced(predicateDefinition);
449 }
450 }
451 }
452
453 private void collectPredicateDefinitionTraced(PredicateDefinition predicateDefinition) {
454 try {
455 collectPredicateDefinition(predicateDefinition);
456 } catch (InvalidClauseException e) {
457 int clauseIndex = e.getClauseIndex();
458 var bodies = predicateDefinition.getBodies();
459 if (clauseIndex < bodies.size()) {
460 throw new TracedException(bodies.get(clauseIndex), e);
461 } else {
462 throw new TracedException(predicateDefinition, e);
463 }
464 } catch (RuntimeException e) {
465 throw TracedException.addTrace(predicateDefinition, e);
466 }
467 }
468
469 private void collectPredicateDefinition(PredicateDefinition predicateDefinition) {
470 var partialRelation = getPartialRelation(predicateDefinition);
471 var query = toQuery(partialRelation.name(), predicateDefinition);
472 boolean mutable;
473 TruthValue defaultValue;
474 if (predicateDefinition.isError()) {
475 mutable = false;
476 defaultValue = TruthValue.FALSE;
477 } else {
478 var seed = modelSeed.getSeed(partialRelation);
479 defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
480 var cursor = seed.getCursor(defaultValue, getNodeCount());
481 // The symbol should be mutable if there is at least one non-default entry in the seed.
482 mutable = cursor.move();
483 }
484 var translator = new PredicateTranslator(partialRelation, query, mutable, defaultValue);
485 storeBuilder.with(translator);
486 }
487
488 private RelationalQuery toQuery(String name, PredicateDefinition predicateDefinition) {
489 var problemParameters = predicateDefinition.getParameters();
490 int arity = problemParameters.size();
491 var parameters = new NodeVariable[arity];
492 var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity);
493 var commonLiterals = new ArrayList<Literal>();
494 for (int i = 0; i < arity; i++) {
495 var problemParameter = problemParameters.get(i);
496 var parameter = Variable.of(problemParameter.getName());
497 parameters[i] = parameter;
498 parameterMap.put(problemParameter, parameter);
499 var parameterType = problemParameter.getParameterType();
500 if (parameterType != null) {
501 var partialType = getPartialRelation(parameterType);
502 commonLiterals.add(partialType.call(parameter));
503 }
504 }
505 var builder = Query.builder(name).parameters(parameters);
506 for (var body : predicateDefinition.getBodies()) {
507 try {
508 var localScope = extendScope(parameterMap, body.getImplicitVariables());
509 var problemLiterals = body.getLiterals();
510 var literals = new ArrayList<>(commonLiterals);
511 for (var problemLiteral : problemLiterals) {
512 toLiteralsTraced(problemLiteral, localScope, literals);
513 }
514 builder.clause(literals);
515 } catch (RuntimeException e) {
516 throw TracedException.addTrace(body, e);
517 }
518 }
519 return builder.build();
520 }
521
522 private Map<tools.refinery.language.model.problem.Variable, Variable> extendScope(
523 Map<tools.refinery.language.model.problem.Variable, Variable> existing,
524 Collection<? extends tools.refinery.language.model.problem.Variable> newVariables) {
525 if (newVariables.isEmpty()) {
526 return existing;
527 }
528 int localScopeSize = existing.size() + newVariables.size();
529 var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize);
530 localScope.putAll(existing);
531 for (var newVariable : newVariables) {
532 localScope.put(newVariable, Variable.of(newVariable.getName()));
533 }
534 return localScope;
535 }
536
537 private void toLiteralsTraced(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
538 List<Literal> literals) {
539 try {
540 toLiterals(expr, localScope, literals);
541 } catch (RuntimeException e) {
542 throw TracedException.addTrace(expr, e);
543 }
544 }
545
546 private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
547 List<Literal> literals) {
548 if (expr instanceof LogicConstant logicConstant) {
549 switch (logicConstant.getLogicValue()) {
550 case TRUE -> literals.add(BooleanLiteral.TRUE);
551 case FALSE -> literals.add(BooleanLiteral.FALSE);
552 default -> throw new TracedException(logicConstant, "Unsupported literal");
553 }
554 } else if (expr instanceof Atom atom) {
555 var target = getPartialRelation(atom.getRelation());
556 var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE;
557 var argumentList = toArgumentList(atom.getArguments(), localScope, literals);
558 literals.add(target.call(polarity, argumentList));
559 } else if (expr instanceof NegationExpr negationExpr) {
560 var body = negationExpr.getBody();
561 if (!(body instanceof Atom atom)) {
562 throw new TracedException(body, "Cannot negate literal");
563 }
564 var target = getPartialRelation(atom.getRelation());
565 Constraint constraint;
566 if (atom.isTransitiveClosure()) {
567 constraint = Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause(
568 target.callTransitive(p1, p2)
569 )).getDnf();
570 } else {
571 constraint = target;
572 }
573 var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables());
574 var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals);
575 literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList));
576 } else if (expr instanceof ComparisonExpr comparisonExpr) {
577 var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()),
578 localScope, literals);
579 boolean positive = switch (comparisonExpr.getOp()) {
580 case EQ -> true;
581 case NOT_EQ -> false;
582 default -> throw new TracedException(
583 comparisonExpr, "Unsupported operator");
584 };
585 literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1)));
586 } else {
587 throw new TracedException(expr, "Unsupported literal");
588 }
589 }
590
591 private List<Variable> toArgumentList(
592 List<Expr> expressions, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
593 List<Literal> literals) {
594 var argumentList = new ArrayList<Variable>(expressions.size());
595 for (var expr : expressions) {
596 if (!(expr instanceof VariableOrNodeExpr variableOrNodeExpr)) {
597 throw new TracedException(expr, "Unsupported argument");
598 }
599 var variableOrNode = variableOrNodeExpr.getVariableOrNode();
600 if (variableOrNode instanceof Node node) {
601 int nodeId = getNodeId(node);
602 var tempVariable = Variable.of(semanticsUtils.getName(node).orElse("_" + nodeId));
603 literals.add(new ConstantLiteral(tempVariable, nodeId));
604 argumentList.add(tempVariable);
605 } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) {
606 if (variableOrNodeExpr.getSingletonVariable() == problemVariable) {
607 argumentList.add(Variable.of(problemVariable.getName()));
608 } else {
609 var variable = localScope.get(problemVariable);
610 if (variable == null) {
611 throw new TracedException(variableOrNode, "Unknown variable: " + problemVariable.getName());
612 }
613 argumentList.add(variable);
614 }
615 } else {
616 throw new TracedException(variableOrNode, "Unknown argument");
617 }
618 }
619 return argumentList;
620 }
621
622 private void collectScopes() {
623 for (var statement : problem.getStatements()) {
624 if (statement instanceof ScopeDeclaration scopeDeclaration) {
625 for (var typeScope : scopeDeclaration.getTypeScopes()) {
626 if (typeScope.isIncrement()) {
627 collectTypeScopeIncrement(typeScope);
628 } else {
629 collectTypeScope(typeScope);
630 }
631 }
632 }
633 }
634 }
635
636 private void collectTypeScopeIncrement(TypeScope typeScope) {
637 if (!(typeScope.getTargetType() instanceof ClassDeclaration classDeclaration)) {
638 throw new TracedException(typeScope, "Target of incremental type scope must be a class declaration");
639 }
640 var newNode = classDeclaration.getNewNode();
641 if (newNode == null) {
642 throw new TracedException(typeScope, "Target of incremental type scope must be concrete class");
643 }
644 int newNodeId = nodeTrace.get(newNode);
645 var type = relationTrace.get(classDeclaration);
646 var typeInfo = metamodel.typeHierarchy().getAnalysisResult(type);
647 if (!typeInfo.getDirectSubtypes().isEmpty()) {
648 throw new TracedException(typeScope, "Target of incremental type scope cannot have any subclasses");
649 }
650 var interval = getCardinalityInterval(typeScope.getMultiplicity());
651 countSeed.compute(Tuple.of(newNodeId), (key, oldValue) ->
652 oldValue == null ? interval : oldValue.meet(interval));
653 }
654
655 private void collectTypeScope(TypeScope typeScope) {
656 var type = relationTrace.get(typeScope.getTargetType());
657 if (type == null) {
658 throw new TracedException(typeScope, "Unknown target type");
659 }
660 var interval = getCardinalityInterval(typeScope.getMultiplicity());
661 if (scopePropagator == null) {
662 scopePropagator = new ScopePropagator();
663 }
664 scopePropagator.scope(type, interval);
665 }
666
667 private record RelationInfo(PartialRelation partialRelation, MutableSeed<TruthValue> assertions,
668 MutableSeed<TruthValue> defaultAssertions) {
669 public RelationInfo(String name, int arity, TruthValue value, TruthValue defaultValue) {
670 this(new PartialRelation(name, arity), value, defaultValue);
671 }
672
673 public RelationInfo(PartialRelation partialRelation, TruthValue value, TruthValue defaultValue) {
674 this(partialRelation, MutableSeed.of(partialRelation.arity(), value),
675 MutableSeed.of(partialRelation.arity(), defaultValue));
676 }
677
678 public Seed<TruthValue> toSeed(int nodeCount) {
679 defaultAssertions.overwriteValues(assertions);
680 if (partialRelation.equals(ReasoningAdapter.EQUALS_SYMBOL)) {
681 for (int i = 0; i < nodeCount; i++) {
682 defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE);
683 }
684 defaultAssertions.setAllMissing(TruthValue.FALSE);
685 }
686 return defaultAssertions;
687 }
688 }
103} 689}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java
new file mode 100644
index 00000000..47c89e9b
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java
@@ -0,0 +1,31 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model;
7
8import com.google.inject.Inject;
9import com.google.inject.Singleton;
10import org.eclipse.emf.ecore.EObject;
11import org.eclipse.xtext.naming.IQualifiedNameConverter;
12import org.eclipse.xtext.naming.IQualifiedNameProvider;
13
14import java.util.Optional;
15
16@Singleton
17public class SemanticsUtils {
18 @Inject
19 private IQualifiedNameProvider qualifiedNameProvider;
20
21 @Inject
22 private IQualifiedNameConverter qualifiedNameConverter;
23
24 public Optional<String> getName(EObject eObject) {
25 var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject);
26 if (qualifiedName == null) {
27 return Optional.empty();
28 }
29 return Optional.of(qualifiedNameConverter.toString(qualifiedName));
30 }
31}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java
new file mode 100644
index 00000000..38fd8a67
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java
@@ -0,0 +1,51 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model;
7
8import org.eclipse.emf.ecore.EObject;
9
10public class TracedException extends RuntimeException {
11 private final transient EObject sourceElement;
12
13 public TracedException(EObject sourceElement) {
14 this.sourceElement = sourceElement;
15 }
16
17 public TracedException(EObject sourceElement, String message) {
18 super(message);
19 this.sourceElement = sourceElement;
20 }
21
22 public TracedException(EObject sourceElement, String message, Throwable cause) {
23 super(message, cause);
24 this.sourceElement = sourceElement;
25 }
26
27 public TracedException(EObject sourceElement, Throwable cause) {
28 super(cause);
29 this.sourceElement = sourceElement;
30 }
31
32 public EObject getSourceElement() {
33 return sourceElement;
34 }
35
36 @Override
37 public String getMessage() {
38 var message = super.getMessage();
39 if (message == null) {
40 return "Internal error";
41 }
42 return message;
43 }
44
45 public static TracedException addTrace(EObject sourceElement, Throwable cause) {
46 if (cause instanceof TracedException tracedException && tracedException.sourceElement != null) {
47 return tracedException;
48 }
49 return new TracedException(sourceElement, cause);
50 }
51}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
index c1afecf9..32112e61 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTree.java
@@ -7,10 +7,10 @@ package tools.refinery.language.semantics.model.internal;
7 7
8import org.eclipse.collections.api.factory.primitive.IntObjectMaps; 8import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
9import tools.refinery.store.map.Cursor; 9import tools.refinery.store.map.Cursor;
10import tools.refinery.store.tuple.Tuple;
11import tools.refinery.store.representation.TruthValue; 10import tools.refinery.store.representation.TruthValue;
11import tools.refinery.store.tuple.Tuple;
12 12
13public class DecisionTree { 13class DecisionTree implements MutableSeed<TruthValue> {
14 private final int levels; 14 private final int levels;
15 15
16 private final DecisionTreeNode root; 16 private final DecisionTreeNode root;
@@ -29,30 +29,53 @@ public class DecisionTree {
29 this(levels, null); 29 this(levels, null);
30 } 30 }
31 31
32 @Override
33 public int arity() {
34 return levels;
35 }
36
37 @Override
38 public Class<TruthValue> valueType() {
39 return TruthValue.class;
40 }
41
42 @Override
43 public TruthValue reducedValue() {
44 return root.getOtherwiseReducedValue().getTruthValue();
45 }
46
47 @Override
32 public TruthValue get(Tuple tuple) { 48 public TruthValue get(Tuple tuple) {
33 return root.getValue(levels - 1, tuple).getTruthValue(); 49 return root.getValue(levels - 1, tuple).getTruthValue();
34 } 50 }
35 51
52 @Override
36 public void mergeValue(Tuple tuple, TruthValue truthValue) { 53 public void mergeValue(Tuple tuple, TruthValue truthValue) {
37 if (truthValue != null) { 54 if (truthValue != null) {
38 root.mergeValue(levels - 1, tuple, truthValue); 55 root.mergeValue(levels - 1, tuple, truthValue);
39 } 56 }
40 } 57 }
41 58
59 @Override
42 public void setIfMissing(Tuple tuple, TruthValue truthValue) { 60 public void setIfMissing(Tuple tuple, TruthValue truthValue) {
43 if (truthValue != null) { 61 if (truthValue != null) {
44 root.setIfMissing(levels - 1, tuple, truthValue); 62 root.setIfMissing(levels - 1, tuple, truthValue);
45 } 63 }
46 } 64 }
47 65
66 @Override
48 public void setAllMissing(TruthValue truthValue) { 67 public void setAllMissing(TruthValue truthValue) {
49 if (truthValue != null) { 68 if (truthValue != null) {
50 root.setAllMissing(truthValue); 69 root.setAllMissing(truthValue);
51 } 70 }
52 } 71 }
53 72
54 public void overwriteValues(DecisionTree values) { 73 @Override
55 root.overwriteValues(values.root); 74 public void overwriteValues(MutableSeed<TruthValue> values) {
75 if (!(values instanceof DecisionTree decisionTree)) {
76 throw new IllegalArgumentException("Incompatible overwrite: " + values);
77 }
78 root.overwriteValues(decisionTree.root);
56 } 79 }
57 80
58 public TruthValue getReducedValue() { 81 public TruthValue getReducedValue() {
@@ -60,6 +83,7 @@ public class DecisionTree {
60 return reducedValue == null ? null : reducedValue.getTruthValue(); 83 return reducedValue == null ? null : reducedValue.getTruthValue();
61 } 84 }
62 85
86 @Override
63 public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) { 87 public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) {
64 return new DecisionTreeCursor(levels, defaultValue, nodeCount, root); 88 return new DecisionTreeCursor(levels, defaultValue, nodeCount, root);
65 } 89 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
index 9a1e15a3..a9fc644a 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/DecisionTreeCursor.java
@@ -67,6 +67,15 @@ class DecisionTreeCursor implements Cursor<Tuple, TruthValue> {
67 67
68 @Override 68 @Override
69 public boolean move() { 69 public boolean move() {
70 while (moveOne()) {
71 if (!value.equals(defaultValue)) {
72 return true;
73 }
74 }
75 return false;
76 }
77
78 private boolean moveOne() {
70 boolean found = false; 79 boolean found = false;
71 if (path.isEmpty() && !terminated) { 80 if (path.isEmpty() && !terminated) {
72 found = root.moveNext(levels - 1, this); 81 found = root.moveNext(levels - 1, this);
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java
new file mode 100644
index 00000000..99019e2a
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/MutableSeed.java
@@ -0,0 +1,28 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model.internal;
7
8import tools.refinery.store.reasoning.seed.Seed;
9import tools.refinery.store.representation.TruthValue;
10import tools.refinery.store.tuple.Tuple;
11
12public interface MutableSeed<T> extends Seed<T> {
13 void mergeValue(Tuple tuple, T value);
14
15 void setIfMissing(Tuple tuple, T value);
16
17 void setAllMissing(T value);
18
19 void overwriteValues(MutableSeed<T> other);
20
21 static MutableSeed<TruthValue> of(int levels, TruthValue initialValue) {
22 if (levels == 0) {
23 return new NullaryMutableSeed(initialValue);
24 } else {
25 return new DecisionTree(levels, initialValue);
26 }
27 }
28}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java
new file mode 100644
index 00000000..80644b1f
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/internal/NullaryMutableSeed.java
@@ -0,0 +1,83 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model.internal;
7
8import tools.refinery.store.map.Cursor;
9import tools.refinery.store.map.Cursors;
10import tools.refinery.store.representation.TruthValue;
11import tools.refinery.store.tuple.Tuple;
12
13class NullaryMutableSeed implements MutableSeed<TruthValue> {
14 private DecisionTreeValue value;
15
16 public NullaryMutableSeed(TruthValue reducedValue) {
17
18 value = DecisionTreeValue.fromTruthValue(reducedValue);
19 }
20
21 @Override
22 public int arity() {
23 return 0;
24 }
25
26 @Override
27 public Class<TruthValue> valueType() {
28 return TruthValue.class;
29 }
30
31 @Override
32 public TruthValue reducedValue() {
33 return value.getTruthValue();
34 }
35
36 @Override
37 public TruthValue get(Tuple key) {
38 validateKey(key);
39 return reducedValue();
40 }
41
42 private static void validateKey(Tuple key) {
43 if (key.getSize() > 0) {
44 throw new IllegalArgumentException("Invalid key: " + key);
45 }
46 }
47
48 @Override
49 public Cursor<Tuple, TruthValue> getCursor(TruthValue defaultValue, int nodeCount) {
50 if (value == DecisionTreeValue.UNSET || value.getTruthValue() == defaultValue) {
51 return Cursors.empty();
52 }
53 return Cursors.singleton(Tuple.of(), value.getTruthValue());
54 }
55
56 @Override
57 public void mergeValue(Tuple tuple, TruthValue value) {
58 this.value = DecisionTreeValue.fromTruthValue(this.value.merge(value));
59 }
60
61 @Override
62 public void setIfMissing(Tuple tuple, TruthValue value) {
63 validateKey(tuple);
64 setAllMissing(value);
65 }
66
67 @Override
68 public void setAllMissing(TruthValue value) {
69 if (this.value == DecisionTreeValue.UNSET) {
70 this.value = DecisionTreeValue.fromTruthValue(value);
71 }
72 }
73
74 @Override
75 public void overwriteValues(MutableSeed<TruthValue> other) {
76 if (!(other instanceof NullaryMutableSeed nullaryMutableSeed)) {
77 throw new IllegalArgumentException("Incompatible overwrite: " + other);
78 }
79 if (nullaryMutableSeed.value != DecisionTreeValue.UNSET) {
80 value = nullaryMutableSeed.value;
81 }
82 }
83}
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java
new file mode 100644
index 00000000..eee2c4ae
--- /dev/null
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java
@@ -0,0 +1,79 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model;
7
8import org.junit.jupiter.api.Test;
9import tools.refinery.store.dse.propagation.PropagationAdapter;
10import tools.refinery.store.dse.propagation.PropagationResult;
11import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
12import tools.refinery.store.model.ModelStore;
13import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
14import tools.refinery.store.reasoning.ReasoningAdapter;
15import tools.refinery.store.reasoning.ReasoningStoreAdapter;
16import tools.refinery.store.reasoning.representation.PartialRelation;
17import tools.refinery.store.reasoning.scope.ScopePropagator;
18import tools.refinery.store.reasoning.seed.ModelSeed;
19import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
20import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy;
21import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
22import tools.refinery.store.representation.TruthValue;
23import tools.refinery.store.representation.cardinality.CardinalityIntervals;
24import tools.refinery.store.tuple.Tuple;
25
26import static org.hamcrest.MatcherAssert.assertThat;
27import static org.hamcrest.Matchers.is;
28
29class CountPropagationTest {
30 @Test
31 void countPropagationTest() {
32 var a1 = new PartialRelation("A1", 1);
33 var c1 = new PartialRelation("C1", 1);
34 var c2 = new PartialRelation("C2", 1);
35
36 var typeHierarchy = TypeHierarchy.builder()
37 .type(a1, true)
38 .type(c1, a1)
39 .type(c2, a1)
40 .build();
41
42 var store = ModelStore.builder()
43 .with(ViatraModelQueryAdapter.builder())
44 .with(PropagationAdapter.builder())
45 .with(DesignSpaceExplorationAdapter.builder())
46 .with(ReasoningAdapter.builder())
47 .with(new MultiObjectTranslator())
48 .with(new TypeHierarchyTranslator(typeHierarchy))
49 .with(new ScopePropagator()
50 .scope(a1, CardinalityIntervals.between(1000, 1100))
51 .scope(c1, CardinalityIntervals.between(100, 150)))
52 .build();
53
54 var modelSeed = ModelSeed.builder(4)
55 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
56 .reducedValue(CardinalityIntervals.ONE)
57 .put(Tuple.of(0), CardinalityIntervals.SET)
58 .put(Tuple.of(1), CardinalityIntervals.SET))
59 .seed(a1, builder -> builder.reducedValue(TruthValue.UNKNOWN))
60 .seed(c1, builder -> builder
61 .reducedValue(TruthValue.FALSE)
62 .put(Tuple.of(0), TruthValue.TRUE)
63 .put(Tuple.of(2), TruthValue.TRUE))
64 .seed(c2, builder -> builder
65 .reducedValue(TruthValue.FALSE)
66 .put(Tuple.of(1), TruthValue.TRUE)
67 .put(Tuple.of(3), TruthValue.TRUE))
68 .build();
69
70 var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
71 var initialState = initialModel.commit();
72
73 var model = store.createModelForState(initialState);
74 var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
75 var propagationAdapter = model.getAdapter(PropagationAdapter.class);
76 reasoningAdapter.split(0);
77 assertThat(propagationAdapter.propagate(), is(PropagationResult.UNCHANGED));
78 }
79}
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java
new file mode 100644
index 00000000..d756099c
--- /dev/null
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java
@@ -0,0 +1,339 @@
1/*
2 * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
3 *
4 * SPDX-License-Identifier: EPL-2.0
5 */
6package tools.refinery.language.semantics.model;
7
8import com.google.inject.Inject;
9import org.eclipse.xtext.testing.InjectWith;
10import org.eclipse.xtext.testing.extensions.InjectionExtension;
11import org.junit.jupiter.api.Disabled;
12import org.junit.jupiter.api.Test;
13import org.junit.jupiter.api.extension.ExtendWith;
14import tools.refinery.language.ProblemStandaloneSetup;
15import tools.refinery.language.model.tests.utils.ProblemParseHelper;
16import tools.refinery.language.tests.ProblemInjectorProvider;
17import tools.refinery.store.dse.propagation.PropagationAdapter;
18import tools.refinery.store.dse.strategy.BestFirstStoreManager;
19import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
20import tools.refinery.store.model.ModelStore;
21import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
22import tools.refinery.store.reasoning.ReasoningAdapter;
23import tools.refinery.store.reasoning.ReasoningStoreAdapter;
24import tools.refinery.store.reasoning.literal.Concreteness;
25import tools.refinery.store.reasoning.representation.PartialRelation;
26import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
27import tools.refinery.store.statecoding.StateCoderAdapter;
28import tools.refinery.visualization.ModelVisualizerAdapter;
29import tools.refinery.visualization.internal.FileFormat;
30
31import java.util.LinkedHashMap;
32
33import static org.hamcrest.MatcherAssert.assertThat;
34import static org.hamcrest.Matchers.empty;
35
36@ExtendWith(InjectionExtension.class)
37@InjectWith(ProblemInjectorProvider.class)
38@Disabled("For debugging purposes only")
39class ModelGenerationTest {
40 @Inject
41 private ProblemParseHelper parseHelper;
42
43 @Inject
44 private ModelInitializer modelInitializer;
45
46 @Test
47 void socialNetworkTest() {
48 var parsedProblem = parseHelper.parse("""
49 % Metamodel
50 class Person {
51 contains Post posts opposite author
52 Person friend opposite friend
53 }
54
55 class Post {
56 container Person[0..1] author opposite posts
57 Post replyTo
58 }
59
60 % Constraints
61 error replyToNotFriend(Post x, Post y) <->
62 replyTo(x, y),
63 author(x, xAuthor),
64 author(y, yAuthor),
65 xAuthor != yAuthor,
66 !friend(xAuthor, yAuthor).
67
68 error replyToCycle(Post x) <-> replyTo+(x, x).
69
70 % Instance model
71 !friend(a, b).
72 author(p1, a).
73 author(p2, b).
74
75 !author(Post::new, a).
76
77 % Scope
78 scope Post = 5, Person = 5.
79 """);
80 assertThat(parsedProblem.errors(), empty());
81 var problem = parsedProblem.problem();
82
83 var storeBuilder = ModelStore.builder()
84 .with(ViatraModelQueryAdapter.builder())
85 .with(ModelVisualizerAdapter.builder()
86 .withOutputPath("test_output")
87 .withFormat(FileFormat.DOT)
88 .withFormat(FileFormat.SVG)
89// .saveStates()
90 .saveDesignSpace())
91 .with(PropagationAdapter.builder())
92 .with(StateCoderAdapter.builder())
93 .with(DesignSpaceExplorationAdapter.builder())
94 .with(ReasoningAdapter.builder());
95
96 var modelSeed = modelInitializer.createModel(problem, storeBuilder);
97
98 var store = storeBuilder.build();
99
100 var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
101
102 var initialVersion = initialModel.commit();
103
104 var bestFirst = new BestFirstStoreManager(store, 1);
105 bestFirst.startExploration(initialVersion);
106 var resultStore = bestFirst.getSolutionStore();
107 System.out.println("states size: " + resultStore.getSolutions().size());
108// initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore());
109 }
110
111 @Test
112 void statechartTest() {
113 var parsedProblem = parseHelper.parse("""
114 // Metamodel
115 abstract class CompositeElement {
116 contains Region[] regions
117 }
118
119 class Region {
120 contains Vertex[] vertices opposite region
121 }
122
123 abstract class Vertex {
124 container Region[0..1] region opposite vertices
125 contains Transition[] outgoingTransition opposite source
126 Transition[] incomingTransition opposite target
127 }
128
129 class Transition {
130 container Vertex[0..1] source opposite outgoingTransition
131 Vertex target opposite incomingTransition
132 }
133
134 abstract class Pseudostate extends Vertex.
135
136 abstract class RegularState extends Vertex.
137
138 class Entry extends Pseudostate.
139
140 class Exit extends Pseudostate.
141
142 class Choice extends Pseudostate.
143
144 class FinalState extends RegularState.
145
146 class State extends RegularState, CompositeElement.
147
148 class Statechart extends CompositeElement.
149
150 // Constraints
151
152 /////////
153 // Entry
154 /////////
155
156 pred entryInRegion(Region r, Entry e) <->
157 vertices(r, e).
158
159 error noEntryInRegion(Region r) <->
160 !entryInRegion(r, _).
161
162 error multipleEntryInRegion(Region r) <->
163 entryInRegion(r, e1),
164 entryInRegion(r, e2),
165 e1 != e2.
166
167 error incomingToEntry(Transition t, Entry e) <->
168 target(t, e).
169
170 error noOutgoingTransitionFromEntry(Entry e) <->
171 !source(_, e).
172
173 error multipleTransitionFromEntry(Entry e, Transition t1, Transition t2) <->
174 outgoingTransition(e, t1),
175 outgoingTransition(e, t2),
176 t1 != t2.
177
178 /////////
179 // Exit
180 /////////
181
182 error outgoingFromExit(Transition t, Exit e) <->
183 source(t, e).
184
185 /////////
186 // Final
187 /////////
188
189 error outgoingFromFinal(Transition t, FinalState e) <->
190 source(t, e).
191
192 /////////
193 // State vs Region
194 /////////
195
196 pred stateInRegion(Region r, State s) <->
197 vertices(r, s).
198
199 error noStateInRegion(Region r) <->
200 !stateInRegion(r, _).
201
202 /////////
203 // Choice
204 /////////
205
206 error choiceHasNoOutgoing(Choice c) <->
207 !source(_, c).
208
209 error choiceHasNoIncoming(Choice c) <->
210 !target(_, c).
211
212 scope node = 200..210, Region = 10..*, Choice = 1..*, Statechart = 1.
213 """);
214 assertThat(parsedProblem.errors(), empty());
215 var problem = parsedProblem.problem();
216
217 var storeBuilder = ModelStore.builder()
218 .with(ViatraModelQueryAdapter.builder())
219// .with(ModelVisualizerAdapter.builder()
220// .withOutputPath("test_output")
221// .withFormat(FileFormat.DOT)
222// .withFormat(FileFormat.SVG)
223// .saveStates()
224// .saveDesignSpace())
225 .with(PropagationAdapter.builder())
226 .with(StateCoderAdapter.builder())
227 .with(DesignSpaceExplorationAdapter.builder())
228 .with(ReasoningAdapter.builder());
229
230 var modelSeed = modelInitializer.createModel(problem, storeBuilder);
231
232 var store = storeBuilder.build();
233
234 var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
235
236 var initialVersion = initialModel.commit();
237
238 var bestFirst = new BestFirstStoreManager(store, 1);
239 bestFirst.startExploration(initialVersion);
240 var resultStore = bestFirst.getSolutionStore();
241 System.out.println("states size: " + resultStore.getSolutions().size());
242
243 var model = store.createModelForState(resultStore.getSolutions().get(0).version());
244 var interpretation = model.getAdapter(ReasoningAdapter.class)
245 .getPartialInterpretation(Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL);
246 var cursor = interpretation.getAll();
247 int max = -1;
248 var types = new LinkedHashMap<PartialRelation, Integer>();
249 var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL);
250 while (cursor.move()) {
251 max = Math.max(max, cursor.getKey().get(0));
252 var type = typeInterpretation.get(cursor.getKey());
253 if (type != null) {
254 types.compute(type.candidateType(), (ignoredKey, oldValue) -> oldValue == null ? 1 : oldValue + 1);
255 }
256 }
257 System.out.println("Model size: " + (max + 1));
258 System.out.println(types);
259// initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore());
260 }
261
262 @Test
263 void filesystemTest() {
264 var parsedProblem = parseHelper.parse("""
265 class Filesystem {
266 contains Entry root
267 }
268
269 abstract class Entry.
270
271 class Directory extends Entry {
272 contains Entry[] entries
273 }
274
275 class File extends Entry.
276
277 Filesystem(fs).
278
279 scope Filesystem += 0, Entry = 100.
280 """);
281 assertThat(parsedProblem.errors(), empty());
282 var problem = parsedProblem.problem();
283
284 var storeBuilder = ModelStore.builder()
285 .with(ViatraModelQueryAdapter.builder())
286// .with(ModelVisualizerAdapter.builder()
287// .withOutputPath("test_output")
288// .withFormat(FileFormat.DOT)
289// .withFormat(FileFormat.SVG)
290// .saveStates()
291// .saveDesignSpace())
292 .with(PropagationAdapter.builder())
293 .with(StateCoderAdapter.builder())
294 .with(DesignSpaceExplorationAdapter.builder())
295 .with(ReasoningAdapter.builder());
296
297 var modelSeed = modelInitializer.createModel(problem, storeBuilder);
298
299 var store = storeBuilder.build();
300
301 var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
302
303 var initialVersion = initialModel.commit();
304
305 var bestFirst = new BestFirstStoreManager(store, 1);
306 bestFirst.startExploration(initialVersion);
307 var resultStore = bestFirst.getSolutionStore();
308 System.out.println("states size: " + resultStore.getSolutions().size());
309
310 var model = store.createModelForState(resultStore.getSolutions().get(0).version());
311 var interpretation = model.getAdapter(ReasoningAdapter.class)
312 .getPartialInterpretation(Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL);
313 var cursor = interpretation.getAll();
314 int max = -1;
315 var types = new LinkedHashMap<PartialRelation, Integer>();
316 var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL);
317 while (cursor.move()) {
318 max = Math.max(max, cursor.getKey().get(0));
319 var type = typeInterpretation.get(cursor.getKey());
320 if (type != null) {
321 types.compute(type.candidateType(), (ignoredKey, oldValue) -> oldValue == null ? 1 : oldValue + 1);
322 }
323 }
324 System.out.println("Model size: " + (max + 1));
325 System.out.println(types);
326// initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore());
327 }
328
329 public static void main(String[] args) {
330 ProblemStandaloneSetup.doSetup();
331 var injector = new ProblemStandaloneSetup().createInjectorAndDoEMFRegistration();
332 var test = injector.getInstance(ModelGenerationTest.class);
333 try {
334 test.statechartTest();
335 } catch (Throwable e) {
336 e.printStackTrace();
337 }
338 }
339}
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/tests/DecisionTreeTests.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/internal/DecisionTreeTests.java
index b3fcbabb..5d039308 100644
--- a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/tests/DecisionTreeTests.java
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/internal/DecisionTreeTests.java
@@ -3,10 +3,9 @@
3 * 3 *
4 * SPDX-License-Identifier: EPL-2.0 4 * SPDX-License-Identifier: EPL-2.0
5 */ 5 */
6package tools.refinery.language.semantics.model.tests; 6package tools.refinery.language.semantics.model.internal;
7 7
8import org.junit.jupiter.api.Test; 8import org.junit.jupiter.api.Test;
9import tools.refinery.language.semantics.model.internal.DecisionTree;
10import tools.refinery.store.representation.TruthValue; 9import tools.refinery.store.representation.TruthValue;
11import tools.refinery.store.tuple.Tuple; 10import tools.refinery.store.tuple.Tuple;
12 11
@@ -134,6 +133,17 @@ class DecisionTreeTests {
134 } 133 }
135 134
136 @Test 135 @Test
136 void overwriteIterationTest() {
137 var sut = new DecisionTree(1, TruthValue.TRUE);
138 var overwrite = new DecisionTree(1, null);
139 overwrite.mergeValue(Tuple.of(0), TruthValue.UNKNOWN);
140 sut.overwriteValues(overwrite);
141 var map = iterateAll(sut, TruthValue.UNKNOWN, 2);
142 assertThat(map.keySet(), hasSize(1));
143 assertThat(map, hasEntry(Tuple.of(1), TruthValue.TRUE));
144 }
145
146 @Test
137 void overwriteNothingTest() { 147 void overwriteNothingTest() {
138 var sut = new DecisionTree(2, TruthValue.UNKNOWN); 148 var sut = new DecisionTree(2, TruthValue.UNKNOWN);
139 var values = new DecisionTree(2, null); 149 var values = new DecisionTree(2, null);
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-27 19:56:29 +0000