From eb5da232b5954895b449957c73e35d0b36e3a902 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 17 Aug 2023 02:32:26 +0200 Subject: feat: basic semantics mapping and visualization --- subprojects/language-semantics/build.gradle.kts | 2 + .../language/semantics/model/ModelInitializer.java | 337 ++++++++++++++++++--- .../language/semantics/model/SemanticsUtils.java | 31 ++ .../semantics/model/internal/DecisionTree.java | 20 +- .../model/internal/DecisionTreeCursor.java | 9 + .../semantics/model/tests/DecisionTreeTests.java | 11 + 6 files changed, 368 insertions(+), 42 deletions(-) create mode 100644 subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/SemanticsUtils.java (limited to 'subprojects/language-semantics') diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts index 38cd9e0d..23668f30 100644 --- a/subprojects/language-semantics/build.gradle.kts +++ b/subprojects/language-semantics/build.gradle.kts @@ -13,5 +13,7 @@ dependencies { implementation(libs.eclipseCollections.api) api(project(":refinery-language")) api(project(":refinery-store")) + api(project(":refinery-store-query")) + api(project(":refinery-store-reasoning")) testImplementation(testFixtures(project(":refinery-language"))) } 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 fe67ed2c..93c7c8e5 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,66 +9,298 @@ import com.google.inject.Inject; import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; import tools.refinery.language.model.problem.*; +import tools.refinery.language.semantics.model.internal.DecisionTree; +import tools.refinery.language.utils.BuiltinSymbols; import tools.refinery.language.utils.ProblemDesugarer; -import tools.refinery.store.representation.Symbol; +import tools.refinery.language.utils.ProblemUtil; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.seed.ModelSeed; +import tools.refinery.store.reasoning.seed.Seed; +import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; +import tools.refinery.store.reasoning.translator.metamodel.Metamodel; +import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder; +import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity; +import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; +import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity; import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.cardinality.CardinalityInterval; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +import tools.refinery.store.representation.cardinality.UpperCardinalities; import tools.refinery.store.tuple.Tuple; -import java.util.HashMap; +import java.util.ArrayList; +import java.util.LinkedHashMap; import java.util.Map; public class ModelInitializer { @Inject private ProblemDesugarer desugarer; + @Inject + private SemanticsUtils semanticsUtils; + + private Problem problem; + + private BuiltinSymbols builtinSymbols; + + private PartialRelation nodeRelation; + private final MutableObjectIntMap nodeTrace = ObjectIntMaps.mutable.empty(); - private final Map> relationTrace = - new HashMap<>(); + private final Map relationInfoMap = new LinkedHashMap<>(); - private int nodeCount = 0; + private Map relationTrace; + + private final MetamodelBuilder metamodelBuilder = Metamodel.builder(); + + public int getNodeCount() { + return nodeTrace.size(); + } + + public MutableObjectIntMap getNodeTrace() { + return nodeTrace; + } - /*public void createModel(Problem problem) { - var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( + public Map getRelationTrace() { + return relationTrace; + } + + public ModelSeed createModel(Problem problem, ModelStoreBuilder builder) { + this.problem = problem; + builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( "Problem has no builtin library")); - var collectedSymbols = desugarer.collectSymbols(problem); - for (var node : collectedSymbols.nodes().keySet()) { - nodeTrace.put(node, nodeCount); - nodeCount += 1; - } - for (var pair : collectedSymbols.relations().entrySet()) { - var relation = pair.getKey(); - var relationInfo = pair.getValue(); - var isEqualsRelation = relation == builtinSymbols.equals(); - var decisionTree = mergeAssertions(relationInfo, isEqualsRelation); - var defaultValue = isEqualsRelation ? TruthValue.FALSE : TruthValue.UNKNOWN; - relationTrace.put(relation, Symbol.of( - relationInfo.name(), relationInfo.arity(), TruthValue.class, defaultValue)); - } - } - - private DecisionTree mergeAssertions(RelationInfo relationInfo, boolean isEqualsRelation) { - var arity = relationInfo.arity(); - var defaultAssertions = new DecisionTree(arity, isEqualsRelation ? null : TruthValue.UNKNOWN); - var assertions = new DecisionTree(arity); - for (var assertion : relationInfo.assertions()) { - var tuple = getTuple(assertion); - var value = getTruthValue(assertion.getValue()); - if (assertion.isDefault()) { - defaultAssertions.mergeValue(tuple, value); + var nodeInfo = collectPartialRelation(builtinSymbols.node(), 1, TruthValue.TRUE, TruthValue.TRUE); + nodeRelation = nodeInfo.partialRelation(); + metamodelBuilder.type(nodeRelation, true); + relationInfoMap.put(builtinSymbols.exists(), new RelationInfo(ReasoningAdapter.EXISTS_SYMBOL, null, + TruthValue.TRUE)); + relationInfoMap.put(builtinSymbols.equals(), new RelationInfo(ReasoningAdapter.EQUALS_SYMBOL, (TruthValue) null, + null)); + relationInfoMap.put(builtinSymbols.contained(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, + null, TruthValue.UNKNOWN)); + relationInfoMap.put(builtinSymbols.contains(), new RelationInfo(ContainmentHierarchyTranslator.CONTAINS_SYMBOL, + null, TruthValue.UNKNOWN)); + relationInfoMap.put(builtinSymbols.invalidNumberOfContainers(), + new RelationInfo(ContainmentHierarchyTranslator.INVALID_NUMBER_OF_CONTAINERS, TruthValue.FALSE, + TruthValue.FALSE)); + collectNodes(); + collectPartialSymbols(); + collectAssertions(); + var metamodel = metamodelBuilder.build(); + builder.with(ReasoningAdapter.builder()); + builder.with(new MultiObjectTranslator()); + builder.with(new MetamodelTranslator(metamodel)); + relationTrace = new LinkedHashMap<>(relationInfoMap.size()); + int nodeCount = getNodeCount(); + var modelSeedBuilder = ModelSeed.builder(nodeCount); + for (var entry : relationInfoMap.entrySet()) { + var relation = entry.getKey(); + var info = entry.getValue(); + var partialRelation = info.partialRelation(); + relationTrace.put(relation, partialRelation); + modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); + } + return modelSeedBuilder.build(); + } + + private void collectNodes() { + for (var statement : problem.getStatements()) { + if (statement instanceof IndividualDeclaration individualDeclaration) { + for (var individual : individualDeclaration.getNodes()) { + collectNode(individual); + } + } else if (statement instanceof ClassDeclaration classDeclaration) { + var newNode = classDeclaration.getNewNode(); + if (newNode != null) { + collectNode(newNode); + } + } else if (statement instanceof EnumDeclaration enumDeclaration) { + for (var literal : enumDeclaration.getLiterals()) { + collectNode(literal); + } + } + } + for (var node : problem.getNodes()) { + collectNode(node); + } + } + + private void collectNode(Node node) { + nodeTrace.getIfAbsentPut(node, this::getNodeCount); + } + + private void collectPartialSymbols() { + for (var statement : problem.getStatements()) { + if (statement instanceof ClassDeclaration classDeclaration) { + collectClassDeclaration(classDeclaration); + } else if (statement instanceof EnumDeclaration enumDeclaration) { + collectPartialRelation(enumDeclaration, 1, null, TruthValue.FALSE); + } else if (statement instanceof PredicateDefinition predicateDefinition) { + // TODO Implement predicate definitions + } + } + } + + private void collectClassDeclaration(ClassDeclaration classDeclaration) { + collectPartialRelation(classDeclaration, 1, null, TruthValue.UNKNOWN); + for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { + if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { + collectPartialRelation(referenceDeclaration, 2, null, TruthValue.UNKNOWN); + var invalidMultiplicityConstraint = referenceDeclaration.getInvalidMultiplicity(); + if (invalidMultiplicityConstraint != null) { + collectPartialRelation(invalidMultiplicityConstraint, 1, TruthValue.FALSE, TruthValue.FALSE); + } } else { - assertions.mergeValue(tuple, value); + throw new IllegalArgumentException("Unknown feature declaration: " + featureDeclaration); + } + } + } + + private RelationInfo collectPartialRelation(Relation relation, int arity, TruthValue value, + TruthValue defaultValue) { + return relationInfoMap.computeIfAbsent(relation, key -> { + var name = getName(relation); + return new RelationInfo(name, arity, value, defaultValue); + }); + } + + private String getName(Relation relation) { + return semanticsUtils.getName(relation).orElseGet(() -> "#" + relationInfoMap.size()); + } + + private void collectAssertions() { + for (var statement : problem.getStatements()) { + if (statement instanceof ClassDeclaration classDeclaration) { + collectClassDeclarationAssertions(classDeclaration); + } else if (statement instanceof EnumDeclaration enumDeclaration) { + collectEnumAssertions(enumDeclaration); + } else if (statement instanceof IndividualDeclaration individualDeclaration) { + for (var individual : individualDeclaration.getNodes()) { + collectIndividualAssertions(individual); + } + } else if (statement instanceof Assertion assertion) { + collectAssertion(assertion); } } - defaultAssertions.overwriteValues(assertions); - if (isEqualsRelation) { - for (int i = 0; i < nodeCount; i++) { - defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE); + } + + private void collectClassDeclarationAssertions(ClassDeclaration classDeclaration) { + var superTypes = classDeclaration.getSuperTypes(); + var partialSuperTypes = new ArrayList(superTypes.size() + 1); + partialSuperTypes.add(nodeRelation); + for (var superType : superTypes) { + partialSuperTypes.add(getRelationInfo(superType).partialRelation()); + } + var info = getRelationInfo(classDeclaration); + metamodelBuilder.type(info.partialRelation(), classDeclaration.isAbstract(), + partialSuperTypes); + var newNode = classDeclaration.getNewNode(); + if (newNode != null) { + var newNodeId = getNodeId(newNode); + collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN); + mergeValue(classDeclaration, Tuple.of(newNodeId), TruthValue.TRUE); + } + for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { + if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { + collectReferenceDeclarationAssertions(classDeclaration, referenceDeclaration); + } else { + throw new IllegalArgumentException("Unknown feature declaration: " + featureDeclaration); } - defaultAssertions.setAllMissing(TruthValue.FALSE); } - return defaultAssertions; - }*/ + } + + private void collectReferenceDeclarationAssertions(ClassDeclaration classDeclaration, + ReferenceDeclaration referenceDeclaration) { + var relation = getRelationInfo(referenceDeclaration).partialRelation(); + var source = getRelationInfo(classDeclaration).partialRelation(); + var target = getRelationInfo(referenceDeclaration.getReferenceType()).partialRelation(); + boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT; + var opposite = referenceDeclaration.getOpposite(); + PartialRelation oppositeRelation = null; + if (opposite != null) { + oppositeRelation = getRelationInfo(opposite).partialRelation(); + } + var multiplicity = getMultiplicityConstraint(referenceDeclaration); + metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation); + } + + private Multiplicity getMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) { + if (!ProblemUtil.hasMultiplicityConstraint(referenceDeclaration)) { + return UnconstrainedMultiplicity.INSTANCE; + } + var problemMultiplicity = referenceDeclaration.getMultiplicity(); + CardinalityInterval interval; + if (problemMultiplicity == null) { + interval = CardinalityIntervals.LONE; + } else if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) { + interval = CardinalityIntervals.exactly(exactMultiplicity.getExactValue()); + } else if (problemMultiplicity instanceof RangeMultiplicity rangeMultiplicity) { + var upperBound = rangeMultiplicity.getUpperBound(); + interval = CardinalityIntervals.between(rangeMultiplicity.getLowerBound(), + upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound)); + } else { + throw new IllegalArgumentException("Unknown multiplicity: " + problemMultiplicity); + } + var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation(); + return ConstrainedMultiplicity.of(interval, constraint); + } + + private void collectEnumAssertions(EnumDeclaration enumDeclaration) { + var info = getRelationInfo(enumDeclaration); + metamodelBuilder.type(info.partialRelation(), nodeRelation); + var overlay = new DecisionTree(1, null); + for (var literal : enumDeclaration.getLiterals()) { + collectIndividualAssertions(literal); + var nodeId = getNodeId(literal); + overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE); + } + info.assertions().overwriteValues(overlay); + } + + private void collectIndividualAssertions(Node node) { + var nodeId = getNodeId(node); + collectCardinalityAssertions(nodeId, TruthValue.TRUE); + } + + private void collectCardinalityAssertions(int nodeId, TruthValue value) { + mergeValue(builtinSymbols.exists(), Tuple.of(nodeId), value); + mergeValue(builtinSymbols.equals(), Tuple.of(nodeId, nodeId), value); + } + + private void collectAssertion(Assertion assertion) { + var relation = assertion.getRelation(); + var tuple = getTuple(assertion); + var value = getTruthValue(assertion.getValue()); + if (assertion.isDefault()) { + mergeDefaultValue(relation, tuple, value); + } else { + mergeValue(relation, tuple, value); + } + } + + private void mergeValue(Relation relation, Tuple key, TruthValue value) { + getRelationInfo(relation).assertions().mergeValue(key, value); + } + + private void mergeDefaultValue(Relation relation, Tuple key, TruthValue value) { + getRelationInfo(relation).defaultAssertions().mergeValue(key, value); + } + + private RelationInfo getRelationInfo(Relation relation) { + var info = relationInfoMap.get(relation); + if (info == null) { + throw new IllegalArgumentException("Unknown relation: " + relation); + } + return info; + } + + private int getNodeId(Node node) { + return nodeTrace.getOrThrow(node); + } private Tuple getTuple(Assertion assertion) { var arguments = assertion.getArguments(); @@ -77,7 +309,7 @@ public class ModelInitializer { for (int i = 0; i < arity; i++) { var argument = arguments.get(i); if (argument instanceof NodeAssertionArgument nodeArgument) { - nodes[i] = nodeTrace.getOrThrow(nodeArgument.getNode()); + nodes[i] = getNodeId(nodeArgument.getNode()); } else if (argument instanceof WildcardAssertionArgument) { nodes[i] = -1; } else { @@ -98,4 +330,27 @@ public class ModelInitializer { case ERROR -> TruthValue.ERROR; }; } + + private record RelationInfo(PartialRelation partialRelation, DecisionTree assertions, + DecisionTree defaultAssertions) { + public RelationInfo(String name, int arity, TruthValue value, TruthValue defaultValue) { + this(new PartialRelation(name, arity), value, defaultValue); + } + + public RelationInfo(PartialRelation partialRelation, TruthValue value, TruthValue defaultValue) { + this(partialRelation, new DecisionTree(partialRelation.arity(), value), + new DecisionTree(partialRelation.arity(), defaultValue)); + } + + public Seed toSeed(int nodeCount) { + defaultAssertions.overwriteValues(assertions); + if (partialRelation.equals(ReasoningAdapter.EQUALS_SYMBOL)) { + for (int i = 0; i < nodeCount; i++) { + defaultAssertions.setIfMissing(Tuple.of(i, i), TruthValue.TRUE); + } + defaultAssertions.setAllMissing(TruthValue.FALSE); + } + return defaultAssertions; + } + } } 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.model; + +import com.google.inject.Inject; +import com.google.inject.Singleton; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.xtext.naming.IQualifiedNameConverter; +import org.eclipse.xtext.naming.IQualifiedNameProvider; + +import java.util.Optional; + +@Singleton +public class SemanticsUtils { + @Inject + private IQualifiedNameProvider qualifiedNameProvider; + + @Inject + private IQualifiedNameConverter qualifiedNameConverter; + + public Optional getName(EObject eObject) { + var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject); + if (qualifiedName == null) { + return Optional.empty(); + } + return Optional.of(qualifiedNameConverter.toString(qualifiedName)); + } +} 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..d693dec3 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,11 @@ package tools.refinery.language.semantics.model.internal; import org.eclipse.collections.api.factory.primitive.IntObjectMaps; import tools.refinery.store.map.Cursor; +import tools.refinery.store.reasoning.seed.Seed; import tools.refinery.store.tuple.Tuple; import tools.refinery.store.representation.TruthValue; -public class DecisionTree { +public class DecisionTree implements Seed { private final int levels; private final DecisionTreeNode root; @@ -29,6 +30,22 @@ public class DecisionTree { this(levels, null); } + @Override + public int arity() { + return levels; + } + + @Override + public Class valueType() { + return TruthValue.class; + } + + @Override + public TruthValue reducedValue() { + return root.getReducedValue().getTruthValue(); + } + + @Override public TruthValue get(Tuple tuple) { return root.getValue(levels - 1, tuple).getTruthValue(); } @@ -60,6 +77,7 @@ public class DecisionTree { return reducedValue == null ? null : reducedValue.getTruthValue(); } + @Override public Cursor getCursor(TruthValue defaultValue, int nodeCount) { return new DecisionTreeCursor(levels, defaultValue, nodeCount, root); } 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 { @Override public boolean move() { + while (moveOne()) { + if (!value.equals(defaultValue)) { + return true; + } + } + return false; + } + + private boolean moveOne() { boolean found = false; if (path.isEmpty() && !terminated) { found = root.moveNext(levels - 1, this); 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/tests/DecisionTreeTests.java index b3fcbabb..3c43d3bd 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/tests/DecisionTreeTests.java @@ -133,6 +133,17 @@ class DecisionTreeTests { assertThat(map, hasEntry(Tuple.of(1, 1), TruthValue.FALSE)); } + @Test + void overwriteIterationTest() { + var sut = new DecisionTree(1, TruthValue.TRUE); + var overwrite = new DecisionTree(1, null); + overwrite.mergeValue(Tuple.of(0), TruthValue.UNKNOWN); + sut.overwriteValues(overwrite); + var map = iterateAll(sut, TruthValue.UNKNOWN, 2); + assertThat(map.keySet(), hasSize(1)); + assertThat(map, hasEntry(Tuple.of(1), TruthValue.TRUE)); + } + @Test void overwriteNothingTest() { var sut = new DecisionTree(2, TruthValue.UNKNOWN); -- cgit v1.2.3-70-g09d2