refactor: matching node names in CLI and web

5 files changed, 121 insertions, 46 deletions

diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/NodeNameProvider.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/NodeNameProvider.java
new file mode 100644
index 00000000..517b8604
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/NodeNameProvider.java
@@ -0,0 +1,62 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics;
+
+import com.google.inject.Inject;
+import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
+import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
+import org.eclipse.xtext.naming.IQualifiedNameConverter;
+import org.eclipse.xtext.naming.QualifiedName;
+import org.eclipse.xtext.scoping.IScopeProvider;
+import tools.refinery.language.model.problem.Node;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.model.problem.ProblemPackage;
+
+import java.util.Locale;
+
+public class NodeNameProvider {
+        @Inject
+        private IQualifiedNameConverter qualifiedNameConverter;
+
+        @Inject
+        private SemanticsUtils semanticsUtils;
+
+        @Inject
+        private IScopeProvider scopeProvider;
+
+        private Problem problem;
+        private final MutableObjectIntMap<String> indexMap = ObjectIntMaps.mutable.empty();
+
+        public void setProblem(Problem problem) {
+                if (this.problem != null) {
+                        throw new IllegalStateException("Problem was already set");
+                }
+                this.problem = problem;
+        }
+
+        public String getNextName(String typeName) {
+                if (problem == null) {
+                        throw new IllegalStateException("Problem was not set");
+                }
+                String namePrefix;
+                if (typeName == null || typeName.isEmpty()) {
+                        namePrefix = "node";
+                } else {
+                        namePrefix = typeName.substring(0, 1).toLowerCase(Locale.ROOT) + typeName.substring(1);
+                }
+                int index = indexMap.getIfAbsent(namePrefix, 0);
+                String nodeName;
+                QualifiedName qualifiedName;
+                var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
+                do {
+                        index++;
+                        nodeName = namePrefix + index;
+                        qualifiedName = qualifiedNameConverter.toQualifiedName(nodeName);
+                } while (semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class) != null);
+                indexMap.put(namePrefix, index);
+                return nodeName;
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
index 57af599e..09ba34fc 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -8,12 +8,9 @@ package tools.refinery.language.semantics;
 import com.google.inject.Inject;
 import com.google.inject.Provider;
 import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
-import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
-import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
 import org.eclipse.emf.common.util.URI;
 import org.eclipse.emf.ecore.util.EcoreUtil;
-import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.IQualifiedNameProvider;
 import org.eclipse.xtext.naming.QualifiedName;
 import org.eclipse.xtext.resource.FileExtensionProvider;
@@ -37,7 +34,6 @@ import tools.refinery.store.tuple.Tuple;
 import java.io.ByteArrayInputStream;
 import java.io.ByteArrayOutputStream;
 import java.io.IOException;
-import java.util.Locale;
 import java.util.Map;
 import java.util.TreeMap;
 import java.util.TreeSet;
@@ -57,9 +53,6 @@ public class SolutionSerializer {
         private IQualifiedNameProvider qualifiedNameProvider;
 
         @Inject
-        private IQualifiedNameConverter qualifiedNameConverter;
-
-        @Inject
         private SemanticsUtils semanticsUtils;
 
         @Inject
@@ -68,6 +61,9 @@ public class SolutionSerializer {
         @Inject
         private ProblemDesugarer desugarer;
 
+        @Inject
+        private NodeNameProvider nameProvider;
+
         private ProblemTrace trace;
         private Model model;
         private ReasoningAdapter reasoningAdapter;
@@ -95,6 +91,7 @@ public class SolutionSerializer {
                 problem = copyProblem(originalProblem, uri);
                 problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement);
                 problem.getNodes().removeIf(this::shouldRemoveNode);
+                nameProvider.setProblem(problem);
                 addExistsAssertions();
                 addClassAssertions();
                 addReferenceAssertions();
@@ -172,11 +169,6 @@ public class SolutionSerializer {
                 return findNode(qualifiedName);
         }
 
-        private Node findNode(String name) {
-                var qualifiedName = qualifiedNameConverter.toQualifiedName(name);
-                return findNode(qualifiedName);
-        }
-
         private Node findNode(QualifiedName qualifiedName) {
                 var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
                 return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class);
@@ -222,19 +214,17 @@ public class SolutionSerializer {
         private void addClassAssertions() {
                 var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream()
                                 .collect(Collectors.toMap(Function.identity(), this::findPartialRelation));
-                var indexMap = ObjectIntMaps.mutable.empty();
                 var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll();
                 while (cursor.move()) {
                         var key = cursor.getKey();
                         var nodeId = key.get(0);
                         if (isExistingNode(nodeId)) {
-                                createNodeAndAssertType(nodeId, cursor.getValue(), types, indexMap);
+                                createNodeAndAssertType(nodeId, cursor.getValue(), types);
                         }
                 }
         }
 
-        private void createNodeAndAssertType(int nodeId, InferredType inferredType, Map<PartialRelation, Relation> types,
-                                                                                 MutableObjectIntMap<Object> indexMap) {
+        private void createNodeAndAssertType(int nodeId, InferredType inferredType, Map<PartialRelation, Relation> types) {
                 var candidateTypeSymbol = inferredType.candidateType();
                 var candidateRelation = types.get(candidateTypeSymbol);
                 if (candidateRelation instanceof EnumDeclaration) {
@@ -243,18 +233,8 @@ public class SolutionSerializer {
                 }
                 Node node = nodes.get(nodeId);
                 if (node == null) {
-                        String typeName = candidateRelation.getName();
-                        if (typeName == null || typeName.isEmpty()) {
-                                typeName = "node";
-                        } else {
-                                typeName = typeName.substring(0, 1).toLowerCase(Locale.ROOT) + typeName.substring(1);
-                        }
-                        int index = indexMap.getIfAbsent(typeName, 0);
-                        String nodeName;
-                        do {
-                                index++;
-                                nodeName = typeName + index;
-                        } while (findNode(nodeName) != null);
+                        var typeName = candidateRelation.getName();
+                        var nodeName = nameProvider.getNextName(typeName);
                         node = ProblemFactory.eINSTANCE.createNode();
                         node.setName(nodeName);
                         problem.getNodes().add(node);
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 <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * 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 <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * 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<SemanticsResult> {
                 }
                 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 <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * 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<NodeNameProvider> 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<NodeMetadata> getNodesMetadata(Model model, boolean preserveNewNodes) {
+        public List<NodeMetadata> 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<String> 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<String> 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);