feat: specify random seed for generation

13 files changed, 83 insertions, 25 deletions

diff --git a/subprojects/frontend/src/editor/AnimatedButton.tsx b/subprojects/frontend/src/editor/AnimatedButton.tsx
index 24ec69be..606aabea 100644
--- a/subprojects/frontend/src/editor/AnimatedButton.tsx
+++ b/subprojects/frontend/src/editor/AnimatedButton.tsx
@@ -45,7 +45,7 @@ export default function AnimatedButton({
   children,
 }: {
   'aria-label'?: string;
-  onClick?: () => void;
+  onClick?: React.MouseEventHandler<HTMLElement>;
   color: 'error' | 'warning' | 'primary' | 'inherit';
   disabled?: boolean;
   startIcon?: JSX.Element;
diff --git a/subprojects/frontend/src/editor/EditorStore.ts b/subprojects/frontend/src/editor/EditorStore.ts
index f9a9a7da..9508858d 100644
--- a/subprojects/frontend/src/editor/EditorStore.ts
+++ b/subprojects/frontend/src/editor/EditorStore.ts
@@ -313,14 +313,14 @@ export default class EditorStore {
     this.disposed = true;
   }
 
-  startModelGeneration(): void {
+  startModelGeneration(randomSeed?: number): void {
     this.client
-      ?.startModelGeneration()
+      ?.startModelGeneration(randomSeed)
       ?.catch((error) => log.error('Could not start model generation', error));
   }
 
-  addGeneratedModel(uuid: string): void {
-    this.generatedModels.set(uuid, new GeneratedModelStore());
+  addGeneratedModel(uuid: string, randomSeed: number): void {
+    this.generatedModels.set(uuid, new GeneratedModelStore(randomSeed));
     this.selectGeneratedModel(uuid);
   }
 
diff --git a/subprojects/frontend/src/editor/GenerateButton.tsx b/subprojects/frontend/src/editor/GenerateButton.tsx
index b8dcd531..b6b1655a 100644
--- a/subprojects/frontend/src/editor/GenerateButton.tsx
+++ b/subprojects/frontend/src/editor/GenerateButton.tsx
@@ -98,7 +98,13 @@ const GenerateButton = observer(function GenerateButton({
       disabled={!editorStore.opened}
       color={warningCount > 0 ? 'warning' : 'primary'}
       startIcon={<PlayArrowIcon />}
-      onClick={() => editorStore.startModelGeneration()}
+      onClick={(event) => {
+        if (event.shiftKey) {
+          editorStore.startModelGeneration(1);
+        } else {
+          editorStore.startModelGeneration();
+        }
+      }}
     >
       {summary === '' ? GENERATE_LABEL : `${GENERATE_LABEL} (${summary})`}
     </AnimatedButton>
diff --git a/subprojects/frontend/src/editor/GeneratedModelStore.ts b/subprojects/frontend/src/editor/GeneratedModelStore.ts
index d0181eed..5088d603 100644
--- a/subprojects/frontend/src/editor/GeneratedModelStore.ts
+++ b/subprojects/frontend/src/editor/GeneratedModelStore.ts
@@ -18,9 +18,9 @@ export default class GeneratedModelStore {
 
   graph: GraphStore | undefined;
 
-  constructor() {
+  constructor(randomSeed: number) {
     const time = new Date().toLocaleTimeString(undefined, { hour12: false });
-    this.title = `Generated at ${time}`;
+    this.title = `Generated at ${time} (${randomSeed})`;
     makeAutoObservable(this);
   }
 
diff --git a/subprojects/frontend/src/xtext/ModelGenerationService.ts b/subprojects/frontend/src/xtext/ModelGenerationService.ts
index 1e9f837a..29a70623 100644
--- a/subprojects/frontend/src/xtext/ModelGenerationService.ts
+++ b/subprojects/frontend/src/xtext/ModelGenerationService.ts
@@ -4,12 +4,18 @@
  * SPDX-License-Identifier: EPL-2.0
  */
 
+import type { Transaction } from '@codemirror/state';
+
 import type EditorStore from '../editor/EditorStore';
 
 import type UpdateService from './UpdateService';
 import { ModelGenerationResult } from './xtextServiceResults';
 
+const INITIAL_RANDOM_SEED = 1;
+
 export default class ModelGenerationService {
+  private nextRandomSeed = INITIAL_RANDOM_SEED;
+
   constructor(
     private readonly store: EditorStore,
     private readonly updateService: UpdateService,
@@ -26,14 +32,24 @@ export default class ModelGenerationService {
     }
   }
 
+  onTransaction(transaction: Transaction): void {
+    if (transaction.docChanged) {
+      this.resetRandomSeed();
+    }
+  }
+
   onDisconnect(): void {
     this.store.modelGenerationCancelled();
+    this.resetRandomSeed();
   }
 
-  async start(): Promise<void> {
-    const result = await this.updateService.startModelGeneration();
+  async start(randomSeed?: number): Promise<void> {
+    const randomSeedOrNext = randomSeed ?? this.nextRandomSeed;
+    this.nextRandomSeed = randomSeedOrNext + 1;
+    const result =
+      await this.updateService.startModelGeneration(randomSeedOrNext);
     if (!result.cancelled) {
-      this.store.addGeneratedModel(result.data.uuid);
+      this.store.addGeneratedModel(result.data.uuid, randomSeedOrNext);
     }
   }
 
@@ -43,4 +59,8 @@ export default class ModelGenerationService {
       this.store.modelGenerationCancelled();
     }
   }
+
+  private resetRandomSeed() {
+    this.nextRandomSeed = INITIAL_RANDOM_SEED;
+  }
 }
diff --git a/subprojects/frontend/src/xtext/UpdateService.ts b/subprojects/frontend/src/xtext/UpdateService.ts
index d1246d5e..70e79764 100644
--- a/subprojects/frontend/src/xtext/UpdateService.ts
+++ b/subprojects/frontend/src/xtext/UpdateService.ts
@@ -343,9 +343,9 @@ export default class UpdateService {
     return { cancelled: false, data: parsedOccurrencesResult };
   }
 
-  async startModelGeneration(): Promise<
-    CancellableResult<ModelGenerationStartedResult>
-  > {
+  async startModelGeneration(
+    randomSeed: number,
+  ): Promise<CancellableResult<ModelGenerationStartedResult>> {
     try {
       await this.updateOrThrow();
     } catch (error) {
@@ -360,6 +360,7 @@ export default class UpdateService {
       serviceType: 'modelGeneration',
       requiredStateId: this.xtextStateId,
       start: true,
+      randomSeed,
     });
     if (isConflictResult(data)) {
       return { cancelled: true };
diff --git a/subprojects/frontend/src/xtext/XtextClient.ts b/subprojects/frontend/src/xtext/XtextClient.ts
index 4df4f57a..7486d737 100644
--- a/subprojects/frontend/src/xtext/XtextClient.ts
+++ b/subprojects/frontend/src/xtext/XtextClient.ts
@@ -99,6 +99,7 @@ export default class XtextClient {
     this.contentAssistService.onTransaction(transaction);
     this.updateService.onTransaction(transaction);
     this.occurrencesService.onTransaction(transaction);
+    this.modelGenerationService.onTransaction(transaction);
   }
 
   private onPush(
@@ -150,8 +151,8 @@ export default class XtextClient {
     return this.contentAssistService.contentAssist(context);
   }
 
-  startModelGeneration(): Promise<void> {
-    return this.modelGenerationService.start();
+  startModelGeneration(randomSeed?: number): Promise<void> {
+    return this.modelGenerationService.start(randomSeed);
   }
 
   cancelModelGeneration(): Promise<void> {
diff --git a/subprojects/frontend/src/xtext/XtextWebSocketClient.ts b/subprojects/frontend/src/xtext/XtextWebSocketClient.ts
index bb84223c..280ac875 100644
--- a/subprojects/frontend/src/xtext/XtextWebSocketClient.ts
+++ b/subprojects/frontend/src/xtext/XtextWebSocketClient.ts
@@ -204,7 +204,7 @@ export default class XtextWebSocketClient {
 
   get state() {
     this.stateAtom.reportObserved();
-    return this.interpreter.state;
+    return this.interpreter.getSnapshot();
   }
 
   get opening(): boolean {
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);
                                 }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
index 02634a02..3d32f84c 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
@@ -44,11 +44,13 @@ public class BestFirstStoreManager {
                 equivalenceClassStore = new FastEquivalenceClassStore(modelStore.getAdapter(StateCoderStoreAdapter.class)) {
                         @Override
                         protected void delegate(VersionWithObjectiveValue version, int[] emptyActivations, boolean accept) {
-                                throw new UnsupportedOperationException("This equivalence storage is not prepared to resolve symmetries!");
+                                throw new UnsupportedOperationException("This equivalence storage is not prepared to resolve " +
+                                                "symmetries!");
                         }
                 };
                 visualizationStore = new VisualizationStoreImpl();
         }
+
         public ModelStore getModelStore() {
                 return modelStore;
         }
@@ -74,7 +76,12 @@ public class BestFirstStoreManager {
         }
 
         public void startExploration(Version initial) {
-                BestFirstExplorer bestFirstExplorer = new BestFirstExplorer(this, modelStore.createModelForState(initial), 1);
+                startExploration(initial, 1);
+        }
+
+        public void startExploration(Version initial, int randomSeed) {
+                BestFirstExplorer bestFirstExplorer = new BestFirstExplorer(this, modelStore.createModelForState(initial),
+                                randomSeed);
                 bestFirstExplorer.explore();
         }
 }