diff options
46 files changed, 1138 insertions, 295 deletions
diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts index 4374f78c..338ae345 100644 --- a/subprojects/language-semantics/build.gradle.kts +++ b/subprojects/language-semantics/build.gradle.kts | |||
@@ -16,4 +16,7 @@ dependencies { | |||
16 | api(project(":refinery-store-reasoning")) | 16 | api(project(":refinery-store-reasoning")) |
17 | implementation(project(":refinery-store-reasoning-scope")) | 17 | implementation(project(":refinery-store-reasoning-scope")) |
18 | runtimeOnly(libs.eclipseCollections) | 18 | runtimeOnly(libs.eclipseCollections) |
19 | testImplementation(project(":refinery-store-dse-visualization")) | ||
20 | testImplementation(project(":refinery-store-query-viatra")) | ||
21 | testImplementation(testFixtures(project(":refinery-language"))) | ||
19 | } | 22 | } |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java index 89c41a8e..a14b40d0 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java | |||
@@ -13,6 +13,7 @@ import tools.refinery.language.semantics.model.internal.MutableSeed; | |||
13 | import tools.refinery.language.utils.BuiltinSymbols; | 13 | import tools.refinery.language.utils.BuiltinSymbols; |
14 | import tools.refinery.language.utils.ProblemDesugarer; | 14 | import tools.refinery.language.utils.ProblemDesugarer; |
15 | import tools.refinery.language.utils.ProblemUtil; | 15 | import tools.refinery.language.utils.ProblemUtil; |
16 | import tools.refinery.store.dse.propagation.PropagationBuilder; | ||
16 | import tools.refinery.store.model.ModelStoreBuilder; | 17 | import tools.refinery.store.model.ModelStoreBuilder; |
17 | import tools.refinery.store.query.Constraint; | 18 | import tools.refinery.store.query.Constraint; |
18 | import tools.refinery.store.query.dnf.InvalidClauseException; | 19 | import tools.refinery.store.query.dnf.InvalidClauseException; |
@@ -24,7 +25,7 @@ import tools.refinery.store.query.term.Variable; | |||
24 | import tools.refinery.store.reasoning.ReasoningAdapter; | 25 | import tools.refinery.store.reasoning.ReasoningAdapter; |
25 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 26 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
26 | import tools.refinery.store.reasoning.representation.PartialRelation; | 27 | import tools.refinery.store.reasoning.representation.PartialRelation; |
27 | import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder; | 28 | import tools.refinery.store.reasoning.scope.ScopePropagator; |
28 | import tools.refinery.store.reasoning.seed.ModelSeed; | 29 | import tools.refinery.store.reasoning.seed.ModelSeed; |
29 | import tools.refinery.store.reasoning.seed.Seed; | 30 | import tools.refinery.store.reasoning.seed.Seed; |
30 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; | 31 | import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; |
@@ -73,7 +74,9 @@ public class ModelInitializer { | |||
73 | 74 | ||
74 | private Metamodel metamodel; | 75 | private Metamodel metamodel; |
75 | 76 | ||
76 | private Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>(); | 77 | private final Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>(); |
78 | |||
79 | private ScopePropagator scopePropagator; | ||
77 | 80 | ||
78 | private ModelSeed modelSeed; | 81 | private ModelSeed modelSeed; |
79 | 82 | ||
@@ -139,6 +142,12 @@ public class ModelInitializer { | |||
139 | modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); | 142 | modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); |
140 | } | 143 | } |
141 | collectScopes(); | 144 | collectScopes(); |
145 | if (scopePropagator != null) { | ||
146 | if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) { | ||
147 | throw new TracedException(problem, "Type scopes require a PropagationBuilder"); | ||
148 | } | ||
149 | storeBuilder.with(scopePropagator); | ||
150 | } | ||
142 | modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | 151 | modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder |
143 | .reducedValue(CardinalityIntervals.SET) | 152 | .reducedValue(CardinalityIntervals.SET) |
144 | .putAll(countSeed)); | 153 | .putAll(countSeed)); |
@@ -534,8 +543,7 @@ public class ModelInitializer { | |||
534 | } | 543 | } |
535 | } | 544 | } |
536 | 545 | ||
537 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, | 546 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, |
538 | Variable> localScope, | ||
539 | List<Literal> literals) { | 547 | List<Literal> literals) { |
540 | if (expr instanceof LogicConstant logicConstant) { | 548 | if (expr instanceof LogicConstant logicConstant) { |
541 | switch (logicConstant.getLogicValue()) { | 549 | switch (logicConstant.getLogicValue()) { |
@@ -645,14 +653,15 @@ public class ModelInitializer { | |||
645 | } | 653 | } |
646 | 654 | ||
647 | private void collectTypeScope(TypeScope typeScope) { | 655 | private void collectTypeScope(TypeScope typeScope) { |
648 | var scopePropagatorBuilder = storeBuilder.tryGetAdapter(ScopePropagatorBuilder.class).orElseThrow( | ||
649 | () -> new TracedException(typeScope, "Type scopes require a ScopePropagatorBuilder")); | ||
650 | var type = relationTrace.get(typeScope.getTargetType()); | 656 | var type = relationTrace.get(typeScope.getTargetType()); |
651 | if (type == null) { | 657 | if (type == null) { |
652 | throw new TracedException(typeScope, "Unknown target type"); | 658 | throw new TracedException(typeScope, "Unknown target type"); |
653 | } | 659 | } |
654 | var interval = getCardinalityInterval(typeScope.getMultiplicity()); | 660 | var interval = getCardinalityInterval(typeScope.getMultiplicity()); |
655 | scopePropagatorBuilder.scope(type, interval); | 661 | if (scopePropagator == null) { |
662 | scopePropagator = new ScopePropagator(); | ||
663 | } | ||
664 | scopePropagator.scope(type, interval); | ||
656 | } | 665 | } |
657 | 666 | ||
658 | private record RelationInfo(PartialRelation partialRelation, MutableSeed<TruthValue> assertions, | 667 | private record RelationInfo(PartialRelation partialRelation, MutableSeed<TruthValue> assertions, |
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java new file mode 100644 index 00000000..a383d043 --- /dev/null +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java | |||
@@ -0,0 +1,82 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.semantics.model; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
10 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
11 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | ||
12 | import tools.refinery.store.model.ModelStore; | ||
13 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
14 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
15 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
16 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
17 | import tools.refinery.store.reasoning.scope.ScopePropagator; | ||
18 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
19 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | ||
20 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy; | ||
21 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; | ||
22 | import tools.refinery.store.representation.TruthValue; | ||
23 | import tools.refinery.store.representation.cardinality.CardinalityIntervals; | ||
24 | import tools.refinery.store.tuple.Tuple; | ||
25 | |||
26 | import static org.hamcrest.MatcherAssert.assertThat; | ||
27 | import static org.hamcrest.Matchers.is; | ||
28 | |||
29 | class CountPropagationTest { | ||
30 | @Test | ||
31 | void countPropagationTest() { | ||
32 | var a1 = new PartialRelation("A1", 1); | ||
33 | var c1 = new PartialRelation("C1", 1); | ||
34 | var c2 = new PartialRelation("C2", 1); | ||
35 | |||
36 | var typeHierarchy = TypeHierarchy.builder() | ||
37 | .type(a1, true) | ||
38 | .type(c1, a1) | ||
39 | .type(c2, a1) | ||
40 | .build(); | ||
41 | |||
42 | var store = ModelStore.builder() | ||
43 | .with(ViatraModelQueryAdapter.builder()) | ||
44 | .with(PropagationAdapter.builder()) | ||
45 | .with(DesignSpaceExplorationAdapter.builder()) | ||
46 | .with(ReasoningAdapter.builder()) | ||
47 | .with(new MultiObjectTranslator()) | ||
48 | .with(new TypeHierarchyTranslator(typeHierarchy)) | ||
49 | .with(new ScopePropagator() | ||
50 | .scope(a1, CardinalityIntervals.between(1000, 1100)) | ||
51 | .scope(c1, CardinalityIntervals.between(100, 150))) | ||
52 | .build(); | ||
53 | |||
54 | var modelSeed = ModelSeed.builder(4) | ||
55 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder | ||
56 | .reducedValue(CardinalityIntervals.ONE) | ||
57 | .put(Tuple.of(0), CardinalityIntervals.SET) | ||
58 | .put(Tuple.of(1), CardinalityIntervals.SET)) | ||
59 | .seed(a1, builder -> builder.reducedValue(TruthValue.UNKNOWN)) | ||
60 | .seed(c1, builder -> builder | ||
61 | .reducedValue(TruthValue.FALSE) | ||
62 | .put(Tuple.of(0), TruthValue.TRUE) | ||
63 | .put(Tuple.of(2), TruthValue.TRUE)) | ||
64 | .seed(c2, builder -> builder | ||
65 | .reducedValue(TruthValue.FALSE) | ||
66 | .put(Tuple.of(1), TruthValue.TRUE) | ||
67 | .put(Tuple.of(3), TruthValue.TRUE)) | ||
68 | .build(); | ||
69 | |||
70 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
71 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
72 | var propagationAdapter = model.getAdapter(PropagationAdapter.class); | ||
73 | model.commit(); | ||
74 | |||
75 | reasoningAdapter.split(0); | ||
76 | assertThat(propagationAdapter.propagate(), is(PropagationResult.UNCHANGED)); | ||
77 | model.commit(); | ||
78 | |||
79 | reasoningAdapter.split(0); | ||
80 | assertThat(propagationAdapter.propagate(), is(PropagationResult.UNCHANGED)); | ||
81 | } | ||
82 | } | ||
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java new file mode 100644 index 00000000..779e18ab --- /dev/null +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java | |||
@@ -0,0 +1,272 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.semantics.model; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.xtext.testing.InjectWith; | ||
10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | ||
11 | import org.junit.jupiter.api.Disabled; | ||
12 | import org.junit.jupiter.api.Test; | ||
13 | import org.junit.jupiter.api.extension.ExtendWith; | ||
14 | import tools.refinery.language.ProblemStandaloneSetup; | ||
15 | import tools.refinery.language.model.tests.utils.ProblemParseHelper; | ||
16 | import tools.refinery.language.tests.ProblemInjectorProvider; | ||
17 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
18 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; | ||
19 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | ||
20 | import tools.refinery.store.model.ModelStore; | ||
21 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | ||
22 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
23 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
24 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
25 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
26 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; | ||
27 | import tools.refinery.store.statecoding.StateCoderAdapter; | ||
28 | import tools.refinery.visualization.ModelVisualizerAdapter; | ||
29 | import tools.refinery.visualization.internal.FileFormat; | ||
30 | |||
31 | import java.util.LinkedHashMap; | ||
32 | |||
33 | import static org.hamcrest.MatcherAssert.assertThat; | ||
34 | import static org.hamcrest.Matchers.empty; | ||
35 | |||
36 | @ExtendWith(InjectionExtension.class) | ||
37 | @InjectWith(ProblemInjectorProvider.class) | ||
38 | @Disabled("For debugging purposes only") | ||
39 | class ModelGenerationTest { | ||
40 | @Inject | ||
41 | private ProblemParseHelper parseHelper; | ||
42 | |||
43 | @Inject | ||
44 | private ModelInitializer modelInitializer; | ||
45 | |||
46 | @Test | ||
47 | void socialNetworkTest() { | ||
48 | var parsedProblem = parseHelper.parse(""" | ||
49 | % Metamodel | ||
50 | class Person { | ||
51 | contains Post posts opposite author | ||
52 | Person friend opposite friend | ||
53 | } | ||
54 | |||
55 | class Post { | ||
56 | container Person[0..1] author opposite posts | ||
57 | Post replyTo | ||
58 | } | ||
59 | |||
60 | % Constraints | ||
61 | error replyToNotFriend(Post x, Post y) <-> | ||
62 | replyTo(x, y), | ||
63 | author(x, xAuthor), | ||
64 | author(y, yAuthor), | ||
65 | xAuthor != yAuthor, | ||
66 | !friend(xAuthor, yAuthor). | ||
67 | |||
68 | error replyToCycle(Post x) <-> replyTo+(x, x). | ||
69 | |||
70 | % Instance model | ||
71 | !friend(a, b). | ||
72 | author(p1, a). | ||
73 | author(p2, b). | ||
74 | |||
75 | !author(Post::new, a). | ||
76 | |||
77 | % Scope | ||
78 | scope Post = 5, Person = 5. | ||
79 | """); | ||
80 | assertThat(parsedProblem.errors(), empty()); | ||
81 | var problem = parsedProblem.problem(); | ||
82 | |||
83 | var storeBuilder = ModelStore.builder() | ||
84 | .with(ViatraModelQueryAdapter.builder()) | ||
85 | .with(ModelVisualizerAdapter.builder() | ||
86 | .withOutputPath("test_output") | ||
87 | .withFormat(FileFormat.DOT) | ||
88 | .withFormat(FileFormat.SVG) | ||
89 | // .saveStates() | ||
90 | .saveDesignSpace()) | ||
91 | .with(PropagationAdapter.builder()) | ||
92 | .with(StateCoderAdapter.builder()) | ||
93 | .with(DesignSpaceExplorationAdapter.builder()) | ||
94 | .with(ReasoningAdapter.builder()); | ||
95 | |||
96 | var modelSeed = modelInitializer.createModel(problem, storeBuilder); | ||
97 | |||
98 | var store = storeBuilder.build(); | ||
99 | |||
100 | var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
101 | |||
102 | var initialVersion = initialModel.commit(); | ||
103 | |||
104 | var bestFirst = new BestFirstStoreManager(store, 1); | ||
105 | bestFirst.startExploration(initialVersion); | ||
106 | var resultStore = bestFirst.getSolutionStore(); | ||
107 | System.out.println("states size: " + resultStore.getSolutions().size()); | ||
108 | // initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore()); | ||
109 | } | ||
110 | |||
111 | @Test | ||
112 | void statechartTest() { | ||
113 | var parsedProblem = parseHelper.parse(""" | ||
114 | // Metamodel | ||
115 | abstract class CompositeElement { | ||
116 | contains Region[] regions | ||
117 | } | ||
118 | |||
119 | class Region { | ||
120 | contains Vertex[] vertices opposite region | ||
121 | } | ||
122 | |||
123 | abstract class Vertex { | ||
124 | container Region[0..1] region opposite vertices | ||
125 | Transition[] outgoingTransition opposite source | ||
126 | Transition[] incomingTransition opposite target | ||
127 | } | ||
128 | |||
129 | class Transition { | ||
130 | Vertex source opposite outgoingTransition | ||
131 | Vertex target opposite incomingTransition | ||
132 | } | ||
133 | |||
134 | abstract class Pseudostate extends Vertex {} | ||
135 | |||
136 | abstract class RegularState extends Vertex {} | ||
137 | |||
138 | class Entry extends Pseudostate {} | ||
139 | |||
140 | class Exit extends Pseudostate {} | ||
141 | |||
142 | class Choice extends Pseudostate {} | ||
143 | |||
144 | class FinalState extends RegularState {} | ||
145 | |||
146 | class State extends RegularState, CompositeElement {} | ||
147 | |||
148 | class Statechart extends CompositeElement {} | ||
149 | |||
150 | // Constraints | ||
151 | |||
152 | ///////// | ||
153 | // Entry | ||
154 | ///////// | ||
155 | |||
156 | pred entryInRegion(Region r, Entry e) <-> | ||
157 | vertices(r, e). | ||
158 | |||
159 | error noEntryInRegion(Region r) <-> | ||
160 | !entryInRegion(r, _). | ||
161 | |||
162 | error multipleEntryInRegion(Region r) <-> | ||
163 | entryInRegion(r, e1), | ||
164 | entryInRegion(r, e2), | ||
165 | e1 != e2. | ||
166 | |||
167 | error incomingToEntry(Transition t, Entry e) <-> | ||
168 | target(t, e). | ||
169 | |||
170 | error noOutgoingTransitionFromEntry(Entry e) <-> | ||
171 | !source(_, e). | ||
172 | |||
173 | error multipleTransitionFromEntry(Entry e, Transition t1, Transition t2) <-> | ||
174 | outgoingTransition(e, t1), | ||
175 | outgoingTransition(e, t2), | ||
176 | t1 != t2. | ||
177 | |||
178 | ///////// | ||
179 | // Exit | ||
180 | ///////// | ||
181 | |||
182 | error outgoingFromExit(Transition t, Exit e) <-> | ||
183 | source(t, e). | ||
184 | |||
185 | ///////// | ||
186 | // Final | ||
187 | ///////// | ||
188 | |||
189 | error outgoingFromFinal(Transition t, FinalState e) <-> | ||
190 | source(t, e). | ||
191 | |||
192 | ///////// | ||
193 | // State vs Region | ||
194 | ///////// | ||
195 | |||
196 | pred stateInRegion(Region r, State s) <-> | ||
197 | vertices(r, s). | ||
198 | |||
199 | error noStateInRegion(Region r) <-> | ||
200 | !stateInRegion(r, _). | ||
201 | |||
202 | ///////// | ||
203 | // Choice | ||
204 | ///////// | ||
205 | |||
206 | error choiceHasNoOutgoing(Choice c) <-> | ||
207 | !source(_, c). | ||
208 | |||
209 | error choiceHasNoIncoming(Choice c) <-> | ||
210 | !target(_, c). | ||
211 | |||
212 | scope node = 50..60, Statechart = 1. | ||
213 | """); | ||
214 | assertThat(parsedProblem.errors(), empty()); | ||
215 | var problem = parsedProblem.problem(); | ||
216 | |||
217 | var storeBuilder = ModelStore.builder() | ||
218 | .with(ViatraModelQueryAdapter.builder()) | ||
219 | // .with(ModelVisualizerAdapter.builder() | ||
220 | // .withOutputPath("test_output") | ||
221 | // .withFormat(FileFormat.DOT) | ||
222 | // .withFormat(FileFormat.SVG) | ||
223 | // .saveStates() | ||
224 | // .saveDesignSpace()) | ||
225 | .with(PropagationAdapter.builder()) | ||
226 | .with(StateCoderAdapter.builder()) | ||
227 | .with(DesignSpaceExplorationAdapter.builder()) | ||
228 | .with(ReasoningAdapter.builder()); | ||
229 | |||
230 | var modelSeed = modelInitializer.createModel(problem, storeBuilder); | ||
231 | |||
232 | var store = storeBuilder.build(); | ||
233 | |||
234 | var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
235 | |||
236 | var initialVersion = initialModel.commit(); | ||
237 | |||
238 | var bestFirst = new BestFirstStoreManager(store, 1); | ||
239 | bestFirst.startExploration(initialVersion); | ||
240 | var resultStore = bestFirst.getSolutionStore(); | ||
241 | System.out.println("states size: " + resultStore.getSolutions().size()); | ||
242 | |||
243 | var model = store.createModelForState(resultStore.getSolutions().get(0).version()); | ||
244 | var interpretation = model.getAdapter(ReasoningAdapter.class) | ||
245 | .getPartialInterpretation(Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL); | ||
246 | var cursor = interpretation.getAll(); | ||
247 | int max = -1; | ||
248 | var types = new LinkedHashMap<PartialRelation, Integer>(); | ||
249 | var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL); | ||
250 | while (cursor.move()) { | ||
251 | max = Math.max(max, cursor.getKey().get(0)); | ||
252 | var type = typeInterpretation.get(cursor.getKey()); | ||
253 | if (type != null) { | ||
254 | types.compute(type.candidateType(), (ignoredKey, oldValue) -> oldValue == null ? 1 : oldValue + 1); | ||
255 | } | ||
256 | } | ||
257 | System.out.println("Model size: " + (max + 1)); | ||
258 | System.out.println(types); | ||
259 | // initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore()); | ||
260 | } | ||
261 | |||
262 | public static void main(String[] args) { | ||
263 | ProblemStandaloneSetup.doSetup(); | ||
264 | var injector = new ProblemStandaloneSetup().createInjectorAndDoEMFRegistration(); | ||
265 | var test = injector.getInstance(ModelGenerationTest.class); | ||
266 | try { | ||
267 | test.statechartTest(); | ||
268 | } catch (AssertionError e) { | ||
269 | e.printStackTrace(); | ||
270 | } | ||
271 | } | ||
272 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java new file mode 100644 index 00000000..5ad61463 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java | |||
@@ -0,0 +1,11 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation; | ||
7 | |||
8 | @FunctionalInterface | ||
9 | public interface BoundPropagator { | ||
10 | PropagationResult propagateOne(); | ||
11 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java new file mode 100644 index 00000000..3ea5a75f --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java | |||
@@ -0,0 +1,20 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelAdapter; | ||
9 | import tools.refinery.store.dse.propagation.impl.PropagationBuilderImpl; | ||
10 | |||
11 | public interface PropagationAdapter extends ModelAdapter { | ||
12 | @Override | ||
13 | PropagationStoreAdapter getStoreAdapter(); | ||
14 | |||
15 | PropagationResult propagate(); | ||
16 | |||
17 | static PropagationBuilder builder() { | ||
18 | return new PropagationBuilderImpl(); | ||
19 | } | ||
20 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java new file mode 100644 index 00000000..f8a89b30 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java | |||
@@ -0,0 +1,32 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelAdapterBuilder; | ||
9 | import tools.refinery.store.dse.transition.Rule; | ||
10 | import tools.refinery.store.model.ModelStore; | ||
11 | |||
12 | import java.util.Collection; | ||
13 | import java.util.List; | ||
14 | |||
15 | @SuppressWarnings("UnusedReturnValue") | ||
16 | public interface PropagationBuilder extends ModelAdapterBuilder { | ||
17 | PropagationBuilder rule(Rule propagationRule); | ||
18 | |||
19 | default PropagationBuilder rules(Rule... propagationRules) { | ||
20 | return rules(List.of(propagationRules)); | ||
21 | } | ||
22 | |||
23 | default PropagationBuilder rules(Collection<Rule> propagationRules) { | ||
24 | propagationRules.forEach(this::rule); | ||
25 | return this; | ||
26 | } | ||
27 | |||
28 | PropagationBuilder propagator(Propagator propagator); | ||
29 | |||
30 | @Override | ||
31 | PropagationStoreAdapter build(ModelStore store); | ||
32 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java index 1bc537d1..ea56653a 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java | |||
@@ -3,17 +3,17 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.refinement; | 6 | package tools.refinery.store.dse.propagation; |
7 | 7 | ||
8 | public enum RefinementResult { | 8 | public enum PropagationResult { |
9 | UNCHANGED, | 9 | UNCHANGED, |
10 | REFINED, | 10 | PROPAGATED, |
11 | REJECTED; | 11 | REJECTED; |
12 | 12 | ||
13 | public RefinementResult andThen(RefinementResult next) { | 13 | public PropagationResult andThen(PropagationResult next) { |
14 | return switch (this) { | 14 | return switch (this) { |
15 | case UNCHANGED -> next; | 15 | case UNCHANGED -> next; |
16 | case REFINED -> next == REJECTED ? REJECTED : REFINED; | 16 | case PROPAGATED -> next == REJECTED ? REJECTED : PROPAGATED; |
17 | case REJECTED -> REJECTED; | 17 | case REJECTED -> REJECTED; |
18 | }; | 18 | }; |
19 | } | 19 | } |
@@ -21,4 +21,8 @@ public enum RefinementResult { | |||
21 | public boolean isRejected() { | 21 | public boolean isRejected() { |
22 | return this == REJECTED; | 22 | return this == REJECTED; |
23 | } | 23 | } |
24 | |||
25 | public boolean isChanged() { | ||
26 | return this == PROPAGATED; | ||
27 | } | ||
24 | } | 28 | } |
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java new file mode 100644 index 00000000..82cba909 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java | |||
@@ -0,0 +1,14 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelStoreAdapter; | ||
9 | import tools.refinery.store.model.Model; | ||
10 | |||
11 | public interface PropagationStoreAdapter extends ModelStoreAdapter { | ||
12 | @Override | ||
13 | PropagationAdapter createModelAdapter(Model model); | ||
14 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java new file mode 100644 index 00000000..c6b4e1c9 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java | |||
@@ -0,0 +1,17 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.model.ModelStoreBuilder; | ||
10 | |||
11 | @FunctionalInterface | ||
12 | public interface Propagator { | ||
13 | default void configure(ModelStoreBuilder storeBuilder) { | ||
14 | } | ||
15 | |||
16 | BoundPropagator bindToModel(Model model); | ||
17 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java new file mode 100644 index 00000000..586a8d7a --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java | |||
@@ -0,0 +1,72 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation.impl; | ||
7 | |||
8 | import tools.refinery.store.dse.propagation.BoundPropagator; | ||
9 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
10 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
11 | import tools.refinery.store.dse.propagation.PropagationStoreAdapter; | ||
12 | import tools.refinery.store.model.Model; | ||
13 | |||
14 | class PropagationAdapterImpl implements PropagationAdapter { | ||
15 | private final Model model; | ||
16 | private final PropagationStoreAdapterImpl storeAdapter; | ||
17 | private final BoundPropagator[] boundPropagators; | ||
18 | |||
19 | public PropagationAdapterImpl(Model model, PropagationStoreAdapterImpl storeAdapter) { | ||
20 | this.model = model; | ||
21 | this.storeAdapter = storeAdapter; | ||
22 | var propagators = storeAdapter.getPropagators(); | ||
23 | boundPropagators = new BoundPropagator[propagators.size()]; | ||
24 | for (int i = 0; i < boundPropagators.length; i++) { | ||
25 | boundPropagators[i] = propagators.get(i).bindToModel(model); | ||
26 | } | ||
27 | } | ||
28 | |||
29 | @Override | ||
30 | public PropagationResult propagate() { | ||
31 | PropagationResult result = PropagationResult.UNCHANGED; | ||
32 | PropagationResult lastResult; | ||
33 | do { | ||
34 | lastResult = propagateOne(); | ||
35 | result = result.andThen(lastResult); | ||
36 | } while (lastResult.isChanged()); | ||
37 | return result; | ||
38 | } | ||
39 | |||
40 | private PropagationResult propagateOne() { | ||
41 | PropagationResult result = PropagationResult.UNCHANGED; | ||
42 | for (int i = 0; i < boundPropagators.length; i++) { | ||
43 | var lastResult = propagateUntilFixedPoint(i); | ||
44 | result = result.andThen(lastResult); | ||
45 | if (result.isRejected()) { | ||
46 | break; | ||
47 | } | ||
48 | } | ||
49 | return result; | ||
50 | } | ||
51 | |||
52 | private PropagationResult propagateUntilFixedPoint(int propagatorIndex) { | ||
53 | var propagator = boundPropagators[propagatorIndex]; | ||
54 | PropagationResult result = PropagationResult.UNCHANGED; | ||
55 | PropagationResult lastResult; | ||
56 | do { | ||
57 | lastResult = propagator.propagateOne(); | ||
58 | result = result.andThen(lastResult); | ||
59 | } while (lastResult.isChanged()); | ||
60 | return result; | ||
61 | } | ||
62 | |||
63 | @Override | ||
64 | public Model getModel() { | ||
65 | return model; | ||
66 | } | ||
67 | |||
68 | @Override | ||
69 | public PropagationStoreAdapter getStoreAdapter() { | ||
70 | return storeAdapter; | ||
71 | } | ||
72 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java new file mode 100644 index 00000000..c844a89f --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java | |||
@@ -0,0 +1,53 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation.impl; | ||
7 | |||
8 | import tools.refinery.store.adapter.AbstractModelAdapterBuilder; | ||
9 | import tools.refinery.store.dse.propagation.PropagationBuilder; | ||
10 | import tools.refinery.store.dse.propagation.PropagationStoreAdapter; | ||
11 | import tools.refinery.store.dse.propagation.Propagator; | ||
12 | import tools.refinery.store.dse.propagation.impl.rule.RuleBasedPropagator; | ||
13 | import tools.refinery.store.dse.transition.Rule; | ||
14 | import tools.refinery.store.model.ModelStore; | ||
15 | import tools.refinery.store.model.ModelStoreBuilder; | ||
16 | |||
17 | import java.util.*; | ||
18 | |||
19 | public class PropagationBuilderImpl extends AbstractModelAdapterBuilder<PropagationStoreAdapter> | ||
20 | implements PropagationBuilder { | ||
21 | private final Set<Rule> propagationRules = new LinkedHashSet<>(); | ||
22 | private final Deque<Propagator> propagators = new ArrayDeque<>(); | ||
23 | |||
24 | @Override | ||
25 | public PropagationBuilder rule(Rule propagationRule) { | ||
26 | checkNotConfigured(); | ||
27 | propagationRules.add(propagationRule); | ||
28 | return this; | ||
29 | } | ||
30 | |||
31 | @Override | ||
32 | public PropagationBuilder propagator(Propagator propagator) { | ||
33 | checkNotConfigured(); | ||
34 | propagators.addFirst(propagator); | ||
35 | return this; | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | ||
40 | super.doConfigure(storeBuilder); | ||
41 | if (!propagationRules.isEmpty()) { | ||
42 | propagators.addFirst(new RuleBasedPropagator(List.copyOf(propagationRules))); | ||
43 | } | ||
44 | for (var propagator : propagators) { | ||
45 | propagator.configure(storeBuilder); | ||
46 | } | ||
47 | } | ||
48 | |||
49 | @Override | ||
50 | protected PropagationStoreAdapter doBuild(ModelStore store) { | ||
51 | return new PropagationStoreAdapterImpl(store, List.copyOf(propagators)); | ||
52 | } | ||
53 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java new file mode 100644 index 00000000..a223caed --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java | |||
@@ -0,0 +1,38 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation.impl; | ||
7 | |||
8 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
9 | import tools.refinery.store.dse.propagation.PropagationStoreAdapter; | ||
10 | import tools.refinery.store.dse.propagation.Propagator; | ||
11 | import tools.refinery.store.model.Model; | ||
12 | import tools.refinery.store.model.ModelStore; | ||
13 | |||
14 | import java.util.List; | ||
15 | |||
16 | class PropagationStoreAdapterImpl implements PropagationStoreAdapter { | ||
17 | private final ModelStore store; | ||
18 | private final List<Propagator> propagators; | ||
19 | |||
20 | PropagationStoreAdapterImpl(ModelStore store, List<Propagator> propagators) { | ||
21 | this.store = store; | ||
22 | this.propagators = propagators; | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public ModelStore getStore() { | ||
27 | return store; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public PropagationAdapter createModelAdapter(Model model) { | ||
32 | return new PropagationAdapterImpl(model, this); | ||
33 | } | ||
34 | |||
35 | List<Propagator> getPropagators() { | ||
36 | return propagators; | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java new file mode 100644 index 00000000..6e6a78d2 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java | |||
@@ -0,0 +1,37 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation.impl.rule; | ||
7 | |||
8 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
9 | import tools.refinery.store.dse.transition.Rule; | ||
10 | import tools.refinery.store.dse.transition.actions.BoundAction; | ||
11 | import tools.refinery.store.model.Model; | ||
12 | import tools.refinery.store.query.ModelQueryAdapter; | ||
13 | import tools.refinery.store.query.resultset.ResultSet; | ||
14 | |||
15 | class BoundPropagationRule { | ||
16 | private final ResultSet<Boolean> resultSet; | ||
17 | private final BoundAction action; | ||
18 | |||
19 | public BoundPropagationRule(Model model, Rule rule) { | ||
20 | resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(rule.getPrecondition()); | ||
21 | action = rule.createAction(model); | ||
22 | } | ||
23 | |||
24 | public PropagationResult fireAll() { | ||
25 | if (resultSet.size() == 0) { | ||
26 | return PropagationResult.UNCHANGED; | ||
27 | } | ||
28 | var cursor = resultSet.getAll(); | ||
29 | while (cursor.move()) { | ||
30 | var result = action.fire(cursor.getKey()); | ||
31 | if (!result) { | ||
32 | return PropagationResult.REJECTED; | ||
33 | } | ||
34 | } | ||
35 | return PropagationResult.PROPAGATED; | ||
36 | } | ||
37 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java new file mode 100644 index 00000000..bd03f923 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java | |||
@@ -0,0 +1,43 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation.impl.rule; | ||
7 | |||
8 | import tools.refinery.store.dse.propagation.BoundPropagator; | ||
9 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
10 | import tools.refinery.store.dse.transition.Rule; | ||
11 | import tools.refinery.store.model.Model; | ||
12 | import tools.refinery.store.query.ModelQueryAdapter; | ||
13 | |||
14 | import java.util.List; | ||
15 | |||
16 | public class BoundRuleBasedPropagator implements BoundPropagator { | ||
17 | private final ModelQueryAdapter queryEngine; | ||
18 | private final BoundPropagationRule[] boundRules; | ||
19 | |||
20 | public BoundRuleBasedPropagator(Model model, List<Rule> propagationRules) { | ||
21 | queryEngine = model.getAdapter(ModelQueryAdapter.class); | ||
22 | boundRules = new BoundPropagationRule[propagationRules.size()]; | ||
23 | for (int i = 0; i < boundRules.length; i++) { | ||
24 | boundRules[i] = new BoundPropagationRule(model, propagationRules.get(i)); | ||
25 | } | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public PropagationResult propagateOne() { | ||
30 | queryEngine.flushChanges(); | ||
31 | PropagationResult result = PropagationResult.UNCHANGED; | ||
32 | // Use a classic for loop to avoid allocating an iterator. | ||
33 | //noinspection ForLoopReplaceableByForEach | ||
34 | for (int i = 0; i < boundRules.length; i++) { | ||
35 | var lastResult = boundRules[i].fireAll(); | ||
36 | result = result.andThen(lastResult); | ||
37 | if (result.isRejected()) { | ||
38 | break; | ||
39 | } | ||
40 | } | ||
41 | return result; | ||
42 | } | ||
43 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java new file mode 100644 index 00000000..709b2416 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java | |||
@@ -0,0 +1,36 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.dse.propagation.impl.rule; | ||
7 | |||
8 | import tools.refinery.store.dse.propagation.BoundPropagator; | ||
9 | import tools.refinery.store.dse.propagation.Propagator; | ||
10 | import tools.refinery.store.dse.transition.Rule; | ||
11 | import tools.refinery.store.model.Model; | ||
12 | import tools.refinery.store.model.ModelStoreBuilder; | ||
13 | import tools.refinery.store.query.ModelQueryBuilder; | ||
14 | |||
15 | import java.util.List; | ||
16 | |||
17 | public class RuleBasedPropagator implements Propagator { | ||
18 | private final List<Rule> propagationRules; | ||
19 | |||
20 | public RuleBasedPropagator(List<Rule> propagationRules) { | ||
21 | this.propagationRules = propagationRules; | ||
22 | } | ||
23 | |||
24 | @Override | ||
25 | public void configure(ModelStoreBuilder storeBuilder) { | ||
26 | var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); | ||
27 | for (var propagationRule : propagationRules) { | ||
28 | queryBuilder.query(propagationRule.getPrecondition()); | ||
29 | } | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public BoundPropagator bindToModel(Model model) { | ||
34 | return new BoundRuleBasedPropagator(model, propagationRules); | ||
35 | } | ||
36 | } | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java index 8f7e3bdc..4a75a3a6 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java | |||
@@ -33,7 +33,11 @@ public class BestFirstExplorer extends BestFirstWorker { | |||
33 | var lastBest = submit().newVersion(); | 33 | var lastBest = submit().newVersion(); |
34 | while (shouldRun()) { | 34 | while (shouldRun()) { |
35 | if (lastBest == null) { | 35 | if (lastBest == null) { |
36 | lastBest = restoreToBest(); | 36 | if (random.nextInt(10) == 0) { |
37 | lastBest = restoreToRandom(random); | ||
38 | } else { | ||
39 | lastBest = restoreToBest(); | ||
40 | } | ||
37 | if (lastBest == null) { | 41 | if (lastBest == null) { |
38 | return; | 42 | return; |
39 | } | 43 | } |
@@ -49,7 +53,7 @@ public class BestFirstExplorer extends BestFirstWorker { | |||
49 | } else { | 53 | } else { |
50 | var newVisit = newSubmit.newVersion(); | 54 | var newVisit = newSubmit.newVersion(); |
51 | int compareResult = compare(lastBest, newVisit); | 55 | int compareResult = compare(lastBest, newVisit); |
52 | if (compareResult >= 0) { | 56 | if (compareResult >= 0) { |
53 | lastBest = newVisit; | 57 | lastBest = newVisit; |
54 | } else { | 58 | } else { |
55 | lastBest = null; | 59 | lastBest = null; |
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java index 5d738297..aca800a3 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java | |||
@@ -5,6 +5,8 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.dse.strategy; | 6 | package tools.refinery.store.dse.strategy; |
7 | 7 | ||
8 | import org.jetbrains.annotations.Nullable; | ||
9 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
8 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | 10 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; |
9 | import tools.refinery.store.dse.transition.ObjectiveValue; | 11 | import tools.refinery.store.dse.transition.ObjectiveValue; |
10 | import tools.refinery.store.dse.transition.VersionWithObjectiveValue; | 12 | import tools.refinery.store.dse.transition.VersionWithObjectiveValue; |
@@ -24,6 +26,7 @@ public class BestFirstWorker { | |||
24 | final StateCoderAdapter stateCoderAdapter; | 26 | final StateCoderAdapter stateCoderAdapter; |
25 | final DesignSpaceExplorationAdapter explorationAdapter; | 27 | final DesignSpaceExplorationAdapter explorationAdapter; |
26 | final ModelQueryAdapter queryAdapter; | 28 | final ModelQueryAdapter queryAdapter; |
29 | final @Nullable PropagationAdapter propagationAdapter; | ||
27 | final VisualizationStore visualizationStore; | 30 | final VisualizationStore visualizationStore; |
28 | final boolean isVisualizationEnabled; | 31 | final boolean isVisualizationEnabled; |
29 | 32 | ||
@@ -34,6 +37,7 @@ public class BestFirstWorker { | |||
34 | explorationAdapter = model.getAdapter(DesignSpaceExplorationAdapter.class); | 37 | explorationAdapter = model.getAdapter(DesignSpaceExplorationAdapter.class); |
35 | stateCoderAdapter = model.getAdapter(StateCoderAdapter.class); | 38 | stateCoderAdapter = model.getAdapter(StateCoderAdapter.class); |
36 | queryAdapter = model.getAdapter(ModelQueryAdapter.class); | 39 | queryAdapter = model.getAdapter(ModelQueryAdapter.class); |
40 | propagationAdapter = model.tryGetAdapter(PropagationAdapter.class).orElse(null); | ||
37 | activationStoreWorker = new ActivationStoreWorker(storeManager.getActivationStore(), | 41 | activationStoreWorker = new ActivationStoreWorker(storeManager.getActivationStore(), |
38 | explorationAdapter.getTransformations()); | 42 | explorationAdapter.getTransformations()); |
39 | visualizationStore = storeManager.getVisualizationStore(); | 43 | visualizationStore = storeManager.getVisualizationStore(); |
@@ -96,7 +100,11 @@ public class BestFirstWorker { | |||
96 | } | 100 | } |
97 | 101 | ||
98 | public VersionWithObjectiveValue restoreToRandom(Random random) { | 102 | public VersionWithObjectiveValue restoreToRandom(Random random) { |
99 | var randomVersion = storeManager.getObjectiveStore().getRandom(random); | 103 | var objectiveStore = storeManager.getObjectiveStore(); |
104 | if (objectiveStore.getSize() == 0) { | ||
105 | return null; | ||
106 | } | ||
107 | var randomVersion = objectiveStore.getRandom(random); | ||
100 | last = randomVersion; | 108 | last = randomVersion; |
101 | if (randomVersion != null) { | 109 | if (randomVersion != null) { |
102 | this.model.restore(randomVersion.version()); | 110 | this.model.restore(randomVersion.version()); |
@@ -108,41 +116,40 @@ public class BestFirstWorker { | |||
108 | return storeManager.getObjectiveStore().getComparator().compare(s1, s2); | 116 | return storeManager.getObjectiveStore().getComparator().compare(s1, s2); |
109 | } | 117 | } |
110 | 118 | ||
111 | public boolean stateHasUnvisited() { | ||
112 | if (!model.hasUncommittedChanges()) { | ||
113 | return storeManager.getActivationStore().hasUnmarkedActivation(last); | ||
114 | } else { | ||
115 | throw new IllegalStateException("The model has uncommitted changes!"); | ||
116 | } | ||
117 | } | ||
118 | |||
119 | public record RandomVisitResult(SubmitResult submitResult, boolean shouldRetry) { | 119 | public record RandomVisitResult(SubmitResult submitResult, boolean shouldRetry) { |
120 | } | 120 | } |
121 | 121 | ||
122 | public RandomVisitResult visitRandomUnvisited(Random random) { | 122 | public RandomVisitResult visitRandomUnvisited(Random random) { |
123 | checkSynchronized(); | 123 | checkSynchronized(); |
124 | if (!model.hasUncommittedChanges()) { | 124 | if (model.hasUncommittedChanges()) { |
125 | var visitResult = activationStoreWorker.fireRandomActivation(this.last, random); | 125 | throw new IllegalStateException("The model has uncommitted changes!"); |
126 | queryAdapter.flushChanges(); | 126 | } |
127 | 127 | ||
128 | if (visitResult.successfulVisit()) { | 128 | var visitResult = activationStoreWorker.fireRandomActivation(this.last, random); |
129 | Version oldVersion = null; | 129 | |
130 | if (isVisualizationEnabled) { | 130 | if (!visitResult.successfulVisit()) { |
131 | oldVersion = last.version(); | 131 | return new RandomVisitResult(null, visitResult.mayHaveMore()); |
132 | } | 132 | } |
133 | var submitResult = submit(); | 133 | |
134 | if (isVisualizationEnabled && submitResult.newVersion() != null) { | 134 | if (propagationAdapter != null) { |
135 | var newVersion = submitResult.newVersion().version(); | 135 | var propagationResult = propagationAdapter.propagate(); |
136 | visualizationStore.addTransition(oldVersion, newVersion, | 136 | if (propagationResult.isRejected()) { |
137 | "fire: " + visitResult.transformation() + ", " + visitResult.activation()); | ||
138 | } | ||
139 | return new RandomVisitResult(submitResult, visitResult.mayHaveMore()); | ||
140 | } else { | ||
141 | return new RandomVisitResult(null, visitResult.mayHaveMore()); | 137 | return new RandomVisitResult(null, visitResult.mayHaveMore()); |
142 | } | 138 | } |
143 | } else { | ||
144 | throw new IllegalStateException("The model has uncommitted changes!"); | ||
145 | } | 139 | } |
140 | queryAdapter.flushChanges(); | ||
141 | |||
142 | Version oldVersion = null; | ||
143 | if (isVisualizationEnabled) { | ||
144 | oldVersion = last.version(); | ||
145 | } | ||
146 | var submitResult = submit(); | ||
147 | if (isVisualizationEnabled && submitResult.newVersion() != null) { | ||
148 | var newVersion = submitResult.newVersion().version(); | ||
149 | visualizationStore.addTransition(oldVersion, newVersion, | ||
150 | "fire: " + visitResult.transformation() + ", " + visitResult.activation()); | ||
151 | } | ||
152 | return new RandomVisitResult(submitResult, visitResult.mayHaveMore()); | ||
146 | } | 153 | } |
147 | 154 | ||
148 | public boolean hasEnoughSolution() { | 155 | public boolean hasEnoughSolution() { |
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java index 55f43735..ed2ff33d 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java | |||
@@ -11,18 +11,14 @@ import tools.refinery.store.tuple.Tuple; | |||
11 | 11 | ||
12 | public class BoundAction { | 12 | public class BoundAction { |
13 | private final Action action; | 13 | private final Action action; |
14 | private final BoundActionLiteral[] boundLiterals; | 14 | private final Model model; |
15 | private BoundActionLiteral @Nullable [] boundLiterals; | ||
15 | private Tuple activation; | 16 | private Tuple activation; |
16 | private final int[] localVariables; | 17 | private final int[] localVariables; |
17 | 18 | ||
18 | BoundAction(Action action, Model model) { | 19 | BoundAction(Action action, Model model) { |
19 | this.action = action; | 20 | this.action = action; |
20 | var actionLiterals = action.getActionLiterals(); | 21 | this.model = model; |
21 | int size = actionLiterals.size(); | ||
22 | boundLiterals = new BoundActionLiteral[size]; | ||
23 | for (int i = 0; i < size; i++) { | ||
24 | boundLiterals[i] = actionLiterals.get(i).bindToModel(model); | ||
25 | } | ||
26 | localVariables = new int[action.getLocalVariables().size()]; | 22 | localVariables = new int[action.getLocalVariables().size()]; |
27 | } | 23 | } |
28 | 24 | ||
@@ -31,6 +27,9 @@ public class BoundAction { | |||
31 | throw new IllegalStateException("Reentrant firing is not allowed"); | 27 | throw new IllegalStateException("Reentrant firing is not allowed"); |
32 | } | 28 | } |
33 | this.activation = activation; | 29 | this.activation = activation; |
30 | if (boundLiterals == null) { | ||
31 | boundLiterals = bindLiterals(); | ||
32 | } | ||
34 | try { | 33 | try { |
35 | int size = boundLiterals.length; | 34 | int size = boundLiterals.length; |
36 | for (int i = 0; i < size; i++) { | 35 | for (int i = 0; i < size; i++) { |
@@ -50,6 +49,16 @@ public class BoundAction { | |||
50 | return true; | 49 | return true; |
51 | } | 50 | } |
52 | 51 | ||
52 | private BoundActionLiteral[] bindLiterals() { | ||
53 | var actionLiterals = action.getActionLiterals(); | ||
54 | int size = actionLiterals.size(); | ||
55 | var boundLiteralsArray = new BoundActionLiteral[size]; | ||
56 | for (int i = 0; i < size; i++) { | ||
57 | boundLiteralsArray[i] = actionLiterals.get(i).bindToModel(model); | ||
58 | } | ||
59 | return boundLiteralsArray; | ||
60 | } | ||
61 | |||
53 | private Tuple getInputTuple(int @Nullable [] inputAllocation) { | 62 | private Tuple getInputTuple(int @Nullable [] inputAllocation) { |
54 | if (inputAllocation == null) { | 63 | if (inputAllocation == null) { |
55 | // Identity allocation. | 64 | // Identity allocation. |
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java index 9f4bb536..5a7ba8f4 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java | |||
@@ -28,9 +28,9 @@ public class QueryObjective implements Objective { | |||
28 | return () -> { | 28 | return () -> { |
29 | var cursor = resultSet.getAll(); | 29 | var cursor = resultSet.getAll(); |
30 | if (!cursor.move()) { | 30 | if (!cursor.move()) { |
31 | throw new IllegalStateException("Query providing the objective function has no values!"); | 31 | return 0; |
32 | } | 32 | } |
33 | return cursor.getValue().doubleValue(); | 33 | return Math.max(cursor.getValue().doubleValue(), 0); |
34 | }; | 34 | }; |
35 | } | 35 | } |
36 | 36 | ||
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java index d9e29eca..82f89db7 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java | |||
@@ -104,9 +104,16 @@ public class ActivationStoreImpl implements ActivationStore { | |||
104 | public synchronized VisitResult getRandomAndMarkAsVisited(VersionWithObjectiveValue version, Random random) { | 104 | public synchronized VisitResult getRandomAndMarkAsVisited(VersionWithObjectiveValue version, Random random) { |
105 | var entries = versionToActivations.get(version); | 105 | var entries = versionToActivations.get(version); |
106 | 106 | ||
107 | var weights = new double[entries.size()]; | ||
108 | double totalWeight = 0; | ||
107 | int numberOfAllUnvisitedActivations = 0; | 109 | int numberOfAllUnvisitedActivations = 0; |
108 | for (var entry : entries) { | 110 | for (int i = 0; i < weights.length; i++) { |
109 | numberOfAllUnvisitedActivations += entry.getNumberOfUnvisitedActivations(); | 111 | var entry = entries.get(i); |
112 | int unvisited = entry.getNumberOfUnvisitedActivations(); | ||
113 | double weight = unvisited == 0 ? 0 : unvisited; //(Math.log(unvisited) + 1.0); | ||
114 | weights[i] = weight; | ||
115 | totalWeight += weight; | ||
116 | numberOfAllUnvisitedActivations += unvisited; | ||
110 | } | 117 | } |
111 | 118 | ||
112 | if (numberOfAllUnvisitedActivations == 0) { | 119 | if (numberOfAllUnvisitedActivations == 0) { |
@@ -114,18 +121,18 @@ public class ActivationStoreImpl implements ActivationStore { | |||
114 | return new VisitResult(false, false, -1, -1); | 121 | return new VisitResult(false, false, -1, -1); |
115 | } | 122 | } |
116 | 123 | ||
117 | int offset = random.nextInt(numberOfAllUnvisitedActivations); | 124 | double offset = random.nextDouble(totalWeight); |
118 | int transformation = 0; | 125 | int transformation = 0; |
119 | for (; transformation < entries.size(); transformation++) { | 126 | for (; transformation < entries.size(); transformation++) { |
120 | var entry = entries.get(transformation); | 127 | double weight = weights[transformation]; |
121 | int unvisited = entry.getNumberOfUnvisitedActivations(); | 128 | if (weight > 0 && offset < weight) { |
122 | if (unvisited > 0 && offset < unvisited) { | 129 | var entry = entries.get(transformation); |
123 | int activation = random.nextInt(entry.getNumberOfActivations()); | 130 | int activation = random.nextInt(entry.getNumberOfActivations()); |
124 | return this.visitActivation(version, transformation, activation); | 131 | return this.visitActivation(version, transformation, activation); |
125 | } | 132 | } |
126 | offset -= unvisited; | 133 | offset -= weight; |
127 | } | 134 | } |
128 | 135 | ||
129 | throw new AssertionError("Unvisited activation %d not found".formatted(offset)); | 136 | throw new AssertionError("Unvisited activation %f not found".formatted(offset)); |
130 | } | 137 | } |
131 | } | 138 | } |
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java index 881b133c..1d7c5ce5 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java | |||
@@ -32,7 +32,7 @@ public class ActivationStoreWorker { | |||
32 | 32 | ||
33 | public ActivationStore.VisitResult fireRandomActivation(VersionWithObjectiveValue thisVersion, Random random) { | 33 | public ActivationStore.VisitResult fireRandomActivation(VersionWithObjectiveValue thisVersion, Random random) { |
34 | var result = store.getRandomAndMarkAsVisited(thisVersion, random); | 34 | var result = store.getRandomAndMarkAsVisited(thisVersion, random); |
35 | if(result.successfulVisit()) { | 35 | if (result.successfulVisit()) { |
36 | int selectedTransformation = result.transformation(); | 36 | int selectedTransformation = result.transformation(); |
37 | int selectedActivation = result.activation(); | 37 | int selectedActivation = result.activation(); |
38 | 38 | ||
@@ -40,13 +40,13 @@ public class ActivationStoreWorker { | |||
40 | var tuple = transformation.getActivation(selectedActivation); | 40 | var tuple = transformation.getActivation(selectedActivation); |
41 | 41 | ||
42 | boolean success = transformation.fireActivation(tuple); | 42 | boolean success = transformation.fireActivation(tuple); |
43 | if(success) { | 43 | if (success) { |
44 | return result; | 44 | return result; |
45 | } else { | 45 | } else { |
46 | return new ActivationStore.VisitResult( | 46 | return new ActivationStore.VisitResult( |
47 | false, | 47 | false, |
48 | result.mayHaveMore(), | 48 | result.mayHaveMore(), |
49 | selectedActivation, | 49 | selectedTransformation, |
50 | selectedActivation); | 50 | selectedActivation); |
51 | } | 51 | } |
52 | } | 52 | } |
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java index 99c501ce..62aadb4a 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java | |||
@@ -3,7 +3,7 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.scope.internal; | 6 | package tools.refinery.store.reasoning.scope; |
7 | 7 | ||
8 | import com.google.ortools.linearsolver.MPConstraint; | 8 | import com.google.ortools.linearsolver.MPConstraint; |
9 | import com.google.ortools.linearsolver.MPObjective; | 9 | import com.google.ortools.linearsolver.MPObjective; |
@@ -13,18 +13,15 @@ import org.eclipse.collections.api.factory.primitive.IntObjectMaps; | |||
13 | import org.eclipse.collections.api.factory.primitive.IntSets; | 13 | import org.eclipse.collections.api.factory.primitive.IntSets; |
14 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; | 14 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; |
15 | import org.eclipse.collections.api.set.primitive.MutableIntSet; | 15 | import org.eclipse.collections.api.set.primitive.MutableIntSet; |
16 | import tools.refinery.store.dse.propagation.BoundPropagator; | ||
17 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
16 | import tools.refinery.store.model.Interpretation; | 18 | import tools.refinery.store.model.Interpretation; |
17 | import tools.refinery.store.model.Model; | 19 | import tools.refinery.store.model.Model; |
18 | import tools.refinery.store.query.ModelQueryAdapter; | 20 | import tools.refinery.store.query.ModelQueryAdapter; |
19 | import tools.refinery.store.reasoning.refinement.RefinementResult; | ||
20 | import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter; | ||
21 | import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; | ||
22 | import tools.refinery.store.representation.cardinality.*; | 21 | import tools.refinery.store.representation.cardinality.*; |
23 | import tools.refinery.store.tuple.Tuple; | 22 | import tools.refinery.store.tuple.Tuple; |
24 | 23 | ||
25 | class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | 24 | class BoundScopePropagator implements BoundPropagator { |
26 | private final Model model; | ||
27 | private final ScopePropagatorStoreAdapterImpl storeAdapter; | ||
28 | private final ModelQueryAdapter queryEngine; | 25 | private final ModelQueryAdapter queryEngine; |
29 | private final Interpretation<CardinalityInterval> countInterpretation; | 26 | private final Interpretation<CardinalityInterval> countInterpretation; |
30 | private final MPSolver solver; | 27 | private final MPSolver solver; |
@@ -34,30 +31,22 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | |||
34 | private final TypeScopePropagator[] propagators; | 31 | private final TypeScopePropagator[] propagators; |
35 | private boolean changed = true; | 32 | private boolean changed = true; |
36 | 33 | ||
37 | public ScopePropagatorAdapterImpl(Model model, ScopePropagatorStoreAdapterImpl storeAdapter) { | 34 | public BoundScopePropagator(Model model, ScopePropagator storeAdapter) { |
38 | this.model = model; | ||
39 | this.storeAdapter = storeAdapter; | ||
40 | queryEngine = model.getAdapter(ModelQueryAdapter.class); | 35 | queryEngine = model.getAdapter(ModelQueryAdapter.class); |
41 | countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); | 36 | countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); |
42 | solver = MPSolver.createSolver("GLOP"); | 37 | solver = MPSolver.createSolver("GLOP"); |
43 | objective = solver.objective(); | 38 | objective = solver.objective(); |
44 | initializeVariables(); | 39 | initializeVariables(); |
45 | countInterpretation.addListener(this::countChanged, true); | 40 | countInterpretation.addListener(this::countChanged, true); |
46 | var propagatorFactories = storeAdapter.getPropagatorFactories(); | 41 | var propagatorFactories = storeAdapter.getTypeScopePropagatorFactories(); |
47 | propagators = new TypeScopePropagator[propagatorFactories.size()]; | 42 | propagators = new TypeScopePropagator[propagatorFactories.size()]; |
48 | for (int i = 0; i < propagators.length; i++) { | 43 | for (int i = 0; i < propagators.length; i++) { |
49 | propagators[i] = propagatorFactories.get(i).createPropagator(this); | 44 | propagators[i] = propagatorFactories.get(i).createPropagator(this); |
50 | } | 45 | } |
51 | } | 46 | } |
52 | 47 | ||
53 | @Override | 48 | ModelQueryAdapter getQueryEngine() { |
54 | public Model getModel() { | 49 | return queryEngine; |
55 | return model; | ||
56 | } | ||
57 | |||
58 | @Override | ||
59 | public ScopePropagatorStoreAdapter getStoreAdapter() { | ||
60 | return storeAdapter; | ||
61 | } | 50 | } |
62 | 51 | ||
63 | private void initializeVariables() { | 52 | private void initializeVariables() { |
@@ -149,29 +138,16 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | |||
149 | } | 138 | } |
150 | 139 | ||
151 | @Override | 140 | @Override |
152 | public RefinementResult propagate() { | 141 | public PropagationResult propagateOne() { |
153 | var result = RefinementResult.UNCHANGED; | ||
154 | RefinementResult currentRoundResult; | ||
155 | do { | ||
156 | currentRoundResult = propagateOne(); | ||
157 | result = result.andThen(currentRoundResult); | ||
158 | if (result.isRejected()) { | ||
159 | return result; | ||
160 | } | ||
161 | } while (currentRoundResult != RefinementResult.UNCHANGED); | ||
162 | return result; | ||
163 | } | ||
164 | |||
165 | private RefinementResult propagateOne() { | ||
166 | queryEngine.flushChanges(); | 142 | queryEngine.flushChanges(); |
167 | if (!changed) { | 143 | if (!changed) { |
168 | return RefinementResult.UNCHANGED; | 144 | return PropagationResult.UNCHANGED; |
169 | } | 145 | } |
170 | changed = false; | 146 | changed = false; |
171 | for (var propagator : propagators) { | 147 | for (var propagator : propagators) { |
172 | propagator.updateBounds(); | 148 | propagator.updateBounds(); |
173 | } | 149 | } |
174 | var result = RefinementResult.UNCHANGED; | 150 | var result = PropagationResult.UNCHANGED; |
175 | if (activeVariables.isEmpty()) { | 151 | if (activeVariables.isEmpty()) { |
176 | return checkEmptiness(); | 152 | return checkEmptiness(); |
177 | } | 153 | } |
@@ -190,16 +166,16 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | |||
190 | return result; | 166 | return result; |
191 | } | 167 | } |
192 | 168 | ||
193 | private RefinementResult checkEmptiness() { | 169 | private PropagationResult checkEmptiness() { |
194 | var emptinessCheckingResult = solver.solve(); | 170 | var emptinessCheckingResult = solver.solve(); |
195 | return switch (emptinessCheckingResult) { | 171 | return switch (emptinessCheckingResult) { |
196 | case OPTIMAL, UNBOUNDED -> RefinementResult.UNCHANGED; | 172 | case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED; |
197 | case INFEASIBLE -> RefinementResult.REJECTED; | 173 | case INFEASIBLE -> PropagationResult.REJECTED; |
198 | default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); | 174 | default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); |
199 | }; | 175 | }; |
200 | } | 176 | } |
201 | 177 | ||
202 | private RefinementResult propagateNode(int nodeId, MPVariable variable) { | 178 | private PropagationResult propagateNode(int nodeId, MPVariable variable) { |
203 | objective.setCoefficient(variable, 1); | 179 | objective.setCoefficient(variable, 1); |
204 | try { | 180 | try { |
205 | objective.setMinimization(); | 181 | objective.setMinimization(); |
@@ -209,7 +185,7 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | |||
209 | case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); | 185 | case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); |
210 | case UNBOUNDED -> lowerBound = 0; | 186 | case UNBOUNDED -> lowerBound = 0; |
211 | case INFEASIBLE -> { | 187 | case INFEASIBLE -> { |
212 | return RefinementResult.REJECTED; | 188 | return PropagationResult.REJECTED; |
213 | } | 189 | } |
214 | default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" | 190 | default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" |
215 | .formatted(variable, minimizationResult)); | 191 | .formatted(variable, minimizationResult)); |
@@ -234,7 +210,7 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { | |||
234 | throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" | 210 | throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" |
235 | .formatted(oldInterval, nodeId, newInterval)); | 211 | .formatted(oldInterval, nodeId, newInterval)); |
236 | } | 212 | } |
237 | return newInterval.equals(oldInterval) ? RefinementResult.UNCHANGED : RefinementResult.REFINED; | 213 | return newInterval.equals(oldInterval) ? PropagationResult.UNCHANGED : PropagationResult.PROPAGATED; |
238 | } finally { | 214 | } finally { |
239 | objective.setCoefficient(variable, 0); | 215 | objective.setCoefficient(variable, 0); |
240 | } | 216 | } |
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java index 393c4b72..5d903f41 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java | |||
@@ -3,7 +3,7 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.scope.internal; | 6 | package tools.refinery.store.reasoning.scope; |
7 | 7 | ||
8 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; | 8 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; |
9 | import tools.refinery.store.dse.transition.objectives.Criteria; | 9 | import tools.refinery.store.dse.transition.objectives.Criteria; |
@@ -28,7 +28,7 @@ import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectT | |||
28 | class LowerTypeScopePropagator extends TypeScopePropagator { | 28 | class LowerTypeScopePropagator extends TypeScopePropagator { |
29 | private final int lowerBound; | 29 | private final int lowerBound; |
30 | 30 | ||
31 | private LowerTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int lowerBound, RelationalQuery allQuery, | 31 | private LowerTypeScopePropagator(BoundScopePropagator adapter, int lowerBound, RelationalQuery allQuery, |
32 | RelationalQuery multiQuery) { | 32 | RelationalQuery multiQuery) { |
33 | super(adapter, allQuery, multiQuery); | 33 | super(adapter, allQuery, multiQuery); |
34 | this.lowerBound = lowerBound; | 34 | this.lowerBound = lowerBound; |
@@ -58,7 +58,7 @@ class LowerTypeScopePropagator extends TypeScopePropagator { | |||
58 | } | 58 | } |
59 | 59 | ||
60 | @Override | 60 | @Override |
61 | public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { | 61 | public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { |
62 | return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); | 62 | return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); |
63 | } | 63 | } |
64 | 64 | ||
@@ -72,10 +72,10 @@ class LowerTypeScopePropagator extends TypeScopePropagator { | |||
72 | super.configure(storeBuilder); | 72 | super.configure(storeBuilder); |
73 | 73 | ||
74 | var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder | 74 | var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder |
75 | .clause(Integer.class, currentCount -> List.of( | 75 | .clause(Integer.class, candidateLowerBound -> List.of( |
76 | new CountCandidateLowerBoundLiteral(currentCount, type, List.of(Variable.of())), | 76 | new CountCandidateLowerBoundLiteral(candidateLowerBound, type, List.of(Variable.of())), |
77 | output.assign(sub(currentCount, constant(lowerBound))), | 77 | output.assign(sub(constant(lowerBound), candidateLowerBound)), |
78 | check(greater(currentCount, constant(0))) | 78 | check(greater(output, constant(0))) |
79 | ))); | 79 | ))); |
80 | 80 | ||
81 | storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); | 81 | storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); |
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java index a6d663ea..986771a1 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java | |||
@@ -3,7 +3,7 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.scope.internal; | 6 | package tools.refinery.store.reasoning.scope; |
7 | 7 | ||
8 | final class RoundingUtil { | 8 | final class RoundingUtil { |
9 | private static final double TOLERANCE = 0.01; | 9 | private static final double TOLERANCE = 0.01; |
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java index 531a7440..25b1966c 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java | |||
@@ -3,15 +3,13 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.scope.internal; | 6 | package tools.refinery.store.reasoning.scope; |
7 | 7 | ||
8 | import com.google.ortools.Loader; | 8 | import com.google.ortools.Loader; |
9 | import tools.refinery.store.adapter.AbstractModelAdapterBuilder; | 9 | import tools.refinery.store.dse.propagation.PropagationBuilder; |
10 | import tools.refinery.store.model.ModelStore; | ||
11 | import tools.refinery.store.model.ModelStoreBuilder; | 10 | import tools.refinery.store.model.ModelStoreBuilder; |
11 | import tools.refinery.store.model.ModelStoreConfiguration; | ||
12 | import tools.refinery.store.reasoning.representation.PartialRelation; | 12 | import tools.refinery.store.reasoning.representation.PartialRelation; |
13 | import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder; | ||
14 | import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; | ||
15 | import tools.refinery.store.reasoning.translator.TranslationException; | 13 | import tools.refinery.store.reasoning.translator.TranslationException; |
16 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; | 14 | import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; |
17 | import tools.refinery.store.representation.Symbol; | 15 | import tools.refinery.store.representation.Symbol; |
@@ -20,14 +18,16 @@ import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | |||
20 | 18 | ||
21 | import java.util.*; | 19 | import java.util.*; |
22 | 20 | ||
23 | public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<ScopePropagatorStoreAdapter> | 21 | public class ScopePropagator implements ModelStoreConfiguration { |
24 | implements ScopePropagatorBuilder { | 22 | private final Symbol<CardinalityInterval> countSymbol; |
25 | private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE; | ||
26 | private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>(); | 23 | private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>(); |
27 | private List<TypeScopePropagator.Factory> typeScopePropagatorFactories; | 24 | private final List<TypeScopePropagator.Factory> typeScopePropagatorFactories = new ArrayList<>(); |
28 | 25 | ||
29 | @Override | 26 | public ScopePropagator() { |
30 | public ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol) { | 27 | this(MultiObjectTranslator.COUNT_STORAGE); |
28 | } | ||
29 | |||
30 | public ScopePropagator(Symbol<CardinalityInterval> countSymbol) { | ||
31 | if (countSymbol.arity() != 1) { | 31 | if (countSymbol.arity() != 1) { |
32 | throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" | 32 | throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" |
33 | .formatted(countSymbol, countSymbol.arity())); | 33 | .formatted(countSymbol, countSymbol.arity())); |
@@ -39,11 +39,9 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop | |||
39 | throw new IllegalArgumentException("Count symbol must default value null"); | 39 | throw new IllegalArgumentException("Count symbol must default value null"); |
40 | } | 40 | } |
41 | this.countSymbol = countSymbol; | 41 | this.countSymbol = countSymbol; |
42 | return this; | ||
43 | } | 42 | } |
44 | 43 | ||
45 | @Override | 44 | public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) { |
46 | public ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval) { | ||
47 | if (type.arity() != 1) { | 45 | if (type.arity() != 1) { |
48 | throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" | 46 | throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" |
49 | .formatted(type, type.arity())); | 47 | .formatted(type, type.arity())); |
@@ -56,9 +54,29 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop | |||
56 | return this; | 54 | return this; |
57 | } | 55 | } |
58 | 56 | ||
57 | public ScopePropagator scopes(Map<PartialRelation, CardinalityInterval> scopes) { | ||
58 | return scopes(scopes.entrySet()); | ||
59 | } | ||
60 | |||
61 | public ScopePropagator scopes(Collection<Map.Entry<PartialRelation, CardinalityInterval>> scopes) { | ||
62 | for (var entry : scopes) { | ||
63 | scope(entry.getKey(), entry.getValue()); | ||
64 | } | ||
65 | return this; | ||
66 | } | ||
67 | |||
59 | @Override | 68 | @Override |
60 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | 69 | public void apply(ModelStoreBuilder storeBuilder) { |
61 | typeScopePropagatorFactories = new ArrayList<>(scopes.size()); | 70 | createTypeScopePropagatorFactories(); |
71 | Loader.loadNativeLibraries(); | ||
72 | for (var factory : typeScopePropagatorFactories) { | ||
73 | factory.configure(storeBuilder); | ||
74 | } | ||
75 | storeBuilder.getAdapter(PropagationBuilder.class) | ||
76 | .propagator(model -> new BoundScopePropagator(model, this)); | ||
77 | } | ||
78 | |||
79 | private void createTypeScopePropagatorFactories() { | ||
62 | for (var entry : scopes.entrySet()) { | 80 | for (var entry : scopes.entrySet()) { |
63 | var type = entry.getKey(); | 81 | var type = entry.getKey(); |
64 | var bounds = entry.getValue(); | 82 | var bounds = entry.getValue(); |
@@ -72,15 +90,13 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop | |||
72 | typeScopePropagatorFactories.add(upperFactory); | 90 | typeScopePropagatorFactories.add(upperFactory); |
73 | } | 91 | } |
74 | } | 92 | } |
75 | for (var factory : typeScopePropagatorFactories) { | ||
76 | factory.configure(storeBuilder); | ||
77 | } | ||
78 | } | 93 | } |
79 | 94 | ||
80 | @Override | 95 | Symbol<CardinalityInterval> getCountSymbol() { |
81 | protected ScopePropagatorStoreAdapter doBuild(ModelStore store) { | 96 | return countSymbol; |
82 | Loader.loadNativeLibraries(); | 97 | } |
83 | return new ScopePropagatorStoreAdapterImpl(store, countSymbol, Collections.unmodifiableMap(scopes), | 98 | |
84 | Collections.unmodifiableList(typeScopePropagatorFactories)); | 99 | List<TypeScopePropagator.Factory> getTypeScopePropagatorFactories() { |
100 | return typeScopePropagatorFactories; | ||
85 | } | 101 | } |
86 | } | 102 | } |
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java deleted file mode 100644 index c2d3f59e..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java +++ /dev/null | |||
@@ -1,21 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.scope; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelAdapter; | ||
9 | import tools.refinery.store.reasoning.refinement.RefinementResult; | ||
10 | import tools.refinery.store.reasoning.scope.internal.ScopePropagatorBuilderImpl; | ||
11 | |||
12 | public interface ScopePropagatorAdapter extends ModelAdapter { | ||
13 | @Override | ||
14 | ScopePropagatorStoreAdapter getStoreAdapter(); | ||
15 | |||
16 | RefinementResult propagate(); | ||
17 | |||
18 | static ScopePropagatorBuilder builder() { | ||
19 | return new ScopePropagatorBuilderImpl(); | ||
20 | } | ||
21 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java deleted file mode 100644 index a17e04a4..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java +++ /dev/null | |||
@@ -1,21 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.scope; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelAdapterBuilder; | ||
9 | import tools.refinery.store.model.ModelStore; | ||
10 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
13 | |||
14 | public interface ScopePropagatorBuilder extends ModelAdapterBuilder { | ||
15 | ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol); | ||
16 | |||
17 | ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval); | ||
18 | |||
19 | @Override | ||
20 | ScopePropagatorStoreAdapter build(ModelStore store); | ||
21 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java deleted file mode 100644 index 65d9c38d..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java +++ /dev/null | |||
@@ -1,16 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.scope; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelStoreAdapter; | ||
9 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
10 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
11 | |||
12 | import java.util.Map; | ||
13 | |||
14 | public interface ScopePropagatorStoreAdapter extends ModelStoreAdapter { | ||
15 | Map<PartialRelation, CardinalityInterval> getScopes(); | ||
16 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java index cfb95829..db80be7f 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java | |||
@@ -3,11 +3,10 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.scope.internal; | 6 | package tools.refinery.store.reasoning.scope; |
7 | 7 | ||
8 | import com.google.ortools.linearsolver.MPConstraint; | 8 | import com.google.ortools.linearsolver.MPConstraint; |
9 | import tools.refinery.store.model.ModelStoreBuilder; | 9 | import tools.refinery.store.model.ModelStoreBuilder; |
10 | import tools.refinery.store.query.ModelQueryAdapter; | ||
11 | import tools.refinery.store.query.ModelQueryBuilder; | 10 | import tools.refinery.store.query.ModelQueryBuilder; |
12 | import tools.refinery.store.query.dnf.AnyQuery; | 11 | import tools.refinery.store.query.dnf.AnyQuery; |
13 | import tools.refinery.store.query.dnf.RelationalQuery; | 12 | import tools.refinery.store.query.dnf.RelationalQuery; |
@@ -17,15 +16,15 @@ import tools.refinery.store.tuple.Tuple; | |||
17 | import java.util.Collection; | 16 | import java.util.Collection; |
18 | 17 | ||
19 | abstract class TypeScopePropagator { | 18 | abstract class TypeScopePropagator { |
20 | private final ScopePropagatorAdapterImpl adapter; | 19 | private final BoundScopePropagator adapter; |
21 | private final ResultSet<Boolean> allNodes; | 20 | private final ResultSet<Boolean> allNodes; |
22 | private final ResultSet<Boolean> multiNodes; | 21 | private final ResultSet<Boolean> multiNodes; |
23 | protected final MPConstraint constraint; | 22 | protected final MPConstraint constraint; |
24 | 23 | ||
25 | protected TypeScopePropagator(ScopePropagatorAdapterImpl adapter, RelationalQuery allQuery, | 24 | protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery, |
26 | RelationalQuery multiQuery) { | 25 | RelationalQuery multiQuery) { |
27 | this.adapter = adapter; | 26 | this.adapter = adapter; |
28 | var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class); | 27 | var queryEngine = adapter.getQueryEngine(); |
29 | allNodes = queryEngine.getResultSet(allQuery); | 28 | allNodes = queryEngine.getResultSet(allQuery); |
30 | multiNodes = queryEngine.getResultSet(multiQuery); | 29 | multiNodes = queryEngine.getResultSet(multiQuery); |
31 | constraint = adapter.makeConstraint(); | 30 | constraint = adapter.makeConstraint(); |
@@ -56,7 +55,7 @@ abstract class TypeScopePropagator { | |||
56 | } | 55 | } |
57 | 56 | ||
58 | public abstract static class Factory { | 57 | public abstract static class Factory { |
59 | public abstract TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter); | 58 | public abstract TypeScopePropagator createPropagator(BoundScopePropagator adapter); |
60 | 59 | ||
61 | protected abstract Collection<AnyQuery> getQueries(); | 60 | protected abstract Collection<AnyQuery> getQueries(); |
62 | 61 | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java index a0be0fb4..062f976c 100644 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java | |||
@@ -3,7 +3,7 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.scope.internal; | 6 | package tools.refinery.store.reasoning.scope; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.AnyQuery; | 8 | import tools.refinery.store.query.dnf.AnyQuery; |
9 | import tools.refinery.store.query.dnf.Query; | 9 | import tools.refinery.store.query.dnf.Query; |
@@ -19,7 +19,7 @@ import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectT | |||
19 | class UpperTypeScopePropagator extends TypeScopePropagator { | 19 | class UpperTypeScopePropagator extends TypeScopePropagator { |
20 | private final int upperBound; | 20 | private final int upperBound; |
21 | 21 | ||
22 | private UpperTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int upperBound, RelationalQuery allQuery, | 22 | private UpperTypeScopePropagator(BoundScopePropagator adapter, int upperBound, RelationalQuery allQuery, |
23 | RelationalQuery multiQuery) { | 23 | RelationalQuery multiQuery) { |
24 | super(adapter, allQuery, multiQuery); | 24 | super(adapter, allQuery, multiQuery); |
25 | this.upperBound = upperBound; | 25 | this.upperBound = upperBound; |
@@ -47,7 +47,7 @@ class UpperTypeScopePropagator extends TypeScopePropagator { | |||
47 | } | 47 | } |
48 | 48 | ||
49 | @Override | 49 | @Override |
50 | public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { | 50 | public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { |
51 | return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); | 51 | return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); |
52 | } | 52 | } |
53 | 53 | ||
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java deleted file mode 100644 index 282ffe6f..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java +++ /dev/null | |||
@@ -1,58 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.scope.internal; | ||
7 | |||
8 | import tools.refinery.store.adapter.ModelAdapter; | ||
9 | import tools.refinery.store.model.Model; | ||
10 | import tools.refinery.store.model.ModelStore; | ||
11 | import tools.refinery.store.reasoning.representation.PartialRelation; | ||
12 | import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; | ||
13 | import tools.refinery.store.representation.Symbol; | ||
14 | import tools.refinery.store.representation.cardinality.CardinalityInterval; | ||
15 | |||
16 | import java.util.List; | ||
17 | import java.util.Map; | ||
18 | |||
19 | // Not a record, because we want to control getter visibility. | ||
20 | @SuppressWarnings("ClassCanBeRecord") | ||
21 | class ScopePropagatorStoreAdapterImpl implements ScopePropagatorStoreAdapter { | ||
22 | private final ModelStore store; | ||
23 | private final Symbol<CardinalityInterval> countSymbol; | ||
24 | private final Map<PartialRelation, CardinalityInterval> scopes; | ||
25 | private final List<TypeScopePropagator.Factory> propagatorFactories; | ||
26 | |||
27 | public ScopePropagatorStoreAdapterImpl( | ||
28 | ModelStore store, Symbol<CardinalityInterval> countSymbol, | ||
29 | Map<PartialRelation, CardinalityInterval> scopes, List<TypeScopePropagator.Factory> propagatorFactories) { | ||
30 | this.store = store; | ||
31 | this.countSymbol = countSymbol; | ||
32 | this.scopes = scopes; | ||
33 | this.propagatorFactories = propagatorFactories; | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | public ModelStore getStore() { | ||
38 | return store; | ||
39 | } | ||
40 | |||
41 | Symbol<CardinalityInterval> getCountSymbol() { | ||
42 | return countSymbol; | ||
43 | } | ||
44 | |||
45 | @Override | ||
46 | public Map<PartialRelation, CardinalityInterval> getScopes() { | ||
47 | return scopes; | ||
48 | } | ||
49 | |||
50 | public List<TypeScopePropagator.Factory> getPropagatorFactories() { | ||
51 | return propagatorFactories; | ||
52 | } | ||
53 | |||
54 | @Override | ||
55 | public ModelAdapter createModelAdapter(Model model) { | ||
56 | return new ScopePropagatorAdapterImpl(model, this); | ||
57 | } | ||
58 | } | ||
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java index 42ce2f56..5fc70ae1 100644 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java | |||
@@ -7,13 +7,14 @@ package tools.refinery.store.reasoning.scope; | |||
7 | 7 | ||
8 | import org.junit.jupiter.api.BeforeEach; | 8 | import org.junit.jupiter.api.BeforeEach; |
9 | import org.junit.jupiter.api.Test; | 9 | import org.junit.jupiter.api.Test; |
10 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
11 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
10 | import tools.refinery.store.model.Interpretation; | 12 | import tools.refinery.store.model.Interpretation; |
11 | import tools.refinery.store.model.Model; | 13 | import tools.refinery.store.model.Model; |
12 | import tools.refinery.store.model.ModelStore; | 14 | import tools.refinery.store.model.ModelStore; |
13 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; | 15 | import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; |
14 | import tools.refinery.store.reasoning.ReasoningAdapter; | 16 | import tools.refinery.store.reasoning.ReasoningAdapter; |
15 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | 17 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; |
16 | import tools.refinery.store.reasoning.refinement.RefinementResult; | ||
17 | import tools.refinery.store.reasoning.representation.PartialRelation; | 18 | import tools.refinery.store.reasoning.representation.PartialRelation; |
18 | import tools.refinery.store.reasoning.seed.ModelSeed; | 19 | import tools.refinery.store.reasoning.seed.ModelSeed; |
19 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 20 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
@@ -38,11 +39,12 @@ class MultiObjectTest { | |||
38 | void beforeEach() { | 39 | void beforeEach() { |
39 | store = ModelStore.builder() | 40 | store = ModelStore.builder() |
40 | .with(ViatraModelQueryAdapter.builder()) | 41 | .with(ViatraModelQueryAdapter.builder()) |
42 | .with(PropagationAdapter.builder()) | ||
41 | .with(ReasoningAdapter.builder()) | 43 | .with(ReasoningAdapter.builder()) |
42 | .with(new MultiObjectTranslator()) | 44 | .with(new MultiObjectTranslator()) |
43 | .with(PartialRelationTranslator.of(person) | 45 | .with(PartialRelationTranslator.of(person) |
44 | .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE))) | 46 | .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE))) |
45 | .with(ScopePropagatorAdapter.builder() | 47 | .with(new ScopePropagator() |
46 | .scope(person, CardinalityIntervals.between(5, 15))) | 48 | .scope(person, CardinalityIntervals.between(5, 15))) |
47 | .build(); | 49 | .build(); |
48 | model = null; | 50 | model = null; |
@@ -57,7 +59,7 @@ class MultiObjectTest { | |||
57 | .put(Tuple.of(0), CardinalityIntervals.SET)) | 59 | .put(Tuple.of(0), CardinalityIntervals.SET)) |
58 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 60 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
59 | .build()); | 61 | .build()); |
60 | assertThat(propagate(), is(RefinementResult.REFINED)); | 62 | assertThat(propagate(), is(PropagationResult.PROPAGATED)); |
61 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12))); | 63 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12))); |
62 | } | 64 | } |
63 | 65 | ||
@@ -69,7 +71,7 @@ class MultiObjectTest { | |||
69 | .put(Tuple.of(0), CardinalityIntervals.between(5, 20))) | 71 | .put(Tuple.of(0), CardinalityIntervals.between(5, 20))) |
70 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 72 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
71 | .build()); | 73 | .build()); |
72 | assertThat(propagate(), is(RefinementResult.REFINED)); | 74 | assertThat(propagate(), is(PropagationResult.PROPAGATED)); |
73 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12))); | 75 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12))); |
74 | } | 76 | } |
75 | 77 | ||
@@ -81,7 +83,7 @@ class MultiObjectTest { | |||
81 | .put(Tuple.of(0), CardinalityIntervals.SET)) | 83 | .put(Tuple.of(0), CardinalityIntervals.SET)) |
82 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 84 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
83 | .build()); | 85 | .build()); |
84 | assertThat(propagate(), is(RefinementResult.REJECTED)); | 86 | assertThat(propagate(), is(PropagationResult.REJECTED)); |
85 | } | 87 | } |
86 | 88 | ||
87 | @Test | 89 | @Test |
@@ -90,7 +92,7 @@ class MultiObjectTest { | |||
90 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) | 92 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) |
91 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 93 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
92 | .build()); | 94 | .build()); |
93 | assertThat(propagate(), is(RefinementResult.UNCHANGED)); | 95 | assertThat(propagate(), is(PropagationResult.UNCHANGED)); |
94 | } | 96 | } |
95 | 97 | ||
96 | @Test | 98 | @Test |
@@ -99,7 +101,7 @@ class MultiObjectTest { | |||
99 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) | 101 | .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) |
100 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 102 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
101 | .build()); | 103 | .build()); |
102 | assertThat(propagate(), is(RefinementResult.REJECTED)); | 104 | assertThat(propagate(), is(PropagationResult.REJECTED)); |
103 | } | 105 | } |
104 | 106 | ||
105 | @Test | 107 | @Test |
@@ -110,7 +112,7 @@ class MultiObjectTest { | |||
110 | .put(Tuple.of(0), CardinalityIntervals.atLeast(20))) | 112 | .put(Tuple.of(0), CardinalityIntervals.atLeast(20))) |
111 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 113 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
112 | .build()); | 114 | .build()); |
113 | assertThat(propagate(), is(RefinementResult.REJECTED)); | 115 | assertThat(propagate(), is(PropagationResult.REJECTED)); |
114 | } | 116 | } |
115 | 117 | ||
116 | @Test | 118 | @Test |
@@ -121,7 +123,7 @@ class MultiObjectTest { | |||
121 | .put(Tuple.of(0), CardinalityIntervals.atMost(1))) | 123 | .put(Tuple.of(0), CardinalityIntervals.atMost(1))) |
122 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 124 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
123 | .build()); | 125 | .build()); |
124 | assertThat(propagate(), is(RefinementResult.REJECTED)); | 126 | assertThat(propagate(), is(PropagationResult.REJECTED)); |
125 | } | 127 | } |
126 | 128 | ||
127 | @Test | 129 | @Test |
@@ -133,7 +135,7 @@ class MultiObjectTest { | |||
133 | .put(Tuple.of(1), CardinalityIntervals.SET)) | 135 | .put(Tuple.of(1), CardinalityIntervals.SET)) |
134 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 136 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
135 | .build()); | 137 | .build()); |
136 | assertThat(propagate(), is(RefinementResult.REFINED)); | 138 | assertThat(propagate(), is(PropagationResult.PROPAGATED)); |
137 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12))); | 139 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12))); |
138 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12))); | 140 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12))); |
139 | } | 141 | } |
@@ -147,7 +149,7 @@ class MultiObjectTest { | |||
147 | .put(Tuple.of(1), CardinalityIntervals.atMost(11))) | 149 | .put(Tuple.of(1), CardinalityIntervals.atMost(11))) |
148 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 150 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
149 | .build()); | 151 | .build()); |
150 | assertThat(propagate(), is(RefinementResult.REFINED)); | 152 | assertThat(propagate(), is(PropagationResult.PROPAGATED)); |
151 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12))); | 153 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12))); |
152 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5))); | 154 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5))); |
153 | } | 155 | } |
@@ -161,7 +163,7 @@ class MultiObjectTest { | |||
161 | .put(Tuple.of(1), CardinalityIntervals.exactly(11))) | 163 | .put(Tuple.of(1), CardinalityIntervals.exactly(11))) |
162 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 164 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
163 | .build()); | 165 | .build()); |
164 | assertThat(propagate(), is(RefinementResult.REJECTED)); | 166 | assertThat(propagate(), is(PropagationResult.REJECTED)); |
165 | } | 167 | } |
166 | 168 | ||
167 | @Test | 169 | @Test |
@@ -173,7 +175,7 @@ class MultiObjectTest { | |||
173 | .put(Tuple.of(1), CardinalityIntervals.atMost(2))) | 175 | .put(Tuple.of(1), CardinalityIntervals.atMost(2))) |
174 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 176 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
175 | .build()); | 177 | .build()); |
176 | assertThat(propagate(), is(RefinementResult.REJECTED)); | 178 | assertThat(propagate(), is(PropagationResult.REJECTED)); |
177 | } | 179 | } |
178 | 180 | ||
179 | @Test | 181 | @Test |
@@ -185,14 +187,14 @@ class MultiObjectTest { | |||
185 | .put(Tuple.of(1), CardinalityIntervals.SET)) | 187 | .put(Tuple.of(1), CardinalityIntervals.SET)) |
186 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) | 188 | .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) |
187 | .build()); | 189 | .build()); |
188 | assertThat(propagate(), is(RefinementResult.REFINED)); | 190 | assertThat(propagate(), is(PropagationResult.PROPAGATED)); |
189 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE)); | 191 | assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE)); |
190 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12))); | 192 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12))); |
191 | countStorage.put(Tuple.of(0), CardinalityIntervals.ONE); | 193 | countStorage.put(Tuple.of(0), CardinalityIntervals.ONE); |
192 | assertThat(propagate(), is(RefinementResult.REFINED)); | 194 | assertThat(propagate(), is(PropagationResult.PROPAGATED)); |
193 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11))); | 195 | assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11))); |
194 | countStorage.put(Tuple.of(1), CardinalityIntervals.ONE); | 196 | countStorage.put(Tuple.of(1), CardinalityIntervals.ONE); |
195 | assertThat(propagate(), is(RefinementResult.UNCHANGED)); | 197 | assertThat(propagate(), is(PropagationResult.UNCHANGED)); |
196 | } | 198 | } |
197 | 199 | ||
198 | private void createModel(ModelSeed modelSeed) { | 200 | private void createModel(ModelSeed modelSeed) { |
@@ -200,7 +202,7 @@ class MultiObjectTest { | |||
200 | countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE); | 202 | countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE); |
201 | } | 203 | } |
202 | 204 | ||
203 | private RefinementResult propagate() { | 205 | private PropagationResult propagate() { |
204 | return model.getAdapter(ScopePropagatorAdapter.class).propagate(); | 206 | return model.getAdapter(PropagationAdapter.class).propagate(); |
205 | } | 207 | } |
206 | } | 208 | } |
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java index 9daed660..e697298e 100644 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java | |||
@@ -3,7 +3,7 @@ | |||
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.scope.internal; | 6 | package tools.refinery.store.reasoning.scope; |
7 | 7 | ||
8 | import org.junit.jupiter.params.ParameterizedTest; | 8 | import org.junit.jupiter.params.ParameterizedTest; |
9 | import org.junit.jupiter.params.provider.Arguments; | 9 | import org.junit.jupiter.params.provider.Arguments; |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java new file mode 100644 index 00000000..62c35cee --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java | |||
@@ -0,0 +1,43 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.actions; | ||
7 | |||
8 | import tools.refinery.store.dse.transition.actions.AbstractActionLiteral; | ||
9 | import tools.refinery.store.dse.transition.actions.BoundActionLiteral; | ||
10 | import tools.refinery.store.model.Model; | ||
11 | import tools.refinery.store.query.term.NodeVariable; | ||
12 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
13 | import tools.refinery.store.tuple.Tuple; | ||
14 | |||
15 | import java.util.List; | ||
16 | |||
17 | public class CleanupActionLiteral extends AbstractActionLiteral { | ||
18 | private final NodeVariable node; | ||
19 | |||
20 | public CleanupActionLiteral(NodeVariable node) { | ||
21 | this.node = node; | ||
22 | } | ||
23 | |||
24 | public NodeVariable getNode() { | ||
25 | return node; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public List<NodeVariable> getInputVariables() { | ||
30 | return List.of(node); | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public List<NodeVariable> getOutputVariables() { | ||
35 | return List.of(); | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public BoundActionLiteral bindToModel(Model model) { | ||
40 | var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
41 | return tuple -> reasoningAdapter.cleanup(tuple.get(0)) ? Tuple.of() : null; | ||
42 | } | ||
43 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java index 990d11e5..f36fde44 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java | |||
@@ -35,4 +35,8 @@ public final class PartialActionLiterals { | |||
35 | public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { | 35 | public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { |
36 | return new FocusActionLiteral(parent, child); | 36 | return new FocusActionLiteral(parent, child); |
37 | } | 37 | } |
38 | |||
39 | public static CleanupActionLiteral cleanup(NodeVariable node) { | ||
40 | return new CleanupActionLiteral(node); | ||
41 | } | ||
38 | } | 42 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java index d2cd2eb0..722458c8 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java | |||
@@ -18,18 +18,19 @@ import tools.refinery.store.query.dnf.Query; | |||
18 | import tools.refinery.store.query.dnf.RelationalQuery; | 18 | import tools.refinery.store.query.dnf.RelationalQuery; |
19 | import tools.refinery.store.reasoning.ReasoningBuilder; | 19 | import tools.refinery.store.reasoning.ReasoningBuilder; |
20 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | 20 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; |
21 | import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; | ||
22 | import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; | ||
23 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
24 | import tools.refinery.store.reasoning.lifting.DnfLifter; | 21 | import tools.refinery.store.reasoning.lifting.DnfLifter; |
25 | import tools.refinery.store.reasoning.literal.Concreteness; | 22 | import tools.refinery.store.reasoning.literal.Concreteness; |
26 | import tools.refinery.store.reasoning.literal.Modality; | 23 | import tools.refinery.store.reasoning.literal.Modality; |
24 | import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; | ||
27 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; | 25 | import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; |
28 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; | 26 | import tools.refinery.store.reasoning.refinement.PartialModelInitializer; |
29 | import tools.refinery.store.reasoning.refinement.StorageRefiner; | 27 | import tools.refinery.store.reasoning.refinement.StorageRefiner; |
30 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | 28 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; |
29 | import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; | ||
30 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | ||
31 | import tools.refinery.store.representation.AnySymbol; | 31 | import tools.refinery.store.representation.AnySymbol; |
32 | import tools.refinery.store.representation.Symbol; | 32 | import tools.refinery.store.representation.Symbol; |
33 | import tools.refinery.store.statecoding.StateCoderBuilder; | ||
33 | 34 | ||
34 | import java.util.*; | 35 | import java.util.*; |
35 | 36 | ||
@@ -109,6 +110,8 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS | |||
109 | @Override | 110 | @Override |
110 | protected void doConfigure(ModelStoreBuilder storeBuilder) { | 111 | protected void doConfigure(ModelStoreBuilder storeBuilder) { |
111 | storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL); | 112 | storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL); |
113 | storeBuilder.tryGetAdapter(StateCoderBuilder.class) | ||
114 | .ifPresent(stateCoderBuilder -> stateCoderBuilder.exclude(ReasoningAdapterImpl.NODE_COUNT_SYMBOL)); | ||
112 | for (var translator : translators.values()) { | 115 | for (var translator : translators.values()) { |
113 | translator.configure(storeBuilder); | 116 | translator.configure(storeBuilder); |
114 | if (translator instanceof PartialRelationTranslator relationConfiguration) { | 117 | if (translator instanceof PartialRelationTranslator relationConfiguration) { |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java index 8eb5a034..9ef6fb16 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.internal; | 6 | package tools.refinery.store.reasoning.internal; |
7 | 7 | ||
8 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
8 | import tools.refinery.store.model.Model; | 9 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.model.ModelStore; | 10 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.query.ModelQueryAdapter; | 11 | import tools.refinery.store.query.ModelQueryAdapter; |
@@ -103,6 +104,11 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { | |||
103 | for (var initializer : initializers) { | 104 | for (var initializer : initializers) { |
104 | initializer.initialize(model, modelSeed); | 105 | initializer.initialize(model, modelSeed); |
105 | } | 106 | } |
107 | model.tryGetAdapter(PropagationAdapter.class).ifPresent(propagationAdapter -> { | ||
108 | if (propagationAdapter.propagate().isRejected()) { | ||
109 | throw new IllegalArgumentException("Inconsistent initial mode: propagation failed"); | ||
110 | } | ||
111 | }); | ||
106 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); | 112 | model.getAdapter(ModelQueryAdapter.class).flushChanges(); |
107 | return model; | 113 | return model; |
108 | } | 114 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java index 5c3298ac..61037be3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java | |||
@@ -243,7 +243,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { | |||
243 | MultiObjectTranslator.MULTI_VIEW.call(multi), | 243 | MultiObjectTranslator.MULTI_VIEW.call(multi), |
244 | not(may(CONTAINED_SYMBOL.call(multi))) | 244 | not(may(CONTAINED_SYMBOL.call(multi))) |
245 | ) | 245 | ) |
246 | .clause((container) -> List.of( | 246 | .clause(container -> List.of( |
247 | MultiObjectTranslator.MULTI_VIEW.call(multi), | 247 | MultiObjectTranslator.MULTI_VIEW.call(multi), |
248 | must(CONTAINS_SYMBOL.call(container, multi)), | 248 | must(CONTAINS_SYMBOL.call(container, multi)), |
249 | not(MultiObjectTranslator.MULTI_VIEW.call(container)) | 249 | not(MultiObjectTranslator.MULTI_VIEW.call(container)) |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java index 90802864..8df23d9a 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java | |||
@@ -8,18 +8,23 @@ package tools.refinery.store.reasoning.translator.containment; | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | 8 | import tools.refinery.store.reasoning.representation.PartialRelation; |
9 | import tools.refinery.store.representation.TruthValue; | 9 | import tools.refinery.store.representation.TruthValue; |
10 | 10 | ||
11 | import java.util.Objects; | ||
11 | import java.util.Set; | 12 | import java.util.Set; |
12 | 13 | ||
13 | record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks, | 14 | final class InferredContainment { |
14 | Set<PartialRelation> forbiddenLinks) { | ||
15 | public static final InferredContainment UNKNOWN = new InferredContainment( | 15 | public static final InferredContainment UNKNOWN = new InferredContainment( |
16 | TruthValue.UNKNOWN, Set.of(), Set.of()); | 16 | TruthValue.UNKNOWN, Set.of(), Set.of()); |
17 | private final TruthValue contains; | ||
18 | private final Set<PartialRelation> mustLinks; | ||
19 | private final Set<PartialRelation> forbiddenLinks; | ||
20 | private final int hashCode; | ||
17 | 21 | ||
18 | public InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks, | 22 | public InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks, |
19 | Set<PartialRelation> forbiddenLinks) { | 23 | Set<PartialRelation> forbiddenLinks) { |
20 | this.contains = adjustContains(contains, mustLinks, forbiddenLinks); | 24 | this.contains = adjustContains(contains, mustLinks, forbiddenLinks); |
21 | this.mustLinks = mustLinks; | 25 | this.mustLinks = mustLinks; |
22 | this.forbiddenLinks = forbiddenLinks; | 26 | this.forbiddenLinks = forbiddenLinks; |
27 | hashCode = Objects.hash(contains, mustLinks, forbiddenLinks); | ||
23 | } | 28 | } |
24 | 29 | ||
25 | private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks, | 30 | private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks, |
@@ -34,4 +39,39 @@ record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks, | |||
34 | } | 39 | } |
35 | return result; | 40 | return result; |
36 | } | 41 | } |
42 | |||
43 | public TruthValue contains() { | ||
44 | return contains; | ||
45 | } | ||
46 | |||
47 | public Set<PartialRelation> mustLinks() { | ||
48 | return mustLinks; | ||
49 | } | ||
50 | |||
51 | public Set<PartialRelation> forbiddenLinks() { | ||
52 | return forbiddenLinks; | ||
53 | } | ||
54 | |||
55 | @Override | ||
56 | public boolean equals(Object obj) { | ||
57 | if (obj == this) return true; | ||
58 | if (obj == null || obj.getClass() != this.getClass()) return false; | ||
59 | var that = (InferredContainment) obj; | ||
60 | return Objects.equals(this.contains, that.contains) && | ||
61 | Objects.equals(this.mustLinks, that.mustLinks) && | ||
62 | Objects.equals(this.forbiddenLinks, that.forbiddenLinks); | ||
63 | } | ||
64 | |||
65 | @Override | ||
66 | public int hashCode() { | ||
67 | return hashCode; | ||
68 | } | ||
69 | |||
70 | @Override | ||
71 | public String toString() { | ||
72 | return "InferredContainment[" + | ||
73 | "contains=" + contains + ", " + | ||
74 | "mustLinks=" + mustLinks + ", " + | ||
75 | "forbiddenLinks=" + forbiddenLinks + ']'; | ||
76 | } | ||
37 | } | 77 | } |
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 05704096..bad96a66 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 | |||
@@ -5,17 +5,21 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.reasoning.translator.multiobject; | 6 | package tools.refinery.store.reasoning.translator.multiobject; |
7 | 7 | ||
8 | import tools.refinery.store.dse.propagation.PropagationBuilder; | ||
9 | import tools.refinery.store.dse.transition.Rule; | ||
8 | import tools.refinery.store.dse.transition.objectives.Criteria; | 10 | import tools.refinery.store.dse.transition.objectives.Criteria; |
9 | import tools.refinery.store.dse.transition.objectives.Objectives; | 11 | import tools.refinery.store.dse.transition.objectives.Objectives; |
10 | import tools.refinery.store.model.ModelStoreBuilder; | 12 | import tools.refinery.store.model.ModelStoreBuilder; |
11 | import tools.refinery.store.model.ModelStoreConfiguration; | 13 | import tools.refinery.store.model.ModelStoreConfiguration; |
12 | import tools.refinery.store.query.dnf.Query; | 14 | import tools.refinery.store.query.dnf.Query; |
15 | import tools.refinery.store.query.literal.Literals; | ||
13 | import tools.refinery.store.query.term.Variable; | 16 | import tools.refinery.store.query.term.Variable; |
14 | import tools.refinery.store.query.term.int_.IntTerms; | 17 | import tools.refinery.store.query.term.int_.IntTerms; |
15 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; | 18 | import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; |
16 | import tools.refinery.store.query.view.AnySymbolView; | 19 | import tools.refinery.store.query.view.AnySymbolView; |
17 | import tools.refinery.store.reasoning.ReasoningAdapter; | 20 | import tools.refinery.store.reasoning.ReasoningAdapter; |
18 | import tools.refinery.store.reasoning.ReasoningBuilder; | 21 | import tools.refinery.store.reasoning.ReasoningBuilder; |
22 | import tools.refinery.store.reasoning.actions.PartialActionLiterals; | ||
19 | import tools.refinery.store.reasoning.representation.PartialFunction; | 23 | import tools.refinery.store.reasoning.representation.PartialFunction; |
20 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 24 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
21 | import tools.refinery.store.reasoning.translator.RoundingMode; | 25 | import tools.refinery.store.reasoning.translator.RoundingMode; |
@@ -66,6 +70,11 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
66 | LOWER_CARDINALITY_VIEW.call(p1, lower), | 70 | LOWER_CARDINALITY_VIEW.call(p1, lower), |
67 | check(greaterEq(lower, constant(1))) | 71 | check(greaterEq(lower, constant(1))) |
68 | )))) | 72 | )))) |
73 | .candidate(Query.of("exists#candidate", (builder, p1) -> builder | ||
74 | .clause( | ||
75 | LOWER_CARDINALITY_VIEW.call(p1, Variable.of(Integer.class)), | ||
76 | Literals.not(MULTI_VIEW.call(p1)) | ||
77 | ))) | ||
69 | .roundingMode(RoundingMode.PREFER_FALSE) | 78 | .roundingMode(RoundingMode.PREFER_FALSE) |
70 | .refiner(ExistsRefiner.of(COUNT_STORAGE)) | 79 | .refiner(ExistsRefiner.of(COUNT_STORAGE)) |
71 | .exclude(null) | 80 | .exclude(null) |
@@ -82,5 +91,17 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
82 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | 91 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); |
83 | reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); | 92 | reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); |
84 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); | 93 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); |
94 | |||
95 | storeBuilder.tryGetAdapter(PropagationBuilder.class) | ||
96 | .ifPresent(propagationBuilder -> propagationBuilder.rule( | ||
97 | Rule.of("exists#cleanup", (builder, node) -> builder | ||
98 | .clause(UpperCardinality.class, upper -> List.of( | ||
99 | UPPER_CARDINALITY_VIEW.call(node, upper), | ||
100 | check(UpperCardinalityTerms.less(upper, | ||
101 | UpperCardinalityTerms.constant(UpperCardinalities.ONE))) | ||
102 | )) | ||
103 | .action( | ||
104 | PartialActionLiterals.cleanup(node) | ||
105 | )))); | ||
85 | } | 106 | } |
86 | } | 107 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java index 1ae94ae1..9a0c2b0f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java | |||
@@ -8,17 +8,22 @@ package tools.refinery.store.reasoning.translator.typehierarchy; | |||
8 | import tools.refinery.store.reasoning.representation.PartialRelation; | 8 | import tools.refinery.store.reasoning.representation.PartialRelation; |
9 | 9 | ||
10 | import java.util.Collections; | 10 | import java.util.Collections; |
11 | import java.util.Objects; | ||
11 | import java.util.Set; | 12 | import java.util.Set; |
12 | 13 | ||
13 | record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, | 14 | public final class InferredType { |
14 | PartialRelation candidateType) { | ||
15 | public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); | 15 | public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); |
16 | private final Set<PartialRelation> mustTypes; | ||
17 | private final Set<PartialRelation> mayConcreteTypes; | ||
18 | private final PartialRelation candidateType; | ||
19 | private final int hashCode; | ||
16 | 20 | ||
17 | public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, | 21 | public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes, |
18 | PartialRelation candidateType) { | 22 | PartialRelation candidateType) { |
19 | this.mustTypes = Collections.unmodifiableSet(mustTypes); | 23 | this.mustTypes = Collections.unmodifiableSet(mustTypes); |
20 | this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); | 24 | this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); |
21 | this.candidateType = candidateType; | 25 | this.candidateType = candidateType; |
26 | hashCode = Objects.hash(mustTypes, mayConcreteTypes, candidateType); | ||
22 | } | 27 | } |
23 | 28 | ||
24 | public boolean isConsistent() { | 29 | public boolean isConsistent() { |
@@ -32,4 +37,40 @@ record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConc | |||
32 | public boolean isMayConcrete(PartialRelation partialRelation) { | 37 | public boolean isMayConcrete(PartialRelation partialRelation) { |
33 | return mayConcreteTypes.contains(partialRelation); | 38 | return mayConcreteTypes.contains(partialRelation); |
34 | } | 39 | } |
40 | |||
41 | |||
42 | public Set<PartialRelation> mustTypes() { | ||
43 | return mustTypes; | ||
44 | } | ||
45 | |||
46 | public Set<PartialRelation> mayConcreteTypes() { | ||
47 | return mayConcreteTypes; | ||
48 | } | ||
49 | |||
50 | public PartialRelation candidateType() { | ||
51 | return candidateType; | ||
52 | } | ||
53 | |||
54 | @Override | ||
55 | public boolean equals(Object o) { | ||
56 | if (this == o) return true; | ||
57 | if (o == null || getClass() != o.getClass()) return false; | ||
58 | InferredType that = (InferredType) o; | ||
59 | return Objects.equals(mustTypes, that.mustTypes) && | ||
60 | Objects.equals(mayConcreteTypes, that.mayConcreteTypes) && | ||
61 | Objects.equals(candidateType, that.candidateType); | ||
62 | } | ||
63 | |||
64 | @Override | ||
65 | public int hashCode() { | ||
66 | return hashCode; | ||
67 | } | ||
68 | |||
69 | @Override | ||
70 | public String toString() { | ||
71 | return "InferredType[" + | ||
72 | "mustTypes=" + mustTypes + ", " + | ||
73 | "mayConcreteTypes=" + mayConcreteTypes + ", " + | ||
74 | "candidateType=" + candidateType + ']'; | ||
75 | } | ||
35 | } | 76 | } |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java index dc8a1d36..37ea1448 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java | |||
@@ -26,7 +26,8 @@ import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMu | |||
26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; | 26 | import static tools.refinery.store.reasoning.literal.PartialLiterals.may; |
27 | 27 | ||
28 | public class TypeHierarchyTranslator implements ModelStoreConfiguration { | 28 | public class TypeHierarchyTranslator implements ModelStoreConfiguration { |
29 | private final Symbol<InferredType> typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED); | 29 | public static final Symbol<InferredType> TYPE_SYMBOL = Symbol.of("TYPE", 1, InferredType.class, |
30 | InferredType.UNTYPED); | ||
30 | private final TypeHierarchy typeHierarchy; | 31 | private final TypeHierarchy typeHierarchy; |
31 | 32 | ||
32 | public TypeHierarchyTranslator(TypeHierarchy typeHierarchy) { | 33 | public TypeHierarchyTranslator(TypeHierarchy typeHierarchy) { |
@@ -39,7 +40,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
39 | return; | 40 | return; |
40 | } | 41 | } |
41 | 42 | ||
42 | storeBuilder.symbol(typeSymbol); | 43 | storeBuilder.symbol(TYPE_SYMBOL); |
43 | 44 | ||
44 | for (var entry : typeHierarchy.getPreservedTypes().entrySet()) { | 45 | for (var entry : typeHierarchy.getPreservedTypes().entrySet()) { |
45 | storeBuilder.with(createPreservedTypeTranslator(entry.getKey(), entry.getValue())); | 46 | storeBuilder.with(createPreservedTypeTranslator(entry.getKey(), entry.getValue())); |
@@ -50,13 +51,13 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
50 | } | 51 | } |
51 | 52 | ||
52 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); | 53 | var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); |
53 | reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, typeSymbol)); | 54 | reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, TYPE_SYMBOL)); |
54 | } | 55 | } |
55 | 56 | ||
56 | private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { | 57 | private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { |
57 | var may = Query.of(type.name() + "#partial#may", (builder, p1) -> { | 58 | var may = Query.of(type.name() + "#partial#may", (builder, p1) -> { |
58 | if (!result.isAbstractType()) { | 59 | if (!result.isAbstractType()) { |
59 | builder.clause(new MayTypeView(typeSymbol, type).call(p1)); | 60 | builder.clause(new MayTypeView(TYPE_SYMBOL, type).call(p1)); |
60 | } | 61 | } |
61 | for (var subtype : result.getDirectSubtypes()) { | 62 | for (var subtype : result.getDirectSubtypes()) { |
62 | builder.clause(may(subtype.call(p1))); | 63 | builder.clause(may(subtype.call(p1))); |
@@ -64,12 +65,12 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
64 | }); | 65 | }); |
65 | 66 | ||
66 | var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause( | 67 | var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause( |
67 | new MustTypeView(typeSymbol, type).call(p1) | 68 | new MustTypeView(TYPE_SYMBOL, type).call(p1) |
68 | )); | 69 | )); |
69 | 70 | ||
70 | var candidate = Query.of(type.name() + "#candidate", (builder, p1) -> { | 71 | var candidate = Query.of(type.name() + "#candidate", (builder, p1) -> { |
71 | if (!result.isAbstractType()) { | 72 | if (!result.isAbstractType()) { |
72 | builder.clause(new CandidateTypeView(typeSymbol, type).call(p1)); | 73 | builder.clause(new CandidateTypeView(TYPE_SYMBOL, type).call(p1)); |
73 | } | 74 | } |
74 | for (var subtype : result.getDirectSubtypes()) { | 75 | for (var subtype : result.getDirectSubtypes()) { |
75 | builder.clause(PartialLiterals.candidateMust(subtype.call(p1))); | 76 | builder.clause(PartialLiterals.candidateMust(subtype.call(p1))); |
@@ -80,7 +81,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { | |||
80 | .may(may) | 81 | .may(may) |
81 | .must(must) | 82 | .must(must) |
82 | .candidate(candidate) | 83 | .candidate(candidate) |
83 | .refiner(InferredTypeRefiner.of(typeSymbol, result)); | 84 | .refiner(InferredTypeRefiner.of(TYPE_SYMBOL, result)); |
84 | 85 | ||
85 | if (!result.isAbstractType()) { | 86 | if (!result.isAbstractType()) { |
86 | var decision = Rule.of(type.name(), (builder, instance) -> builder | 87 | var decision = Rule.of(type.name(), (builder, instance) -> builder |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java index 088e3925..b63a8637 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java | |||
@@ -67,4 +67,17 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi | |||
67 | } | 67 | } |
68 | throw new IllegalArgumentException("Unknown UpperCardinality: " + other); | 68 | throw new IllegalArgumentException("Unknown UpperCardinality: " + other); |
69 | } | 69 | } |
70 | |||
71 | @Override | ||
72 | public boolean equals(Object o) { | ||
73 | if (this == o) return true; | ||
74 | if (o == null || getClass() != o.getClass()) return false; | ||
75 | FiniteUpperCardinality that = (FiniteUpperCardinality) o; | ||
76 | return finiteUpperBound == that.finiteUpperBound; | ||
77 | } | ||
78 | |||
79 | @Override | ||
80 | public int hashCode() { | ||
81 | return finiteUpperBound; | ||
82 | } | ||
70 | } | 83 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java index bfaeea25..6bd66df7 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java | |||
@@ -5,6 +5,7 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.representation.cardinality; | 6 | package tools.refinery.store.representation.cardinality; |
7 | 7 | ||
8 | import java.util.Objects; | ||
8 | import java.util.function.BinaryOperator; | 9 | import java.util.function.BinaryOperator; |
9 | import java.util.function.IntBinaryOperator; | 10 | import java.util.function.IntBinaryOperator; |
10 | 11 | ||
@@ -89,4 +90,17 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper | |||
89 | } | 90 | } |
90 | return "[%d..%s]".formatted(lowerBound, upperBound); | 91 | return "[%d..%s]".formatted(lowerBound, upperBound); |
91 | } | 92 | } |
93 | |||
94 | @Override | ||
95 | public boolean equals(Object o) { | ||
96 | if (this == o) return true; | ||
97 | if (o == null || getClass() != o.getClass()) return false; | ||
98 | NonEmptyCardinalityInterval that = (NonEmptyCardinalityInterval) o; | ||
99 | return lowerBound == that.lowerBound && Objects.equals(upperBound, that.upperBound); | ||
100 | } | ||
101 | |||
102 | @Override | ||
103 | public int hashCode() { | ||
104 | return lowerBound * 31 + upperBound.hashCode(); | ||
105 | } | ||
92 | } | 106 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java index e3a334cd..03c701ae 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java | |||
@@ -53,4 +53,14 @@ public final class UnboundedUpperCardinality implements UpperCardinality { | |||
53 | public String toString() { | 53 | public String toString() { |
54 | return "*"; | 54 | return "*"; |
55 | } | 55 | } |
56 | |||
57 | @Override | ||
58 | public boolean equals(Object obj) { | ||
59 | return this == obj || (obj != null && getClass() == obj.getClass()); | ||
60 | } | ||
61 | |||
62 | @Override | ||
63 | public int hashCode() { | ||
64 | return -1; | ||
65 | } | ||
56 | } | 66 | } |