aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-02-15 12:42:15 -0500
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-02-15 12:42:15 -0500
commitf1d9a50a3be2bfabc6091d51e120ca63ac1ab2d4 (patch)
tree90b96d89d5e6f7f4e6c15b06d34851753350e35d /Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated
parentFix FAM Test. Begin Grammar Fix. (diff)
downloadVIATRA-Generator-f1d9a50a3be2bfabc6091d51e120ca63ac1ab2d4.tar.gz
VIATRA-Generator-f1d9a50a3be2bfabc6091d51e120ca63ac1ab2d4.tar.zst
VIATRA-Generator-f1d9a50a3be2bfabc6091d51e120ca63ac1ab2d4.zip
Set up #19
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated1472
1 files changed, 1472 insertions, 0 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated
new file mode 100644
index 00000000..6d8fc404
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/outputs/yakindu/debug/generated3valued.vql_deactivated
@@ -0,0 +1,1472 @@
1import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
2import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
3import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
4
5//////////
6// 0. Util
7//////////
8private pattern interpretation(problem:LogicProblem, interpretation:PartialInterpretation) {
9 PartialInterpretation.problem(interpretation,problem);
10}
11
12/////////////////////////
13// 0.1 Existence
14/////////////////////////
15private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
16 find interpretation(problem,interpretation);
17 LogicProblem.elements(problem,element);
18} or {
19 find interpretation(problem,interpretation);
20 PartialInterpretation.newElements(interpretation,element);
21}
22
23private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
24 find mustExist(problem,interpretation,element);
25} or {
26 find interpretation(problem,interpretation);
27 neg find elementCloseWorld(element);
28 PartialInterpretation.openWorldElements(interpretation,element);
29}
30
31private pattern elementCloseWorld(element:DefinedElement) {
32 PartialInterpretation.openWorldElements(i,element);
33 PartialInterpretation.maxNewElements(i,0);
34} or {
35 Scope.targetTypeInterpretation(scope,interpretation);
36 PartialTypeInterpratation.elements(interpretation,element);
37 Scope.maxNewElements(scope,0);
38}
39
40////////////////////////
41// 0.2 Equivalence
42////////////////////////
43pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
44 find mayExist(problem,interpretation,a);
45 find mayExist(problem,interpretation,b);
46 a == b;
47}
48
49////////////////////////
50// 0.3 Required Patterns by TypeIndexer
51////////////////////////
52private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) {
53 find interpretation(problem,interpretation);
54 LogicProblem.types(problem,type);
55 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
56 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
57}
58
59private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) {
60 find interpretation(problem,interpretation);
61 LogicProblem.types(problem,type);
62 TypeDefinition.elements(type,element);
63} or {
64 find interpretation(problem,interpretation);
65 find typeInterpretation(problem,interpretation,type,typeInterpretation);
66 PartialComplexTypeInterpretation.elements(typeInterpretation,element);
67}
68
69private pattern isPrimitive(element: PrimitiveElement) {
70 PrimitiveElement(element);
71}
72
73//////////
74// 1. Problem-Specific Base Indexers
75//////////
76// 1.1 Type Indexers
77//////////
78// 1.1.1 primitive Type Indexers
79//////////
80
81//////////
82// 1.1.2 domain-specific Type Indexers
83//////////
84/**
85 * An element must be an instance of type "Pseudostate class".
86 */
87private pattern mustInstanceOfPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
88 Type.name(type,"Pseudostate class");
89 find directInstanceOf(problem,interpretation,element,type);
90}
91private pattern scopeDisallowsNewPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation) {
92 find interpretation(problem,interpretation);
93 PartialInterpretation.scopes(interpretation,scope);
94 Scope.targetTypeInterpretation(scope,typeInterpretation);
95 Scope.maxNewElements(scope,0);
96 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
97 Type.name(type,"Pseudostate class");
98}
99
100/**
101 * An element may be an instance of type "Pseudostate class".
102 */
103private pattern mayInstanceOfPseudostate_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
104{
105 find interpretation(problem,interpretation);
106 PartialInterpretation.newElements(interpretation,element);
107 neg find mustInstanceOfExit_class(problem,interpretation,element);
108 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
109 neg find mustInstanceOfRegion_class(problem,interpretation,element);
110 neg find mustInstanceOfTransition_class(problem,interpretation,element);
111 neg find mustInstanceOfChoice_class(problem,interpretation,element);
112 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
113 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
114 neg find mustInstanceOfEntry_class(problem,interpretation,element);
115 neg find scopeDisallowsNewPseudostate_class(problem, interpretation);
116 neg find isPrimitive(element);
117} or {
118 find interpretation(problem,interpretation);
119 PartialInterpretation.openWorldElements(interpretation,element);
120 neg find mustInstanceOfExit_class(problem,interpretation,element);
121 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
122 neg find mustInstanceOfRegion_class(problem,interpretation,element);
123 neg find mustInstanceOfTransition_class(problem,interpretation,element);
124 neg find mustInstanceOfChoice_class(problem,interpretation,element);
125 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
126 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
127 neg find mustInstanceOfEntry_class(problem,interpretation,element);
128 neg find scopeDisallowsNewPseudostate_class(problem, interpretation);
129 neg find isPrimitive(element);
130} or
131{ find mustInstanceOfPseudostate_class(problem,interpretation,element); }
132/**
133 * An element must be an instance of type "Vertex class".
134 */
135private pattern mustInstanceOfVertex_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
136 Type.name(type,"Vertex class");
137 find directInstanceOf(problem,interpretation,element,type);
138}
139private pattern scopeDisallowsNewVertex_class(problem:LogicProblem, interpretation:PartialInterpretation) {
140 find interpretation(problem,interpretation);
141 PartialInterpretation.scopes(interpretation,scope);
142 Scope.targetTypeInterpretation(scope,typeInterpretation);
143 Scope.maxNewElements(scope,0);
144 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
145 Type.name(type,"Vertex class");
146}
147
148/**
149 * An element may be an instance of type "Vertex class".
150 */
151private pattern mayInstanceOfVertex_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
152{
153 find interpretation(problem,interpretation);
154 PartialInterpretation.newElements(interpretation,element);
155 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
156 neg find mustInstanceOfTransition_class(problem,interpretation,element);
157 neg find mustInstanceOfRegion_class(problem,interpretation,element);
158 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
159 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
160 neg find scopeDisallowsNewVertex_class(problem, interpretation);
161 neg find isPrimitive(element);
162} or {
163 find interpretation(problem,interpretation);
164 PartialInterpretation.openWorldElements(interpretation,element);
165 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
166 neg find mustInstanceOfTransition_class(problem,interpretation,element);
167 neg find mustInstanceOfRegion_class(problem,interpretation,element);
168 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
169 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
170 neg find scopeDisallowsNewVertex_class(problem, interpretation);
171 neg find isPrimitive(element);
172} or
173{ find mustInstanceOfVertex_class(problem,interpretation,element); }
174/**
175 * An element must be an instance of type "Region class".
176 */
177private pattern mustInstanceOfRegion_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
178 Type.name(type,"Region class");
179 find directInstanceOf(problem,interpretation,element,type);
180}
181private pattern scopeDisallowsNewRegion_class(problem:LogicProblem, interpretation:PartialInterpretation) {
182 find interpretation(problem,interpretation);
183 PartialInterpretation.scopes(interpretation,scope);
184 Scope.targetTypeInterpretation(scope,typeInterpretation);
185 Scope.maxNewElements(scope,0);
186 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
187 Type.name(type,"Region class");
188}
189
190/**
191 * An element may be an instance of type "Region class".
192 */
193private pattern mayInstanceOfRegion_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
194{
195 find interpretation(problem,interpretation);
196 PartialInterpretation.newElements(interpretation,element);
197 neg find mustInstanceOfTransition_class(problem,interpretation,element);
198 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
199 neg find mustInstanceOfVertex_class(problem,interpretation,element);
200 neg find scopeDisallowsNewRegion_class(problem, interpretation);
201 neg find isPrimitive(element);
202} or {
203 find interpretation(problem,interpretation);
204 PartialInterpretation.openWorldElements(interpretation,element);
205 neg find mustInstanceOfTransition_class(problem,interpretation,element);
206 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
207 neg find mustInstanceOfVertex_class(problem,interpretation,element);
208 neg find scopeDisallowsNewRegion_class(problem, interpretation);
209 neg find isPrimitive(element);
210} or
211{ find mustInstanceOfRegion_class(problem,interpretation,element); }
212/**
213 * An element must be an instance of type "Transition class".
214 */
215private pattern mustInstanceOfTransition_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
216 Type.name(type,"Transition class");
217 find directInstanceOf(problem,interpretation,element,type);
218}
219private pattern scopeDisallowsNewTransition_class(problem:LogicProblem, interpretation:PartialInterpretation) {
220 find interpretation(problem,interpretation);
221 PartialInterpretation.scopes(interpretation,scope);
222 Scope.targetTypeInterpretation(scope,typeInterpretation);
223 Scope.maxNewElements(scope,0);
224 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
225 Type.name(type,"Transition class");
226}
227
228/**
229 * An element may be an instance of type "Transition class".
230 */
231private pattern mayInstanceOfTransition_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
232{
233 find interpretation(problem,interpretation);
234 PartialInterpretation.newElements(interpretation,element);
235 neg find mustInstanceOfRegion_class(problem,interpretation,element);
236 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
237 neg find mustInstanceOfVertex_class(problem,interpretation,element);
238 neg find scopeDisallowsNewTransition_class(problem, interpretation);
239 neg find isPrimitive(element);
240} or {
241 find interpretation(problem,interpretation);
242 PartialInterpretation.openWorldElements(interpretation,element);
243 neg find mustInstanceOfRegion_class(problem,interpretation,element);
244 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
245 neg find mustInstanceOfVertex_class(problem,interpretation,element);
246 neg find scopeDisallowsNewTransition_class(problem, interpretation);
247 neg find isPrimitive(element);
248} or
249{ find mustInstanceOfTransition_class(problem,interpretation,element); }
250/**
251 * An element must be an instance of type "Statechart class".
252 */
253private pattern mustInstanceOfStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
254 Type.name(type,"Statechart class");
255 find directInstanceOf(problem,interpretation,element,type);
256}
257private pattern scopeDisallowsNewStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation) {
258 find interpretation(problem,interpretation);
259 PartialInterpretation.scopes(interpretation,scope);
260 Scope.targetTypeInterpretation(scope,typeInterpretation);
261 Scope.maxNewElements(scope,0);
262 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
263 Type.name(type,"Statechart class");
264}
265
266/**
267 * An element may be an instance of type "Statechart class".
268 */
269private pattern mayInstanceOfStatechart_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
270{
271 find interpretation(problem,interpretation);
272 PartialInterpretation.newElements(interpretation,element);
273 neg find mustInstanceOfRegion_class(problem,interpretation,element);
274 neg find mustInstanceOfTransition_class(problem,interpretation,element);
275 neg find mustInstanceOfVertex_class(problem,interpretation,element);
276 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
277 neg find scopeDisallowsNewStatechart_class(problem, interpretation);
278 neg find isPrimitive(element);
279} or {
280 find interpretation(problem,interpretation);
281 PartialInterpretation.openWorldElements(interpretation,element);
282 neg find mustInstanceOfRegion_class(problem,interpretation,element);
283 neg find mustInstanceOfTransition_class(problem,interpretation,element);
284 neg find mustInstanceOfVertex_class(problem,interpretation,element);
285 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
286 neg find scopeDisallowsNewStatechart_class(problem, interpretation);
287 neg find isPrimitive(element);
288} or
289{ find mustInstanceOfStatechart_class(problem,interpretation,element); }
290/**
291 * An element must be an instance of type "Entry class".
292 */
293private pattern mustInstanceOfEntry_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
294 Type.name(type,"Entry class");
295 find directInstanceOf(problem,interpretation,element,type);
296}
297private pattern scopeDisallowsNewEntry_class(problem:LogicProblem, interpretation:PartialInterpretation) {
298 find interpretation(problem,interpretation);
299 PartialInterpretation.scopes(interpretation,scope);
300 Scope.targetTypeInterpretation(scope,typeInterpretation);
301 Scope.maxNewElements(scope,0);
302 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
303 Type.name(type,"Entry class");
304}
305
306/**
307 * An element may be an instance of type "Entry class".
308 */
309private pattern mayInstanceOfEntry_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
310{
311 find interpretation(problem,interpretation);
312 PartialInterpretation.newElements(interpretation,element);
313 neg find mustInstanceOfExit_class(problem,interpretation,element);
314 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
315 neg find mustInstanceOfTransition_class(problem,interpretation,element);
316 neg find mustInstanceOfRegion_class(problem,interpretation,element);
317 neg find mustInstanceOfChoice_class(problem,interpretation,element);
318 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
319 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
320 neg find scopeDisallowsNewEntry_class(problem, interpretation);
321 neg find isPrimitive(element);
322} or {
323 find interpretation(problem,interpretation);
324 PartialInterpretation.openWorldElements(interpretation,element);
325 neg find mustInstanceOfExit_class(problem,interpretation,element);
326 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
327 neg find mustInstanceOfTransition_class(problem,interpretation,element);
328 neg find mustInstanceOfRegion_class(problem,interpretation,element);
329 neg find mustInstanceOfChoice_class(problem,interpretation,element);
330 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
331 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
332 neg find scopeDisallowsNewEntry_class(problem, interpretation);
333 neg find isPrimitive(element);
334} or
335{ find mustInstanceOfEntry_class(problem,interpretation,element); }
336/**
337 * An element must be an instance of type "Synchronization class".
338 */
339private pattern mustInstanceOfSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
340 Type.name(type,"Synchronization class");
341 find directInstanceOf(problem,interpretation,element,type);
342}
343private pattern scopeDisallowsNewSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation) {
344 find interpretation(problem,interpretation);
345 PartialInterpretation.scopes(interpretation,scope);
346 Scope.targetTypeInterpretation(scope,typeInterpretation);
347 Scope.maxNewElements(scope,0);
348 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
349 Type.name(type,"Synchronization class");
350}
351
352/**
353 * An element may be an instance of type "Synchronization class".
354 */
355private pattern mayInstanceOfSynchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
356{
357 find interpretation(problem,interpretation);
358 PartialInterpretation.newElements(interpretation,element);
359 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
360 neg find mustInstanceOfExit_class(problem,interpretation,element);
361 neg find mustInstanceOfRegion_class(problem,interpretation,element);
362 neg find mustInstanceOfTransition_class(problem,interpretation,element);
363 neg find mustInstanceOfChoice_class(problem,interpretation,element);
364 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
365 neg find mustInstanceOfEntry_class(problem,interpretation,element);
366 neg find scopeDisallowsNewSynchronization_class(problem, interpretation);
367 neg find isPrimitive(element);
368} or {
369 find interpretation(problem,interpretation);
370 PartialInterpretation.openWorldElements(interpretation,element);
371 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
372 neg find mustInstanceOfExit_class(problem,interpretation,element);
373 neg find mustInstanceOfRegion_class(problem,interpretation,element);
374 neg find mustInstanceOfTransition_class(problem,interpretation,element);
375 neg find mustInstanceOfChoice_class(problem,interpretation,element);
376 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
377 neg find mustInstanceOfEntry_class(problem,interpretation,element);
378 neg find scopeDisallowsNewSynchronization_class(problem, interpretation);
379 neg find isPrimitive(element);
380} or
381{ find mustInstanceOfSynchronization_class(problem,interpretation,element); }
382/**
383 * An element must be an instance of type "State class".
384 */
385private pattern mustInstanceOfState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
386 Type.name(type,"State class");
387 find directInstanceOf(problem,interpretation,element,type);
388}
389private pattern scopeDisallowsNewState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
390 find interpretation(problem,interpretation);
391 PartialInterpretation.scopes(interpretation,scope);
392 Scope.targetTypeInterpretation(scope,typeInterpretation);
393 Scope.maxNewElements(scope,0);
394 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
395 Type.name(type,"State class");
396}
397
398/**
399 * An element may be an instance of type "State class".
400 */
401private pattern mayInstanceOfState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
402{
403 find interpretation(problem,interpretation);
404 PartialInterpretation.newElements(interpretation,element);
405 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
406 neg find mustInstanceOfRegion_class(problem,interpretation,element);
407 neg find mustInstanceOfTransition_class(problem,interpretation,element);
408 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
409 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
410 neg find scopeDisallowsNewState_class(problem, interpretation);
411 neg find isPrimitive(element);
412} or {
413 find interpretation(problem,interpretation);
414 PartialInterpretation.openWorldElements(interpretation,element);
415 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
416 neg find mustInstanceOfRegion_class(problem,interpretation,element);
417 neg find mustInstanceOfTransition_class(problem,interpretation,element);
418 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
419 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
420 neg find scopeDisallowsNewState_class(problem, interpretation);
421 neg find isPrimitive(element);
422} or
423{ find mustInstanceOfState_class(problem,interpretation,element); }
424/**
425 * An element must be an instance of type "RegularState class".
426 */
427private pattern mustInstanceOfRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
428 Type.name(type,"RegularState class");
429 find directInstanceOf(problem,interpretation,element,type);
430}
431private pattern scopeDisallowsNewRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
432 find interpretation(problem,interpretation);
433 PartialInterpretation.scopes(interpretation,scope);
434 Scope.targetTypeInterpretation(scope,typeInterpretation);
435 Scope.maxNewElements(scope,0);
436 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
437 Type.name(type,"RegularState class");
438}
439
440/**
441 * An element may be an instance of type "RegularState class".
442 */
443private pattern mayInstanceOfRegularState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
444{
445 find interpretation(problem,interpretation);
446 PartialInterpretation.newElements(interpretation,element);
447 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
448 neg find mustInstanceOfTransition_class(problem,interpretation,element);
449 neg find mustInstanceOfRegion_class(problem,interpretation,element);
450 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
451 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
452 neg find scopeDisallowsNewRegularState_class(problem, interpretation);
453 neg find isPrimitive(element);
454} or {
455 find interpretation(problem,interpretation);
456 PartialInterpretation.openWorldElements(interpretation,element);
457 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
458 neg find mustInstanceOfTransition_class(problem,interpretation,element);
459 neg find mustInstanceOfRegion_class(problem,interpretation,element);
460 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
461 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
462 neg find scopeDisallowsNewRegularState_class(problem, interpretation);
463 neg find isPrimitive(element);
464} or
465{ find mustInstanceOfRegularState_class(problem,interpretation,element); }
466/**
467 * An element must be an instance of type "CompositeElement class".
468 */
469private pattern mustInstanceOfCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
470 Type.name(type,"CompositeElement class");
471 find directInstanceOf(problem,interpretation,element,type);
472}
473private pattern scopeDisallowsNewCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation) {
474 find interpretation(problem,interpretation);
475 PartialInterpretation.scopes(interpretation,scope);
476 Scope.targetTypeInterpretation(scope,typeInterpretation);
477 Scope.maxNewElements(scope,0);
478 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
479 Type.name(type,"CompositeElement class");
480}
481
482/**
483 * An element may be an instance of type "CompositeElement class".
484 */
485private pattern mayInstanceOfCompositeElement_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
486{
487 find interpretation(problem,interpretation);
488 PartialInterpretation.newElements(interpretation,element);
489 neg find mustInstanceOfTransition_class(problem,interpretation,element);
490 neg find mustInstanceOfRegion_class(problem,interpretation,element);
491 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
492 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
493 neg find mustInstanceOfVertex_class(problem,interpretation,element);
494 neg find scopeDisallowsNewCompositeElement_class(problem, interpretation);
495 neg find isPrimitive(element);
496} or {
497 find interpretation(problem,interpretation);
498 PartialInterpretation.openWorldElements(interpretation,element);
499 neg find mustInstanceOfTransition_class(problem,interpretation,element);
500 neg find mustInstanceOfRegion_class(problem,interpretation,element);
501 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
502 neg find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element);
503 neg find mustInstanceOfVertex_class(problem,interpretation,element);
504 neg find scopeDisallowsNewCompositeElement_class(problem, interpretation);
505 neg find isPrimitive(element);
506} or
507{ find mustInstanceOfCompositeElement_class(problem,interpretation,element); }
508/**
509 * An element must be an instance of type "Choice class".
510 */
511private pattern mustInstanceOfChoice_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
512 Type.name(type,"Choice class");
513 find directInstanceOf(problem,interpretation,element,type);
514}
515private pattern scopeDisallowsNewChoice_class(problem:LogicProblem, interpretation:PartialInterpretation) {
516 find interpretation(problem,interpretation);
517 PartialInterpretation.scopes(interpretation,scope);
518 Scope.targetTypeInterpretation(scope,typeInterpretation);
519 Scope.maxNewElements(scope,0);
520 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
521 Type.name(type,"Choice class");
522}
523
524/**
525 * An element may be an instance of type "Choice class".
526 */
527private pattern mayInstanceOfChoice_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
528{
529 find interpretation(problem,interpretation);
530 PartialInterpretation.newElements(interpretation,element);
531 neg find mustInstanceOfExit_class(problem,interpretation,element);
532 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
533 neg find mustInstanceOfRegion_class(problem,interpretation,element);
534 neg find mustInstanceOfTransition_class(problem,interpretation,element);
535 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
536 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
537 neg find mustInstanceOfEntry_class(problem,interpretation,element);
538 neg find scopeDisallowsNewChoice_class(problem, interpretation);
539 neg find isPrimitive(element);
540} or {
541 find interpretation(problem,interpretation);
542 PartialInterpretation.openWorldElements(interpretation,element);
543 neg find mustInstanceOfExit_class(problem,interpretation,element);
544 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
545 neg find mustInstanceOfRegion_class(problem,interpretation,element);
546 neg find mustInstanceOfTransition_class(problem,interpretation,element);
547 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
548 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
549 neg find mustInstanceOfEntry_class(problem,interpretation,element);
550 neg find scopeDisallowsNewChoice_class(problem, interpretation);
551 neg find isPrimitive(element);
552} or
553{ find mustInstanceOfChoice_class(problem,interpretation,element); }
554/**
555 * An element must be an instance of type "Exit class".
556 */
557private pattern mustInstanceOfExit_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
558 Type.name(type,"Exit class");
559 find directInstanceOf(problem,interpretation,element,type);
560}
561private pattern scopeDisallowsNewExit_class(problem:LogicProblem, interpretation:PartialInterpretation) {
562 find interpretation(problem,interpretation);
563 PartialInterpretation.scopes(interpretation,scope);
564 Scope.targetTypeInterpretation(scope,typeInterpretation);
565 Scope.maxNewElements(scope,0);
566 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
567 Type.name(type,"Exit class");
568}
569
570/**
571 * An element may be an instance of type "Exit class".
572 */
573private pattern mayInstanceOfExit_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
574{
575 find interpretation(problem,interpretation);
576 PartialInterpretation.newElements(interpretation,element);
577 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
578 neg find mustInstanceOfTransition_class(problem,interpretation,element);
579 neg find mustInstanceOfRegion_class(problem,interpretation,element);
580 neg find mustInstanceOfChoice_class(problem,interpretation,element);
581 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
582 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
583 neg find mustInstanceOfEntry_class(problem,interpretation,element);
584 neg find scopeDisallowsNewExit_class(problem, interpretation);
585 neg find isPrimitive(element);
586} or {
587 find interpretation(problem,interpretation);
588 PartialInterpretation.openWorldElements(interpretation,element);
589 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
590 neg find mustInstanceOfTransition_class(problem,interpretation,element);
591 neg find mustInstanceOfRegion_class(problem,interpretation,element);
592 neg find mustInstanceOfChoice_class(problem,interpretation,element);
593 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
594 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
595 neg find mustInstanceOfEntry_class(problem,interpretation,element);
596 neg find scopeDisallowsNewExit_class(problem, interpretation);
597 neg find isPrimitive(element);
598} or
599{ find mustInstanceOfExit_class(problem,interpretation,element); }
600/**
601 * An element must be an instance of type "FinalState class".
602 */
603private pattern mustInstanceOfFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
604 Type.name(type,"FinalState class");
605 find directInstanceOf(problem,interpretation,element,type);
606}
607private pattern scopeDisallowsNewFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation) {
608 find interpretation(problem,interpretation);
609 PartialInterpretation.scopes(interpretation,scope);
610 Scope.targetTypeInterpretation(scope,typeInterpretation);
611 Scope.maxNewElements(scope,0);
612 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
613 Type.name(type,"FinalState class");
614}
615
616/**
617 * An element may be an instance of type "FinalState class".
618 */
619private pattern mayInstanceOfFinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
620{
621 find interpretation(problem,interpretation);
622 PartialInterpretation.newElements(interpretation,element);
623 neg find mustInstanceOfTransition_class(problem,interpretation,element);
624 neg find mustInstanceOfRegion_class(problem,interpretation,element);
625 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
626 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
627 neg find scopeDisallowsNewFinalState_class(problem, interpretation);
628 neg find isPrimitive(element);
629} or {
630 find interpretation(problem,interpretation);
631 PartialInterpretation.openWorldElements(interpretation,element);
632 neg find mustInstanceOfTransition_class(problem,interpretation,element);
633 neg find mustInstanceOfRegion_class(problem,interpretation,element);
634 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
635 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
636 neg find scopeDisallowsNewFinalState_class(problem, interpretation);
637 neg find isPrimitive(element);
638} or
639{ find mustInstanceOfFinalState_class(problem,interpretation,element); }
640/**
641 * An element must be an instance of type "Statechart class DefinedPart".
642 */
643private pattern mustInstanceOfStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
644 Type.name(type,"Statechart class DefinedPart");
645 find directInstanceOf(problem,interpretation,element,type);
646}
647private pattern scopeDisallowsNewStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
648 find interpretation(problem,interpretation);
649 PartialInterpretation.scopes(interpretation,scope);
650 Scope.targetTypeInterpretation(scope,typeInterpretation);
651 Scope.maxNewElements(scope,0);
652 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
653 Type.name(type,"Statechart class DefinedPart");
654}
655
656/**
657 * An element may be an instance of type "Statechart class DefinedPart".
658 */
659private pattern mayInstanceOfStatechart_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
660{ find mustInstanceOfStatechart_class_DefinedPart(problem,interpretation,element); }
661/**
662 * An element must be an instance of type "Statechart class UndefinedPart".
663 */
664private pattern mustInstanceOfStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
665 Type.name(type,"Statechart class UndefinedPart");
666 find directInstanceOf(problem,interpretation,element,type);
667}
668private pattern scopeDisallowsNewStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
669 find interpretation(problem,interpretation);
670 PartialInterpretation.scopes(interpretation,scope);
671 Scope.targetTypeInterpretation(scope,typeInterpretation);
672 Scope.maxNewElements(scope,0);
673 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
674 Type.name(type,"Statechart class UndefinedPart");
675}
676
677/**
678 * An element may be an instance of type "Statechart class UndefinedPart".
679 */
680private pattern mayInstanceOfStatechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
681{
682 find interpretation(problem,interpretation);
683 PartialInterpretation.newElements(interpretation,element);
684 neg find mustInstanceOfRegion_class(problem,interpretation,element);
685 neg find mustInstanceOfTransition_class(problem,interpretation,element);
686 neg find mustInstanceOfVertex_class(problem,interpretation,element);
687 neg find scopeDisallowsNewStatechart_class_UndefinedPart(problem, interpretation);
688 neg find isPrimitive(element);
689} or {
690 find interpretation(problem,interpretation);
691 PartialInterpretation.openWorldElements(interpretation,element);
692 neg find mustInstanceOfRegion_class(problem,interpretation,element);
693 neg find mustInstanceOfTransition_class(problem,interpretation,element);
694 neg find mustInstanceOfVertex_class(problem,interpretation,element);
695 neg find scopeDisallowsNewStatechart_class_UndefinedPart(problem, interpretation);
696 neg find isPrimitive(element);
697} or
698{ find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element); }
699/**
700 * An element must be an instance of type "CompositeElement class DefinedPart".
701 */
702private pattern mustInstanceOfCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
703 Type.name(type,"CompositeElement class DefinedPart");
704 find directInstanceOf(problem,interpretation,element,type);
705}
706private pattern scopeDisallowsNewCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
707 find interpretation(problem,interpretation);
708 PartialInterpretation.scopes(interpretation,scope);
709 Scope.targetTypeInterpretation(scope,typeInterpretation);
710 Scope.maxNewElements(scope,0);
711 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
712 Type.name(type,"CompositeElement class DefinedPart");
713}
714
715/**
716 * An element may be an instance of type "CompositeElement class DefinedPart".
717 */
718private pattern mayInstanceOfCompositeElement_class_DefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
719{ find mustInstanceOfCompositeElement_class_DefinedPart(problem,interpretation,element); }
720/**
721 * An element must be an instance of type "CompositeElement class UndefinedPart".
722 */
723private pattern mustInstanceOfCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
724 Type.name(type,"CompositeElement class UndefinedPart");
725 find directInstanceOf(problem,interpretation,element,type);
726}
727private pattern scopeDisallowsNewCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation) {
728 find interpretation(problem,interpretation);
729 PartialInterpretation.scopes(interpretation,scope);
730 Scope.targetTypeInterpretation(scope,typeInterpretation);
731 Scope.maxNewElements(scope,0);
732 PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);
733 Type.name(type,"CompositeElement class UndefinedPart");
734}
735
736/**
737 * An element may be an instance of type "CompositeElement class UndefinedPart".
738 */
739private pattern mayInstanceOfCompositeElement_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement)
740{
741 find interpretation(problem,interpretation);
742 PartialInterpretation.newElements(interpretation,element);
743 neg find mustInstanceOfRegion_class(problem,interpretation,element);
744 neg find mustInstanceOfTransition_class(problem,interpretation,element);
745 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
746 neg find mustInstanceOfVertex_class(problem,interpretation,element);
747 neg find scopeDisallowsNewCompositeElement_class_UndefinedPart(problem, interpretation);
748 neg find isPrimitive(element);
749} or {
750 find interpretation(problem,interpretation);
751 PartialInterpretation.openWorldElements(interpretation,element);
752 neg find mustInstanceOfRegion_class(problem,interpretation,element);
753 neg find mustInstanceOfTransition_class(problem,interpretation,element);
754 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
755 neg find mustInstanceOfVertex_class(problem,interpretation,element);
756 neg find scopeDisallowsNewCompositeElement_class_UndefinedPart(problem, interpretation);
757 neg find isPrimitive(element);
758} or
759{ find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,element); }
760
761//////////
762// 1.2 Relation Declaration Indexers
763//////////
764/**
765 * Matcher for detecting tuples t where []incomingTransitions reference Vertex(source,target)
766 */
767private pattern mustInRelationincomingTransitions_reference_Vertex(
768 problem:LogicProblem, interpretation:PartialInterpretation,
769 source: DefinedElement, target:DefinedElement)
770{
771 find interpretation(problem,interpretation);
772 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
773 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"incomingTransitions reference Vertex");
774 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
775 BinaryElementRelationLink.param1(link,source);
776 BinaryElementRelationLink.param2(link,target);
777}
778/**
779 * Matcher for detecting tuples t where <>incomingTransitions reference Vertex(source,target)
780 */
781private pattern mayInRelationincomingTransitions_reference_Vertex(
782 problem:LogicProblem, interpretation:PartialInterpretation,
783 source: DefinedElement, target:DefinedElement)
784{
785 find interpretation(problem,interpretation);
786 // The two endpoint of the link have to exist
787 find mayExist(problem, interpretation, source);
788 find mayExist(problem, interpretation, target);
789 // Type consistency
790 find mayInstanceOfVertex_class(problem,interpretation,source);
791 find mayInstanceOfTransition_class(problem,interpretation,target);
792 // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
793 // the upper bound of the opposite reference multiplicity should be considered.
794 numberOfExistingOppositeReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,target,_);
795 check(numberOfExistingOppositeReferences < 1);
796} or {
797 find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,source,target);
798}
799/**
800 * Matcher for detecting tuples t where []outgoingTransitions reference Vertex(source,target)
801 */
802private pattern mustInRelationoutgoingTransitions_reference_Vertex(
803 problem:LogicProblem, interpretation:PartialInterpretation,
804 source: DefinedElement, target:DefinedElement)
805{
806 find interpretation(problem,interpretation);
807 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
808 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"outgoingTransitions reference Vertex");
809 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
810 BinaryElementRelationLink.param1(link,source);
811 BinaryElementRelationLink.param2(link,target);
812}
813/**
814 * Matcher for detecting tuples t where <>outgoingTransitions reference Vertex(source,target)
815 */
816private pattern mayInRelationoutgoingTransitions_reference_Vertex(
817 problem:LogicProblem, interpretation:PartialInterpretation,
818 source: DefinedElement, target:DefinedElement)
819{
820 find interpretation(problem,interpretation);
821 // The two endpoint of the link have to exist
822 find mayExist(problem, interpretation, source);
823 find mayExist(problem, interpretation, target);
824 // Type consistency
825 find mayInstanceOfVertex_class(problem,interpretation,source);
826 find mayInstanceOfTransition_class(problem,interpretation,target);
827 // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
828 // the upper bound of the opposite reference multiplicity should be considered.
829 numberOfExistingOppositeReferences == count find mustInRelationsource_reference_Transition(problem,interpretation,target,_);
830 check(numberOfExistingOppositeReferences < 1);
831 // The reference is containment, then a new reference cannot be create if:
832 // 1. Multiple parents
833 neg find mustContains4(problem,interpretation,_,target);
834 // 2. Circle in the containment hierarchy
835 neg find mustTransitiveContains(source,target);
836} or {
837 find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,source,target);
838}
839/**
840 * Matcher for detecting tuples t where []vertices reference Region(source,target)
841 */
842private pattern mustInRelationvertices_reference_Region(
843 problem:LogicProblem, interpretation:PartialInterpretation,
844 source: DefinedElement, target:DefinedElement)
845{
846 find interpretation(problem,interpretation);
847 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
848 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"vertices reference Region");
849 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
850 BinaryElementRelationLink.param1(link,source);
851 BinaryElementRelationLink.param2(link,target);
852}
853/**
854 * Matcher for detecting tuples t where <>vertices reference Region(source,target)
855 */
856private pattern mayInRelationvertices_reference_Region(
857 problem:LogicProblem, interpretation:PartialInterpretation,
858 source: DefinedElement, target:DefinedElement)
859{
860 find interpretation(problem,interpretation);
861 // The two endpoint of the link have to exist
862 find mayExist(problem, interpretation, source);
863 find mayExist(problem, interpretation, target);
864 // Type consistency
865 find mayInstanceOfRegion_class(problem,interpretation,source);
866 find mayInstanceOfVertex_class(problem,interpretation,target);
867 // The reference is containment, then a new reference cannot be create if:
868 // 1. Multiple parents
869 neg find mustContains4(problem,interpretation,_,target);
870 // 2. Circle in the containment hierarchy
871 neg find mustTransitiveContains(source,target);
872} or {
873 find mustInRelationvertices_reference_Region(problem,interpretation,source,target);
874}
875/**
876 * Matcher for detecting tuples t where []target reference Transition(source,target)
877 */
878private pattern mustInRelationtarget_reference_Transition(
879 problem:LogicProblem, interpretation:PartialInterpretation,
880 source: DefinedElement, target:DefinedElement)
881{
882 find interpretation(problem,interpretation);
883 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
884 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"target reference Transition");
885 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
886 BinaryElementRelationLink.param1(link,source);
887 BinaryElementRelationLink.param2(link,target);
888}
889/**
890 * Matcher for detecting tuples t where <>target reference Transition(source,target)
891 */
892private pattern mayInRelationtarget_reference_Transition(
893 problem:LogicProblem, interpretation:PartialInterpretation,
894 source: DefinedElement, target:DefinedElement)
895{
896 find interpretation(problem,interpretation);
897 // The two endpoint of the link have to exist
898 find mayExist(problem, interpretation, source);
899 find mayExist(problem, interpretation, target);
900 // Type consistency
901 find mayInstanceOfTransition_class(problem,interpretation,source);
902 find mayInstanceOfVertex_class(problem,interpretation,target);
903 // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
904 // the upper bound of the multiplicity should be considered.
905 numberOfExistingReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,source,_);
906 check(numberOfExistingReferences < 1);
907} or {
908 find mustInRelationtarget_reference_Transition(problem,interpretation,source,target);
909}
910/**
911 * Matcher for detecting tuples t where []source reference Transition(source,target)
912 */
913private pattern mustInRelationsource_reference_Transition(
914 problem:LogicProblem, interpretation:PartialInterpretation,
915 source: DefinedElement, target:DefinedElement)
916{
917 find interpretation(problem,interpretation);
918 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
919 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"source reference Transition");
920 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
921 BinaryElementRelationLink.param1(link,source);
922 BinaryElementRelationLink.param2(link,target);
923}
924/**
925 * Matcher for detecting tuples t where <>source reference Transition(source,target)
926 */
927private pattern mayInRelationsource_reference_Transition(
928 problem:LogicProblem, interpretation:PartialInterpretation,
929 source: DefinedElement, target:DefinedElement)
930{
931 find interpretation(problem,interpretation);
932 // The two endpoint of the link have to exist
933 find mayExist(problem, interpretation, source);
934 find mayExist(problem, interpretation, target);
935 // Type consistency
936 find mayInstanceOfTransition_class(problem,interpretation,source);
937 find mayInstanceOfVertex_class(problem,interpretation,target);
938 // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
939 // the upper bound of the multiplicity should be considered.
940 numberOfExistingReferences == count find mustInRelationsource_reference_Transition(problem,interpretation,source,_);
941 check(numberOfExistingReferences < 1);
942 // The eOpposite of the reference is containment, then a referene cannot be created if
943 // 1. Multiple parents
944 neg find mustContains4(problem,interpretation,source,_);
945 // 2. Circle in the containment hierarchy
946 neg find mustTransitiveContains(source,target);
947} or {
948 find mustInRelationsource_reference_Transition(problem,interpretation,source,target);
949}
950/**
951 * Matcher for detecting tuples t where []regions reference CompositeElement(source,target)
952 */
953private pattern mustInRelationregions_reference_CompositeElement(
954 problem:LogicProblem, interpretation:PartialInterpretation,
955 source: DefinedElement, target:DefinedElement)
956{
957 find interpretation(problem,interpretation);
958 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
959 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"regions reference CompositeElement");
960 PartialRelationInterpretation.relationlinks(relationIterpretation,link);
961 BinaryElementRelationLink.param1(link,source);
962 BinaryElementRelationLink.param2(link,target);
963}
964/**
965 * Matcher for detecting tuples t where <>regions reference CompositeElement(source,target)
966 */
967private pattern mayInRelationregions_reference_CompositeElement(
968 problem:LogicProblem, interpretation:PartialInterpretation,
969 source: DefinedElement, target:DefinedElement)
970{
971 find interpretation(problem,interpretation);
972 // The two endpoint of the link have to exist
973 find mayExist(problem, interpretation, source);
974 find mayExist(problem, interpretation, target);
975 // Type consistency
976 find mayInstanceOfCompositeElement_class(problem,interpretation,source);
977 find mayInstanceOfRegion_class(problem,interpretation,target);
978 // The reference is containment, then a new reference cannot be create if:
979 // 1. Multiple parents
980 neg find mustContains4(problem,interpretation,_,target);
981 // 2. Circle in the containment hierarchy
982 neg find mustTransitiveContains(source,target);
983} or {
984 find mustInRelationregions_reference_CompositeElement(problem,interpretation,source,target);
985}
986
987//////////
988// 1.3 Relation Definition Indexers
989//////////
990
991//////////
992// 1.4 Containment Indexer
993//////////
994private pattern mustContains2(source: DefinedElement, target: DefinedElement) {
995 find mustContains4(_,_,source,target);
996}
997
998private pattern mustContains4(problem:LogicProblem, interpretation:PartialInterpretation,
999 source: DefinedElement, target: DefinedElement)
1000 { find mustInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,source,target); }or
1001
1002 { find mustInRelationvertices_reference_Region(problem,interpretation,source,target); }or
1003
1004 { find mustInRelationregions_reference_CompositeElement(problem,interpretation,source,target); }
1005
1006private pattern mustTransitiveContains(source,target) {
1007 find mustContains2+(source,target);
1008}
1009
1010//////////
1011// 2. Invalidation Indexers
1012//////////
1013// 2.1 Invalidated by WF Queries
1014//////////
1015
1016//////////
1017// 3. Unfinishedness Indexers
1018//////////
1019// 3.1 Unfinishedness Measured by Multiplicity
1020//////////
1021pattern unfinishedLowerMultiplicity_target_reference_Transition(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) {
1022 find interpretation(problem,interpretation);
1023 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
1024 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"target reference Transition");
1025 find mustInstanceOfTransition_class(problem,interpretation,object);
1026 numberOfExistingReferences == count find mustInRelationtarget_reference_Transition(problem,interpretation,object,_);
1027 check(numberOfExistingReferences < 1);
1028 missingMultiplicity == eval(1-numberOfExistingReferences);
1029}
1030
1031//////////
1032// 3.2 Unfinishedness Measured by WF Queries
1033//////////
1034
1035//////////
1036// 4. Refinement Indexers
1037//////////
1038// 4.1 Object constructors
1039//////////
1040private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation)
1041{
1042 find interpretation(problem,interpretation);
1043 find mustInstanceOfPseudostate_class(problem,interpretation,root);
1044 find mustExist(problem, interpretation, root);
1045}or{
1046 find interpretation(problem,interpretation);
1047 find mustInstanceOfCompositeElement_class(problem,interpretation,root);
1048 find mustExist(problem, interpretation, root);
1049}or{
1050 find interpretation(problem,interpretation);
1051 find mustInstanceOfTransition_class(problem,interpretation,root);
1052 find mustExist(problem, interpretation, root);
1053}or{
1054 find interpretation(problem,interpretation);
1055 find mustInstanceOfState_class(problem,interpretation,root);
1056 find mustExist(problem, interpretation, root);
1057}or{
1058 find interpretation(problem,interpretation);
1059 find mustInstanceOfSynchronization_class(problem,interpretation,root);
1060 find mustExist(problem, interpretation, root);
1061}or{
1062 find interpretation(problem,interpretation);
1063 find mustInstanceOfEntry_class(problem,interpretation,root);
1064 find mustExist(problem, interpretation, root);
1065}or{
1066 find interpretation(problem,interpretation);
1067 find mustInstanceOfRegularState_class(problem,interpretation,root);
1068 find mustExist(problem, interpretation, root);
1069}or{
1070 find interpretation(problem,interpretation);
1071 find mustInstanceOfChoice_class(problem,interpretation,root);
1072 find mustExist(problem, interpretation, root);
1073}or{
1074 find interpretation(problem,interpretation);
1075 find mustInstanceOfVertex_class(problem,interpretation,root);
1076 find mustExist(problem, interpretation, root);
1077}or{
1078 find interpretation(problem,interpretation);
1079 find mustInstanceOfStatechart_class(problem,interpretation,root);
1080 find mustExist(problem, interpretation, root);
1081}or{
1082 find interpretation(problem,interpretation);
1083 find mustInstanceOfExit_class(problem,interpretation,root);
1084 find mustExist(problem, interpretation, root);
1085}or{
1086 find interpretation(problem,interpretation);
1087 find mustInstanceOfFinalState_class(problem,interpretation,root);
1088 find mustExist(problem, interpretation, root);
1089}or{
1090 find interpretation(problem,interpretation);
1091 find mustInstanceOfRegion_class(problem,interpretation,root);
1092 find mustExist(problem, interpretation, root);
1093}or{
1094 find interpretation(problem,interpretation);
1095 find mustInstanceOfStatechart_class_DefinedPart(problem,interpretation,root);
1096 find mustExist(problem, interpretation, root);
1097}or{
1098 find interpretation(problem,interpretation);
1099 find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,root);
1100 find mustExist(problem, interpretation, root);
1101}or{
1102 find interpretation(problem,interpretation);
1103 find mustInstanceOfCompositeElement_class_DefinedPart(problem,interpretation,root);
1104 find mustExist(problem, interpretation, root);
1105}or{
1106 find interpretation(problem,interpretation);
1107 find mustInstanceOfCompositeElement_class_UndefinedPart(problem,interpretation,root);
1108 find mustExist(problem, interpretation, root);
1109}
1110pattern createObject_Exit_class_by_vertices_reference_Region(
1111 problem:LogicProblem, interpretation:PartialInterpretation,
1112 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1113 container:DefinedElement)
1114{
1115 find interpretation(problem,interpretation);
1116 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1117 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Exit class");
1118 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1119 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
1120 find mustInstanceOfRegion_class(problem,interpretation,container);
1121 find mayInstanceOfExit_class(problem,interpretation,newObject);
1122 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
1123 find mustExist(problem, interpretation, container);
1124 neg find mustExist(problem, interpretation, newObject);
1125}
1126pattern createObject_Exit_class(
1127 problem:LogicProblem, interpretation:PartialInterpretation,
1128 typeInterpretation:PartialComplexTypeInterpretation)
1129{
1130 find interpretation(problem,interpretation);
1131 neg find hasElementInContainment(problem,interpretation);
1132 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1133 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Exit class");
1134 find mayInstanceOfExit_class(problem,interpretation,newObject);
1135 find mayExist(problem, interpretation, newObject);
1136 neg find mustExist(problem, interpretation, newObject);
1137}
1138pattern createObject_FinalState_class_by_vertices_reference_Region(
1139 problem:LogicProblem, interpretation:PartialInterpretation,
1140 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1141 container:DefinedElement)
1142{
1143 find interpretation(problem,interpretation);
1144 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1145 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"FinalState class");
1146 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1147 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
1148 find mustInstanceOfRegion_class(problem,interpretation,container);
1149 find mayInstanceOfFinalState_class(problem,interpretation,newObject);
1150 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
1151 find mustExist(problem, interpretation, container);
1152 neg find mustExist(problem, interpretation, newObject);
1153}
1154pattern createObject_FinalState_class(
1155 problem:LogicProblem, interpretation:PartialInterpretation,
1156 typeInterpretation:PartialComplexTypeInterpretation)
1157{
1158 find interpretation(problem,interpretation);
1159 neg find hasElementInContainment(problem,interpretation);
1160 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1161 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"FinalState class");
1162 find mayInstanceOfFinalState_class(problem,interpretation,newObject);
1163 find mayExist(problem, interpretation, newObject);
1164 neg find mustExist(problem, interpretation, newObject);
1165}
1166pattern createObject_Transition_class_by_outgoingTransitions_reference_Vertex_with_source_reference_Transition(
1167 problem:LogicProblem, interpretation:PartialInterpretation,
1168 relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1169 container:DefinedElement)
1170{
1171 find interpretation(problem,interpretation);
1172 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1173 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Transition class");
1174 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1175 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"outgoingTransitions reference Vertex");
1176 PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation);
1177 PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"source reference Transition");
1178 find mustInstanceOfVertex_class(problem,interpretation,container);
1179 find mayInstanceOfTransition_class(problem,interpretation,newObject);
1180 find mayInRelationoutgoingTransitions_reference_Vertex(problem,interpretation,container,newObject);
1181 find mustExist(problem, interpretation, container);
1182 neg find mustExist(problem, interpretation, newObject);
1183}
1184pattern createObject_Transition_class(
1185 problem:LogicProblem, interpretation:PartialInterpretation,
1186 typeInterpretation:PartialComplexTypeInterpretation)
1187{
1188 find interpretation(problem,interpretation);
1189 neg find hasElementInContainment(problem,interpretation);
1190 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1191 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Transition class");
1192 find mayInstanceOfTransition_class(problem,interpretation,newObject);
1193 find mayExist(problem, interpretation, newObject);
1194 neg find mustExist(problem, interpretation, newObject);
1195}
1196pattern createObject_Region_class_by_regions_reference_CompositeElement(
1197 problem:LogicProblem, interpretation:PartialInterpretation,
1198 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1199 container:DefinedElement)
1200{
1201 find interpretation(problem,interpretation);
1202 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1203 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Region class");
1204 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1205 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"regions reference CompositeElement");
1206 find mustInstanceOfCompositeElement_class(problem,interpretation,container);
1207 find mayInstanceOfRegion_class(problem,interpretation,newObject);
1208 find mayInRelationregions_reference_CompositeElement(problem,interpretation,container,newObject);
1209 find mustExist(problem, interpretation, container);
1210 neg find mustExist(problem, interpretation, newObject);
1211}
1212pattern createObject_Region_class(
1213 problem:LogicProblem, interpretation:PartialInterpretation,
1214 typeInterpretation:PartialComplexTypeInterpretation)
1215{
1216 find interpretation(problem,interpretation);
1217 neg find hasElementInContainment(problem,interpretation);
1218 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1219 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Region class");
1220 find mayInstanceOfRegion_class(problem,interpretation,newObject);
1221 find mayExist(problem, interpretation, newObject);
1222 neg find mustExist(problem, interpretation, newObject);
1223}
1224pattern createObject_Choice_class_by_vertices_reference_Region(
1225 problem:LogicProblem, interpretation:PartialInterpretation,
1226 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1227 container:DefinedElement)
1228{
1229 find interpretation(problem,interpretation);
1230 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1231 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Choice class");
1232 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1233 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
1234 find mustInstanceOfRegion_class(problem,interpretation,container);
1235 find mayInstanceOfChoice_class(problem,interpretation,newObject);
1236 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
1237 find mustExist(problem, interpretation, container);
1238 neg find mustExist(problem, interpretation, newObject);
1239}
1240pattern createObject_Choice_class(
1241 problem:LogicProblem, interpretation:PartialInterpretation,
1242 typeInterpretation:PartialComplexTypeInterpretation)
1243{
1244 find interpretation(problem,interpretation);
1245 neg find hasElementInContainment(problem,interpretation);
1246 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1247 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Choice class");
1248 find mayInstanceOfChoice_class(problem,interpretation,newObject);
1249 find mayExist(problem, interpretation, newObject);
1250 neg find mustExist(problem, interpretation, newObject);
1251}
1252pattern createObject_Synchronization_class_by_vertices_reference_Region(
1253 problem:LogicProblem, interpretation:PartialInterpretation,
1254 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1255 container:DefinedElement)
1256{
1257 find interpretation(problem,interpretation);
1258 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1259 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Synchronization class");
1260 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1261 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
1262 find mustInstanceOfRegion_class(problem,interpretation,container);
1263 find mayInstanceOfSynchronization_class(problem,interpretation,newObject);
1264 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
1265 find mustExist(problem, interpretation, container);
1266 neg find mustExist(problem, interpretation, newObject);
1267}
1268pattern createObject_Synchronization_class(
1269 problem:LogicProblem, interpretation:PartialInterpretation,
1270 typeInterpretation:PartialComplexTypeInterpretation)
1271{
1272 find interpretation(problem,interpretation);
1273 neg find hasElementInContainment(problem,interpretation);
1274 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1275 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Synchronization class");
1276 find mayInstanceOfSynchronization_class(problem,interpretation,newObject);
1277 find mayExist(problem, interpretation, newObject);
1278 neg find mustExist(problem, interpretation, newObject);
1279}
1280pattern createObject_Statechart_class_UndefinedPart(
1281 problem:LogicProblem, interpretation:PartialInterpretation,
1282 typeInterpretation:PartialComplexTypeInterpretation)
1283{
1284 find interpretation(problem,interpretation);
1285 neg find hasElementInContainment(problem,interpretation);
1286 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1287 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Statechart class UndefinedPart");
1288 find mayInstanceOfStatechart_class_UndefinedPart(problem,interpretation,newObject);
1289 find mayExist(problem, interpretation, newObject);
1290 neg find mustExist(problem, interpretation, newObject);
1291}
1292pattern createObject_Entry_class_by_vertices_reference_Region(
1293 problem:LogicProblem, interpretation:PartialInterpretation,
1294 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1295 container:DefinedElement)
1296{
1297 find interpretation(problem,interpretation);
1298 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1299 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Entry class");
1300 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1301 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
1302 find mustInstanceOfRegion_class(problem,interpretation,container);
1303 find mayInstanceOfEntry_class(problem,interpretation,newObject);
1304 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
1305 find mustExist(problem, interpretation, container);
1306 neg find mustExist(problem, interpretation, newObject);
1307}
1308pattern createObject_Entry_class(
1309 problem:LogicProblem, interpretation:PartialInterpretation,
1310 typeInterpretation:PartialComplexTypeInterpretation)
1311{
1312 find interpretation(problem,interpretation);
1313 neg find hasElementInContainment(problem,interpretation);
1314 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1315 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"Entry class");
1316 find mayInstanceOfEntry_class(problem,interpretation,newObject);
1317 find mayExist(problem, interpretation, newObject);
1318 neg find mustExist(problem, interpretation, newObject);
1319}
1320pattern createObject_State_class_by_vertices_reference_Region(
1321 problem:LogicProblem, interpretation:PartialInterpretation,
1322 relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation,
1323 container:DefinedElement)
1324{
1325 find interpretation(problem,interpretation);
1326 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1327 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"State class");
1328 PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation);
1329 PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"vertices reference Region");
1330 find mustInstanceOfRegion_class(problem,interpretation,container);
1331 find mayInstanceOfState_class(problem,interpretation,newObject);
1332 find mayInRelationvertices_reference_Region(problem,interpretation,container,newObject);
1333 find mustExist(problem, interpretation, container);
1334 neg find mustExist(problem, interpretation, newObject);
1335}
1336pattern createObject_State_class(
1337 problem:LogicProblem, interpretation:PartialInterpretation,
1338 typeInterpretation:PartialComplexTypeInterpretation)
1339{
1340 find interpretation(problem,interpretation);
1341 neg find hasElementInContainment(problem,interpretation);
1342 PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);
1343 PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"State class");
1344 find mayInstanceOfState_class(problem,interpretation,newObject);
1345 find mayExist(problem, interpretation, newObject);
1346 neg find mustExist(problem, interpretation, newObject);
1347}
1348
1349//////////
1350// 4.2 Type refinement
1351//////////
1352pattern refineTypeTo_Exit_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1353 find interpretation(problem,interpretation);
1354 PartialInterpretation.newElements(interpretation,element);
1355 find mayInstanceOfExit_class(problem,interpretation,element);
1356 neg find mustInstanceOfExit_class(problem,interpretation,element);
1357 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
1358 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1359 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1360 neg find mustInstanceOfChoice_class(problem,interpretation,element);
1361 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
1362 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
1363 neg find mustInstanceOfEntry_class(problem,interpretation,element);
1364}
1365pattern refineTypeTo_FinalState_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1366 find interpretation(problem,interpretation);
1367 PartialInterpretation.newElements(interpretation,element);
1368 find mayInstanceOfFinalState_class(problem,interpretation,element);
1369 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
1370 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1371 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1372 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
1373 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
1374}
1375pattern refineTypeTo_Transition_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1376 find interpretation(problem,interpretation);
1377 PartialInterpretation.newElements(interpretation,element);
1378 find mayInstanceOfTransition_class(problem,interpretation,element);
1379 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1380 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1381 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
1382 neg find mustInstanceOfVertex_class(problem,interpretation,element);
1383}
1384pattern refineTypeTo_Region_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1385 find interpretation(problem,interpretation);
1386 PartialInterpretation.newElements(interpretation,element);
1387 find mayInstanceOfRegion_class(problem,interpretation,element);
1388 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1389 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1390 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
1391 neg find mustInstanceOfVertex_class(problem,interpretation,element);
1392}
1393pattern refineTypeTo_Choice_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1394 find interpretation(problem,interpretation);
1395 PartialInterpretation.newElements(interpretation,element);
1396 find mayInstanceOfChoice_class(problem,interpretation,element);
1397 neg find mustInstanceOfExit_class(problem,interpretation,element);
1398 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
1399 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1400 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1401 neg find mustInstanceOfChoice_class(problem,interpretation,element);
1402 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
1403 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
1404 neg find mustInstanceOfEntry_class(problem,interpretation,element);
1405}
1406pattern refineTypeTo_Synchronization_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1407 find interpretation(problem,interpretation);
1408 PartialInterpretation.newElements(interpretation,element);
1409 find mayInstanceOfSynchronization_class(problem,interpretation,element);
1410 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
1411 neg find mustInstanceOfExit_class(problem,interpretation,element);
1412 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1413 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1414 neg find mustInstanceOfChoice_class(problem,interpretation,element);
1415 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
1416 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
1417 neg find mustInstanceOfEntry_class(problem,interpretation,element);
1418}
1419pattern refineTypeTo_Statechart_class_UndefinedPart(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1420 find interpretation(problem,interpretation);
1421 PartialInterpretation.newElements(interpretation,element);
1422 find mayInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element);
1423 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1424 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1425 neg find mustInstanceOfStatechart_class_UndefinedPart(problem,interpretation,element);
1426 neg find mustInstanceOfVertex_class(problem,interpretation,element);
1427}
1428pattern refineTypeTo_Entry_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1429 find interpretation(problem,interpretation);
1430 PartialInterpretation.newElements(interpretation,element);
1431 find mayInstanceOfEntry_class(problem,interpretation,element);
1432 neg find mustInstanceOfExit_class(problem,interpretation,element);
1433 neg find mustInstanceOfRegularState_class(problem,interpretation,element);
1434 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1435 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1436 neg find mustInstanceOfChoice_class(problem,interpretation,element);
1437 neg find mustInstanceOfSynchronization_class(problem,interpretation,element);
1438 neg find mustInstanceOfCompositeElement_class(problem,interpretation,element);
1439 neg find mustInstanceOfEntry_class(problem,interpretation,element);
1440}
1441pattern refineTypeTo_State_class(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) {
1442 find interpretation(problem,interpretation);
1443 PartialInterpretation.newElements(interpretation,element);
1444 find mayInstanceOfState_class(problem,interpretation,element);
1445 neg find mustInstanceOfFinalState_class(problem,interpretation,element);
1446 neg find mustInstanceOfRegion_class(problem,interpretation,element);
1447 neg find mustInstanceOfTransition_class(problem,interpretation,element);
1448 neg find mustInstanceOfPseudostate_class(problem,interpretation,element);
1449 neg find mustInstanceOfStatechart_class(problem,interpretation,element);
1450 neg find mustInstanceOfState_class(problem,interpretation,element);
1451}
1452
1453//////////
1454// 4.3 Relation refinement
1455//////////
1456pattern refineRelation_incomingTransitions_reference_Vertex_and_target_reference_Transition(
1457 problem:LogicProblem, interpretation:PartialInterpretation,
1458 relationIterpretation:PartialRelationInterpretation, oppositeInterpretation:PartialRelationInterpretation,
1459 from: DefinedElement, to: DefinedElement)
1460{
1461 find interpretation(problem,interpretation);
1462 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
1463 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"incomingTransitions reference Vertex");
1464 PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation);
1465 PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"target reference Transition");
1466 find mustExist(problem, interpretation, from);
1467 find mustExist(problem, interpretation, to);
1468 find mustInstanceOfVertex_class(problem,interpretation,from);
1469 find mustInstanceOfTransition_class(problem,interpretation,to);
1470 find mayInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
1471 neg find mustInRelationincomingTransitions_reference_Vertex(problem,interpretation,from,to);
1472}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 07:19:21 +0000