diff options
author | 2023-09-09 12:57:49 +0200 | |
---|---|---|
committer | 2023-09-09 12:57:49 +0200 | |
commit | 0bdb400deef88cb2a7c0b8c90afebf84b29c04d5 (patch) | |
tree | d8cf379d3f1321cb1e3e44e19226c48634ae97f2 /subprojects/language-semantics/src/test/java/tools | |
parent | refactor(store): neighborhood optimization (diff) | |
download | refinery-0bdb400deef88cb2a7c0b8c90afebf84b29c04d5.tar.gz refinery-0bdb400deef88cb2a7c0b8c90afebf84b29c04d5.tar.zst refinery-0bdb400deef88cb2a7c0b8c90afebf84b29c04d5.zip |
feat: integrate DSE with partial interpretation
Diffstat (limited to 'subprojects/language-semantics/src/test/java/tools')
2 files changed, 354 insertions, 0 deletions
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 | } | ||