feat: improve semantics error reporting

Also makes model seeds cancellable to reduce server load during semantic
analysis.

9 files changed, 196 insertions, 28 deletions

diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/CancellableSeed.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/CancellableSeed.java
new file mode 100644
index 00000000..aa14f39d
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/CancellableSeed.java
@@ -0,0 +1,99 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.semantics;
+
+import tools.refinery.store.map.AnyVersionedMap;
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.reasoning.seed.Seed;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.viatra.runtime.CancellationToken;
+
+import java.util.Set;
+
+class CancellableSeed<T> implements Seed<T> {
+        private final CancellationToken cancellationToken;
+        private final Seed<T> seed;
+
+        private CancellableSeed(CancellationToken cancellationToken, Seed<T> seed) {
+                this.cancellationToken = cancellationToken;
+                this.seed = seed;
+        }
+
+        @Override
+        public int arity() {
+                return seed.arity();
+        }
+
+        @Override
+        public Class<T> valueType() {
+                return seed.valueType();
+        }
+
+        @Override
+        public T reducedValue() {
+                return seed.reducedValue();
+        }
+
+        @Override
+        public T get(Tuple key) {
+                return seed.get(key);
+        }
+
+        @Override
+        public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) {
+                return new CancellableCursor<>(cancellationToken, seed.getCursor(defaultValue, nodeCount));
+        }
+
+        public static ModelSeed wrap(CancellationToken cancellationToken, ModelSeed modelSeed) {
+                var builder = ModelSeed.builder(modelSeed.getNodeCount());
+                for (var partialSymbol : modelSeed.getSeededSymbols()) {
+                        wrap(cancellationToken, (PartialSymbol<?, ?>) partialSymbol, modelSeed, builder);
+                }
+                return builder.build();
+        }
+
+        private static <A, C> void wrap(CancellationToken cancellationToken, PartialSymbol<A, C> partialSymbol,
+                                                                        ModelSeed originalModelSeed, ModelSeed.Builder builder) {
+                var originalSeed = originalModelSeed.getSeed(partialSymbol);
+                builder.seed(partialSymbol, new CancellableSeed<>(cancellationToken, originalSeed));
+        }
+
+        private record CancellableCursor<T>(CancellationToken cancellationToken, Cursor<Tuple, T> cursor)
+                        implements Cursor<Tuple, T> {
+                @Override
+                public Tuple getKey() {
+                        return cursor.getKey();
+                }
+
+                @Override
+                public T getValue() {
+                        return cursor.getValue();
+                }
+
+                @Override
+                public boolean isTerminated() {
+                        return cursor.isTerminated();
+                }
+
+                @Override
+                public boolean move() {
+                        cancellationToken.checkCancelled();
+                        return cursor.move();
+                }
+
+                @Override
+                public boolean isDirty() {
+                        return cursor.isDirty();
+                }
+
+                @Override
+                public Set<AnyVersionedMap> getDependingMaps() {
+                        return cursor.getDependingMaps();
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsErrorResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsInternalErrorResult.java
index ce34ef6c..ff592e93 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsErrorResult.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsInternalErrorResult.java
@@ -5,5 +5,5 @@
  */
 package tools.refinery.language.web.semantics;
 
-public record SemanticsErrorResult(String error) implements SemanticsResult {
+public record SemanticsInternalErrorResult(String error) implements SemanticsResult {
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsIssuesResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsIssuesResult.java
new file mode 100644
index 00000000..644bd179
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsIssuesResult.java
@@ -0,0 +1,13 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.semantics;
+
+import org.eclipse.xtext.web.server.validation.ValidationResult;
+
+import java.util.List;
+
+public record SemanticsIssuesResult(List<ValidationResult.Issue> issues) implements SemanticsResult {
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsResult.java
index 92639578..a2e19a2f 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsResult.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsResult.java
@@ -7,5 +7,6 @@ package tools.refinery.language.web.semantics;
 
 import org.eclipse.xtext.web.server.IServiceResult;
 
-public sealed interface SemanticsResult extends IServiceResult permits SemanticsSuccessResult, SemanticsErrorResult {
+public sealed interface SemanticsResult extends IServiceResult permits SemanticsSuccessResult,
+                SemanticsInternalErrorResult, SemanticsIssuesResult {
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java
index 39191162..56b2cbc1 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java
@@ -5,9 +5,11 @@
  */
 package tools.refinery.language.web.semantics;
 
+import com.google.gson.JsonObject;
 import com.google.inject.Inject;
 import com.google.inject.Provider;
 import com.google.inject.Singleton;
+import org.eclipse.xtext.ide.ExecutorServiceProvider;
 import org.eclipse.xtext.service.OperationCanceledManager;
 import org.eclipse.xtext.util.CancelIndicator;
 import org.eclipse.xtext.web.server.model.AbstractCachedService;
@@ -19,6 +21,7 @@ import org.slf4j.LoggerFactory;
 import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.web.xtext.server.push.PushWebDocument;
 
+import java.util.List;
 import java.util.concurrent.*;
 
 @Singleton
@@ -34,7 +37,12 @@ public class SemanticsService extends AbstractCachedService<SemanticsResult> {
         @Inject
         private ValidationService validationService;
 
-        private final ExecutorService executorService = Executors.newCachedThreadPool();
+        private ExecutorService executorService;
+
+        @Inject
+        public void setExecutorServiceProvider(ExecutorServiceProvider provider) {
+                executorService = provider.get(this.getClass().getName());
+        }
 
         @Override
         public SemanticsResult compute(IXtextWebDocument doc, CancelIndicator cancelIndicator) {
@@ -42,12 +50,15 @@ public class SemanticsService extends AbstractCachedService<SemanticsResult> {
                 if (LOG.isTraceEnabled()) {
                         start = System.currentTimeMillis();
                 }
-                var problem = getProblem(doc, cancelIndicator);
-                if (problem == null) {
+                if (hasError(doc, cancelIndicator)) {
                         return null;
                 }
+                var problem = getProblem(doc);
+                if (problem == null) {
+                        return new SemanticsSuccessResult(List.of(), new JsonObject());
+                }
                 var worker = workerProvider.get();
-                worker.setProblem(problem,cancelIndicator);
+                worker.setProblem(problem, cancelIndicator);
                 var future = executorService.submit(worker);
                 SemanticsResult result = null;
                 try {
@@ -58,11 +69,19 @@ public class SemanticsService extends AbstractCachedService<SemanticsResult> {
                         Thread.currentThread().interrupt();
                 } catch (ExecutionException e) {
                         operationCanceledManager.propagateAsErrorIfCancelException(e.getCause());
-                        throw new IllegalStateException(e);
+                        LOG.debug("Error while computing semantics", e);
+                        if (e.getCause() instanceof Error error) {
+                                throw error;
+                        }
+                        String message = e.getMessage();
+                        if (message == null) {
+                                message = "Partial interpretation error";
+                        }
+                        return new SemanticsInternalErrorResult(message);
                 } catch (TimeoutException e) {
                         future.cancel(true);
                         LOG.trace("Semantics service timeout", e);
-                        return new SemanticsErrorResult("Partial interpretation timed out");
+                        return new SemanticsInternalErrorResult("Partial interpretation timed out");
                 }
                 if (LOG.isTraceEnabled()) {
                         long end = System.currentTimeMillis();
@@ -72,17 +91,17 @@ public class SemanticsService extends AbstractCachedService<SemanticsResult> {
                 return result;
         }
 
-        @Nullable
-        private Problem getProblem(IXtextWebDocument doc, CancelIndicator cancelIndicator) {
+        private boolean hasError(IXtextWebDocument doc, CancelIndicator cancelIndicator) {
                 if (!(doc instanceof PushWebDocument pushDoc)) {
                         throw new IllegalArgumentException("Unexpected IXtextWebDocument: " + doc);
                 }
                 var validationResult = pushDoc.getCachedServiceResult(validationService, cancelIndicator, true);
-                boolean hasError = validationResult.getIssues().stream()
+                return validationResult.getIssues().stream()
                                 .anyMatch(issue -> "error".equals(issue.getSeverity()));
-                if (hasError) {
-                        return null;
-                }
+        }
+
+        @Nullable
+        private Problem getProblem(IXtextWebDocument doc) {
                 var contents = doc.getResource().getContents();
                 if (contents.isEmpty()) {
                         return null;
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 25589260..43d0238c 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
@@ -8,13 +8,19 @@ package tools.refinery.language.web.semantics;
 import com.google.gson.JsonArray;
 import com.google.gson.JsonObject;
 import com.google.inject.Inject;
+import org.eclipse.emf.common.util.Diagnostic;
+import org.eclipse.emf.ecore.EObject;
 import org.eclipse.xtext.service.OperationCanceledManager;
 import org.eclipse.xtext.util.CancelIndicator;
-import org.slf4j.Logger;
-import org.slf4j.LoggerFactory;
+import org.eclipse.xtext.validation.CheckType;
+import org.eclipse.xtext.validation.FeatureBasedDiagnostic;
+import org.eclipse.xtext.validation.IDiagnosticConverter;
+import org.eclipse.xtext.validation.Issue;
+import org.eclipse.xtext.web.server.validation.ValidationResult;
 import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.semantics.model.ModelInitializer;
 import tools.refinery.language.semantics.model.SemanticsUtils;
+import tools.refinery.language.semantics.model.TracedException;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
@@ -22,17 +28,19 @@ import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.ReasoningStoreAdapter;
 import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.representation.TruthValue;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.viatra.runtime.CancellationToken;
 
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.List;
 import java.util.TreeMap;
 import java.util.concurrent.Callable;
 
 class SemanticsWorker implements Callable<SemanticsResult> {
-        private static final Logger LOG = LoggerFactory.getLogger(SemanticsWorker.class);
+        private static final String DIAGNOSTIC_ID = "tools.refinery.language.semantics.SemanticError";
 
         @Inject
         private SemanticsUtils semanticsUtils;
@@ -41,6 +49,9 @@ class SemanticsWorker implements Callable<SemanticsResult> {
         private OperationCanceledManager operationCanceledManager;
 
         @Inject
+        private IDiagnosticConverter diagnosticConverter;
+
+        @Inject
         private ModelInitializer initializer;
 
         private Problem problem;
@@ -71,15 +82,17 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                         cancellationToken.checkCancelled();
                         var store = builder.build();
                         cancellationToken.checkCancelled();
-                        var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+                        var cancellableModelSeed = CancellableSeed.wrap(cancellationToken, modelSeed);
+                        var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(cancellableModelSeed);
                         cancellationToken.checkCancelled();
                         var partialInterpretation = getPartialInterpretation(initializer, model);
 
                         return new SemanticsSuccessResult(nodeTrace, partialInterpretation);
-                } catch (RuntimeException e) {
-                        LOG.debug("Error while computing semantics", e);
-                        var message = e.getMessage();
-                        return new SemanticsErrorResult(message == null ? "Partial interpretation error" : e.getMessage());
+                } catch (TracedException e) {
+                        return getTracedErrorResult(e.getSourceElement(), e.getMessage());
+                } catch (TranslationException e) {
+                        var sourceElement = initializer.getInverseTrace(e.getPartialSymbol());
+                        return getTracedErrorResult(sourceElement, e.getMessage());
                 }
         }
 
@@ -130,4 +143,19 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                 json.add(value.toString());
                 return json;
         }
+
+        private SemanticsResult getTracedErrorResult(EObject sourceElement, String message) {
+                if (sourceElement == null || !problem.eResource().equals(sourceElement.eResource())) {
+                        return new SemanticsInternalErrorResult(message);
+                }
+                var diagnostic = new FeatureBasedDiagnostic(Diagnostic.ERROR, message, sourceElement, null, 0,
+                                CheckType.EXPENSIVE, DIAGNOSTIC_ID);
+                var xtextIssues = new ArrayList<Issue>();
+                diagnosticConverter.convertValidatorDiagnostic(diagnostic, xtextIssues::add);
+                var issues = xtextIssues.stream()
+                                .map(issue -> new ValidationResult.Issue(issue.getMessage(), "error", issue.getLineNumber(),
+                                                issue.getColumn(), issue.getOffset(), issue.getLength()))
+                                .toList();
+                return new SemanticsIssuesResult(issues);
+        }
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocument.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocument.java
index 1542c694..2d43fb26 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocument.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocument.java
@@ -53,10 +53,9 @@ public class PushWebDocument extends XtextWebDocument {
         public <T extends IServiceResult> void precomputeServiceResult(AbstractCachedService<T> service, String serviceName,
                         CancelIndicator cancelIndicator, boolean logCacheMiss) {
                 var serviceClass = service.getClass();
-                var previousResult = precomputedServices.get(serviceClass);
                 var result = getCachedServiceResult(service, cancelIndicator, logCacheMiss);
                 precomputedServices.put(serviceClass, result);
-                if (result != null && !result.equals(previousResult)) {
+                if (result != null) {
                         notifyPrecomputationListeners(serviceName, result);
                 }
         }
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/ProblemWebSocketServletIntegrationTest.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/ProblemWebSocketServletIntegrationTest.java
index 99ca5420..889a55cb 100644
--- a/subprojects/language-web/src/test/java/tools/refinery/language/web/ProblemWebSocketServletIntegrationTest.java
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/ProblemWebSocketServletIntegrationTest.java
@@ -93,7 +93,7 @@ class ProblemWebSocketServletIntegrationTest {
                 clientSocket.waitForTestResult();
                 assertThat(clientSocket.getCloseStatusCode(), equalTo(StatusCode.NORMAL));
                 var responses = clientSocket.getResponses();
-                assertThat(responses, hasSize(7));
+                assertThat(responses, hasSize(8));
                 assertThat(responses.get(0), equalTo("{\"id\":\"foo\",\"response\":{\"stateId\":\"-80000000\"}}"));
                 assertThat(responses.get(1), startsWith(
                                 "{\"resource\":\"test.problem\",\"stateId\":\"-80000000\",\"service\":\"highlight\"," +
@@ -108,7 +108,10 @@ class ProblemWebSocketServletIntegrationTest {
                 assertThat(responses.get(5), startsWith(
                                 "{\"resource\":\"test.problem\",\"stateId\":\"-7fffffff\",\"service\":\"highlight\"," +
                                                 "\"push\":{\"regions\":["));
-                assertThat(responses.get(6), startsWith(
+                assertThat(responses.get(6), equalTo(
+                                "{\"resource\":\"test.problem\",\"stateId\":\"-7fffffff\",\"service\":\"validate\"," +
+                                                "\"push\":{\"issues\":[]}}"));
+                assertThat(responses.get(7), startsWith(
                                 "{\"resource\":\"test.problem\",\"stateId\":\"-7fffffff\",\"service\":\"semantics\"," +
                                                 "\"push\":{"));
         }
@@ -130,7 +133,7 @@ class ProblemWebSocketServletIntegrationTest {
                                                         "\"deltaOffset\":\"0\",\"deltaReplaceLength\":\"0\"}}",
                                         Callback.NOOP
                         );
-                        case 7 -> session.close();
+                        case 8 -> session.close();
                         }
                 }
         }
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/xtext/servlet/TransactionExecutorTest.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/xtext/servlet/TransactionExecutorTest.java
index b7142506..22ce1b47 100644
--- a/subprojects/language-web/src/test/java/tools/refinery/language/web/xtext/servlet/TransactionExecutorTest.java
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/xtext/servlet/TransactionExecutorTest.java
@@ -18,6 +18,7 @@ import org.junit.jupiter.api.Test;
 import org.junit.jupiter.api.extension.ExtendWith;
 import org.mockito.ArgumentCaptor;
 import org.mockito.junit.jupiter.MockitoExtension;
+import tools.refinery.language.web.semantics.SemanticsService;
 import tools.refinery.language.web.tests.AwaitTerminationExecutorServiceProvider;
 import tools.refinery.language.web.tests.ProblemWebInjectorProvider;
 import tools.refinery.language.web.xtext.server.ResponseHandler;
@@ -59,11 +60,16 @@ class TransactionExecutorTest {
         @Inject
         private AwaitTerminationExecutorServiceProvider executorServices;
 
+        @Inject
+        private SemanticsService semanticsService;
+
         private TransactionExecutor transactionExecutor;
 
         @BeforeEach
         void beforeEach() {
                 transactionExecutor = new TransactionExecutor(new SimpleSession(), resourceServiceProviderRegistry);
+                // Manually re-create the semantics analysis thread pool if it was disposed by the previous test.
+                semanticsService.setExecutorServiceProvider(executorServices);
         }
 
         @Test
@@ -95,7 +101,7 @@ class TransactionExecutorTest {
                                                 "0")));
 
                 var captor = newCaptor();
-                verify(responseHandler, times(3)).onResponse(captor.capture());
+                verify(responseHandler, times(4)).onResponse(captor.capture());
                 var newStateId = getStateId("bar", captor.getAllValues().get(0));
                 assertHighlightingResponse(newStateId, captor.getAllValues().get(1));
         }