diff options
author | 2024-07-09 21:17:59 +0200 | |
---|---|---|
committer | 2024-07-10 00:11:07 +0200 | |
commit | bf3b06f8cc775216e69e7f3e14d595a1db244f05 (patch) | |
tree | bfb6511e249cbe07d5cb183b42dac11cda9f94f7 | |
parent | build: do not build shadow jars (diff) | |
download | refinery-bf3b06f8cc775216e69e7f3e14d595a1db244f05.tar.gz refinery-bf3b06f8cc775216e69e7f3e14d595a1db244f05.tar.zst refinery-bf3b06f8cc775216e69e7f3e14d595a1db244f05.zip |
feat: generator facade timeout and non-existent objects
Quality of life improvements for the semantics and generator facade APIs.
17 files changed, 356 insertions, 54 deletions
diff --git a/subprojects/frontend/src/graph/GraphStore.ts b/subprojects/frontend/src/graph/GraphStore.ts index 86ffd802..30d0a2f3 100644 --- a/subprojects/frontend/src/graph/GraphStore.ts +++ b/subprojects/frontend/src/graph/GraphStore.ts | |||
@@ -233,4 +233,9 @@ export default class GraphStore { | |||
233 | get name(): string { | 233 | get name(): string { |
234 | return this.nameOverride ?? this.editorStore.simpleNameOrFallback; | 234 | return this.nameOverride ?? this.editorStore.simpleNameOrFallback; |
235 | } | 235 | } |
236 | |||
237 | get showNonExistent(): boolean { | ||
238 | const existsVisibility = this.visibility.get('builtin::exists') ?? 'none'; | ||
239 | return existsVisibility !== 'none' || this.scopes; | ||
240 | } | ||
236 | } | 241 | } |
diff --git a/subprojects/frontend/src/graph/GraphTheme.tsx b/subprojects/frontend/src/graph/GraphTheme.tsx index bdc01b78..1127a46d 100644 --- a/subprojects/frontend/src/graph/GraphTheme.tsx +++ b/subprojects/frontend/src/graph/GraphTheme.tsx | |||
@@ -143,6 +143,21 @@ export function createGraphTheme({ | |||
143 | 'text.label-ERROR': { | 143 | 'text.label-ERROR': { |
144 | fill: theme.palette.error.main, | 144 | fill: theme.palette.error.main, |
145 | }, | 145 | }, |
146 | '.node-exists-FALSE': { | ||
147 | 'text:not(.label-ERROR)': { | ||
148 | fill: theme.palette.text.secondary, | ||
149 | }, | ||
150 | '.node-outline': { | ||
151 | stroke: theme.palette.text.secondary, | ||
152 | strokeDasharray: '2 4', | ||
153 | }, | ||
154 | '.node-header': { | ||
155 | fill: theme.palette.background.default, | ||
156 | }, | ||
157 | '.icon-TRUE': { | ||
158 | fill: theme.palette.text.secondary, | ||
159 | }, | ||
160 | }, | ||
146 | }; | 161 | }; |
147 | } | 162 | } |
148 | 163 | ||
diff --git a/subprojects/frontend/src/graph/dotSource.ts b/subprojects/frontend/src/graph/dotSource.ts index ce504c37..9099cd09 100644 --- a/subprojects/frontend/src/graph/dotSource.ts +++ b/subprojects/frontend/src/graph/dotSource.ts | |||
@@ -128,11 +128,16 @@ function createNodes( | |||
128 | const { | 128 | const { |
129 | semantics: { nodes }, | 129 | semantics: { nodes }, |
130 | scopes, | 130 | scopes, |
131 | showNonExistent, | ||
131 | } = graph; | 132 | } = graph; |
132 | 133 | ||
133 | nodes.forEach((node, i) => { | 134 | nodes.forEach((node, i) => { |
134 | const data = nodeData[i]; | 135 | const data = nodeData[i]; |
135 | if (data === undefined || data.isolated || data.exists === 'FALSE') { | 136 | if ( |
137 | data === undefined || | ||
138 | data.isolated || | ||
139 | (!showNonExistent && data.exists === 'FALSE') | ||
140 | ) { | ||
136 | return; | 141 | return; |
137 | } | 142 | } |
138 | const classList = [ | 143 | const classList = [ |
@@ -255,6 +260,7 @@ function createRelationEdges( | |||
255 | ): void { | 260 | ): void { |
256 | const { | 261 | const { |
257 | semantics: { nodes, partialInterpretation }, | 262 | semantics: { nodes, partialInterpretation }, |
263 | showNonExistent, | ||
258 | } = graph; | 264 | } = graph; |
259 | const { detail } = relation; | 265 | const { detail } = relation; |
260 | 266 | ||
@@ -297,9 +303,9 @@ function createRelationEdges( | |||
297 | const toData = nodeData[to]; | 303 | const toData = nodeData[to]; |
298 | if ( | 304 | if ( |
299 | fromData === undefined || | 305 | fromData === undefined || |
300 | fromData.exists === 'FALSE' || | ||
301 | toData === undefined || | 306 | toData === undefined || |
302 | toData.exists === 'FALSE' | 307 | (!showNonExistent && |
308 | (fromData.exists === 'FALSE' || toData.exists === 'FALSE')) | ||
303 | ) { | 309 | ) { |
304 | return; | 310 | return; |
305 | } | 311 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/CancellableCancellationToken.java b/subprojects/generator/src/main/java/tools/refinery/generator/CancellableCancellationToken.java new file mode 100644 index 00000000..53bac196 --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/CancellableCancellationToken.java | |||
@@ -0,0 +1,38 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | import tools.refinery.store.util.CancellationToken; | ||
9 | |||
10 | class CancellableCancellationToken implements CancellationToken { | ||
11 | private volatile boolean cancelled; | ||
12 | |||
13 | private final CancellationToken wrappedToken; | ||
14 | |||
15 | public CancellableCancellationToken(CancellationToken wrappedToken) { | ||
16 | this.wrappedToken = wrappedToken; | ||
17 | } | ||
18 | |||
19 | public boolean isCancelled() { | ||
20 | return cancelled; | ||
21 | } | ||
22 | |||
23 | public void cancel() { | ||
24 | cancelled = true; | ||
25 | } | ||
26 | |||
27 | public void reset() { | ||
28 | cancelled = false; | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public void checkCancelled() { | ||
33 | wrappedToken.checkCancelled(); | ||
34 | if (cancelled) { | ||
35 | throw new GeneratorTimeoutException(); | ||
36 | } | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/FilteredInterpretation.java b/subprojects/generator/src/main/java/tools/refinery/generator/FilteredInterpretation.java new file mode 100644 index 00000000..c068615f --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/FilteredInterpretation.java | |||
@@ -0,0 +1,108 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | import tools.refinery.logic.AbstractValue; | ||
9 | import tools.refinery.logic.term.truthvalue.TruthValue; | ||
10 | import tools.refinery.store.map.AnyVersionedMap; | ||
11 | import tools.refinery.store.map.Cursor; | ||
12 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
13 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
14 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
15 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | import java.util.Set; | ||
19 | |||
20 | public class FilteredInterpretation<A extends AbstractValue<A, C>, C> implements PartialInterpretation<A, C> { | ||
21 | private final PartialInterpretation<A, C> wrappedInterpretation; | ||
22 | private final PartialInterpretation<TruthValue, Boolean> existsInterpretation; | ||
23 | |||
24 | public FilteredInterpretation(PartialInterpretation<A, C> wrappedInterpretation, PartialInterpretation<TruthValue, | ||
25 | Boolean> existsInterpretation) { | ||
26 | this.wrappedInterpretation = wrappedInterpretation; | ||
27 | this.existsInterpretation = existsInterpretation; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public ReasoningAdapter getAdapter() { | ||
32 | return wrappedInterpretation.getAdapter(); | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public PartialSymbol<A, C> getPartialSymbol() { | ||
37 | return wrappedInterpretation.getPartialSymbol(); | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public Concreteness getConcreteness() { | ||
42 | return wrappedInterpretation.getConcreteness(); | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public A get(Tuple key) { | ||
47 | return tupleExists(key) ? wrappedInterpretation.get(key) : | ||
48 | wrappedInterpretation.getPartialSymbol().defaultValue(); | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public Cursor<Tuple, A> getAll() { | ||
53 | return new FilteredCursor(wrappedInterpretation.getAll()); | ||
54 | } | ||
55 | |||
56 | private boolean tupleExists(Tuple key) { | ||
57 | int arity = key.getSize(); | ||
58 | for (int i = 0; i < arity; i++) { | ||
59 | if (!existsInterpretation.get(Tuple.of(key.get(i))).may()) { | ||
60 | return false; | ||
61 | } | ||
62 | } | ||
63 | return true; | ||
64 | } | ||
65 | |||
66 | private class FilteredCursor implements Cursor<Tuple, A> { | ||
67 | private final Cursor<Tuple, A> wrappedCursor; | ||
68 | |||
69 | private FilteredCursor(Cursor<Tuple, A> wrappedCursor) { | ||
70 | this.wrappedCursor = wrappedCursor; | ||
71 | } | ||
72 | |||
73 | @Override | ||
74 | public Tuple getKey() { | ||
75 | return wrappedCursor.getKey(); | ||
76 | } | ||
77 | |||
78 | @Override | ||
79 | public A getValue() { | ||
80 | return wrappedCursor.getValue(); | ||
81 | } | ||
82 | |||
83 | @Override | ||
84 | public boolean isTerminated() { | ||
85 | return wrappedCursor.isTerminated(); | ||
86 | } | ||
87 | |||
88 | @Override | ||
89 | public boolean move() { | ||
90 | while (wrappedCursor.move()) { | ||
91 | if (tupleExists(getKey())) { | ||
92 | return true; | ||
93 | } | ||
94 | } | ||
95 | return false; | ||
96 | } | ||
97 | |||
98 | @Override | ||
99 | public boolean isDirty() { | ||
100 | return wrappedCursor.isDirty(); | ||
101 | } | ||
102 | |||
103 | @Override | ||
104 | public Set<AnyVersionedMap> getDependingMaps() { | ||
105 | return wrappedCursor.getDependingMaps(); | ||
106 | } | ||
107 | } | ||
108 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/GeneratorResult.java b/subprojects/generator/src/main/java/tools/refinery/generator/GeneratorResult.java new file mode 100644 index 00000000..3ce2631a --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/GeneratorResult.java | |||
@@ -0,0 +1,29 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | public enum GeneratorResult { | ||
9 | SUCCESS { | ||
10 | @Override | ||
11 | public void orThrow() { | ||
12 | // No need to throw on error. | ||
13 | } | ||
14 | }, | ||
15 | UNSATISFIABLE { | ||
16 | @Override | ||
17 | public void orThrow() { | ||
18 | throw new UnsatisfiableProblemException(); | ||
19 | } | ||
20 | }, | ||
21 | TIMEOUT { | ||
22 | @Override | ||
23 | public void orThrow() { | ||
24 | throw new GeneratorTimeoutException(); | ||
25 | } | ||
26 | }; | ||
27 | |||
28 | public abstract void orThrow(); | ||
29 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/GeneratorTimeoutException.java b/subprojects/generator/src/main/java/tools/refinery/generator/GeneratorTimeoutException.java new file mode 100644 index 00000000..4312a324 --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/GeneratorTimeoutException.java | |||
@@ -0,0 +1,12 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | public class GeneratorTimeoutException extends RuntimeException { | ||
9 | public GeneratorTimeoutException() { | ||
10 | super("Model generation timed out"); | ||
11 | } | ||
12 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelFacadeFactory.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelFacadeFactory.java new file mode 100644 index 00000000..75ca5082 --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelFacadeFactory.java | |||
@@ -0,0 +1,49 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import com.google.inject.Provider; | ||
10 | import tools.refinery.language.semantics.ModelInitializer; | ||
11 | import tools.refinery.store.util.CancellationToken; | ||
12 | |||
13 | public abstract sealed class ModelFacadeFactory<T extends ModelFacadeFactory<T>> permits ModelSemanticsFactory, | ||
14 | ModelGeneratorFactory { | ||
15 | @Inject | ||
16 | private Provider<ModelInitializer> initializerProvider; | ||
17 | |||
18 | private CancellationToken cancellationToken = CancellationToken.NONE; | ||
19 | |||
20 | private boolean keepNonExistingObjects = false; | ||
21 | |||
22 | protected abstract T getSelf(); | ||
23 | |||
24 | public T cancellationToken(CancellationToken cancellationToken) { | ||
25 | this.cancellationToken = cancellationToken; | ||
26 | return getSelf(); | ||
27 | } | ||
28 | |||
29 | public T keepNonExistingObjects(boolean removeNonExistentObjects) { | ||
30 | this.keepNonExistingObjects = removeNonExistentObjects; | ||
31 | return getSelf(); | ||
32 | } | ||
33 | |||
34 | protected ModelInitializer createModelInitializer() { | ||
35 | return initializerProvider.get(); | ||
36 | } | ||
37 | |||
38 | protected CancellationToken getCancellationToken() { | ||
39 | return cancellationToken; | ||
40 | } | ||
41 | |||
42 | protected boolean isKeepNonExistingObjects() { | ||
43 | return keepNonExistingObjects; | ||
44 | } | ||
45 | |||
46 | protected void checkCancelled() { | ||
47 | cancellationToken.checkCancelled(); | ||
48 | } | ||
49 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java index 8dff5622..2f459eb9 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java | |||
@@ -10,26 +10,38 @@ import tools.refinery.language.model.problem.Problem; | |||
10 | import tools.refinery.language.semantics.ProblemTrace; | 10 | import tools.refinery.language.semantics.ProblemTrace; |
11 | import tools.refinery.language.semantics.SolutionSerializer; | 11 | import tools.refinery.language.semantics.SolutionSerializer; |
12 | import tools.refinery.logic.AbstractValue; | 12 | import tools.refinery.logic.AbstractValue; |
13 | import tools.refinery.logic.term.truthvalue.TruthValue; | ||
13 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; | 14 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; |
14 | import tools.refinery.store.dse.transition.statespace.SolutionStore; | 15 | import tools.refinery.store.dse.transition.statespace.SolutionStore; |
15 | import tools.refinery.store.map.Version; | 16 | import tools.refinery.store.map.Version; |
16 | import tools.refinery.store.model.ModelStore; | 17 | import tools.refinery.store.model.ModelStore; |
18 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
17 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | 19 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; |
18 | import tools.refinery.store.reasoning.literal.Concreteness; | 20 | import tools.refinery.store.reasoning.literal.Concreteness; |
19 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 21 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
20 | import tools.refinery.store.reasoning.seed.ModelSeed; | 22 | import tools.refinery.store.reasoning.seed.ModelSeed; |
21 | 23 | ||
24 | import java.util.concurrent.Executors; | ||
25 | import java.util.concurrent.TimeUnit; | ||
26 | |||
22 | public class ModelGenerator extends ModelFacade { | 27 | public class ModelGenerator extends ModelFacade { |
23 | private final Version initialVersion; | 28 | private final Version initialVersion; |
24 | private final Provider<SolutionSerializer> solutionSerializerProvider; | 29 | private final Provider<SolutionSerializer> solutionSerializerProvider; |
30 | private final CancellableCancellationToken cancellationToken; | ||
31 | private final boolean keepNonExistingObjects; | ||
32 | private final PartialInterpretation<TruthValue, Boolean> existsInterpretation; | ||
25 | private long randomSeed = 1; | 33 | private long randomSeed = 1; |
26 | private int maxNumberOfSolutions = 1; | 34 | private int maxNumberOfSolutions = 1; |
27 | private SolutionStore solutionStore; | 35 | private SolutionStore solutionStore; |
28 | 36 | ||
29 | ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed, | 37 | ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed, |
30 | Provider<SolutionSerializer> solutionSerializerProvider) { | 38 | Provider<SolutionSerializer> solutionSerializerProvider, |
39 | CancellableCancellationToken cancellationToken, boolean keepNonExistingObjects) { | ||
31 | super(problemTrace, store, modelSeed, Concreteness.CANDIDATE); | 40 | super(problemTrace, store, modelSeed, Concreteness.CANDIDATE); |
32 | this.solutionSerializerProvider = solutionSerializerProvider; | 41 | this.solutionSerializerProvider = solutionSerializerProvider; |
42 | this.cancellationToken = cancellationToken; | ||
43 | this.keepNonExistingObjects = keepNonExistingObjects; | ||
44 | existsInterpretation = super.getPartialInterpretation(ReasoningAdapter.EXISTS_SYMBOL); | ||
33 | initialVersion = getModel().commit(); | 45 | initialVersion = getModel().commit(); |
34 | } | 46 | } |
35 | 47 | ||
@@ -71,33 +83,52 @@ public class ModelGenerator extends ModelFacade { | |||
71 | return solutionStore != null; | 83 | return solutionStore != null; |
72 | } | 84 | } |
73 | 85 | ||
74 | // This method only makes sense if it returns {@code true} on success. | 86 | public GeneratorResult tryGenerate() { |
75 | @SuppressWarnings("BooleanMethodIsAlwaysInverted") | 87 | if (cancellationToken.isCancelled()) { |
76 | public boolean tryGenerate() { | 88 | throw new IllegalStateException("Model generation was previously cancelled"); |
89 | } | ||
77 | solutionStore = null; | 90 | solutionStore = null; |
78 | randomSeed++; | 91 | randomSeed++; |
79 | var bestFirst = new BestFirstStoreManager(getModelStore(), maxNumberOfSolutions); | 92 | var bestFirst = new BestFirstStoreManager(getModelStore(), maxNumberOfSolutions); |
80 | bestFirst.startExploration(initialVersion, randomSeed); | 93 | bestFirst.startExploration(initialVersion, randomSeed); |
81 | var solutions = bestFirst.getSolutionStore().getSolutions(); | 94 | var solutions = bestFirst.getSolutionStore().getSolutions(); |
82 | if (solutions.isEmpty()) { | 95 | if (solutions.isEmpty()) { |
83 | return false; | 96 | return GeneratorResult.UNSATISFIABLE; |
84 | } | 97 | } |
85 | getModel().restore(solutions.getFirst().version()); | 98 | getModel().restore(solutions.getFirst().version()); |
86 | solutionStore = bestFirst.getSolutionStore(); | 99 | solutionStore = bestFirst.getSolutionStore(); |
87 | return true; | 100 | return GeneratorResult.SUCCESS; |
88 | } | 101 | } |
89 | 102 | ||
90 | public void generate() { | 103 | public void generate() { |
91 | if (!tryGenerate()) { | 104 | tryGenerate().orThrow(); |
92 | throw new UnsatisfiableProblemException(); | 105 | } |
106 | |||
107 | public GeneratorResult tryGenerateWithTimeout(long l, TimeUnit timeUnit) { | ||
108 | try (var executorService = Executors.newSingleThreadScheduledExecutor()) { | ||
109 | var timeoutFuture = executorService.schedule(cancellationToken::cancel, l, timeUnit); | ||
110 | try { | ||
111 | return tryGenerate(); | ||
112 | } catch (GeneratorTimeoutException e) { | ||
113 | return GeneratorResult.TIMEOUT; | ||
114 | } finally { | ||
115 | timeoutFuture.cancel(true); | ||
116 | cancellationToken.reset(); | ||
117 | } | ||
93 | } | 118 | } |
94 | } | 119 | } |
95 | 120 | ||
121 | public void generateWithTimeout(long l, TimeUnit timeUnit) { | ||
122 | tryGenerateWithTimeout(l, timeUnit).orThrow(); | ||
123 | } | ||
124 | |||
96 | @Override | 125 | @Override |
97 | public <A extends AbstractValue<A, C>, C> PartialInterpretation<A, C> getPartialInterpretation( | 126 | public <A extends AbstractValue<A, C>, C> PartialInterpretation<A, C> getPartialInterpretation( |
98 | PartialSymbol<A, C> partialSymbol) { | 127 | PartialSymbol<A, C> partialSymbol) { |
99 | checkSuccessfulGeneration(); | 128 | checkSuccessfulGeneration(); |
100 | return super.getPartialInterpretation(partialSymbol); | 129 | var partialInterpretation = super.getPartialInterpretation(partialSymbol); |
130 | return keepNonExistingObjects ? partialInterpretation : | ||
131 | new FilteredInterpretation<>(partialInterpretation, existsInterpretation); | ||
101 | } | 132 | } |
102 | 133 | ||
103 | public Problem serializeSolution() { | 134 | public Problem serializeSolution() { |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java index 0a1b4396..b041c8f6 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java | |||
@@ -8,7 +8,6 @@ package tools.refinery.generator; | |||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import com.google.inject.Provider; | 9 | import com.google.inject.Provider; |
10 | import tools.refinery.language.model.problem.Problem; | 10 | import tools.refinery.language.model.problem.Problem; |
11 | import tools.refinery.language.semantics.ModelInitializer; | ||
12 | import tools.refinery.language.semantics.SolutionSerializer; | 11 | import tools.refinery.language.semantics.SolutionSerializer; |
13 | import tools.refinery.store.dse.propagation.PropagationAdapter; | 12 | import tools.refinery.store.dse.propagation.PropagationAdapter; |
14 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | 13 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; |
@@ -20,30 +19,24 @@ import tools.refinery.store.reasoning.literal.Concreteness; | |||
20 | import tools.refinery.store.statecoding.StateCodeCalculatorFactory; | 19 | import tools.refinery.store.statecoding.StateCodeCalculatorFactory; |
21 | import tools.refinery.store.statecoding.StateCoderAdapter; | 20 | import tools.refinery.store.statecoding.StateCoderAdapter; |
22 | import tools.refinery.store.statecoding.neighborhood.NeighborhoodCalculator; | 21 | import tools.refinery.store.statecoding.neighborhood.NeighborhoodCalculator; |
23 | import tools.refinery.store.util.CancellationToken; | ||
24 | 22 | ||
25 | import java.util.Collection; | 23 | import java.util.Collection; |
26 | import java.util.Set; | 24 | import java.util.Set; |
27 | 25 | ||
28 | // This class is used as a fluent builder, so it's not necessary to use the return value of all of its methods. | 26 | // This class is used as a fluent builder, so it's not necessary to use the return value of all of its methods. |
29 | @SuppressWarnings("UnusedReturnValue") | 27 | @SuppressWarnings("UnusedReturnValue") |
30 | public final class ModelGeneratorFactory { | 28 | public final class ModelGeneratorFactory extends ModelFacadeFactory<ModelGeneratorFactory> { |
31 | @Inject | ||
32 | private Provider<ModelInitializer> initializerProvider; | ||
33 | |||
34 | @Inject | 29 | @Inject |
35 | private Provider<SolutionSerializer> solutionSerializerProvider; | 30 | private Provider<SolutionSerializer> solutionSerializerProvider; |
36 | 31 | ||
37 | private CancellationToken cancellationToken = CancellationToken.NONE; | ||
38 | |||
39 | private boolean debugPartialInterpretations; | 32 | private boolean debugPartialInterpretations; |
40 | 33 | ||
41 | private boolean partialInterpretationBasedNeighborhoods; | 34 | private boolean partialInterpretationBasedNeighborhoods; |
42 | 35 | ||
43 | private int stateCoderDepth = NeighborhoodCalculator.DEFAULT_DEPTH; | 36 | private int stateCoderDepth = NeighborhoodCalculator.DEFAULT_DEPTH; |
44 | 37 | ||
45 | public ModelGeneratorFactory cancellationToken(CancellationToken cancellationToken) { | 38 | @Override |
46 | this.cancellationToken = cancellationToken; | 39 | protected ModelGeneratorFactory getSelf() { |
47 | return this; | 40 | return this; |
48 | } | 41 | } |
49 | 42 | ||
@@ -64,22 +57,23 @@ public final class ModelGeneratorFactory { | |||
64 | } | 57 | } |
65 | 58 | ||
66 | public ModelGenerator createGenerator(Problem problem) { | 59 | public ModelGenerator createGenerator(Problem problem) { |
67 | var initializer = initializerProvider.get(); | 60 | var initializer = createModelInitializer(); |
68 | initializer.readProblem(problem); | 61 | initializer.readProblem(problem); |
69 | cancellationToken.checkCancelled(); | 62 | checkCancelled(); |
63 | var cancellationToken = new CancellableCancellationToken(getCancellationToken()); | ||
70 | var storeBuilder = ModelStore.builder() | 64 | var storeBuilder = ModelStore.builder() |
71 | .cancellationToken(cancellationToken) | 65 | .cancellationToken(cancellationToken) |
72 | .with(QueryInterpreterAdapter.builder()) | 66 | .with(QueryInterpreterAdapter.builder()) |
73 | .with(PropagationAdapter.builder()) | 67 | .with(PropagationAdapter.builder()) |
74 | .with(StateCoderAdapter.builder() | 68 | .with(StateCoderAdapter.builder() |
75 | .stateCodeCalculatorFactory(getStateCoderCalculatorFactory())) | 69 | .stateCodeCalculatorFactory(getStateCodeCalculatorFactory())) |
76 | .with(DesignSpaceExplorationAdapter.builder()) | 70 | .with(DesignSpaceExplorationAdapter.builder()) |
77 | .with(ReasoningAdapter.builder() | 71 | .with(ReasoningAdapter.builder() |
78 | .requiredInterpretations(getRequiredInterpretations())); | 72 | .requiredInterpretations(getRequiredInterpretations())); |
79 | initializer.configureStoreBuilder(storeBuilder); | 73 | initializer.configureStoreBuilder(storeBuilder, isKeepNonExistingObjects()); |
80 | var store = storeBuilder.build(); | 74 | var store = storeBuilder.build(); |
81 | var generator = new ModelGenerator(initializer.getProblemTrace(), store, initializer.getModelSeed(), | 75 | var generator = new ModelGenerator(initializer.getProblemTrace(), store, initializer.getModelSeed(), |
82 | solutionSerializerProvider); | 76 | solutionSerializerProvider, cancellationToken, isKeepNonExistingObjects()); |
83 | generator.getPropagationResult().throwIfRejected(); | 77 | generator.getPropagationResult().throwIfRejected(); |
84 | return generator; | 78 | return generator; |
85 | } | 79 | } |
@@ -90,7 +84,7 @@ public final class ModelGeneratorFactory { | |||
90 | Set.of(Concreteness.CANDIDATE); | 84 | Set.of(Concreteness.CANDIDATE); |
91 | } | 85 | } |
92 | 86 | ||
93 | private StateCodeCalculatorFactory getStateCoderCalculatorFactory() { | 87 | private StateCodeCalculatorFactory getStateCodeCalculatorFactory() { |
94 | return partialInterpretationBasedNeighborhoods ? | 88 | return partialInterpretationBasedNeighborhoods ? |
95 | PartialNeighborhoodCalculator.factory(Concreteness.PARTIAL, stateCoderDepth) : | 89 | PartialNeighborhoodCalculator.factory(Concreteness.PARTIAL, stateCoderDepth) : |
96 | NeighborhoodCalculator.factory(stateCoderDepth); | 90 | NeighborhoodCalculator.factory(stateCoderDepth); |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsFactory.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsFactory.java index 3c3488df..43427502 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsFactory.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsFactory.java | |||
@@ -5,27 +5,18 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.generator; | 6 | package tools.refinery.generator; |
7 | 7 | ||
8 | import com.google.inject.Inject; | ||
9 | import com.google.inject.Provider; | ||
10 | import tools.refinery.language.model.problem.Problem; | 8 | import tools.refinery.language.model.problem.Problem; |
11 | import tools.refinery.language.semantics.ModelInitializer; | ||
12 | import tools.refinery.store.dse.propagation.PropagationAdapter; | 9 | import tools.refinery.store.dse.propagation.PropagationAdapter; |
13 | import tools.refinery.store.model.ModelStore; | 10 | import tools.refinery.store.model.ModelStore; |
14 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; | 11 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; |
15 | import tools.refinery.store.reasoning.ReasoningAdapter; | 12 | import tools.refinery.store.reasoning.ReasoningAdapter; |
16 | import tools.refinery.store.reasoning.literal.Concreteness; | 13 | import tools.refinery.store.reasoning.literal.Concreteness; |
17 | import tools.refinery.store.util.CancellationToken; | ||
18 | 14 | ||
19 | import java.util.Set; | 15 | import java.util.Set; |
20 | 16 | ||
21 | public final class ModelSemanticsFactory { | 17 | public final class ModelSemanticsFactory extends ModelFacadeFactory<ModelSemanticsFactory> { |
22 | @Inject | 18 | @Override |
23 | private Provider<ModelInitializer> initializerProvider; | 19 | protected ModelSemanticsFactory getSelf() { |
24 | |||
25 | private CancellationToken cancellationToken = CancellationToken.NONE; | ||
26 | |||
27 | public ModelSemanticsFactory cancellationToken(CancellationToken cancellationToken) { | ||
28 | this.cancellationToken = cancellationToken; | ||
29 | return this; | 20 | return this; |
30 | } | 21 | } |
31 | 22 | ||
@@ -36,16 +27,17 @@ public final class ModelSemanticsFactory { | |||
36 | } | 27 | } |
37 | 28 | ||
38 | public ModelSemantics tryCreateSemantics(Problem problem) { | 29 | public ModelSemantics tryCreateSemantics(Problem problem) { |
39 | var initializer = initializerProvider.get(); | 30 | var initializer = createModelInitializer(); |
40 | initializer.readProblem(problem); | 31 | initializer.readProblem(problem); |
32 | checkCancelled(); | ||
41 | var storeBuilder = ModelStore.builder() | 33 | var storeBuilder = ModelStore.builder() |
42 | .cancellationToken(cancellationToken) | 34 | .cancellationToken(getCancellationToken()) |
43 | .with(QueryInterpreterAdapter.builder()) | 35 | .with(QueryInterpreterAdapter.builder()) |
44 | .with(PropagationAdapter.builder() | 36 | .with(PropagationAdapter.builder() |
45 | .throwOnFatalRejection(false)) | 37 | .throwOnFatalRejection(false)) |
46 | .with(ReasoningAdapter.builder() | 38 | .with(ReasoningAdapter.builder() |
47 | .requiredInterpretations(Set.of(Concreteness.PARTIAL))); | 39 | .requiredInterpretations(Set.of(Concreteness.PARTIAL))); |
48 | initializer.configureStoreBuilder(storeBuilder); | 40 | initializer.configureStoreBuilder(storeBuilder, isKeepNonExistingObjects()); |
49 | var store = storeBuilder.build(); | 41 | var store = storeBuilder.build(); |
50 | return new ModelSemantics(initializer.getProblemTrace(), store, initializer.getModelSeed()); | 42 | return new ModelSemantics(initializer.getProblemTrace(), store, initializer.getModelSeed()); |
51 | } | 43 | } |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index d71cf35f..6aea3132 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | |||
@@ -180,9 +180,13 @@ public class ModelInitializer { | |||
180 | } | 180 | } |
181 | 181 | ||
182 | public void configureStoreBuilder(ModelStoreBuilder storeBuilder) { | 182 | public void configureStoreBuilder(ModelStoreBuilder storeBuilder) { |
183 | configureStoreBuilder(storeBuilder, false); | ||
184 | } | ||
185 | |||
186 | public void configureStoreBuilder(ModelStoreBuilder storeBuilder, boolean keepNonExistingObjects) { | ||
183 | checkProblem(); | 187 | checkProblem(); |
184 | try { | 188 | try { |
185 | storeBuilder.with(new MultiObjectTranslator()); | 189 | storeBuilder.with(new MultiObjectTranslator(keepNonExistingObjects)); |
186 | storeBuilder.with(new MetamodelTranslator(metamodel)); | 190 | storeBuilder.with(new MetamodelTranslator(metamodel)); |
187 | if (scopePropagator != null) { | 191 | if (scopePropagator != null) { |
188 | if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) { | 192 | if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) { |
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 7febce7d..e7facbf7 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 | |||
@@ -9,11 +9,8 @@ import com.google.inject.Inject; | |||
9 | import org.eclipse.xtext.service.OperationCanceledManager; | 9 | import org.eclipse.xtext.service.OperationCanceledManager; |
10 | import org.slf4j.Logger; | 10 | import org.slf4j.Logger; |
11 | import org.slf4j.LoggerFactory; | 11 | import org.slf4j.LoggerFactory; |
12 | import tools.refinery.generator.ModelGenerator; | 12 | import tools.refinery.generator.*; |
13 | import tools.refinery.generator.ModelGeneratorFactory; | ||
14 | import tools.refinery.language.web.semantics.metadata.MetadataCreator; | 13 | import tools.refinery.language.web.semantics.metadata.MetadataCreator; |
15 | import tools.refinery.generator.ProblemLoader; | ||
16 | import tools.refinery.generator.ValidationErrorsException; | ||
17 | import tools.refinery.language.web.semantics.PartialInterpretation2Json; | 14 | import tools.refinery.language.web.semantics.PartialInterpretation2Json; |
18 | import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider; | 15 | import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider; |
19 | import tools.refinery.language.web.xtext.server.push.PushWebDocument; | 16 | import tools.refinery.language.web.xtext.server.push.PushWebDocument; |
@@ -149,7 +146,7 @@ public class ModelGenerationWorker implements Runnable { | |||
149 | } | 146 | } |
150 | notifyResult(new ModelGenerationStatusResult(uuid, "Generating model")); | 147 | notifyResult(new ModelGenerationStatusResult(uuid, "Generating model")); |
151 | generator.setRandomSeed(randomSeed); | 148 | generator.setRandomSeed(randomSeed); |
152 | if (!generator.tryGenerate()) { | 149 | if (generator.tryGenerate() != GeneratorResult.SUCCESS) { |
153 | return new ModelGenerationErrorResult(uuid, "Problem is unsatisfiable"); | 150 | return new ModelGenerationErrorResult(uuid, "Problem is unsatisfiable"); |
154 | } | 151 | } |
155 | notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model")); | 152 | notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model")); |
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java index a96b68f9..508e716e 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java | |||
@@ -72,7 +72,10 @@ class SemanticsWorker implements Callable<SemanticsResult> { | |||
72 | cancellationToken.checkCancelled(); | 72 | cancellationToken.checkCancelled(); |
73 | ModelSemantics semantics; | 73 | ModelSemantics semantics; |
74 | try { | 74 | try { |
75 | semantics = semanticsFactory.cancellationToken(cancellationToken).tryCreateSemantics(problem); | 75 | semantics = semanticsFactory |
76 | .cancellationToken(cancellationToken) | ||
77 | .keepNonExistingObjects(true) | ||
78 | .tryCreateSemantics(problem); | ||
76 | } catch (TranslationException e) { | 79 | } catch (TranslationException e) { |
77 | return new SemanticsResult(e.getMessage()); | 80 | return new SemanticsResult(e.getMessage()); |
78 | } catch (TracedException e) { | 81 | } catch (TracedException e) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java index 386ae1d8..b83d162e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java | |||
@@ -204,6 +204,8 @@ class ReasoningAdapterImpl implements ReasoningAdapter { | |||
204 | if (nodeToDelete == currentModelSize - 1) { | 204 | if (nodeToDelete == currentModelSize - 1) { |
205 | nodeCountInterpretation.put(Tuple.of(), nodeToDelete); | 205 | nodeCountInterpretation.put(Tuple.of(), nodeToDelete); |
206 | } | 206 | } |
207 | // We mustn't reuse the ID of {@code nodeToDelete} in any circumstance, because clients may depend on stable | ||
208 | // node IDs for nodes in the initial partial model. | ||
207 | return true; | 209 | return true; |
208 | } | 210 | } |
209 | 211 | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java index f14b4783..6feccae3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java | |||
@@ -11,6 +11,7 @@ import tools.refinery.logic.term.uppercardinality.UpperCardinalities; | |||
11 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; | 11 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; |
12 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; | 12 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; |
13 | import tools.refinery.store.dse.propagation.BoundPropagator; | 13 | import tools.refinery.store.dse.propagation.BoundPropagator; |
14 | import tools.refinery.store.dse.propagation.PropagationRejectedResult; | ||
14 | import tools.refinery.store.dse.propagation.PropagationResult; | 15 | import tools.refinery.store.dse.propagation.PropagationResult; |
15 | import tools.refinery.store.dse.propagation.Propagator; | 16 | import tools.refinery.store.dse.propagation.Propagator; |
16 | import tools.refinery.store.model.Model; | 17 | import tools.refinery.store.model.Model; |
@@ -48,7 +49,7 @@ public class CleanupPropagator implements Propagator { | |||
48 | return new BoundCleanupPropagator(model); | 49 | return new BoundCleanupPropagator(model); |
49 | } | 50 | } |
50 | 51 | ||
51 | private static class BoundCleanupPropagator implements BoundPropagator { | 52 | private class BoundCleanupPropagator implements BoundPropagator { |
52 | private final Model model; | 53 | private final Model model; |
53 | private final ModelQueryAdapter queryEngine; | 54 | private final ModelQueryAdapter queryEngine; |
54 | private final ResultSet<Boolean> resultSet; | 55 | private final ResultSet<Boolean> resultSet; |
@@ -70,7 +71,11 @@ public class CleanupPropagator implements Propagator { | |||
70 | var cursor = resultSet.getAll(); | 71 | var cursor = resultSet.getAll(); |
71 | while (cursor.move()) { | 72 | while (cursor.move()) { |
72 | propagated = true; | 73 | propagated = true; |
73 | reasoningAdapter.cleanup(cursor.getKey().get(0)); | 74 | var nodeToDelete = cursor.getKey().get(0); |
75 | if (!reasoningAdapter.cleanup(nodeToDelete)) { | ||
76 | return new PropagationRejectedResult(CleanupPropagator.this, | ||
77 | "Failed to remove node: " + nodeToDelete, true); | ||
78 | } | ||
74 | } | 79 | } |
75 | return propagated ? PropagationResult.PROPAGATED : PropagationResult.UNCHANGED; | 80 | return propagated ? PropagationResult.PROPAGATED : PropagationResult.UNCHANGED; |
76 | } | 81 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java index 05d96689..7b3be76d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java | |||
@@ -41,6 +41,16 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
41 | public static final PartialFunction<CardinalityInterval, Integer> COUNT_SYMBOL = new PartialFunction<>("COUNT", 1, | 41 | public static final PartialFunction<CardinalityInterval, Integer> COUNT_SYMBOL = new PartialFunction<>("COUNT", 1, |
42 | CardinalityDomain.INSTANCE); | 42 | CardinalityDomain.INSTANCE); |
43 | 43 | ||
44 | private final boolean keepNonExistingObjects; | ||
45 | |||
46 | public MultiObjectTranslator(boolean keepNonExistingObjects) { | ||
47 | this.keepNonExistingObjects = keepNonExistingObjects; | ||
48 | } | ||
49 | |||
50 | public MultiObjectTranslator() { | ||
51 | this(true); | ||
52 | } | ||
53 | |||
44 | @Override | 54 | @Override |
45 | public void apply(ModelStoreBuilder storeBuilder) { | 55 | public void apply(ModelStoreBuilder storeBuilder) { |
46 | storeBuilder.symbol(COUNT_STORAGE); | 56 | storeBuilder.symbol(COUNT_STORAGE); |
@@ -90,7 +100,9 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
90 | reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); | 100 | reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); |
91 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); | 101 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); |
92 | 102 | ||
93 | storeBuilder.tryGetAdapter(PropagationBuilder.class) | 103 | if (!keepNonExistingObjects) { |
94 | .ifPresent(propagationBuilder -> propagationBuilder.propagator(new CleanupPropagator())); | 104 | storeBuilder.tryGetAdapter(PropagationBuilder.class) |
105 | .ifPresent(propagationBuilder -> propagationBuilder.propagator(new CleanupPropagator())); | ||
106 | } | ||
95 | } | 107 | } |
96 | } | 108 | } |