diff options
Diffstat (limited to 'subprojects/language-semantics/src')
21 files changed, 1609 insertions, 50 deletions
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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.emf.ecore.EObject; | ||
10 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | ||
11 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | ||
12 | import org.eclipse.xtext.naming.QualifiedName; | ||
13 | import org.eclipse.xtext.scoping.IScope; | ||
14 | import org.eclipse.xtext.scoping.IScopeProvider; | ||
15 | import tools.refinery.language.model.problem.*; | ||
16 | import tools.refinery.language.semantics.model.ModelInitializer; | ||
17 | import tools.refinery.language.semantics.model.TracedException; | ||
18 | import tools.refinery.language.utils.ProblemUtil; | ||
19 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
20 | |||
21 | import java.util.*; | ||
22 | |||
23 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.metadata; | ||
7 | |||
8 | public 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; | |||
9 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; | 9 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; |
10 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; | 10 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; |
11 | import tools.refinery.language.model.problem.*; | 11 | import tools.refinery.language.model.problem.*; |
12 | import tools.refinery.language.semantics.model.internal.DecisionTree; | 12 | import tools.refinery.language.semantics.model.internal.MutableSeed; |
13 | import tools.refinery.language.utils.BuiltinSymbols; | ||
13 | import tools.refinery.language.utils.ProblemDesugarer; | 14 | import tools.refinery.language.utils.ProblemDesugarer; |
14 | import tools.refinery.language.utils.RelationInfo; | 15 | import tools.refinery.language.utils.ProblemUtil; |
15 | import tools.refinery.store.representation.Symbol; | 16 | import tools.refinery.store.dse.propagation.PropagationBuilder; |
17 | import tools.refinery.store.model.ModelStoreBuilder; | ||
18 | import tools.refinery.store.query.Constraint; | ||
19 | import tools.refinery.store.query.dnf.InvalidClauseException; | ||
20 | import tools.refinery.store.query.dnf.Query; | ||
21 | import tools.refinery.store.query.dnf.RelationalQuery; | ||
22 | import tools.refinery.store.query.literal.*; | ||
23 | import tools.refinery.store.query.term.NodeVariable; | ||
24 | import tools.refinery.store.query.term.Variable; | ||
25 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
26 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
27 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
28 | import tools.refinery.store.reasoning.scope.ScopePropagator; | ||
29 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
30 | import tools.refinery.store.reasoning.seed.Seed; | ||
31 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; | ||
32 | import tools.refinery.store.reasoning.translator.metamodel.Metamodel; | ||
33 | import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder; | ||
34 | import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator; | ||
35 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
36 | import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; | ||
37 | import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; | ||
38 | import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity; | ||
39 | import tools.refinery.store.reasoning.translator.predicate.PredicateTranslator; | ||
16 | import tools.refinery.store.representation.TruthValue; | 40 | import tools.refinery.store.representation.TruthValue; |
41 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
42 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
43 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
17 | import tools.refinery.store.tuple.Tuple; | 44 | import tools.refinery.store.tuple.Tuple; |
18 | 45 | ||
19 | import java.util.HashMap; | 46 | import java.util.*; |
20 | import java.util.Map; | ||
21 | 47 | ||
22 | public class ModelInitializer { | 48 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.model; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import com.google.inject.Singleton; | ||
10 | import org.eclipse.emf.ecore.EObject; | ||
11 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | ||
12 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | ||
13 | |||
14 | import java.util.Optional; | ||
15 | |||
16 | @Singleton | ||
17 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.model; | ||
7 | |||
8 | import org.eclipse.emf.ecore.EObject; | ||
9 | |||
10 | public 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 | ||
8 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; | 8 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; |
9 | import tools.refinery.store.map.Cursor; | 9 | import tools.refinery.store.map.Cursor; |
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | import tools.refinery.store.representation.TruthValue; | 10 | import tools.refinery.store.representation.TruthValue; |
11 | import tools.refinery.store.tuple.Tuple; | ||
12 | 12 | ||
13 | public class DecisionTree { | 13 | class 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 | */ | ||
6 | package tools.refinery.language.semantics.model.internal; | ||
7 | |||
8 | import tools.refinery.store.reasoning.seed.Seed; | ||
9 | import tools.refinery.store.representation.TruthValue; | ||
10 | import tools.refinery.store.tuple.Tuple; | ||
11 | |||
12 | public 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 | */ | ||
6 | package tools.refinery.language.semantics.model.internal; | ||
7 | |||
8 | import tools.refinery.store.map.Cursor; | ||
9 | import tools.refinery.store.map.Cursors; | ||
10 | import tools.refinery.store.representation.TruthValue; | ||
11 | import tools.refinery.store.tuple.Tuple; | ||
12 | |||
13 | class 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 | */ | ||
6 | package tools.refinery.language.semantics.model; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
10 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
11 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | ||
12 | import tools.refinery.store.model.ModelStore; | ||
13 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
14 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
15 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
17 | import tools.refinery.store.reasoning.scope.ScopePropagator; | ||
18 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
19 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
20 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy; | ||
21 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; | ||
22 | import tools.refinery.store.representation.TruthValue; | ||
23 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
24 | import tools.refinery.store.tuple.Tuple; | ||
25 | |||
26 | import static org.hamcrest.MatcherAssert.assertThat; | ||
27 | import static org.hamcrest.Matchers.is; | ||
28 | |||
29 | class 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 | */ | ||
6 | package tools.refinery.language.semantics.model; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.xtext.testing.InjectWith; | ||
10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | ||
11 | import org.junit.jupiter.api.Disabled; | ||
12 | import org.junit.jupiter.api.Test; | ||
13 | import org.junit.jupiter.api.extension.ExtendWith; | ||
14 | import tools.refinery.language.ProblemStandaloneSetup; | ||
15 | import tools.refinery.language.model.tests.utils.ProblemParseHelper; | ||
16 | import tools.refinery.language.tests.ProblemInjectorProvider; | ||
17 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
18 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; | ||
19 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | ||
20 | import tools.refinery.store.model.ModelStore; | ||
21 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
22 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
23 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
24 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
25 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
26 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; | ||
27 | import tools.refinery.store.statecoding.StateCoderAdapter; | ||
28 | import tools.refinery.visualization.ModelVisualizerAdapter; | ||
29 | import tools.refinery.visualization.internal.FileFormat; | ||
30 | |||
31 | import java.util.LinkedHashMap; | ||
32 | |||
33 | import static org.hamcrest.MatcherAssert.assertThat; | ||
34 | import static org.hamcrest.Matchers.empty; | ||
35 | |||
36 | @ExtendWith(InjectionExtension.class) | ||
37 | @InjectWith(ProblemInjectorProvider.class) | ||
38 | @Disabled("For debugging purposes only") | ||
39 | class 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 | */ |
6 | package tools.refinery.language.semantics.model.tests; | 6 | package tools.refinery.language.semantics.model.internal; |
7 | 7 | ||
8 | import org.junit.jupiter.api.Test; | 8 | import org.junit.jupiter.api.Test; |
9 | import tools.refinery.language.semantics.model.internal.DecisionTree; | ||
10 | import tools.refinery.store.representation.TruthValue; | 9 | import tools.refinery.store.representation.TruthValue; |
11 | import tools.refinery.store.tuple.Tuple; | 10 | import 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); |