From a2a4696fdbd6440269d576aeba7b25b2ea40d9bf Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 12 Sep 2023 21:59:50 +0200 Subject: feat: connect model generator to UI --- .../generator/ModelGenerationCancelledResult.java | 11 + .../web/generator/ModelGenerationErrorResult.java | 11 + .../web/generator/ModelGenerationManager.java | 41 ++++ .../web/generator/ModelGenerationResult.java | 15 ++ .../web/generator/ModelGenerationService.java | 60 ++++++ .../generator/ModelGenerationStartedResult.java | 13 ++ .../web/generator/ModelGenerationStatusResult.java | 11 + .../generator/ModelGenerationSuccessResult.java | 17 ++ .../web/generator/ModelGenerationWorker.java | 228 +++++++++++++++++++++ .../web/semantics/PartialInterpretation2Json.java | 81 ++++++++ .../language/web/semantics/SemanticsService.java | 2 +- .../language/web/semantics/SemanticsWorker.java | 63 +----- .../server/ThreadPoolExecutorServiceProvider.java | 32 ++- .../web/xtext/server/TransactionExecutor.java | 2 +- .../xtext/server/push/PushServiceDispatcher.java | 39 ++++ .../web/xtext/server/push/PushWebDocument.java | 20 +- .../xtext/server/push/PushWebDocumentAccess.java | 4 + 17 files changed, 580 insertions(+), 70 deletions(-) create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationCancelledResult.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationErrorResult.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationManager.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationResult.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationService.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStartedResult.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationStatusResult.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationSuccessResult.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java create mode 100644 subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java (limited to 'subprojects/language-web') 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 + * + * 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 + * + * 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 + * + * 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 + * + * 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 + * + * 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 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 + * + * 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 + * + * 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 + * + * 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 nodes, List 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 + * + * 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 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 + * + * 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 cursor) { + var map = new TreeMap(); + 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 { warmupTimeoutMs = getTimeout("REFINERY_SEMANTICS_WARMUP_TIMEOUT_MS").orElse(timeoutMs * 2); } - private static Optional getTimeout(String name) { + public static Optional 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 { 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 { 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 { } } - 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 cursor) { - var map = new TreeMap(); - 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 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 precomputationListeners = new ArrayList<>(); - private final Map, 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 void precomputeServiceResult(AbstractCachedService 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 void notifyPrecomputationListeners(String serviceName, T result) { + public 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(); + } } -- cgit v1.2.3-54-g00ecf