From a3f1e6872f4f768d14899a1e70bbdc14f32e478d Mon Sep 17 00:00:00 2001
From: Kristóf Marussy <kristof@marussy.com>
Date: Sun, 20 Aug 2023 19:41:32 +0200
Subject: feat: improve semantics error reporting

Also makes model seeds cancellable to reduce server load during semantic
analysis.
---
 subprojects/frontend/src/editor/AnimatedButton.tsx | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'subprojects/frontend/src/editor/AnimatedButton.tsx')

diff --git a/subprojects/frontend/src/editor/AnimatedButton.tsx b/subprojects/frontend/src/editor/AnimatedButton.tsx
index dbbda618..24ec69be 100644
--- a/subprojects/frontend/src/editor/AnimatedButton.tsx
+++ b/subprojects/frontend/src/editor/AnimatedButton.tsx
@@ -48,7 +48,7 @@ export default function AnimatedButton({
   onClick?: () => void;
   color: 'error' | 'warning' | 'primary' | 'inherit';
   disabled?: boolean;
-  startIcon: JSX.Element;
+  startIcon?: JSX.Element;
   sx?: SxProps<Theme> | undefined;
   children?: ReactNode;
 }): JSX.Element {
@@ -79,7 +79,11 @@ export default function AnimatedButton({
       className="rounded shaded"
       disabled={disabled ?? false}
       startIcon={startIcon}
-      width={width === undefined ? 'auto' : `calc(${width} + 50px)`}
+      width={
+        width === undefined
+          ? 'auto'
+          : `calc(${width} + ${startIcon === undefined ? 28 : 50}px)`
+      }
     >
       <Box
         display="flex"
@@ -100,6 +104,7 @@ AnimatedButton.defaultProps = {
   'aria-label': undefined,
   onClick: undefined,
   disabled: false,
+  startIcon: undefined,
   sx: undefined,
   children: undefined,
 };
-- 
cgit v1.2.3-54-g00ecf


From 13b464db253566290be6a1063ad8e296288d3339 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy <kristof@marussy.com>
Date: Thu, 14 Sep 2023 03:05:28 +0200
Subject: feat: specify random seed for generation

---
 subprojects/frontend/src/editor/AnimatedButton.tsx |  2 +-
 subprojects/frontend/src/editor/EditorStore.ts     |  8 +++----
 subprojects/frontend/src/editor/GenerateButton.tsx |  8 ++++++-
 .../frontend/src/editor/GeneratedModelStore.ts     |  4 ++--
 .../frontend/src/xtext/ModelGenerationService.ts   | 26 +++++++++++++++++++---
 subprojects/frontend/src/xtext/UpdateService.ts    |  7 +++---
 subprojects/frontend/src/xtext/XtextClient.ts      |  5 +++--
 .../frontend/src/xtext/XtextWebSocketClient.ts     |  2 +-
 .../web/generator/ModelGenerationService.java      |  4 ++--
 .../web/generator/ModelGenerationWorker.java       |  7 ++++--
 .../server/ThreadPoolExecutorServiceProvider.java  | 20 ++++++++++++++++-
 .../xtext/server/push/PushServiceDispatcher.java   |  4 +++-
 .../store/dse/strategy/BestFirstStoreManager.java  | 11 +++++++--
 13 files changed, 83 insertions(+), 25 deletions(-)

(limited to 'subprojects/frontend/src/editor/AnimatedButton.tsx')

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();
 	}
 }
-- 
cgit v1.2.3-54-g00ecf

