feat: specify random seed for generation

4 files changed, 29 insertions, 6 deletions

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
index 5a60007f..9f72e462 100644
--- 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
@@ -34,13 +34,13 @@ public class ModelGenerationService {
                 timeoutSec = SemanticsService.getTimeout("REFINERY_MODEL_GENERATION_TIMEOUT_SEC").orElse(600L);
         }
 
-        public ModelGenerationStartedResult generateModel(PushWebDocumentAccess document){
+        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, timeoutSec);
+                                worker.setState(pushState, randomSeed, timeoutSec);
                                 var manager = pushState.getModelGenerationManager();
                                 worker.start();
                                 boolean canceled = manager.setActiveModelGenerationWorker(worker, cancelIndicator);
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
index 77fc7484..9ee74207 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
@@ -79,6 +79,8 @@ public class ModelGenerationWorker implements Runnable {
 
         private ScheduledExecutorService scheduledExecutorService;
 
+        private int randomSeed;
+
         private long timeoutSec;
 
         private Future<?> future;
@@ -97,8 +99,9 @@ public class ModelGenerationWorker implements Runnable {
                 scheduledExecutorService = provider.getScheduled(ModelGenerationService.MODEL_GENERATION_TIMEOUT_EXECUTOR);
         }
 
-        public void setState(PushWebDocument state, long timeoutSec) {
+        public void setState(PushWebDocument state, int randomSeed, long timeoutSec) {
                 this.state = state;
+                this.randomSeed = randomSeed;
                 this.timeoutSec = timeoutSec;
                 text = state.getText();
         }
@@ -188,7 +191,7 @@ public class ModelGenerationWorker implements Runnable {
                 cancellationToken.checkCancelled();
                 notifyResult(new ModelGenerationStatusResult(uuid, "Generating model"));
                 var bestFirst = new BestFirstStoreManager(store, 1);
-                bestFirst.startExploration(initialVersion);
+                bestFirst.startExploration(initialVersion, randomSeed);
                 cancellationToken.checkCancelled();
                 var solutionStore = bestFirst.getSolutionStore();
                 if (solutionStore.getSolutions().isEmpty()) {
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 625909b9..ff8f4943 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
@@ -9,6 +9,9 @@ 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;
@@ -25,6 +28,7 @@ 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);
 
@@ -33,6 +37,7 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
         private final int executorThreadCount;
         private final int lockExecutorThreadCount;
         private final int semanticsExecutorThreadCount;
+        private final int generatorExecutorThreadCount;
 
         static {
                 var lookup = MethodHandles.lookup();
@@ -57,7 +62,18 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
         public ThreadPoolExecutorServiceProvider() {
                 executorThreadCount = getCount("REFINERY_XTEXT_THREAD_COUNT").orElse(0);
                 lockExecutorThreadCount = getCount("REFINERY_XTEXT_LOCKING_THREAD_COUNT").orElse(executorThreadCount);
-                semanticsExecutorThreadCount = getCount("REFINERY_XTEXT_SEMANTICS_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) {
@@ -94,6 +110,8 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider {
         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 {
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 a04ee226..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
@@ -62,11 +62,13 @@ public class PushServiceDispatcher extends XtextServiceDispatcher {
                 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);
+                                        return modelGenerationService.generateModel(document, randomSeed);
                                 } else {
                                         return modelGenerationService.cancelModelGeneration(document);
                                 }