From a496f9ae10b1c7d0fd0a876f9dae48923075d8b3 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 1 Jan 2024 19:14:51 +0100 Subject: refactor: matching node names in CLI and web --- .../web/generator/ModelGenerationWorker.java | 7 +-- .../language/web/semantics/SemanticsWorker.java | 5 +- .../web/semantics/metadata/MetadataCreator.java | 55 +++++++++++++++++----- 3 files changed, 50 insertions(+), 17 deletions(-) (limited to 'subprojects/language-web/src/main/java') diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java index a3b6ca82..7febce7d 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -17,6 +17,7 @@ import tools.refinery.generator.ValidationErrorsException; import tools.refinery.language.web.semantics.PartialInterpretation2Json; import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider; import tools.refinery.language.web.xtext.server.push.PushWebDocument; +import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.util.CancellationToken; import java.io.IOException; @@ -142,7 +143,7 @@ public class ModelGenerationWorker implements Runnable { } catch (ValidationErrorsException e) { var errors = e.getErrors(); if (errors != null && !errors.isEmpty()) { - return new ModelGenerationErrorResult(uuid, "Validation error: " + errors.get(0).getMessage()); + return new ModelGenerationErrorResult(uuid, "Validation error: " + errors.getFirst().getMessage()); } throw e; } @@ -154,7 +155,7 @@ public class ModelGenerationWorker implements Runnable { notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model")); cancellationToken.checkCancelled(); metadataCreator.setProblemTrace(generator.getProblemTrace()); - var nodesMetadata = metadataCreator.getNodesMetadata(generator.getModel(), false); + var nodesMetadata = metadataCreator.getNodesMetadata(generator.getModel(), Concreteness.CANDIDATE); cancellationToken.checkCancelled(); var relationsMetadata = metadataCreator.getRelationsMetadata(); cancellationToken.checkCancelled(); diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java index 44974869..fed3c8a3 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -20,6 +20,7 @@ import tools.refinery.generator.ModelSemanticsFactory; import tools.refinery.language.model.problem.Problem; import tools.refinery.language.web.semantics.metadata.MetadataCreator; import tools.refinery.language.semantics.TracedException; +import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.translator.TranslationException; import tools.refinery.store.util.CancellationToken; @@ -73,7 +74,7 @@ class SemanticsWorker implements Callable { } cancellationToken.checkCancelled(); metadataCreator.setProblemTrace(semantics.getProblemTrace()); - var nodesMetadata = metadataCreator.getNodesMetadata(semantics.getModel(), true); + var nodesMetadata = metadataCreator.getNodesMetadata(semantics.getModel(), Concreteness.PARTIAL); cancellationToken.checkCancelled(); var relationsMetadata = metadataCreator.getRelationsMetadata(); cancellationToken.checkCancelled(); diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java index 3fbc5d2d..67ef82ce 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java @@ -1,29 +1,36 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.language.web.semantics.metadata; import com.google.inject.Inject; +import com.google.inject.Provider; import org.eclipse.emf.ecore.EObject; import org.eclipse.xtext.naming.IQualifiedNameConverter; import org.eclipse.xtext.naming.IQualifiedNameProvider; import org.eclipse.xtext.naming.QualifiedName; import org.eclipse.xtext.scoping.IScope; import org.eclipse.xtext.scoping.IScopeProvider; +import org.jetbrains.annotations.NotNull; import tools.refinery.language.model.problem.*; +import tools.refinery.language.semantics.NodeNameProvider; import tools.refinery.language.semantics.ProblemTrace; import tools.refinery.language.semantics.TracedException; import tools.refinery.language.utils.ProblemUtil; import tools.refinery.store.model.Model; import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; +import tools.refinery.store.tuple.Tuple; import java.util.ArrayList; import java.util.Collections; import java.util.Comparator; import java.util.List; +import java.util.function.IntFunction; public class MetadataCreator { @Inject @@ -35,10 +42,11 @@ public class MetadataCreator { @Inject private IQualifiedNameConverter qualifiedNameConverter; - private ProblemTrace problemTrace; + @Inject + private Provider nodeNameProviderProvider; + private ProblemTrace problemTrace; private IScope nodeScope; - private IScope relationScope; public void setProblemTrace(ProblemTrace problemTrace) { @@ -51,32 +59,55 @@ public class MetadataCreator { relationScope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION); } - public static String unnamedNode(int nodeId) { - return "::" + nodeId; - } - - public List getNodesMetadata(Model model, boolean preserveNewNodes) { + public List getNodesMetadata(Model model, Concreteness concreteness) { int nodeCount = model.getAdapter(ReasoningAdapter.class).getNodeCount(); var nodeTrace = problemTrace.getNodeTrace(); var nodes = new NodeMetadata[Math.max(nodeTrace.size(), nodeCount)]; + var getName = makeGetName(model, concreteness); + boolean preserveNewNodes = concreteness == Concreteness.PARTIAL; for (var entry : nodeTrace.keyValuesView()) { var node = entry.getOne(); var id = entry.getTwo(); - nodes[id] = getNodeMetadata(id, node, preserveNewNodes); + nodes[id] = getNodeMetadata(id, node, preserveNewNodes, getName); } for (int i = 0; i < nodes.length; i++) { if (nodes[i] == null) { - var nodeName = unnamedNode(i); + var nodeName = getName.apply(i); nodes[i] = new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT); } } return List.of(nodes); } - private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes) { + @NotNull + private IntFunction makeGetName(Model model, Concreteness concreteness) { + var nodeNameProvider = nodeNameProviderProvider.get(); + nodeNameProvider.setProblem(problemTrace.getProblem()); + var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL); + var existsInterpretation = model.getAdapter(ReasoningAdapter.class).getPartialInterpretation(concreteness, + ReasoningAdapter.EXISTS_SYMBOL); + return nodeId -> { + var key = Tuple.of(nodeId); + var inferredType = typeInterpretation.get(key); + if (inferredType == null || inferredType.candidateType() == null) { + return nodeNameProvider.getNextName(null); + } + if (concreteness == Concreteness.CANDIDATE && !existsInterpretation.get(key).may()) { + // Do not increment the node name counter for non-existent nodes in the candidate interpretation. + // While non-existent nodes may appear in the partial interpretation, they are never displayed in the + // candidate interpretation. + return "::" + nodeId; + } + var relation = problemTrace.getRelation(inferredType.candidateType()); + return nodeNameProvider.getNextName(relation.getName()); + }; + } + + private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes, + IntFunction getName) { var kind = getNodeKind(node); if (!preserveNewNodes && kind == NodeKind.NEW) { - var nodeName = unnamedNode(nodeId); + var nodeName = getName.apply(nodeId); return new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT); } var qualifiedName = getQualifiedName(node); -- cgit v1.2.3-54-g00ecf