diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-09-14 03:05:28 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-09-14 03:43:26 +0200 |
commit | 13b464db253566290be6a1063ad8e296288d3339 (patch) | |
tree | 29e0a9a346f66974d6c0be0482f511e9becab51c /subprojects | |
parent | fix(frontend): keep live while model generation (diff) | |
download | refinery-13b464db253566290be6a1063ad8e296288d3339.tar.gz refinery-13b464db253566290be6a1063ad8e296288d3339.tar.zst refinery-13b464db253566290be6a1063ad8e296288d3339.zip |
feat: specify random seed for generation
Diffstat (limited to 'subprojects')
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({ | |||
45 | children, | 45 | children, |
46 | }: { | 46 | }: { |
47 | 'aria-label'?: string; | 47 | 'aria-label'?: string; |
48 | onClick?: () => void; | 48 | onClick?: React.MouseEventHandler<HTMLElement>; |
49 | color: 'error' | 'warning' | 'primary' | 'inherit'; | 49 | color: 'error' | 'warning' | 'primary' | 'inherit'; |
50 | disabled?: boolean; | 50 | disabled?: boolean; |
51 | startIcon?: JSX.Element; | 51 | 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 { | |||
313 | this.disposed = true; | 313 | this.disposed = true; |
314 | } | 314 | } |
315 | 315 | ||
316 | startModelGeneration(): void { | 316 | startModelGeneration(randomSeed?: number): void { |
317 | this.client | 317 | this.client |
318 | ?.startModelGeneration() | 318 | ?.startModelGeneration(randomSeed) |
319 | ?.catch((error) => log.error('Could not start model generation', error)); | 319 | ?.catch((error) => log.error('Could not start model generation', error)); |
320 | } | 320 | } |
321 | 321 | ||
322 | addGeneratedModel(uuid: string): void { | 322 | addGeneratedModel(uuid: string, randomSeed: number): void { |
323 | this.generatedModels.set(uuid, new GeneratedModelStore()); | 323 | this.generatedModels.set(uuid, new GeneratedModelStore(randomSeed)); |
324 | this.selectGeneratedModel(uuid); | 324 | this.selectGeneratedModel(uuid); |
325 | } | 325 | } |
326 | 326 | ||
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({ | |||
98 | disabled={!editorStore.opened} | 98 | disabled={!editorStore.opened} |
99 | color={warningCount > 0 ? 'warning' : 'primary'} | 99 | color={warningCount > 0 ? 'warning' : 'primary'} |
100 | startIcon={<PlayArrowIcon />} | 100 | startIcon={<PlayArrowIcon />} |
101 | onClick={() => editorStore.startModelGeneration()} | 101 | onClick={(event) => { |
102 | if (event.shiftKey) { | ||
103 | editorStore.startModelGeneration(1); | ||
104 | } else { | ||
105 | editorStore.startModelGeneration(); | ||
106 | } | ||
107 | }} | ||
102 | > | 108 | > |
103 | {summary === '' ? GENERATE_LABEL : `${GENERATE_LABEL} (${summary})`} | 109 | {summary === '' ? GENERATE_LABEL : `${GENERATE_LABEL} (${summary})`} |
104 | </AnimatedButton> | 110 | </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 { | |||
18 | 18 | ||
19 | graph: GraphStore | undefined; | 19 | graph: GraphStore | undefined; |
20 | 20 | ||
21 | constructor() { | 21 | constructor(randomSeed: number) { |
22 | const time = new Date().toLocaleTimeString(undefined, { hour12: false }); | 22 | const time = new Date().toLocaleTimeString(undefined, { hour12: false }); |
23 | this.title = `Generated at ${time}`; | 23 | this.title = `Generated at ${time} (${randomSeed})`; |
24 | makeAutoObservable(this); | 24 | makeAutoObservable(this); |
25 | } | 25 | } |
26 | 26 | ||
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 @@ | |||
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | 6 | ||
7 | import type { Transaction } from '@codemirror/state'; | ||
8 | |||
7 | import type EditorStore from '../editor/EditorStore'; | 9 | import type EditorStore from '../editor/EditorStore'; |
8 | 10 | ||
9 | import type UpdateService from './UpdateService'; | 11 | import type UpdateService from './UpdateService'; |
10 | import { ModelGenerationResult } from './xtextServiceResults'; | 12 | import { ModelGenerationResult } from './xtextServiceResults'; |
11 | 13 | ||
14 | const INITIAL_RANDOM_SEED = 1; | ||
15 | |||
12 | export default class ModelGenerationService { | 16 | export default class ModelGenerationService { |
17 | private nextRandomSeed = INITIAL_RANDOM_SEED; | ||
18 | |||
13 | constructor( | 19 | constructor( |
14 | private readonly store: EditorStore, | 20 | private readonly store: EditorStore, |
15 | private readonly updateService: UpdateService, | 21 | private readonly updateService: UpdateService, |
@@ -26,14 +32,24 @@ export default class ModelGenerationService { | |||
26 | } | 32 | } |
27 | } | 33 | } |
28 | 34 | ||
35 | onTransaction(transaction: Transaction): void { | ||
36 | if (transaction.docChanged) { | ||
37 | this.resetRandomSeed(); | ||
38 | } | ||
39 | } | ||
40 | |||
29 | onDisconnect(): void { | 41 | onDisconnect(): void { |
30 | this.store.modelGenerationCancelled(); | 42 | this.store.modelGenerationCancelled(); |
43 | this.resetRandomSeed(); | ||
31 | } | 44 | } |
32 | 45 | ||
33 | async start(): Promise<void> { | 46 | async start(randomSeed?: number): Promise<void> { |
34 | const result = await this.updateService.startModelGeneration(); | 47 | const randomSeedOrNext = randomSeed ?? this.nextRandomSeed; |
48 | this.nextRandomSeed = randomSeedOrNext + 1; | ||
49 | const result = | ||
50 | await this.updateService.startModelGeneration(randomSeedOrNext); | ||
35 | if (!result.cancelled) { | 51 | if (!result.cancelled) { |
36 | this.store.addGeneratedModel(result.data.uuid); | 52 | this.store.addGeneratedModel(result.data.uuid, randomSeedOrNext); |
37 | } | 53 | } |
38 | } | 54 | } |
39 | 55 | ||
@@ -43,4 +59,8 @@ export default class ModelGenerationService { | |||
43 | this.store.modelGenerationCancelled(); | 59 | this.store.modelGenerationCancelled(); |
44 | } | 60 | } |
45 | } | 61 | } |
62 | |||
63 | private resetRandomSeed() { | ||
64 | this.nextRandomSeed = INITIAL_RANDOM_SEED; | ||
65 | } | ||
46 | } | 66 | } |
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 { | |||
343 | return { cancelled: false, data: parsedOccurrencesResult }; | 343 | return { cancelled: false, data: parsedOccurrencesResult }; |
344 | } | 344 | } |
345 | 345 | ||
346 | async startModelGeneration(): Promise< | 346 | async startModelGeneration( |
347 | CancellableResult<ModelGenerationStartedResult> | 347 | randomSeed: number, |
348 | > { | 348 | ): Promise<CancellableResult<ModelGenerationStartedResult>> { |
349 | try { | 349 | try { |
350 | await this.updateOrThrow(); | 350 | await this.updateOrThrow(); |
351 | } catch (error) { | 351 | } catch (error) { |
@@ -360,6 +360,7 @@ export default class UpdateService { | |||
360 | serviceType: 'modelGeneration', | 360 | serviceType: 'modelGeneration', |
361 | requiredStateId: this.xtextStateId, | 361 | requiredStateId: this.xtextStateId, |
362 | start: true, | 362 | start: true, |
363 | randomSeed, | ||
363 | }); | 364 | }); |
364 | if (isConflictResult(data)) { | 365 | if (isConflictResult(data)) { |
365 | return { cancelled: true }; | 366 | 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 { | |||
99 | this.contentAssistService.onTransaction(transaction); | 99 | this.contentAssistService.onTransaction(transaction); |
100 | this.updateService.onTransaction(transaction); | 100 | this.updateService.onTransaction(transaction); |
101 | this.occurrencesService.onTransaction(transaction); | 101 | this.occurrencesService.onTransaction(transaction); |
102 | this.modelGenerationService.onTransaction(transaction); | ||
102 | } | 103 | } |
103 | 104 | ||
104 | private onPush( | 105 | private onPush( |
@@ -150,8 +151,8 @@ export default class XtextClient { | |||
150 | return this.contentAssistService.contentAssist(context); | 151 | return this.contentAssistService.contentAssist(context); |
151 | } | 152 | } |
152 | 153 | ||
153 | startModelGeneration(): Promise<void> { | 154 | startModelGeneration(randomSeed?: number): Promise<void> { |
154 | return this.modelGenerationService.start(); | 155 | return this.modelGenerationService.start(randomSeed); |
155 | } | 156 | } |
156 | 157 | ||
157 | cancelModelGeneration(): Promise<void> { | 158 | 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 { | |||
204 | 204 | ||
205 | get state() { | 205 | get state() { |
206 | this.stateAtom.reportObserved(); | 206 | this.stateAtom.reportObserved(); |
207 | return this.interpreter.state; | 207 | return this.interpreter.getSnapshot(); |
208 | } | 208 | } |
209 | 209 | ||
210 | get opening(): boolean { | 210 | 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 { | |||
34 | timeoutSec = SemanticsService.getTimeout("REFINERY_MODEL_GENERATION_TIMEOUT_SEC").orElse(600L); | 34 | timeoutSec = SemanticsService.getTimeout("REFINERY_MODEL_GENERATION_TIMEOUT_SEC").orElse(600L); |
35 | } | 35 | } |
36 | 36 | ||
37 | public ModelGenerationStartedResult generateModel(PushWebDocumentAccess document){ | 37 | public ModelGenerationStartedResult generateModel(PushWebDocumentAccess document, int randomSeed) { |
38 | return document.modify(new CancelableUnitOfWork<>() { | 38 | return document.modify(new CancelableUnitOfWork<>() { |
39 | @Override | 39 | @Override |
40 | public ModelGenerationStartedResult exec(IXtextWebDocument state, CancelIndicator cancelIndicator) { | 40 | public ModelGenerationStartedResult exec(IXtextWebDocument state, CancelIndicator cancelIndicator) { |
41 | var pushState = (PushWebDocument) state; | 41 | var pushState = (PushWebDocument) state; |
42 | var worker = workerProvider.get(); | 42 | var worker = workerProvider.get(); |
43 | worker.setState(pushState, timeoutSec); | 43 | worker.setState(pushState, randomSeed, timeoutSec); |
44 | var manager = pushState.getModelGenerationManager(); | 44 | var manager = pushState.getModelGenerationManager(); |
45 | worker.start(); | 45 | worker.start(); |
46 | boolean canceled = manager.setActiveModelGenerationWorker(worker, cancelIndicator); | 46 | 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 { | |||
79 | 79 | ||
80 | private ScheduledExecutorService scheduledExecutorService; | 80 | private ScheduledExecutorService scheduledExecutorService; |
81 | 81 | ||
82 | private int randomSeed; | ||
83 | |||
82 | private long timeoutSec; | 84 | private long timeoutSec; |
83 | 85 | ||
84 | private Future<?> future; | 86 | private Future<?> future; |
@@ -97,8 +99,9 @@ public class ModelGenerationWorker implements Runnable { | |||
97 | scheduledExecutorService = provider.getScheduled(ModelGenerationService.MODEL_GENERATION_TIMEOUT_EXECUTOR); | 99 | scheduledExecutorService = provider.getScheduled(ModelGenerationService.MODEL_GENERATION_TIMEOUT_EXECUTOR); |
98 | } | 100 | } |
99 | 101 | ||
100 | public void setState(PushWebDocument state, long timeoutSec) { | 102 | public void setState(PushWebDocument state, int randomSeed, long timeoutSec) { |
101 | this.state = state; | 103 | this.state = state; |
104 | this.randomSeed = randomSeed; | ||
102 | this.timeoutSec = timeoutSec; | 105 | this.timeoutSec = timeoutSec; |
103 | text = state.getText(); | 106 | text = state.getText(); |
104 | } | 107 | } |
@@ -188,7 +191,7 @@ public class ModelGenerationWorker implements Runnable { | |||
188 | cancellationToken.checkCancelled(); | 191 | cancellationToken.checkCancelled(); |
189 | notifyResult(new ModelGenerationStatusResult(uuid, "Generating model")); | 192 | notifyResult(new ModelGenerationStatusResult(uuid, "Generating model")); |
190 | var bestFirst = new BestFirstStoreManager(store, 1); | 193 | var bestFirst = new BestFirstStoreManager(store, 1); |
191 | bestFirst.startExploration(initialVersion); | 194 | bestFirst.startExploration(initialVersion, randomSeed); |
192 | cancellationToken.checkCancelled(); | 195 | cancellationToken.checkCancelled(); |
193 | var solutionStore = bestFirst.getSolutionStore(); | 196 | var solutionStore = bestFirst.getSolutionStore(); |
194 | if (solutionStore.getSolutions().isEmpty()) { | 197 | 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; | |||
9 | import org.eclipse.xtext.ide.ExecutorServiceProvider; | 9 | import org.eclipse.xtext.ide.ExecutorServiceProvider; |
10 | import org.eclipse.xtext.web.server.model.XtextWebDocumentAccess; | 10 | import org.eclipse.xtext.web.server.model.XtextWebDocumentAccess; |
11 | import org.jetbrains.annotations.NotNull; | 11 | import org.jetbrains.annotations.NotNull; |
12 | import org.slf4j.Logger; | ||
13 | import org.slf4j.LoggerFactory; | ||
14 | import tools.refinery.language.web.generator.ModelGenerationService; | ||
12 | import tools.refinery.language.web.semantics.SemanticsService; | 15 | import tools.refinery.language.web.semantics.SemanticsService; |
13 | 16 | ||
14 | import java.lang.invoke.MethodHandle; | 17 | import java.lang.invoke.MethodHandle; |
@@ -25,6 +28,7 @@ import java.util.concurrent.atomic.AtomicInteger; | |||
25 | 28 | ||
26 | @Singleton | 29 | @Singleton |
27 | public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider { | 30 | public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider { |
31 | private static final Logger LOG = LoggerFactory.getLogger(ThreadPoolExecutorServiceProvider.class); | ||
28 | private static final String DOCUMENT_LOCK_EXECUTOR; | 32 | private static final String DOCUMENT_LOCK_EXECUTOR; |
29 | private static final AtomicInteger POOL_ID = new AtomicInteger(1); | 33 | private static final AtomicInteger POOL_ID = new AtomicInteger(1); |
30 | 34 | ||
@@ -33,6 +37,7 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider { | |||
33 | private final int executorThreadCount; | 37 | private final int executorThreadCount; |
34 | private final int lockExecutorThreadCount; | 38 | private final int lockExecutorThreadCount; |
35 | private final int semanticsExecutorThreadCount; | 39 | private final int semanticsExecutorThreadCount; |
40 | private final int generatorExecutorThreadCount; | ||
36 | 41 | ||
37 | static { | 42 | static { |
38 | var lookup = MethodHandles.lookup(); | 43 | var lookup = MethodHandles.lookup(); |
@@ -57,7 +62,18 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider { | |||
57 | public ThreadPoolExecutorServiceProvider() { | 62 | public ThreadPoolExecutorServiceProvider() { |
58 | executorThreadCount = getCount("REFINERY_XTEXT_THREAD_COUNT").orElse(0); | 63 | executorThreadCount = getCount("REFINERY_XTEXT_THREAD_COUNT").orElse(0); |
59 | lockExecutorThreadCount = getCount("REFINERY_XTEXT_LOCKING_THREAD_COUNT").orElse(executorThreadCount); | 64 | lockExecutorThreadCount = getCount("REFINERY_XTEXT_LOCKING_THREAD_COUNT").orElse(executorThreadCount); |
60 | semanticsExecutorThreadCount = getCount("REFINERY_XTEXT_SEMANTICS_THREAD_COUNT").orElse(executorThreadCount); | 65 | int semanticsCount = getCount("REFINERY_XTEXT_SEMANTICS_THREAD_COUNT").orElse(0); |
66 | if (semanticsCount == 0 || executorThreadCount == 0) { | ||
67 | semanticsExecutorThreadCount = 0; | ||
68 | } else { | ||
69 | semanticsExecutorThreadCount = Math.max(semanticsCount, executorThreadCount); | ||
70 | } | ||
71 | if (semanticsExecutorThreadCount != semanticsCount) { | ||
72 | LOG.warn("Setting REFINERY_XTEXT_SEMANTICS_THREAD_COUNT to {} to avoid deadlock. This value must be " + | ||
73 | "either 0 or at least as large as REFINERY_XTEXT_THREAD_COUNT to avoid lock contention.", | ||
74 | semanticsExecutorThreadCount); | ||
75 | } | ||
76 | generatorExecutorThreadCount = getCount("REFINERY_MODEL_GENERATION_THREAD_COUNT").orElse(executorThreadCount); | ||
61 | } | 77 | } |
62 | 78 | ||
63 | private static Optional<Integer> getCount(String name) { | 79 | private static Optional<Integer> getCount(String name) { |
@@ -94,6 +110,8 @@ public class ThreadPoolExecutorServiceProvider extends ExecutorServiceProvider { | |||
94 | private int getSize(String key) { | 110 | private int getSize(String key) { |
95 | if (SemanticsService.SEMANTICS_EXECUTOR.equals(key)) { | 111 | if (SemanticsService.SEMANTICS_EXECUTOR.equals(key)) { |
96 | return semanticsExecutorThreadCount; | 112 | return semanticsExecutorThreadCount; |
113 | } else if (ModelGenerationService.MODEL_GENERATION_EXECUTOR.equals(key)) { | ||
114 | return generatorExecutorThreadCount; | ||
97 | } else if (DOCUMENT_LOCK_EXECUTOR.equals(key)) { | 115 | } else if (DOCUMENT_LOCK_EXECUTOR.equals(key)) { |
98 | return lockExecutorThreadCount; | 116 | return lockExecutorThreadCount; |
99 | } else { | 117 | } 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 { | |||
62 | if (!start && !cancel) { | 62 | if (!start && !cancel) { |
63 | throw new InvalidRequestException("Either start of cancel must be specified"); | 63 | throw new InvalidRequestException("Either start of cancel must be specified"); |
64 | } | 64 | } |
65 | @SuppressWarnings({"squid:S4738"}) | ||
66 | int randomSeed = start ? getInt(context, "randomSeed", Optional.absent()) : 0; | ||
65 | var descriptor = new ServiceDescriptor(); | 67 | var descriptor = new ServiceDescriptor(); |
66 | descriptor.setService(() -> { | 68 | descriptor.setService(() -> { |
67 | try { | 69 | try { |
68 | if (start) { | 70 | if (start) { |
69 | return modelGenerationService.generateModel(document); | 71 | return modelGenerationService.generateModel(document, randomSeed); |
70 | } else { | 72 | } else { |
71 | return modelGenerationService.cancelModelGeneration(document); | 73 | return modelGenerationService.cancelModelGeneration(document); |
72 | } | 74 | } |
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 { | |||
44 | equivalenceClassStore = new FastEquivalenceClassStore(modelStore.getAdapter(StateCoderStoreAdapter.class)) { | 44 | equivalenceClassStore = new FastEquivalenceClassStore(modelStore.getAdapter(StateCoderStoreAdapter.class)) { |
45 | @Override | 45 | @Override |
46 | protected void delegate(VersionWithObjectiveValue version, int[] emptyActivations, boolean accept) { | 46 | protected void delegate(VersionWithObjectiveValue version, int[] emptyActivations, boolean accept) { |
47 | throw new UnsupportedOperationException("This equivalence storage is not prepared to resolve symmetries!"); | 47 | throw new UnsupportedOperationException("This equivalence storage is not prepared to resolve " + |
48 | "symmetries!"); | ||
48 | } | 49 | } |
49 | }; | 50 | }; |
50 | visualizationStore = new VisualizationStoreImpl(); | 51 | visualizationStore = new VisualizationStoreImpl(); |
51 | } | 52 | } |
53 | |||
52 | public ModelStore getModelStore() { | 54 | public ModelStore getModelStore() { |
53 | return modelStore; | 55 | return modelStore; |
54 | } | 56 | } |
@@ -74,7 +76,12 @@ public class BestFirstStoreManager { | |||
74 | } | 76 | } |
75 | 77 | ||
76 | public void startExploration(Version initial) { | 78 | public void startExploration(Version initial) { |
77 | BestFirstExplorer bestFirstExplorer = new BestFirstExplorer(this, modelStore.createModelForState(initial), 1); | 79 | startExploration(initial, 1); |
80 | } | ||
81 | |||
82 | public void startExploration(Version initial, int randomSeed) { | ||
83 | BestFirstExplorer bestFirstExplorer = new BestFirstExplorer(this, modelStore.createModelForState(initial), | ||
84 | randomSeed); | ||
78 | bestFirstExplorer.explore(); | 85 | bestFirstExplorer.explore(); |
79 | } | 86 | } |
80 | } | 87 | } |