feat: connect model generator to UI

17 files changed, 580 insertions, 70 deletions

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..5a60007f
--- /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){
+                return document.modify(new CancelableUnitOfWork<>() {
+                        @Override
+                        public ModelGenerationStartedResult exec(IXtextWebDocument state, CancelIndicator cancelIndicator) {
+                                var pushState = (PushWebDocument) state;
+                                var worker = workerProvider.get();
+                                worker.setState(pushState, 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..1f430da6
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
@@ -0,0 +1,228 @@
+/*
+ * 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 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, long timeoutSec) {
+                this.state = state;
+                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());
+                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);
+                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());
+                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/SemanticsService.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java
index 26924f0a..331ef84b 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsService.java
@@ -54,7 +54,7 @@ public class SemanticsService extends AbstractCachedService<SemanticsResult> {
                 warmupTimeoutMs = getTimeout("REFINERY_SEMANTICS_WARMUP_TIMEOUT_MS").orElse(timeoutMs * 2);
         }
 
-        private static Optional<Long> getTimeout(String name) {
+        public static Optional<Long> getTimeout(String name) {
                 return Optional.ofNullable(System.getenv(name)).map(Long::parseUnsignedLong);
         }
 
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
index 33b1c4fb..512c2778 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
@@ -5,8 +5,6 @@
  */
 package tools.refinery.language.web.semantics;
 
-import com.google.gson.JsonArray;
-import com.google.gson.JsonObject;
 import com.google.inject.Inject;
 import org.eclipse.emf.common.util.Diagnostic;
 import org.eclipse.emf.ecore.EObject;
@@ -20,31 +18,24 @@ 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.SemanticsUtils;
 import tools.refinery.language.semantics.model.TracedException;
 import tools.refinery.store.dse.propagation.PropagationAdapter;
-import tools.refinery.store.map.Cursor;
-import tools.refinery.store.model.Model;
 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.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.TranslationException;
-import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
-import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.util.CancellationToken;
 
 import java.util.ArrayList;
-import java.util.TreeMap;
 import java.util.concurrent.Callable;
 
 class SemanticsWorker implements Callable<SemanticsResult> {
         private static final String DIAGNOSTIC_ID = "tools.refinery.language.semantics.SemanticError";
 
         @Inject
-        private SemanticsUtils semanticsUtils;
+        private PartialInterpretation2Json partialInterpretation2Json;
 
         @Inject
         private OperationCanceledManager operationCanceledManager;
@@ -93,7 +84,8 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                         cancellationToken.checkCancelled();
                         var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
                         cancellationToken.checkCancelled();
-                        var partialInterpretation = getPartialInterpretation(initializer, model);
+                        var partialInterpretation = partialInterpretation2Json.getPartialInterpretation(initializer, model,
+                                        Concreteness.PARTIAL, cancellationToken);
 
                         return new SemanticsSuccessResult(nodesMetadata, relationsMetadata, partialInterpretation);
                 } catch (TracedException e) {
@@ -104,55 +96,6 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                 }
         }
 
-        private JsonObject getPartialInterpretation(ModelInitializer initializer, Model model) {
-                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, 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, PartialRelation partialSymbol) {
-                var interpretation = adapter.getPartialInterpretation(Concreteness.PARTIAL, 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);
-        }
-
         private SemanticsResult getTracedErrorResult(EObject sourceElement, String message) {
                 if (sourceElement == null || !problem.eResource().equals(sourceElement.eResource())) {
                         return new SemanticsInternalErrorResult(message);
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
index ba26ff58..625909b9 100644
--- 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
@@ -13,9 +13,13 @@ 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;
 
@@ -24,6 +28,8 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
         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;
@@ -58,11 +64,15 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
                 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 + "-";
+                        name = name + "-" + key;
                 }
                 var threadFactory = new Factory(name, 5);
                 int size = getSize(key);
@@ -72,6 +82,15 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
                 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;
@@ -82,6 +101,17 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
                 }
         }
 
+        @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")
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 74456604..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
@@ -187,7 +187,7 @@ public class TransactionExecutor implements IDisposable, PrecomputationListener
                         var document = subscription.get();
                         if (document != null) {
                                 document.removePrecomputationListener(this);
-                                document.cancelBackgroundWork();
+                                document.dispose();
                         }
                 }
         }
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 d4a8c433..a04ee226 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,14 +5,17 @@
  */
 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;
 
@@ -21,6 +24,9 @@ public class PushServiceDispatcher extends XtextServiceDispatcher {
         @Inject
         private SemanticsService semanticsService;
 
+        @Inject
+        private ModelGenerationService modelGenerationService;
+
         @Override
         @Inject
         protected void registerPreComputedServices(PrecomputedServiceRegistry registry) {
@@ -37,4 +43,37 @@ 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");
+                }
+                var descriptor = new ServiceDescriptor();
+                descriptor.setService(() -> {
+                        try {
+                                if (start) {
+                                        return modelGenerationService.generateModel(document);
+                                } 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 2d43fb26..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
@@ -13,19 +13,18 @@ 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 tools.refinery.language.web.generator.ModelGenerationManager;
 import tools.refinery.language.web.xtext.server.ResponseHandlerException;
 
 import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.List;
-import java.util.Map;
 
 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;
 
@@ -34,6 +33,10 @@ public class PushWebDocument extends XtextWebDocument {
                 this.synchronizer = synchronizer;
         }
 
+        public ModelGenerationManager getModelGenerationManager() {
+                return modelGenerationManager;
+        }
+
         public void addPrecomputationListener(PrecomputationListener listener) {
                 synchronized (precomputationListeners) {
                         if (precomputationListeners.contains(listener)) {
@@ -52,15 +55,13 @@ public class PushWebDocument extends XtextWebDocument {
 
         public <T extends IServiceResult> void precomputeServiceResult(AbstractCachedService<T> service, String serviceName,
                         CancelIndicator cancelIndicator, boolean logCacheMiss) {
-                var serviceClass = service.getClass();
                 var result = getCachedServiceResult(service, cancelIndicator, logCacheMiss);
-                precomputedServices.put(serviceClass, result);
                 if (result != null) {
                         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;
@@ -86,7 +87,12 @@ public class PushWebDocument extends XtextWebDocument {
                 }
         }
 
-        public void cancelBackgroundWork() {
+        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 c72e8e67..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
@@ -74,4 +74,8 @@ public class PushWebDocumentAccess extends XtextWebDocumentAccess {
                 }
                 throw new IllegalArgumentException("Unknown precomputed service: " + service);
         }
+
+        public void cancelModelGeneration() {
+                pushDocument.cancelModelGeneration();
+        }
 }