From a3f1e6872f4f768d14899a1e70bbdc14f32e478d Mon Sep 17 00:00:00 2001 From: Kristóf Marussy 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 | 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)` + } > 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; 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={} - onClick={() => editorStore.startModelGeneration()} + onClick={(event) => { + if (event.shiftKey) { + editorStore.startModelGeneration(1); + } else { + editorStore.startModelGeneration(); + } + }} > {summary === '' ? GENERATE_LABEL : `${GENERATE_LABEL} (${summary})`} 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 { - const result = await this.updateService.startModelGeneration(); + async start(randomSeed?: number): Promise { + 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 - > { + async startModelGeneration( + randomSeed: number, + ): Promise> { 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 { - return this.modelGenerationService.start(); + startModelGeneration(randomSeed?: number): Promise { + return this.modelGenerationService.start(randomSeed); } cancelModelGeneration(): Promise { 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 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