Merge pull request #39 from kris7t/partial-interpretation

Implement partial interpretation based model generation

37 files changed, 1489 insertions, 97 deletions

diff --git a/subprojects/language-web/build.gradle.kts b/subprojects/language-web/build.gradle.kts
index 562a1bd9..88dccdf3 100644
--- a/subprojects/language-web/build.gradle.kts
+++ b/subprojects/language-web/build.gradle.kts
@@ -17,6 +17,10 @@ val webapp: Configuration by configurations.creating {
 dependencies {
         implementation(project(":refinery-language"))
         implementation(project(":refinery-language-ide"))
+        implementation(project(":refinery-language-semantics"))
+        implementation(project(":refinery-store-query-viatra"))
+        implementation(project(":refinery-store-reasoning-scope"))
+        implementation(libs.gson)
         implementation(libs.jetty.server)
         implementation(libs.jetty.servlet)
         implementation(libs.jetty.websocket.api)
@@ -60,9 +64,18 @@ tasks {
                 classpath(mainRuntimeClasspath)
                 mainClass.set(application.mainClass)
                 standardInput = System.`in`
-                val baseResource = webapp.incoming.artifacts.artifactFiles.first()
-                environment("BASE_RESOURCE", baseResource)
+                environment("REFINERY_BASE_RESOURCE", webapp.singleFile)
                 group = "run"
-                description = "Start a Jetty web server serving the Xtex API and assets."
+                description = "Start a Jetty web server serving the Xtext API and assets."
+        }
+
+        register<JavaExec>("serveBackendOnly") {
+                val mainRuntimeClasspath = sourceSets.main.map { it.runtimeClasspath }
+                dependsOn(mainRuntimeClasspath)
+                classpath(mainRuntimeClasspath)
+                mainClass.set(application.mainClass)
+                standardInput = System.`in`
+                group = "run"
+                description = "Start a Jetty web server serving the Xtext API without assets."
         }
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebModule.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebModule.java
index b0197c01..6a6e0107 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebModule.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebModule.java
@@ -9,11 +9,13 @@
  */
 package tools.refinery.language.web;
 
+import org.eclipse.xtext.ide.ExecutorServiceProvider;
 import org.eclipse.xtext.web.server.XtextServiceDispatcher;
 import org.eclipse.xtext.web.server.model.IWebDocumentProvider;
 import org.eclipse.xtext.web.server.model.XtextWebDocumentAccess;
 import org.eclipse.xtext.web.server.occurrences.OccurrencesService;
 import tools.refinery.language.web.occurrences.ProblemOccurrencesService;
+import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider;
 import tools.refinery.language.web.xtext.server.push.PushServiceDispatcher;
 import tools.refinery.language.web.xtext.server.push.PushWebDocumentAccess;
 import tools.refinery.language.web.xtext.server.push.PushWebDocumentProvider;
@@ -37,4 +39,8 @@ public class ProblemWebModule extends AbstractProblemWebModule {
         public Class<? extends OccurrencesService> bindOccurrencesService() {
                 return ProblemOccurrencesService.class;
         }
+
+        public Class<? extends ExecutorServiceProvider> bindExecutorServiceProvider() {
+                return ThreadPoolExecutorServiceProvider.class;
+        }
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSocketServlet.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSocketServlet.java
index 7b48cde8..e98d115e 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSocketServlet.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSocketServlet.java
@@ -10,8 +10,10 @@ import org.eclipse.xtext.util.DisposableRegistry;
 import jakarta.servlet.ServletException;
 import tools.refinery.language.web.xtext.servlet.XtextWebSocketServlet;
 
-public class ProblemWebSocketServlet extends XtextWebSocketServlet {
+import java.io.Serial;
 
+public class ProblemWebSocketServlet extends XtextWebSocketServlet {
+        @Serial
         private static final long serialVersionUID = -7040955470384797008L;
 
         private transient DisposableRegistry disposableRegistry;
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/SecurityHeadersFilter.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/SecurityHeadersFilter.java
index 7b094fde..fab94689 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/SecurityHeadersFilter.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/SecurityHeadersFilter.java
@@ -16,7 +16,7 @@ public class SecurityHeadersFilter implements Filter {
                         ServletException {
                 if (response instanceof HttpServletResponse httpResponse) {
                         httpResponse.setHeader("Content-Security-Policy", "default-src 'none'; " +
-                                        "script-src 'self'; " +
+                                        "script-src 'self' 'wasm-unsafe-eval'; " +
                                         // CodeMirror needs inline styles, see e.g.,
                                         // https://discuss.codemirror.net/t/inline-styles-and-content-security-policy/1311/2
                                         "style-src 'self' 'unsafe-inline'; " +
@@ -25,7 +25,7 @@ public class SecurityHeadersFilter implements Filter {
                                         "font-src 'self'; " +
                                         "connect-src 'self'; " +
                                         "manifest-src 'self'; " +
-                                        "worker-src 'self';");
+                                        "worker-src 'self' blob:;");
                         httpResponse.setHeader("X-Content-Type-Options", "nosniff");
                         httpResponse.setHeader("X-Frame-Options", "DENY");
                         httpResponse.setHeader("Referrer-Policy", "strict-origin");
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/ServerLauncher.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/ServerLauncher.java
index ad19e77d..155efc6f 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/ServerLauncher.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/ServerLauncher.java
@@ -33,7 +33,7 @@ import java.util.EnumSet;
 import java.util.Set;
 
 public class ServerLauncher {
-        public static final String DEFAULT_LISTEN_ADDRESS = "localhost";
+        public static final String DEFAULT_LISTEN_HOST = "localhost";
 
         public static final int DEFAULT_LISTEN_PORT = 1312;
 
@@ -105,7 +105,7 @@ public class ServerLauncher {
 
         private Resource getBaseResource() {
                 var factory = ResourceFactory.of(server);
-                var baseResourceOverride = System.getenv("BASE_RESOURCE");
+                var baseResourceOverride = System.getenv("REFINERY_BASE_RESOURCE");
                 if (baseResourceOverride != null) {
                         // If a user override is provided, use it.
                         return factory.newResource(baseResourceOverride);
@@ -115,7 +115,10 @@ public class ServerLauncher {
                         // If the app is packaged in the jar, serve it.
                         URI webRootUri;
                         try {
-                                webRootUri = URI.create(indexUrlInJar.toURI().toASCIIString().replaceFirst("/index.html$", "/"));
+                                webRootUri = URI.create(indexUrlInJar.toURI().toASCIIString()
+                                                .replaceFirst("/index.html$", "/")
+                                                // Enable running without warnings from a jar.
+                                                .replaceFirst("^jar:file:", "jar:file://"));
                         } catch (URISyntaxException e) {
                                 throw new IllegalStateException("Jar has invalid base resource URI", e);
                         }
@@ -152,17 +155,17 @@ public class ServerLauncher {
         }
 
         private static String getListenAddress() {
-                var listenAddress = System.getenv("LISTEN_ADDRESS");
+                var listenAddress = System.getenv("REFINERY_LISTEN_HOST");
                 if (listenAddress == null) {
-                        return DEFAULT_LISTEN_ADDRESS;
+                        return DEFAULT_LISTEN_HOST;
                 }
                 return listenAddress;
         }
 
         private static int getListenPort() {
-                var portStr = System.getenv("LISTEN_PORT");
+                var portStr = System.getenv("REFINERY_LISTEN_PORT");
                 if (portStr != null) {
-                        return Integer.parseInt(portStr);
+                        return Integer.parseUnsignedInt(portStr);
                 }
                 return DEFAULT_LISTEN_PORT;
         }
@@ -174,7 +177,7 @@ public class ServerLauncher {
         }
 
         private static String getPublicHost() {
-                var publicHost = System.getenv("PUBLIC_HOST");
+                var publicHost = System.getenv("REFINERY_PUBLIC_HOST");
                 if (publicHost != null) {
                         return publicHost.toLowerCase();
                 }
@@ -182,15 +185,15 @@ public class ServerLauncher {
         }
 
         private static int getPublicPort() {
-                var portStr = System.getenv("PUBLIC_PORT");
+                var portStr = System.getenv("REFINERY_PUBLIC_PORT");
                 if (portStr != null) {
-                        return Integer.parseInt(portStr);
+                        return Integer.parseUnsignedInt(portStr);
                 }
                 return DEFAULT_PUBLIC_PORT;
         }
 
         private static String[] getAllowedOrigins() {
-                var allowedOrigins = System.getenv("ALLOWED_ORIGINS");
+                var allowedOrigins = System.getenv("REFINERY_ALLOWED_ORIGINS");
                 if (allowedOrigins != null) {
                         return allowedOrigins.split(ALLOWED_ORIGINS_SEPARATOR);
                 }
@@ -219,12 +222,10 @@ public class ServerLauncher {
                 int port;
                 var publicHost = getPublicHost();
                 if (publicHost == null) {
-                        host = getListenAddress();
-                        port = getListenPort();
-                } else {
-                        host = publicHost;
-                        port = getPublicPort();
+                        return null;
                 }
+                host = publicHost;
+                port = getPublicPort();
                 var scheme = port == HTTPS_DEFAULT_PORT ? "wss" : "ws";
                 return String.format("%s://%s:%d/xtext-service", scheme, host, port);
         }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/config/BackendConfigServlet.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/config/BackendConfigServlet.java
index a2f04e34..7d0a5122 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/config/BackendConfigServlet.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/config/BackendConfigServlet.java
@@ -25,9 +25,6 @@ public class BackendConfigServlet extends HttpServlet {
         public void init(ServletConfig config) throws ServletException {
                 super.init(config);
                 var webSocketUrl = config.getInitParameter(WEBSOCKET_URL_INIT_PARAM);
-                if (webSocketUrl == null) {
-                        throw new IllegalArgumentException("Init parameter " + WEBSOCKET_URL_INIT_PARAM + " is mandatory");
-                }
                 var backendConfig = new BackendConfig(webSocketUrl);
                 var gson = new Gson();
                 serializedConfig = gson.toJson(backendConfig);
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationCancelledResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationCancelledResult.java
new file mode 100644
index 00000000..fc06fd2e
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationCancelledResult.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import org.eclipse.xtext.web.server.IServiceResult;
+
+public record ModelGenerationCancelledResult() implements IServiceResult {
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationErrorResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationErrorResult.java
new file mode 100644
index 00000000..bedaeb35
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationErrorResult.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import java.util.UUID;
+
+public record ModelGenerationErrorResult(UUID uuid, String error) implements ModelGenerationResult {
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationManager.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationManager.java
new file mode 100644
index 00000000..b0a1912c
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationManager.java
@@ -0,0 +1,41 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import org.eclipse.xtext.util.CancelIndicator;
+
+public class ModelGenerationManager {
+        private final Object lockObject = new Object();
+        private ModelGenerationWorker worker;
+        private boolean disposed;
+
+        boolean setActiveModelGenerationWorker(ModelGenerationWorker worker, CancelIndicator cancelIndicator) {
+                synchronized (lockObject) {
+                        cancel();
+                        if (disposed || cancelIndicator.isCanceled()) {
+                                return true;
+                        }
+                        this.worker = worker;
+                }
+                return false;
+        }
+
+        public void cancel() {
+                synchronized (lockObject) {
+                        if (worker != null) {
+                                worker.cancel();
+                                worker = null;
+                        }
+                }
+        }
+
+        public void dispose() {
+                synchronized (lockObject) {
+                        disposed = true;
+                        cancel();
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationResult.java
new file mode 100644
index 00000000..cf06f447
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationResult.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import org.eclipse.xtext.web.server.IServiceResult;
+
+import java.util.UUID;
+
+public sealed interface ModelGenerationResult extends IServiceResult permits ModelGenerationSuccessResult,
+                ModelGenerationErrorResult, ModelGenerationStatusResult {
+        UUID uuid();
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationService.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationService.java
new file mode 100644
index 00000000..9f72e462
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationService.java
@@ -0,0 +1,60 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import com.google.inject.Singleton;
+import org.eclipse.xtext.service.OperationCanceledManager;
+import org.eclipse.xtext.util.CancelIndicator;
+import org.eclipse.xtext.util.concurrent.CancelableUnitOfWork;
+import org.eclipse.xtext.web.server.model.IXtextWebDocument;
+import tools.refinery.language.web.semantics.SemanticsService;
+import tools.refinery.language.web.xtext.server.push.PushWebDocument;
+import tools.refinery.language.web.xtext.server.push.PushWebDocumentAccess;
+
+@Singleton
+public class ModelGenerationService {
+        public static final String SERVICE_NAME = "modelGeneration";
+        public static final String MODEL_GENERATION_EXECUTOR = "modelGeneration";
+        public static final String MODEL_GENERATION_TIMEOUT_EXECUTOR = "modelGenerationTimeout";
+
+        @Inject
+        private OperationCanceledManager operationCanceledManager;
+
+        @Inject
+        private Provider<ModelGenerationWorker> workerProvider;
+
+        private final long timeoutSec;
+
+        public ModelGenerationService() {
+                timeoutSec = SemanticsService.getTimeout("REFINERY_MODEL_GENERATION_TIMEOUT_SEC").orElse(600L);
+        }
+
+        public ModelGenerationStartedResult generateModel(PushWebDocumentAccess document, int randomSeed) {
+                return document.modify(new CancelableUnitOfWork<>() {
+                        @Override
+                        public ModelGenerationStartedResult exec(IXtextWebDocument state, CancelIndicator cancelIndicator) {
+                                var pushState = (PushWebDocument) state;
+                                var worker = workerProvider.get();
+                                worker.setState(pushState, randomSeed, timeoutSec);
+                                var manager = pushState.getModelGenerationManager();
+                                worker.start();
+                                boolean canceled = manager.setActiveModelGenerationWorker(worker, cancelIndicator);
+                                if (canceled) {
+                                        worker.cancel();
+                                        operationCanceledManager.throwOperationCanceledException();
+                                }
+                                return new ModelGenerationStartedResult(worker.getUuid());
+                        }
+                });
+        }
+
+        public ModelGenerationCancelledResult cancelModelGeneration(PushWebDocumentAccess document) {
+                document.cancelModelGeneration();
+                return new ModelGenerationCancelledResult();
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStartedResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStartedResult.java
new file mode 100644
index 00000000..8c0e73c7
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStartedResult.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.generator;
+
+import org.eclipse.xtext.web.server.IServiceResult;
+
+import java.util.UUID;
+
+public record ModelGenerationStartedResult(UUID uuid) implements IServiceResult {
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStatusResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStatusResult.java
new file mode 100644
index 00000000..a6589870
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStatusResult.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import java.util.UUID;
+
+public record ModelGenerationStatusResult(UUID uuid, String status) implements ModelGenerationResult {
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationSuccessResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationSuccessResult.java
new file mode 100644
index 00000000..21be4e08
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationSuccessResult.java
@@ -0,0 +1,17 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import com.google.gson.JsonObject;
+import tools.refinery.language.semantics.metadata.NodeMetadata;
+import tools.refinery.language.semantics.metadata.RelationMetadata;
+
+import java.util.List;
+import java.util.UUID;
+
+public record ModelGenerationSuccessResult(UUID uuid, List<NodeMetadata> nodes, List<RelationMetadata> relations,
+                                                                                   JsonObject partialInterpretation) implements ModelGenerationResult {
+}
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
new file mode 100644
index 00000000..9ee74207
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
@@ -0,0 +1,233 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.generator;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.xtext.diagnostics.Severity;
+import org.eclipse.xtext.resource.IResourceFactory;
+import org.eclipse.xtext.resource.XtextResourceSet;
+import org.eclipse.xtext.service.OperationCanceledManager;
+import org.eclipse.xtext.util.LazyStringInputStream;
+import org.eclipse.xtext.validation.CheckMode;
+import org.eclipse.xtext.validation.IResourceValidator;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.semantics.metadata.MetadataCreator;
+import tools.refinery.language.semantics.model.ModelInitializer;
+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.dse.propagation.PropagationAdapter;
+import tools.refinery.store.dse.strategy.BestFirstStoreManager;
+import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.statecoding.StateCoderAdapter;
+import tools.refinery.store.util.CancellationToken;
+
+import java.io.IOException;
+import java.util.Map;
+import java.util.UUID;
+import java.util.concurrent.*;
+
+public class ModelGenerationWorker implements Runnable {
+        private static final Logger LOG = LoggerFactory.getLogger(ModelGenerationWorker.class);
+
+        private final UUID uuid = UUID.randomUUID();
+
+        private PushWebDocument state;
+
+        private String text;
+
+        private volatile boolean timedOut;
+
+        private volatile boolean cancelled;
+
+        @Inject
+        private OperationCanceledManager operationCanceledManager;
+
+        @Inject
+        private Provider<XtextResourceSet> resourceSetProvider;
+
+        @Inject
+        private IResourceFactory resourceFactory;
+
+        @Inject
+        private IResourceValidator resourceValidator;
+
+        @Inject
+        private ModelInitializer initializer;
+
+        @Inject
+        private MetadataCreator metadataCreator;
+
+        @Inject
+        private PartialInterpretation2Json partialInterpretation2Json;
+
+        private final Object lockObject = new Object();
+
+        private ExecutorService executorService;
+
+        private ScheduledExecutorService scheduledExecutorService;
+
+        private int randomSeed;
+
+        private long timeoutSec;
+
+        private Future<?> future;
+
+        private ScheduledFuture<?> timeoutFuture;
+
+        private final CancellationToken cancellationToken = () -> {
+                if (cancelled || Thread.interrupted()) {
+                        operationCanceledManager.throwOperationCanceledException();
+                }
+        };
+
+        @Inject
+        public void setExecutorServiceProvider(ThreadPoolExecutorServiceProvider provider) {
+                executorService = provider.get(ModelGenerationService.MODEL_GENERATION_EXECUTOR);
+                scheduledExecutorService = provider.getScheduled(ModelGenerationService.MODEL_GENERATION_TIMEOUT_EXECUTOR);
+        }
+
+        public void setState(PushWebDocument state, int randomSeed, long timeoutSec) {
+                this.state = state;
+                this.randomSeed = randomSeed;
+                this.timeoutSec = timeoutSec;
+                text = state.getText();
+        }
+
+        public UUID getUuid() {
+                return uuid;
+        }
+
+        public void start() {
+                synchronized (lockObject) {
+                        LOG.debug("Enqueueing model generation: {}", uuid);
+                        future = executorService.submit(this);
+                }
+        }
+
+        public void startTimeout() {
+                synchronized (lockObject) {
+                        LOG.debug("Starting model generation: {}", uuid);
+                        cancellationToken.checkCancelled();
+                        timeoutFuture = scheduledExecutorService.schedule(() -> cancel(true), timeoutSec, TimeUnit.SECONDS);
+                }
+        }
+
+        // We catch {@code Throwable} to handle {@code OperationCancelledError}, but we rethrow fatal JVM errors.
+        @SuppressWarnings("squid:S1181")
+        @Override
+        public void run() {
+                startTimeout();
+                notifyResult(new ModelGenerationStatusResult(uuid, "Initializing model generator"));
+                ModelGenerationResult result;
+                try {
+                        result = doRun();
+                } catch (Throwable e) {
+                        if (operationCanceledManager.isOperationCanceledException(e)) {
+                                var message = timedOut ? "Model generation timed out" : "Model generation cancelled";
+                                LOG.debug("{}: {}", message, uuid);
+                                notifyResult(new ModelGenerationErrorResult(uuid, message));
+                        } else if (e instanceof Error error) {
+                                // Make sure we don't try to recover from any fatal JVM errors.
+                                throw error;
+                        } else {
+                                LOG.debug("Model generation error", e);
+                                notifyResult(new ModelGenerationErrorResult(uuid, e.toString()));
+                        }
+                        return;
+                }
+                notifyResult(result);
+        }
+
+        private void notifyResult(ModelGenerationResult result) {
+                state.notifyPrecomputationListeners(ModelGenerationService.SERVICE_NAME, result);
+        }
+
+        public ModelGenerationResult doRun() throws IOException {
+                cancellationToken.checkCancelled();
+                var resourceSet = resourceSetProvider.get();
+                var uri = URI.createURI("__synthetic_" + uuid + ".problem");
+                var resource = resourceFactory.createResource(uri);
+                resourceSet.getResources().add(resource);
+                var inputStream = new LazyStringInputStream(text);
+                resource.load(inputStream, Map.of());
+                cancellationToken.checkCancelled();
+                var issues = resourceValidator.validate(resource, CheckMode.ALL, () -> cancelled || Thread.interrupted());
+                cancellationToken.checkCancelled();
+                for (var issue : issues) {
+                        if (issue.getSeverity() == Severity.ERROR) {
+                                return new ModelGenerationErrorResult(uuid, "Validation error: " + issue.getMessage());
+                        }
+                }
+                if (resource.getContents().isEmpty() || !(resource.getContents().get(0) instanceof Problem problem)) {
+                        return new ModelGenerationErrorResult(uuid, "Model generation problem not found");
+                }
+                cancellationToken.checkCancelled();
+                var storeBuilder = ModelStore.builder()
+                                .cancellationToken(cancellationToken)
+                                .with(ViatraModelQueryAdapter.builder())
+                                .with(PropagationAdapter.builder())
+                                .with(StateCoderAdapter.builder())
+                                .with(DesignSpaceExplorationAdapter.builder())
+                                .with(ReasoningAdapter.builder()
+                                                .requiredInterpretations(Concreteness.CANDIDATE));
+                var modelSeed = initializer.createModel(problem, storeBuilder);
+                var store = storeBuilder.build();
+                cancellationToken.checkCancelled();
+                var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+                var initialVersion = model.commit();
+                cancellationToken.checkCancelled();
+                notifyResult(new ModelGenerationStatusResult(uuid, "Generating model"));
+                var bestFirst = new BestFirstStoreManager(store, 1);
+                bestFirst.startExploration(initialVersion, randomSeed);
+                cancellationToken.checkCancelled();
+                var solutionStore = bestFirst.getSolutionStore();
+                if (solutionStore.getSolutions().isEmpty()) {
+                        return new ModelGenerationErrorResult(uuid, "Problem is unsatisfiable");
+                }
+                notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model"));
+                model.restore(solutionStore.getSolutions().get(0).version());
+                cancellationToken.checkCancelled();
+                metadataCreator.setInitializer(initializer);
+                var nodesMetadata = metadataCreator.getNodesMetadata(model.getAdapter(ReasoningAdapter.class).getNodeCount(),
+                                false);
+                cancellationToken.checkCancelled();
+                var relationsMetadata = metadataCreator.getRelationsMetadata();
+                cancellationToken.checkCancelled();
+                var partialInterpretation = partialInterpretation2Json.getPartialInterpretation(initializer, model,
+                                Concreteness.CANDIDATE, cancellationToken);
+                return new ModelGenerationSuccessResult(uuid, nodesMetadata, relationsMetadata, partialInterpretation);
+        }
+
+        public void cancel() {
+                cancel(false);
+        }
+
+        public void cancel(boolean timedOut) {
+                synchronized (lockObject) {
+                        LOG.trace("Cancelling model generation: {}", uuid);
+                        this.timedOut = timedOut;
+                        cancelled = true;
+                        if (future != null) {
+                                future.cancel(true);
+                                future = null;
+                        }
+                        if (timeoutFuture != null) {
+                                timeoutFuture.cancel(true);
+                                timeoutFuture = null;
+                        }
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java
new file mode 100644
index 00000000..5d5da8fe
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java
@@ -0,0 +1,81 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.semantics;
+
+import com.google.gson.JsonArray;
+import com.google.gson.JsonObject;
+import com.google.inject.Inject;
+import com.google.inject.Singleton;
+import tools.refinery.language.semantics.model.ModelInitializer;
+import tools.refinery.language.semantics.model.SemanticsUtils;
+import tools.refinery.store.map.Cursor;
+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.multiobject.MultiObjectTranslator;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.util.CancellationToken;
+
+import java.util.TreeMap;
+
+@Singleton
+public class PartialInterpretation2Json {
+        @Inject
+        private SemanticsUtils semanticsUtils;
+
+        public JsonObject getPartialInterpretation(ModelInitializer initializer, Model model, Concreteness concreteness,
+                                                                                           CancellationToken cancellationToken) {
+                var adapter = model.getAdapter(ReasoningAdapter.class);
+                var json = new JsonObject();
+                for (var entry : initializer.getRelationTrace().entrySet()) {
+                        var relation = entry.getKey();
+                        var partialSymbol = entry.getValue();
+                        var tuples = getTuplesJson(adapter, concreteness, partialSymbol);
+                        var name = semanticsUtils.getName(relation).orElse(partialSymbol.name());
+                        json.add(name, tuples);
+                        cancellationToken.checkCancelled();
+                }
+                json.add("builtin::count", getCountJson(model));
+                return json;
+        }
+
+        private static JsonArray getTuplesJson(ReasoningAdapter adapter, Concreteness concreteness,
+                                                                                   PartialRelation partialSymbol) {
+                var interpretation = adapter.getPartialInterpretation(concreteness, partialSymbol);
+                var cursor = interpretation.getAll();
+                return getTuplesJson(cursor);
+        }
+
+        private static JsonArray getTuplesJson(Cursor<Tuple, ?> cursor) {
+                var map = new TreeMap<Tuple, Object>();
+                while (cursor.move()) {
+                        map.put(cursor.getKey(), cursor.getValue());
+                }
+                var tuples = new JsonArray();
+                for (var entry : map.entrySet()) {
+                        tuples.add(toArray(entry.getKey(), entry.getValue()));
+                }
+                return tuples;
+        }
+
+        private static JsonArray toArray(Tuple tuple, Object value) {
+                int arity = tuple.getSize();
+                var json = new JsonArray(arity + 1);
+                for (int i = 0; i < arity; i++) {
+                        json.add(tuple.get(i));
+                }
+                json.add(value.toString());
+                return json;
+        }
+
+        private static JsonArray getCountJson(Model model) {
+                var interpretation = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE);
+                var cursor = interpretation.getAll();
+                return getTuplesJson(cursor);
+
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsInternalErrorResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsInternalErrorResult.java
new file mode 100644
index 00000000..ff592e93
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsInternalErrorResult.java
@@ -0,0 +1,9 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.semantics;
+
+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
new file mode 100644
index 00000000..a2e19a2f
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsResult.java
@@ -0,0 +1,12 @@
+/*
+ * 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.IServiceResult;
+
+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
new file mode 100644
index 00000000..331ef84b
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java
@@ -0,0 +1,142 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+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;
+import org.eclipse.xtext.web.server.model.IXtextWebDocument;
+import org.eclipse.xtext.web.server.validation.ValidationService;
+import org.jetbrains.annotations.Nullable;
+import org.slf4j.Logger;
+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.Optional;
+import java.util.concurrent.*;
+import java.util.concurrent.atomic.AtomicBoolean;
+
+@Singleton
+public class SemanticsService extends AbstractCachedService<SemanticsResult> {
+        public static final String SEMANTICS_EXECUTOR = "semantics";
+
+        private static final Logger LOG = LoggerFactory.getLogger(SemanticsService.class);
+
+        @Inject
+        private Provider<SemanticsWorker> workerProvider;
+
+        @Inject
+        private OperationCanceledManager operationCanceledManager;
+
+        @Inject
+        private ValidationService validationService;
+
+        private ExecutorService executorService;
+
+        private final long timeoutMs;
+
+        private final long warmupTimeoutMs;
+
+        private final AtomicBoolean warmedUp = new AtomicBoolean(false);
+
+        public SemanticsService() {
+                timeoutMs = getTimeout("REFINERY_SEMANTICS_TIMEOUT_MS").orElse(1000L);
+                warmupTimeoutMs = getTimeout("REFINERY_SEMANTICS_WARMUP_TIMEOUT_MS").orElse(timeoutMs * 2);
+        }
+
+        public static Optional<Long> getTimeout(String name) {
+                return Optional.ofNullable(System.getenv(name)).map(Long::parseUnsignedLong);
+        }
+
+        @Inject
+        public void setExecutorServiceProvider(ExecutorServiceProvider provider) {
+                executorService = provider.get(SEMANTICS_EXECUTOR);
+        }
+
+        @Override
+        public SemanticsResult compute(IXtextWebDocument doc, CancelIndicator cancelIndicator) {
+                long start = 0;
+                if (LOG.isTraceEnabled()) {
+                        start = System.currentTimeMillis();
+                }
+                if (hasError(doc, cancelIndicator)) {
+                        return null;
+                }
+                var problem = getProblem(doc);
+                if (problem == null) {
+                        return new SemanticsSuccessResult(List.of(), List.of(), new JsonObject());
+                }
+                var worker = workerProvider.get();
+                worker.setProblem(problem, cancelIndicator);
+                var future = executorService.submit(worker);
+                boolean warmedUpCurrently = warmedUp.get();
+                long timeout = warmedUpCurrently ? timeoutMs : warmupTimeoutMs;
+                SemanticsResult result = null;
+                try {
+                        result = future.get(timeout, TimeUnit.MILLISECONDS);
+                        if (!warmedUpCurrently) {
+                                warmedUp.set(true);
+                        }
+                } catch (InterruptedException e) {
+                        future.cancel(true);
+                        LOG.error("Semantics service interrupted", e);
+                        Thread.currentThread().interrupt();
+                } catch (ExecutionException e) {
+                        operationCanceledManager.propagateAsErrorIfCancelException(e.getCause());
+                        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);
+                        if (!warmedUpCurrently) {
+                                warmedUp.set(true);
+                        }
+                        LOG.trace("Semantics service timeout", e);
+                        return new SemanticsInternalErrorResult("Partial interpretation timed out");
+                }
+                if (LOG.isTraceEnabled()) {
+                        long end = System.currentTimeMillis();
+                        LOG.trace("Computed semantics for {} ({}) in {}ms", doc.getResourceId(), doc.getStateId(),
+                                        end - start);
+                }
+                return result;
+        }
+
+        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);
+                return validationResult.getIssues().stream()
+                                .anyMatch(issue -> "error".equals(issue.getSeverity()));
+        }
+
+        @Nullable
+        private Problem getProblem(IXtextWebDocument doc) {
+                var contents = doc.getResource().getContents();
+                if (contents.isEmpty()) {
+                        return null;
+                }
+                var model = contents.get(0);
+                if (!(model instanceof Problem problem)) {
+                        return null;
+                }
+                return problem;
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsSuccessResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsSuccessResult.java
new file mode 100644
index 00000000..350b0b2b
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsSuccessResult.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.semantics;
+
+import com.google.gson.JsonObject;
+import tools.refinery.language.semantics.metadata.NodeMetadata;
+import tools.refinery.language.semantics.metadata.RelationMetadata;
+
+import java.util.List;
+
+public record SemanticsSuccessResult(List<NodeMetadata> nodes, List<RelationMetadata> relations,
+                                                                         JsonObject partialInterpretation) implements SemanticsResult {
+}
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
new file mode 100644
index 00000000..512c2778
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
@@ -0,0 +1,113 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.semantics;
+
+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.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.metadata.MetadataCreator;
+import tools.refinery.language.semantics.model.ModelInitializer;
+import tools.refinery.language.semantics.model.TracedException;
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.translator.TranslationException;
+import tools.refinery.store.util.CancellationToken;
+
+import java.util.ArrayList;
+import java.util.concurrent.Callable;
+
+class SemanticsWorker implements Callable<SemanticsResult> {
+        private static final String DIAGNOSTIC_ID = "tools.refinery.language.semantics.SemanticError";
+
+        @Inject
+        private PartialInterpretation2Json partialInterpretation2Json;
+
+        @Inject
+        private OperationCanceledManager operationCanceledManager;
+
+        @Inject
+        private IDiagnosticConverter diagnosticConverter;
+
+        @Inject
+        private ModelInitializer initializer;
+
+        @Inject
+        private MetadataCreator metadataCreator;
+
+        private Problem problem;
+
+        private CancellationToken cancellationToken;
+
+        public void setProblem(Problem problem, CancelIndicator parentIndicator) {
+                this.problem = problem;
+                cancellationToken = () -> {
+                        if (Thread.interrupted() || parentIndicator.isCanceled()) {
+                                operationCanceledManager.throwOperationCanceledException();
+                        }
+                };
+        }
+
+        @Override
+        public SemanticsResult call() {
+                var builder = ModelStore.builder()
+                                .cancellationToken(cancellationToken)
+                                .with(ViatraModelQueryAdapter.builder())
+                                .with(PropagationAdapter.builder())
+                                .with(ReasoningAdapter.builder()
+                                                .requiredInterpretations(Concreteness.PARTIAL));
+                cancellationToken.checkCancelled();
+                try {
+                        var modelSeed = initializer.createModel(problem, builder);
+                        cancellationToken.checkCancelled();
+                        metadataCreator.setInitializer(initializer);
+                        cancellationToken.checkCancelled();
+                        var nodesMetadata = metadataCreator.getNodesMetadata();
+                        cancellationToken.checkCancelled();
+                        var relationsMetadata = metadataCreator.getRelationsMetadata();
+                        cancellationToken.checkCancelled();
+                        var store = builder.build();
+                        cancellationToken.checkCancelled();
+                        var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+                        cancellationToken.checkCancelled();
+                        var partialInterpretation = partialInterpretation2Json.getPartialInterpretation(initializer, model,
+                                        Concreteness.PARTIAL, cancellationToken);
+
+                        return new SemanticsSuccessResult(nodesMetadata, relationsMetadata, partialInterpretation);
+                } catch (TracedException e) {
+                        return getTracedErrorResult(e.getSourceElement(), e.getMessage());
+                } catch (TranslationException e) {
+                        var sourceElement = initializer.getInverseTrace(e.getPartialSymbol());
+                        return getTracedErrorResult(sourceElement, e.getMessage());
+                }
+        }
+
+        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/ThreadPoolExecutorServiceProvider.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ThreadPoolExecutorServiceProvider.java
new file mode 100644
index 00000000..ff8f4943
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ThreadPoolExecutorServiceProvider.java
@@ -0,0 +1,158 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.xtext.server;
+
+import com.google.inject.Singleton;
+import org.eclipse.xtext.ide.ExecutorServiceProvider;
+import org.eclipse.xtext.web.server.model.XtextWebDocumentAccess;
+import org.jetbrains.annotations.NotNull;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+import tools.refinery.language.web.generator.ModelGenerationService;
+import tools.refinery.language.web.semantics.SemanticsService;
+
+import java.lang.invoke.MethodHandle;
+import java.lang.invoke.MethodHandles;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Optional;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.ScheduledExecutorService;
+import java.util.concurrent.ThreadFactory;
+import java.util.concurrent.atomic.AtomicInteger;
+
+@Singleton
+public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
+        private static final Logger LOG = LoggerFactory.getLogger(ThreadPoolExecutorServiceProvider.class);
+        private static final String DOCUMENT_LOCK_EXECUTOR;
+        private static final AtomicInteger POOL_ID = new AtomicInteger(1);
+
+        private final Map<String, ScheduledExecutorService> scheduledInstanceCache =
+                        Collections.synchronizedMap(new HashMap<>());
+        private final int executorThreadCount;
+        private final int lockExecutorThreadCount;
+        private final int semanticsExecutorThreadCount;
+        private final int generatorExecutorThreadCount;
+
+        static {
+                var lookup = MethodHandles.lookup();
+                MethodHandle getter;
+                try {
+                        var privateLookup = MethodHandles.privateLookupIn(XtextWebDocumentAccess.class, lookup);
+                        getter = privateLookup.findStaticGetter(XtextWebDocumentAccess.class, "DOCUMENT_LOCK_EXECUTOR",
+                                        String.class);
+                } catch (IllegalAccessException | NoSuchFieldException e) {
+                        throw new IllegalStateException("Failed to find getter", e);
+                }
+                try {
+                        DOCUMENT_LOCK_EXECUTOR = (String) getter.invokeExact();
+                } catch (Error e) {
+                        // Rethrow JVM errors.
+                        throw e;
+                } catch (Throwable e) {
+                        throw new IllegalStateException("Failed to get DOCUMENT_LOCK_EXECUTOR", e);
+                }
+        }
+
+        public ThreadPoolExecutorServiceProvider() {
+                executorThreadCount = getCount("REFINERY_XTEXT_THREAD_COUNT").orElse(0);
+                lockExecutorThreadCount = getCount("REFINERY_XTEXT_LOCKING_THREAD_COUNT").orElse(executorThreadCount);
+                int semanticsCount = getCount("REFINERY_XTEXT_SEMANTICS_THREAD_COUNT").orElse(0);
+                if (semanticsCount == 0 || executorThreadCount == 0) {
+                        semanticsExecutorThreadCount = 0;
+                } else {
+                        semanticsExecutorThreadCount = Math.max(semanticsCount, executorThreadCount);
+                }
+                if (semanticsExecutorThreadCount != semanticsCount) {
+                        LOG.warn("Setting REFINERY_XTEXT_SEMANTICS_THREAD_COUNT to {} to avoid deadlock. This value must be " +
+                                                        "either 0 or at least as large as REFINERY_XTEXT_THREAD_COUNT to avoid lock contention.",
+                                        semanticsExecutorThreadCount);
+                }
+                generatorExecutorThreadCount = getCount("REFINERY_MODEL_GENERATION_THREAD_COUNT").orElse(executorThreadCount);
+        }
+
+        private static Optional<Integer> getCount(String name) {
+                return Optional.ofNullable(System.getenv(name)).map(Integer::parseUnsignedInt);
+        }
+
+        public ScheduledExecutorService getScheduled(String key) {
+                return scheduledInstanceCache.computeIfAbsent(key, this::createScheduledInstance);
+        }
+
+        @Override
+        protected ExecutorService createInstance(String key) {
+                String name = "xtext-" + POOL_ID.getAndIncrement();
+                if (key != null) {
+                        name = name + "-" + key;
+                }
+                var threadFactory = new Factory(name, 5);
+                int size = getSize(key);
+                if (size == 0) {
+                        return Executors.newCachedThreadPool(threadFactory);
+                }
+                return Executors.newFixedThreadPool(size, threadFactory);
+        }
+
+        protected ScheduledExecutorService createScheduledInstance(String key) {
+                String name = "xtext-scheduled-" + POOL_ID.getAndIncrement();
+                if (key != null) {
+                        name = name + "-" + key;
+                }
+                var threadFactory = new Factory(name, 5);
+                return Executors.newScheduledThreadPool(1, threadFactory);
+        }
+
+        private int getSize(String key) {
+                if (SemanticsService.SEMANTICS_EXECUTOR.equals(key)) {
+                        return semanticsExecutorThreadCount;
+                } else if (ModelGenerationService.MODEL_GENERATION_EXECUTOR.equals(key)) {
+                        return generatorExecutorThreadCount;
+                } else if (DOCUMENT_LOCK_EXECUTOR.equals(key)) {
+                        return lockExecutorThreadCount;
+                } else {
+                        return executorThreadCount;
+                }
+        }
+
+        @Override
+        public void dispose() {
+                super.dispose();
+                synchronized (scheduledInstanceCache) {
+                        for (var instance : scheduledInstanceCache.values()) {
+                                instance.shutdown();
+                        }
+                        scheduledInstanceCache.clear();
+                }
+        }
+
+        private static class Factory implements ThreadFactory {
+                // We have to explicitly store the {@link ThreadGroup} to create a {@link ThreadFactory}.
+                @SuppressWarnings("squid:S3014")
+                private final ThreadGroup threadGroup = Thread.currentThread().getThreadGroup();
+                private final AtomicInteger threadId = new AtomicInteger(1);
+                private final String namePrefix;
+                private final int priority;
+
+                public Factory(String name, int priority) {
+                        namePrefix = name + "-thread-";
+                        this.priority = priority;
+                }
+
+                @Override
+                public Thread newThread(@NotNull Runnable runnable) {
+                        var thread = new Thread(threadGroup, runnable, namePrefix + threadId.getAndIncrement());
+                        if (thread.isDaemon()) {
+                                thread.setDaemon(false);
+                        }
+                        if (thread.getPriority() != priority) {
+                                thread.setPriority(priority);
+                        }
+                        return thread;
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/TransactionExecutor.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/TransactionExecutor.java
index 0135d8f5..a3792bac 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/TransactionExecutor.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/TransactionExecutor.java
@@ -42,6 +42,8 @@ public class TransactionExecutor implements IDisposable, PrecomputationListener
 
         private final List<XtextWebPushMessage> pendingPushMessages = new ArrayList<>();
 
+        private volatile boolean disposed;
+
         public TransactionExecutor(ISession session, IResourceServiceProvider.Registry resourceServiceProviderRegistry) {
                 this.session = session;
                 this.resourceServiceProviderRegistry = resourceServiceProviderRegistry;
@@ -52,10 +54,13 @@ public class TransactionExecutor implements IDisposable, PrecomputationListener
         }
 
         public void handleRequest(XtextWebRequest request) throws ResponseHandlerException {
+                if (disposed) {
+                        return;
+                }
                 var serviceContext = new SimpleServiceContext(session, request.getRequestData());
                 var ping = serviceContext.getParameter("ping");
                 if (ping != null) {
-                        responseHandler.onResponse(new XtextWebOkResponse(request, new PongResult(ping)));
+                        onResponse(new XtextWebOkResponse(request, new PongResult(ping)));
                         return;
                 }
                 synchronized (callPendingLock) {
@@ -72,23 +77,36 @@ public class TransactionExecutor implements IDisposable, PrecomputationListener
                         var serviceDispatcher = injector.getInstance(XtextServiceDispatcher.class);
                         var service = serviceDispatcher.getService(new SubscribingServiceContext(serviceContext, this));
                         var serviceResult = service.getService().apply();
-                        responseHandler.onResponse(new XtextWebOkResponse(request, serviceResult));
+                        onResponse(new XtextWebOkResponse(request, serviceResult));
                 } catch (InvalidRequestException e) {
-                        responseHandler.onResponse(new XtextWebErrorResponse(request, XtextWebErrorKind.REQUEST_ERROR, e));
+                        onResponse(new XtextWebErrorResponse(request, XtextWebErrorKind.REQUEST_ERROR, e));
                 } catch (RuntimeException e) {
-                        responseHandler.onResponse(new XtextWebErrorResponse(request, XtextWebErrorKind.SERVER_ERROR, e));
+                        onResponse(new XtextWebErrorResponse(request, XtextWebErrorKind.SERVER_ERROR, e));
                 } finally {
-                        synchronized (callPendingLock) {
-                                for (var message : pendingPushMessages) {
-                                        try {
-                                                responseHandler.onResponse(message);
-                                        } catch (ResponseHandlerException | RuntimeException e) {
-                                                LOG.error("Error while flushing push message", e);
-                                        }
+                        flushPendingPushMessages();
+                }
+        }
+
+        private void onResponse(XtextWebResponse response) throws ResponseHandlerException {
+                if (!disposed) {
+                        responseHandler.onResponse(response);
+                }
+        }
+
+        private void flushPendingPushMessages() {
+                synchronized (callPendingLock) {
+                        for (var message : pendingPushMessages) {
+                                if (disposed) {
+                                        return;
+                                }
+                                try {
+                                        responseHandler.onResponse(message);
+                                } catch (ResponseHandlerException | RuntimeException e) {
+                                        LOG.error("Error while flushing push message", e);
                                 }
-                                pendingPushMessages.clear();
-                                callPending = false;
                         }
+                        pendingPushMessages.clear();
+                        callPending = false;
                 }
         }
 
@@ -134,7 +152,7 @@ public class TransactionExecutor implements IDisposable, PrecomputationListener
          * @throws UnknownLanguageException if the Xtext language cannot be determined
          */
         protected Injector getInjector(IServiceContext context) {
-                IResourceServiceProvider resourceServiceProvider = null;
+                IResourceServiceProvider resourceServiceProvider;
                 var resourceName = context.getParameter("resource");
                 if (resourceName == null) {
                         resourceName = "";
@@ -164,10 +182,12 @@ public class TransactionExecutor implements IDisposable, PrecomputationListener
 
         @Override
         public void dispose() {
+                disposed = true;
                 for (var subscription : subscriptions.values()) {
                         var document = subscription.get();
                         if (document != null) {
                                 document.removePrecomputationListener(this);
+                                document.dispose();
                         }
                 }
         }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebOkResponse.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebOkResponse.java
index 73527ee5..c3379329 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebOkResponse.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebOkResponse.java
@@ -5,12 +5,11 @@
  */
 package tools.refinery.language.web.xtext.server.message;
 
-import java.util.Objects;
-
+import com.google.gson.annotations.SerializedName;
 import org.eclipse.xtext.web.server.IServiceResult;
 import org.eclipse.xtext.web.server.IUnwrappableServiceResult;
 
-import com.google.gson.annotations.SerializedName;
+import java.util.Objects;
 
 public final class XtextWebOkResponse implements XtextWebResponse {
         private String id;
@@ -19,7 +18,6 @@ public final class XtextWebOkResponse implements XtextWebResponse {
         private Object responseData;
 
         public XtextWebOkResponse(String id, Object responseData) {
-                super();
                 this.id = id;
                 this.responseData = responseData;
         }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebRequest.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebRequest.java
index ff788e94..7c4562bf 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebRequest.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebRequest.java
@@ -5,19 +5,22 @@
  */
 package tools.refinery.language.web.xtext.server.message;
 
+import com.google.gson.annotations.SerializedName;
+
 import java.util.Map;
 import java.util.Objects;
 
-import com.google.gson.annotations.SerializedName;
-
 public class XtextWebRequest {
         private String id;
 
         @SerializedName("request")
         private Map<String, String> requestData;
 
+        public XtextWebRequest() {
+                this(null, null);
+        }
+
         public XtextWebRequest(String id, Map<String, String> requestData) {
-                super();
                 this.id = id;
                 this.requestData = requestData;
         }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebResponse.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebResponse.java
index 61444c99..c370fb56 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebResponse.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebResponse.java
@@ -5,5 +5,5 @@
  */
 package tools.refinery.language.web.xtext.server.message;
 
-public sealed interface XtextWebResponse permits XtextWebOkResponse,XtextWebErrorResponse,XtextWebPushMessage {
+public sealed interface XtextWebResponse permits XtextWebOkResponse, XtextWebErrorResponse, XtextWebPushMessage {
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushServiceDispatcher.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushServiceDispatcher.java
index 4c9135c8..e1d00d8f 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushServiceDispatcher.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushServiceDispatcher.java
@@ -5,16 +5,34 @@
  */
 package tools.refinery.language.web.xtext.server.push;
 
+import com.google.common.base.Optional;
+import com.google.inject.Inject;
 import org.eclipse.xtext.web.server.IServiceContext;
+import org.eclipse.xtext.web.server.InvalidRequestException;
 import org.eclipse.xtext.web.server.XtextServiceDispatcher;
+import org.eclipse.xtext.web.server.model.PrecomputedServiceRegistry;
 import org.eclipse.xtext.web.server.model.XtextWebDocument;
 
 import com.google.inject.Singleton;
 
+import tools.refinery.language.web.generator.ModelGenerationService;
+import tools.refinery.language.web.semantics.SemanticsService;
 import tools.refinery.language.web.xtext.server.SubscribingServiceContext;
 
 @Singleton
 public class PushServiceDispatcher extends XtextServiceDispatcher {
+        @Inject
+        private SemanticsService semanticsService;
+
+        @Inject
+        private ModelGenerationService modelGenerationService;
+
+        @Override
+        @Inject
+        protected void registerPreComputedServices(PrecomputedServiceRegistry registry) {
+                super.registerPreComputedServices(registry);
+                registry.addPrecomputedService(semanticsService);
+        }
 
         @Override
         protected XtextWebDocument getFullTextDocument(String fullText, String resourceId, IServiceContext context) {
@@ -25,4 +43,39 @@ public class PushServiceDispatcher extends XtextServiceDispatcher {
                 }
                 return document;
         }
+
+        @Override
+        protected ServiceDescriptor createServiceDescriptor(String serviceType, IServiceContext context) {
+                if (ModelGenerationService.SERVICE_NAME.equals(serviceType)) {
+                        return getModelGenerationService(context);
+                }
+                return super.createServiceDescriptor(serviceType, context);
+        }
+
+        protected ServiceDescriptor getModelGenerationService(IServiceContext context) throws InvalidRequestException {
+                var document = (PushWebDocumentAccess) getDocumentAccess(context);
+                // Using legacy Guava methods because of the Xtext dependency.
+                @SuppressWarnings({"Guava", "squid:S4738"})
+                boolean start = getBoolean(context, "start", Optional.of(false));
+                @SuppressWarnings({"Guava", "squid:S4738"})
+                boolean cancel = getBoolean(context, "cancel", Optional.of(false));
+                if (!start && !cancel) {
+                        throw new InvalidRequestException("Either start of cancel must be specified");
+                }
+                @SuppressWarnings({"squid:S4738"})
+                int randomSeed = start ? getInt(context, "randomSeed", Optional.absent()) : 0;
+                var descriptor = new ServiceDescriptor();
+                descriptor.setService(() -> {
+                        try {
+                                if (start) {
+                                        return modelGenerationService.generateModel(document, randomSeed);
+                                } else {
+                                        return modelGenerationService.cancelModelGeneration(document);
+                                }
+                        } catch (RuntimeException e) {
+                                return handleError(descriptor, e);
+                        }
+                });
+                return descriptor;
+        }
 }
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 56fd12c9..ca97147a 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
@@ -5,11 +5,7 @@
  */
 package tools.refinery.language.web.xtext.server.push;
 
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-
+import com.google.common.collect.ImmutableList;
 import org.eclipse.xtext.util.CancelIndicator;
 import org.eclipse.xtext.web.server.IServiceResult;
 import org.eclipse.xtext.web.server.model.AbstractCachedService;
@@ -17,60 +13,59 @@ import org.eclipse.xtext.web.server.model.DocumentSynchronizer;
 import org.eclipse.xtext.web.server.model.XtextWebDocument;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
-
-import com.google.common.collect.ImmutableList;
-
+import tools.refinery.language.web.generator.ModelGenerationManager;
 import tools.refinery.language.web.xtext.server.ResponseHandlerException;
 
+import java.util.ArrayList;
+import java.util.List;
+
 public class PushWebDocument extends XtextWebDocument {
         private static final Logger LOG = LoggerFactory.getLogger(PushWebDocument.class);
 
         private final List<PrecomputationListener> precomputationListeners = new ArrayList<>();
 
-        private final Map<Class<?>, IServiceResult> precomputedServices = new HashMap<>();
+        private final ModelGenerationManager modelGenerationManager = new ModelGenerationManager();
+
+        private final DocumentSynchronizer synchronizer;
 
         public PushWebDocument(String resourceId, DocumentSynchronizer synchronizer) {
                 super(resourceId, synchronizer);
-                if (resourceId == null) {
-                        throw new IllegalArgumentException("resourceId must not be null");
-                }
+                this.synchronizer = synchronizer;
         }
 
-        public boolean addPrecomputationListener(PrecomputationListener listener) {
+        public ModelGenerationManager getModelGenerationManager() {
+                return modelGenerationManager;
+        }
+
+        public void addPrecomputationListener(PrecomputationListener listener) {
                 synchronized (precomputationListeners) {
                         if (precomputationListeners.contains(listener)) {
-                                return false;
+                                return;
                         }
                         precomputationListeners.add(listener);
                         listener.onSubscribeToPrecomputationEvents(getResourceId(), this);
-                        return true;
                 }
         }
 
-        public boolean removePrecomputationListener(PrecomputationListener listener) {
+        public void removePrecomputationListener(PrecomputationListener listener) {
                 synchronized (precomputationListeners) {
-                        return precomputationListeners.remove(listener);
+                        precomputationListeners.remove(listener);
                 }
         }
 
         public <T extends IServiceResult> void precomputeServiceResult(AbstractCachedService<T> service, String serviceName,
                         CancelIndicator cancelIndicator, boolean logCacheMiss) {
                 var result = getCachedServiceResult(service, cancelIndicator, logCacheMiss);
-                if (result == null) {
-                        LOG.error("{} service returned null result", serviceName);
-                        return;
+                if (result != null) {
+                        notifyPrecomputationListeners(serviceName, result);
                 }
-                var serviceClass = service.getClass();
-                var previousResult = precomputedServices.get(serviceClass);
-                if (previousResult != null && previousResult.equals(result)) {
-                        return;
-                }
-                precomputedServices.put(serviceClass, result);
-                notifyPrecomputationListeners(serviceName, result);
         }
 
-        private <T extends IServiceResult> void notifyPrecomputationListeners(String serviceName, T result) {
+        public <T extends IServiceResult> void notifyPrecomputationListeners(String serviceName, T result) {
                 var resourceId = getResourceId();
+                if (resourceId == null) {
+                        return;
+                }
                 var stateId = getStateId();
                 List<PrecomputationListener> copyOfListeners;
                 synchronized (precomputationListeners) {
@@ -91,4 +86,13 @@ public class PushWebDocument extends XtextWebDocument {
                         }
                 }
         }
+
+        public void cancelModelGeneration() {
+                modelGenerationManager.cancel();
+        }
+
+        public void dispose() {
+                synchronizer.setCanceled(true);
+                modelGenerationManager.dispose();
+        }
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentAccess.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentAccess.java
index d9e548cd..1e68b244 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentAccess.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentAccess.java
@@ -18,6 +18,7 @@ import org.eclipse.xtext.web.server.syntaxcoloring.HighlightingService;
 import org.eclipse.xtext.web.server.validation.ValidationService;
 
 import com.google.inject.Inject;
+import tools.refinery.language.web.semantics.SemanticsService;
 
 public class PushWebDocumentAccess extends XtextWebDocumentAccess {
 
@@ -49,7 +50,7 @@ public class PushWebDocumentAccess extends XtextWebDocumentAccess {
                         precomputeServiceResult(service, false);
                 }
         }
-        
+
         protected <T extends IServiceResult> void precomputeServiceResult(AbstractCachedService<T> service, boolean logCacheMiss) {
                 var serviceName = getPrecomputedServiceName(service);
                 readOnly(new CancelableUnitOfWork<Void, IXtextWebDocument>() {
@@ -60,7 +61,7 @@ public class PushWebDocumentAccess extends XtextWebDocumentAccess {
                         }
                 });
         }
-        
+
         protected String getPrecomputedServiceName(AbstractCachedService<? extends IServiceResult> service) {
                 if (service instanceof ValidationService) {
                         return "validate";
@@ -68,6 +69,13 @@ public class PushWebDocumentAccess extends XtextWebDocumentAccess {
                 if (service instanceof HighlightingService) {
                         return "highlight";
                 }
+                if (service instanceof SemanticsService) {
+                        return "semantics";
+                }
                 throw new IllegalArgumentException("Unknown precomputed service: " + service);
         }
+
+        public void cancelModelGeneration() {
+                pushDocument.cancelModelGeneration();
+        }
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentProvider.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentProvider.java
index b6f4fb43..ec6204ef 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentProvider.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentProvider.java
@@ -27,12 +27,7 @@ public class PushWebDocumentProvider implements IWebDocumentProvider {
 
         @Override
         public XtextWebDocument get(String resourceId, IServiceContext serviceContext) {
-                if (resourceId == null) {
-                        return new XtextWebDocument(null, synchronizerProvider.get());
-                } else {
-                        // We only need to send push messages if a resourceId is specified.
-                        return new PushWebDocument(resourceId,
-                                        serviceContext.getSession().get(DocumentSynchronizer.class, () -> this.synchronizerProvider.get()));
-                }
+                return new PushWebDocument(resourceId,
+                                serviceContext.getSession().get(DocumentSynchronizer.class, () -> this.synchronizerProvider.get()));
         }
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/RuntimeTypeAdapterFactory.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/RuntimeTypeAdapterFactory.java
new file mode 100644
index 00000000..b16cf7df
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/RuntimeTypeAdapterFactory.java
@@ -0,0 +1,304 @@
+/*
+ * Copyright (C) 2011 Google Inc.
+ * Copyright (C) 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *
+ * This file was copied into Refinery according to upstream instructions at
+ * https://github.com/google/gson/issues/1104#issuecomment-309582470.
+ * However, we changed the package name below to avoid potential clashes
+ * with other jars on the classpath.
+ */
+package tools.refinery.language.web.xtext.servlet;
+
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.google.gson.Gson;
+import com.google.gson.JsonElement;
+import com.google.gson.JsonObject;
+import com.google.gson.JsonParseException;
+import com.google.gson.JsonPrimitive;
+import com.google.gson.TypeAdapter;
+import com.google.gson.TypeAdapterFactory;
+import com.google.gson.reflect.TypeToken;
+import com.google.gson.stream.JsonReader;
+import com.google.gson.stream.JsonWriter;
+import java.io.IOException;
+import java.util.LinkedHashMap;
+import java.util.Map;
+
+/**
+ * Adapts values whose runtime type may differ from their declaration type. This
+ * is necessary when a field's type is not the same type that GSON should create
+ * when deserializing that field. For example, consider these types:
+ * <pre>   {@code
+ *   abstract class Shape {
+ *     int x;
+ *     int y;
+ *   }
+ *   class Circle extends Shape {
+ *     int radius;
+ *   }
+ *   class Rectangle extends Shape {
+ *     int width;
+ *     int height;
+ *   }
+ *   class Diamond extends Shape {
+ *     int width;
+ *     int height;
+ *   }
+ *   class Drawing {
+ *     Shape bottomShape;
+ *     Shape topShape;
+ *   }
+ * }</pre>
+ * <p>Without additional type information, the serialized JSON is ambiguous. Is
+ * the bottom shape in this drawing a rectangle or a diamond? <pre>   {@code
+ *   {
+ *     "bottomShape": {
+ *       "width": 10,
+ *       "height": 5,
+ *       "x": 0,
+ *       "y": 0
+ *     },
+ *     "topShape": {
+ *       "radius": 2,
+ *       "x": 4,
+ *       "y": 1
+ *     }
+ *   }}</pre>
+ * This class addresses this problem by adding type information to the
+ * serialized JSON and honoring that type information when the JSON is
+ * deserialized: <pre>   {@code
+ *   {
+ *     "bottomShape": {
+ *       "type": "Diamond",
+ *       "width": 10,
+ *       "height": 5,
+ *       "x": 0,
+ *       "y": 0
+ *     },
+ *     "topShape": {
+ *       "type": "Circle",
+ *       "radius": 2,
+ *       "x": 4,
+ *       "y": 1
+ *     }
+ *   }}</pre>
+ * Both the type field name ({@code "type"}) and the type labels ({@code
+ * "Rectangle"}) are configurable.
+ *
+ * <h2>Registering Types</h2>
+ * Create a {@code RuntimeTypeAdapterFactory} by passing the base type and type field
+ * name to the {@link #of} factory method. If you don't supply an explicit type
+ * field name, {@code "type"} will be used. <pre>   {@code
+ *   RuntimeTypeAdapterFactory<Shape> shapeAdapterFactory
+ *       = RuntimeTypeAdapterFactory.of(Shape.class, "type");
+ * }</pre>
+ * Next register all of your subtypes. Every subtype must be explicitly
+ * registered. This protects your application from injection attacks. If you
+ * don't supply an explicit type label, the type's simple name will be used.
+ * <pre>   {@code
+ *   shapeAdapterFactory.registerSubtype(Rectangle.class, "Rectangle");
+ *   shapeAdapterFactory.registerSubtype(Circle.class, "Circle");
+ *   shapeAdapterFactory.registerSubtype(Diamond.class, "Diamond");
+ * }</pre>
+ * Finally, register the type adapter factory in your application's GSON builder:
+ * <pre>   {@code
+ *   Gson gson = new GsonBuilder()
+ *       .registerTypeAdapterFactory(shapeAdapterFactory)
+ *       .create();
+ * }</pre>
+ * Like {@code GsonBuilder}, this API supports chaining: <pre>   {@code
+ *   RuntimeTypeAdapterFactory<Shape> shapeAdapterFactory = RuntimeTypeAdapterFactory.of(Shape.class)
+ *       .registerSubtype(Rectangle.class)
+ *       .registerSubtype(Circle.class)
+ *       .registerSubtype(Diamond.class);
+ * }</pre>
+ *
+ * <h2>Serialization and deserialization</h2>
+ * In order to serialize and deserialize a polymorphic object,
+ * you must specify the base type explicitly.
+ * <pre>   {@code
+ *   Diamond diamond = new Diamond();
+ *   String json = gson.toJson(diamond, Shape.class);
+ * }</pre>
+ * And then:
+ * <pre>   {@code
+ *   Shape shape = gson.fromJson(json, Shape.class);
+ * }</pre>
+ */
+public final class RuntimeTypeAdapterFactory<T> implements TypeAdapterFactory {
+        private final Class<?> baseType;
+        private final String typeFieldName;
+        private final Map<String, Class<?>> labelToSubtype = new LinkedHashMap<>();
+        private final Map<Class<?>, String> subtypeToLabel = new LinkedHashMap<>();
+        private final boolean maintainType;
+        private boolean recognizeSubtypes;
+
+        private RuntimeTypeAdapterFactory(
+                        Class<?> baseType, String typeFieldName, boolean maintainType) {
+                if (typeFieldName == null || baseType == null) {
+                        throw new NullPointerException();
+                }
+                this.baseType = baseType;
+                this.typeFieldName = typeFieldName;
+                this.maintainType = maintainType;
+        }
+
+        /**
+         * Creates a new runtime type adapter using for {@code baseType} using {@code
+         * typeFieldName} as the type field name. Type field names are case sensitive.
+         *
+         * @param maintainType true if the type field should be included in deserialized objects
+         */
+        public static <T> RuntimeTypeAdapterFactory<T> of(Class<T> baseType, String typeFieldName, boolean maintainType) {
+                return new RuntimeTypeAdapterFactory<>(baseType, typeFieldName, maintainType);
+        }
+
+        /**
+         * Creates a new runtime type adapter using for {@code baseType} using {@code
+         * typeFieldName} as the type field name. Type field names are case sensitive.
+         */
+        public static <T> RuntimeTypeAdapterFactory<T> of(Class<T> baseType, String typeFieldName) {
+                return new RuntimeTypeAdapterFactory<>(baseType, typeFieldName, false);
+        }
+
+        /**
+         * Creates a new runtime type adapter for {@code baseType} using {@code "type"} as
+         * the type field name.
+         */
+        public static <T> RuntimeTypeAdapterFactory<T> of(Class<T> baseType) {
+                return new RuntimeTypeAdapterFactory<>(baseType, "type", false);
+        }
+
+        /**
+         * Ensures that this factory will handle not just the given {@code baseType}, but any subtype
+         * of that type.
+         */
+        @CanIgnoreReturnValue
+        public RuntimeTypeAdapterFactory<T> recognizeSubtypes() {
+                this.recognizeSubtypes = true;
+                return this;
+        }
+
+        /**
+         * Registers {@code type} identified by {@code label}. Labels are case
+         * sensitive.
+         *
+         * @throws IllegalArgumentException if either {@code type} or {@code label}
+         *     have already been registered on this type adapter.
+         */
+        @CanIgnoreReturnValue
+        public RuntimeTypeAdapterFactory<T> registerSubtype(Class<? extends T> type, String label) {
+                if (type == null || label == null) {
+                        throw new NullPointerException();
+                }
+                if (subtypeToLabel.containsKey(type) || labelToSubtype.containsKey(label)) {
+                        throw new IllegalArgumentException("types and labels must be unique");
+                }
+                labelToSubtype.put(label, type);
+                subtypeToLabel.put(type, label);
+                return this;
+        }
+
+        /**
+         * Registers {@code type} identified by its {@link Class#getSimpleName simple
+         * name}. Labels are case sensitive.
+         *
+         * @throws IllegalArgumentException if either {@code type} or its simple name
+         *     have already been registered on this type adapter.
+         */
+        @CanIgnoreReturnValue
+        public RuntimeTypeAdapterFactory<T> registerSubtype(Class<? extends T> type) {
+                return registerSubtype(type, type.getSimpleName());
+        }
+
+        @Override
+        public <R> TypeAdapter<R> create(Gson gson, TypeToken<R> type) {
+                if (type == null) {
+                        return null;
+                }
+                Class<?> rawType = type.getRawType();
+                boolean handle =
+                                recognizeSubtypes ? baseType.isAssignableFrom(rawType) : baseType.equals(rawType);
+                if (!handle) {
+                        return null;
+                }
+
+                final TypeAdapter<JsonElement> jsonElementAdapter = gson.getAdapter(JsonElement.class);
+                final Map<String, TypeAdapter<?>> labelToDelegate = new LinkedHashMap<>();
+                final Map<Class<?>, TypeAdapter<?>> subtypeToDelegate = new LinkedHashMap<>();
+                for (Map.Entry<String, Class<?>> entry : labelToSubtype.entrySet()) {
+                        TypeAdapter<?> delegate = gson.getDelegateAdapter(this, TypeToken.get(entry.getValue()));
+                        labelToDelegate.put(entry.getKey(), delegate);
+                        subtypeToDelegate.put(entry.getValue(), delegate);
+                }
+
+                return new TypeAdapter<R>() {
+                        @Override public R read(JsonReader in) throws IOException {
+                                JsonElement jsonElement = jsonElementAdapter.read(in);
+                                JsonElement labelJsonElement;
+                                if (maintainType) {
+                                        labelJsonElement = jsonElement.getAsJsonObject().get(typeFieldName);
+                                } else {
+                                        labelJsonElement = jsonElement.getAsJsonObject().remove(typeFieldName);
+                                }
+
+                                if (labelJsonElement == null) {
+                                        throw new JsonParseException("cannot deserialize " + baseType
+                                                        + " because it does not define a field named " + typeFieldName);
+                                }
+                                String label = labelJsonElement.getAsString();
+                                @SuppressWarnings("unchecked") // registration requires that subtype extends T
+                                TypeAdapter<R> delegate = (TypeAdapter<R>) labelToDelegate.get(label);
+                                if (delegate == null) {
+                                        throw new JsonParseException("cannot deserialize " + baseType + " subtype named "
+                                                        + label + "; did you forget to register a subtype?");
+                                }
+                                return delegate.fromJsonTree(jsonElement);
+                        }
+
+                        @Override public void write(JsonWriter out, R value) throws IOException {
+                                Class<?> srcType = value.getClass();
+                                String label = subtypeToLabel.get(srcType);
+                                @SuppressWarnings("unchecked") // registration requires that subtype extends T
+                                TypeAdapter<R> delegate = (TypeAdapter<R>) subtypeToDelegate.get(srcType);
+                                if (delegate == null) {
+                                        throw new JsonParseException("cannot serialize " + srcType.getName()
+                                                        + "; did you forget to register a subtype?");
+                                }
+                                JsonObject jsonObject = delegate.toJsonTree(value).getAsJsonObject();
+
+                                if (maintainType) {
+                                        jsonElementAdapter.write(out, jsonObject);
+                                        return;
+                                }
+
+                                JsonObject clone = new JsonObject();
+
+                                if (jsonObject.has(typeFieldName)) {
+                                        throw new JsonParseException("cannot serialize " + srcType.getName()
+                                                        + " because it already defines a field named " + typeFieldName);
+                                }
+                                clone.add(typeFieldName, new JsonPrimitive(label));
+
+                                for (Map.Entry<String, JsonElement> e : jsonObject.entrySet()) {
+                                        clone.add(e.getKey(), e.getValue());
+                                }
+                                jsonElementAdapter.write(out, clone);
+                        }
+                }.nullSafe();
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java
index 043d318c..1fde1be5 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java
@@ -6,6 +6,7 @@
 package tools.refinery.language.web.xtext.servlet;
 
 import com.google.gson.Gson;
+import com.google.gson.GsonBuilder;
 import com.google.gson.JsonIOException;
 import com.google.gson.JsonParseException;
 import org.eclipse.jetty.websocket.api.Callback;
@@ -16,6 +17,7 @@ import org.eclipse.xtext.resource.IResourceServiceProvider;
 import org.eclipse.xtext.web.server.ISession;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
+import tools.refinery.language.semantics.metadata.*;
 import tools.refinery.language.web.xtext.server.ResponseHandler;
 import tools.refinery.language.web.xtext.server.ResponseHandlerException;
 import tools.refinery.language.web.xtext.server.TransactionExecutor;
@@ -28,7 +30,15 @@ import java.io.Reader;
 public class XtextWebSocket implements ResponseHandler {
         private static final Logger LOG = LoggerFactory.getLogger(XtextWebSocket.class);
 
-        private final Gson gson = new Gson();
+        private final Gson gson = new GsonBuilder()
+                        .disableJdkUnsafe()
+                        .registerTypeAdapterFactory(RuntimeTypeAdapterFactory.of(RelationDetail.class, "type")
+                                        .registerSubtype(ClassDetail.class, "class")
+                                        .registerSubtype(ReferenceDetail.class, "reference")
+                                        .registerSubtype(OppositeReferenceDetail.class, "opposite")
+                                        .registerSubtype(PredicateDetail.class, "predicate")
+                                        .registerSubtype(BuiltInDetail.class, "builtin"))
+                        .create();
 
         private final TransactionExecutor executor;
 
@@ -70,10 +80,11 @@ public class XtextWebSocket implements ResponseHandler {
 
         @OnWebSocketError
         public void onError(Throwable error) {
+                executor.dispose();
                 if (webSocketSession == null) {
                         return;
                 }
-                LOG.error("Internal websocket error in connection from" + webSocketSession.getRemoteSocketAddress(), error);
+                LOG.error("Internal websocket error in connection from " + webSocketSession.getRemoteSocketAddress(), error);
         }
 
         @OnWebSocketMessage
@@ -86,14 +97,18 @@ public class XtextWebSocket implements ResponseHandler {
                 try {
                         request = gson.fromJson(reader, XtextWebRequest.class);
                 } catch (JsonIOException e) {
-                        LOG.error("Cannot read from websocket from" + webSocketSession.getRemoteSocketAddress(), e);
+                        LOG.error("Cannot read from websocket from " + webSocketSession.getRemoteSocketAddress(), e);
                         if (webSocketSession.isOpen()) {
+                                executor.dispose();
                                 webSocketSession.close(StatusCode.SERVER_ERROR, "Cannot read payload", Callback.NOOP);
                         }
                         return;
                 } catch (JsonParseException e) {
-                        LOG.warn("Malformed websocket request from" + webSocketSession.getRemoteSocketAddress(), e);
-                        webSocketSession.close(XtextStatusCode.INVALID_JSON, "Invalid JSON payload", Callback.NOOP);
+                        LOG.warn("Malformed websocket request from " + webSocketSession.getRemoteSocketAddress(), e);
+                        if (webSocketSession.isOpen()) {
+                                executor.dispose();
+                                webSocketSession.close(XtextStatusCode.INVALID_JSON, "Invalid JSON payload", Callback.NOOP);
+                        }
                         return;
                 }
                 try {
@@ -101,6 +116,7 @@ public class XtextWebSocket implements ResponseHandler {
                 } catch (ResponseHandlerException e) {
                         LOG.warn("Cannot write websocket response", e);
                         if (webSocketSession.isOpen()) {
+                                executor.dispose();
                                 webSocketSession.close(StatusCode.SERVER_ERROR, "Cannot write response", Callback.NOOP);
                         }
                 }
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 927eeab1..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(5));
+                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\"," +
@@ -101,10 +101,19 @@ class ProblemWebSocketServletIntegrationTest {
                 assertThat(responses.get(2), equalTo(
                                 "{\"resource\":\"test.problem\",\"stateId\":\"-80000000\",\"service\":\"validate\"," +
                                                 "\"push\":{\"issues\":[]}}"));
-                assertThat(responses.get(3), equalTo("{\"id\":\"bar\",\"response\":{\"stateId\":\"-7fffffff\"}}"));
-                assertThat(responses.get(4), startsWith(
+                assertThat(responses.get(3), startsWith(
+                                "{\"resource\":\"test.problem\",\"stateId\":\"-80000000\",\"service\":\"semantics\"," +
+                                                "\"push\":{"));
+                assertThat(responses.get(4), equalTo("{\"id\":\"bar\",\"response\":{\"stateId\":\"-7fffffff\"}}"));
+                assertThat(responses.get(5), startsWith(
                                 "{\"resource\":\"test.problem\",\"stateId\":\"-7fffffff\",\"service\":\"highlight\"," +
                                                 "\"push\":{\"regions\":["));
+                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\":{"));
         }
 
         @WebSocket
@@ -117,14 +126,14 @@ class ProblemWebSocketServletIntegrationTest {
                                                         "\"fullText\":\"class Person.\n\"}}",
                                         Callback.NOOP
                         );
-                        case 3 -> //noinspection TextBlockMigration
+                        case 4 -> //noinspection TextBlockMigration
                                         session.sendText(
                                         "{\"id\":\"bar\",\"request\":{\"resource\":\"test.problem\",\"serviceType\":\"update\"," +
                                                         "\"requiredStateId\":\"-80000000\",\"deltaText\":\"indiv q.\nnode(q).\n\"," +
                                                         "\"deltaOffset\":\"0\",\"deltaReplaceLength\":\"0\"}}",
                                         Callback.NOOP
                         );
-                        case 5 -> session.close();
+                        case 8 -> session.close();
                         }
                 }
         }
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/ProblemWebInjectorProvider.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/ProblemWebInjectorProvider.java
index 4a5eed95..e9d889c4 100644
--- a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/ProblemWebInjectorProvider.java
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/ProblemWebInjectorProvider.java
@@ -34,6 +34,7 @@ public class ProblemWebInjectorProvider extends ProblemInjectorProvider {
                 // the tasks in the service and the {@link
                 // org.eclipse.xtext.testing.extensions.InjectionExtension}.
                 return new ProblemWebModule() {
+                        @Override
                         @SuppressWarnings("unused")
                         public Class<? extends ExecutorServiceProvider> bindExecutorServiceProvider() {
                                 return AwaitTerminationExecutorServiceProvider.class;
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/RestartableCachedThreadPool.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/RestartableCachedThreadPool.java
index 09079aa8..991ff114 100644
--- a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/RestartableCachedThreadPool.java
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/RestartableCachedThreadPool.java
@@ -35,7 +35,7 @@ public class RestartableCachedThreadPool implements ExecutorService {
         public void waitForTermination() {
                 boolean result = false;
                 try {
-                        result = delegate.awaitTermination(1, TimeUnit.SECONDS);
+                        result = delegate.awaitTermination(10, TimeUnit.SECONDS);
                 } catch (InterruptedException e) {
                         LOG.warn("Interrupted while waiting for delegate executor to stop", e);
                 }
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 841bacd3..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(2)).onResponse(captor.capture());
+                verify(responseHandler, times(4)).onResponse(captor.capture());
                 var newStateId = getStateId("bar", captor.getAllValues().get(0));
                 assertHighlightingResponse(newStateId, captor.getAllValues().get(1));
         }
@@ -126,7 +132,7 @@ class TransactionExecutorTest {
         private String updateFullText(ArgumentCaptor<XtextWebResponse> captor) throws ResponseHandlerException {
                 var responseHandler = sendRequestAndWaitForAllResponses(new XtextWebRequest("foo", UPDATE_FULL_TEXT_PARAMS));
 
-                verify(responseHandler, times(3)).onResponse(captor.capture());
+                verify(responseHandler, times(4)).onResponse(captor.capture());
                 return getStateId("foo", captor.getAllValues().get(0));
         }