diff options
Diffstat (limited to 'subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java')
-rw-r--r-- | subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java | 339 |
1 files changed, 339 insertions, 0 deletions
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..d756099c --- /dev/null +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java | |||
@@ -0,0 +1,339 @@ | |||
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 | contains Transition[] outgoingTransition opposite source | ||
126 | Transition[] incomingTransition opposite target | ||
127 | } | ||
128 | |||
129 | class Transition { | ||
130 | container Vertex[0..1] 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 = 200..210, Region = 10..*, Choice = 1..*, 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 | @Test | ||
263 | void filesystemTest() { | ||
264 | var parsedProblem = parseHelper.parse(""" | ||
265 | class Filesystem { | ||
266 | contains Entry root | ||
267 | } | ||
268 | |||
269 | abstract class Entry. | ||
270 | |||
271 | class Directory extends Entry { | ||
272 | contains Entry[] entries | ||
273 | } | ||
274 | |||
275 | class File extends Entry. | ||
276 | |||
277 | Filesystem(fs). | ||
278 | |||
279 | scope Filesystem += 0, Entry = 100. | ||
280 | """); | ||
281 | assertThat(parsedProblem.errors(), empty()); | ||
282 | var problem = parsedProblem.problem(); | ||
283 | |||
284 | var storeBuilder = ModelStore.builder() | ||
285 | .with(ViatraModelQueryAdapter.builder()) | ||
286 | // .with(ModelVisualizerAdapter.builder() | ||
287 | // .withOutputPath("test_output") | ||
288 | // .withFormat(FileFormat.DOT) | ||
289 | // .withFormat(FileFormat.SVG) | ||
290 | // .saveStates() | ||
291 | // .saveDesignSpace()) | ||
292 | .with(PropagationAdapter.builder()) | ||
293 | .with(StateCoderAdapter.builder()) | ||
294 | .with(DesignSpaceExplorationAdapter.builder()) | ||
295 | .with(ReasoningAdapter.builder()); | ||
296 | |||
297 | var modelSeed = modelInitializer.createModel(problem, storeBuilder); | ||
298 | |||
299 | var store = storeBuilder.build(); | ||
300 | |||
301 | var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
302 | |||
303 | var initialVersion = initialModel.commit(); | ||
304 | |||
305 | var bestFirst = new BestFirstStoreManager(store, 1); | ||
306 | bestFirst.startExploration(initialVersion); | ||
307 | var resultStore = bestFirst.getSolutionStore(); | ||
308 | System.out.println("states size: " + resultStore.getSolutions().size()); | ||
309 | |||
310 | var model = store.createModelForState(resultStore.getSolutions().get(0).version()); | ||
311 | var interpretation = model.getAdapter(ReasoningAdapter.class) | ||
312 | .getPartialInterpretation(Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL); | ||
313 | var cursor = interpretation.getAll(); | ||
314 | int max = -1; | ||
315 | var types = new LinkedHashMap<PartialRelation, Integer>(); | ||
316 | var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL); | ||
317 | while (cursor.move()) { | ||
318 | max = Math.max(max, cursor.getKey().get(0)); | ||
319 | var type = typeInterpretation.get(cursor.getKey()); | ||
320 | if (type != null) { | ||
321 | types.compute(type.candidateType(), (ignoredKey, oldValue) -> oldValue == null ? 1 : oldValue + 1); | ||
322 | } | ||
323 | } | ||
324 | System.out.println("Model size: " + (max + 1)); | ||
325 | System.out.println(types); | ||
326 | // initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore()); | ||
327 | } | ||
328 | |||
329 | public static void main(String[] args) { | ||
330 | ProblemStandaloneSetup.doSetup(); | ||
331 | var injector = new ProblemStandaloneSetup().createInjectorAndDoEMFRegistration(); | ||
332 | var test = injector.getInstance(ModelGenerationTest.class); | ||
333 | try { | ||
334 | test.statechartTest(); | ||
335 | } catch (Throwable e) { | ||
336 | e.printStackTrace(); | ||
337 | } | ||
338 | } | ||
339 | } | ||