diff options
Diffstat (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu')
2 files changed, 42 insertions, 292 deletions
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/mutated/mutated.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/mutated/mutated.vql deleted file mode 100644 index 58f66fe2..00000000 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/mutated/mutated.vql +++ /dev/null | |||
@@ -1,270 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated | ||
2 | |||
3 | import epackage "hu.bme.mit.inf.yakindumm" | ||
4 | |||
5 | ///////// | ||
6 | // Entry | ||
7 | ///////// | ||
8 | |||
9 | pattern entryInRegion_M0(r1 : Region, e1 : Entry) { | ||
10 | Region.vertices(r1, e1); | ||
11 | } | ||
12 | pattern entryInRegion_M1(r1 : Region, e1) { | ||
13 | Region.vertices(r1, e1); | ||
14 | } | ||
15 | pattern entryInRegion_M2(r1 : Region, e1: Entry) { | ||
16 | // For positive constraint | ||
17 | Region(r1);Entry(e1); | ||
18 | } | ||
19 | |||
20 | |||
21 | //@Constraint(severity="error", message="error", key = {r1}) | ||
22 | pattern noEntryInRegion_M0(r1 : Region) { | ||
23 | neg find entryInRegion_M0(r1, _); | ||
24 | } | ||
25 | pattern noEntryInRegion_M1(r1 : Region) { | ||
26 | neg find entryInRegion_M1(r1, _); | ||
27 | } | ||
28 | pattern noEntryInRegion_M2(r1 : Region) { | ||
29 | neg find entryInRegion_M2(r1, _); | ||
30 | } | ||
31 | pattern noEntryInRegion_M3(r1 : Region) { | ||
32 | find entryInRegion_M0(r1, _); | ||
33 | } | ||
34 | pattern noEntryInRegion_M4(r1 : Region) { | ||
35 | find entryInRegion_M1(r1, _); | ||
36 | } | ||
37 | pattern noEntryInRegion_M5(r1 : Region) { | ||
38 | find entryInRegion_M2(r1, _); | ||
39 | } | ||
40 | |||
41 | //@Constraint(severity="error", message="error", key = {r}) | ||
42 | pattern multipleEntryInRegion_M0(r : Region) { | ||
43 | find entryInRegion_M0(r, e1); | ||
44 | find entryInRegion_M0(r, e2); | ||
45 | e1 != e2; | ||
46 | } | ||
47 | pattern multipleEntryInRegion_M1(r : Region) { | ||
48 | find entryInRegion_M1(r, e1); | ||
49 | find entryInRegion_M0(r, e2); | ||
50 | e1 != e2; | ||
51 | } | ||
52 | pattern multipleEntryInRegion_M2(r : Region) { | ||
53 | find entryInRegion_M2(r, e1); | ||
54 | find entryInRegion_M0(r, e2); | ||
55 | e1 != e2; | ||
56 | } | ||
57 | pattern multipleEntryInRegion_M3(r : Region) { | ||
58 | find entryInRegion_M0(r, e1); | ||
59 | find entryInRegion_M1(r, e2); | ||
60 | e1 != e2; | ||
61 | } | ||
62 | pattern multipleEntryInRegion_M4(r : Region) { | ||
63 | find entryInRegion_M2(r, e1); | ||
64 | find entryInRegion_M2(r, e2); | ||
65 | e1 != e2; | ||
66 | } | ||
67 | pattern multipleEntryInRegion_M5(r : Region) { | ||
68 | find entryInRegion_M0(r, e1); | ||
69 | find entryInRegion_M0(r, e2); | ||
70 | } | ||
71 | |||
72 | |||
73 | pattern transition_M0(t : Transition, src : Vertex, trg : Vertex) { | ||
74 | Transition.source(t, src); | ||
75 | Transition.target(t, trg); | ||
76 | } | ||
77 | pattern transition_M1(t : Transition, src : Vertex, trg : Vertex) { | ||
78 | Transition.source(t, src); | ||
79 | Vertex(trg); | ||
80 | } | ||
81 | pattern transition_M2(t : Transition, src : Vertex, trg : Vertex) { | ||
82 | Vertex(src); | ||
83 | Transition.target(t, trg); | ||
84 | } | ||
85 | pattern transition_M3(t : Transition, src : Vertex, trg : Vertex) { | ||
86 | Transition.source(t_x, src); | ||
87 | Transition.target(t, trg); | ||
88 | } | ||
89 | pattern transition_M4(t : Transition, src : Vertex, trg : Vertex) { | ||
90 | Transition.source(t, src); | ||
91 | Transition.target(t_x, trg); | ||
92 | } | ||
93 | |||
94 | //@Constraint(severity="error", message="error", key = {e}) | ||
95 | pattern incomingToEntry_M0(t : Transition, e : Entry) { | ||
96 | find transition_M0(t, _, e); | ||
97 | } | ||
98 | pattern incomingToEntry_1(t : Transition, e) { | ||
99 | find transition_M0(t, _, e); | ||
100 | } | ||
101 | pattern incomingToEntry_2(t : Transition, e : Entry) { | ||
102 | find transition_M1(t, _, e); | ||
103 | } | ||
104 | pattern incomingToEntry_3(t : Transition, e : Entry) { | ||
105 | find transition_M2(t, _, e); | ||
106 | } | ||
107 | pattern incomingToEntry_4(t : Transition, e : Entry) { | ||
108 | find transition_M3(t, _, e); | ||
109 | } | ||
110 | pattern incomingToEntry_5(t : Transition, e : Entry) { | ||
111 | find transition_M4(t, _, e); | ||
112 | } | ||
113 | |||
114 | pattern noOutgoingTransitionFromEntry_M0(e : Entry) { | ||
115 | neg find transition_M0(_, e, _); | ||
116 | } | ||
117 | |||
118 | pattern noOutgoingTransitionFromEntry_M1(e) { | ||
119 | Vertex(e); | ||
120 | neg find transition_M0(_, e, _); | ||
121 | } | ||
122 | pattern noOutgoingTransitionFromEntry_M2(e : Entry) { | ||
123 | neg find transition_M1(_, e, _); | ||
124 | } | ||
125 | pattern noOutgoingTransitionFromEntry_M3(e : Entry) { | ||
126 | neg find transition_M2(_, e, _); | ||
127 | } | ||
128 | pattern noOutgoingTransitionFromEntry_M4(e : Entry) { | ||
129 | neg find transition_M3(_, e, _); | ||
130 | } | ||
131 | pattern noOutgoingTransitionFromEntry_M5(e : Entry) { | ||
132 | neg find transition_M4(_, e, _); | ||
133 | } | ||
134 | |||
135 | |||
136 | //@Constraint(severity="error", message="error", key = {e}) | ||
137 | pattern multipleTransitionFromEntry_M0(e : Entry, t1 : Transition, t2: Transition) { | ||
138 | Entry.outgoingTransitions(e,t1); | ||
139 | Entry.outgoingTransitions(e,t2); | ||
140 | t1!=t2; | ||
141 | } | ||
142 | pattern multipleTransitionFromEntry_M1(e, t1 : Transition, t2: Transition) { | ||
143 | Entry.outgoingTransitions(e,t1); | ||
144 | Entry.outgoingTransitions(e,t2); | ||
145 | t1!=t2; | ||
146 | } | ||
147 | pattern multipleTransitionFromEntry_M2(e : Entry, t1 : Transition, t2: Transition) { | ||
148 | Transition(t1); | ||
149 | Entry.outgoingTransitions(e,t2); | ||
150 | t1!=t2; | ||
151 | } | ||
152 | pattern multipleTransitionFromEntry_M3(e : Entry, t1 : Transition, t2: Transition) { | ||
153 | Entry.outgoingTransitions(e,t1); | ||
154 | Transition(t2); | ||
155 | t1!=t2; | ||
156 | } | ||
157 | pattern multipleTransitionFromEntry_M4(e : Entry, t1 : Transition, t2: Transition) { | ||
158 | Entry.outgoingTransitions(e,t1); | ||
159 | Entry.outgoingTransitions(e,t2); | ||
160 | } | ||
161 | |||
162 | ///////// | ||
163 | // Exit | ||
164 | ///////// | ||
165 | |||
166 | //@Constraint(severity="error", message="error", key = {e}) | ||
167 | pattern outgoingFromExit_M0(t : Transition, e : Exit) { | ||
168 | Exit.outgoingTransitions(e,t); | ||
169 | } | ||
170 | pattern outgoingFromExit_M1(t : Transition, e) { | ||
171 | Vertex.outgoingTransitions(e,t); | ||
172 | } | ||
173 | pattern outgoingFromExit_M2(t : Transition, e : Exit) { | ||
174 | Transition(t); | ||
175 | Exit(e); | ||
176 | } | ||
177 | |||
178 | ///////// | ||
179 | // Final | ||
180 | ///////// | ||
181 | |||
182 | //@Constraint(severity="error", message="error", key = {f}) | ||
183 | pattern outgoingFromFinal_M0(t : Transition, f : FinalState) { | ||
184 | FinalState.outgoingTransitions(f,t); | ||
185 | } | ||
186 | pattern outgoingFromFinal_M1(t : Transition, f) { | ||
187 | Vertex.outgoingTransitions(f,t); | ||
188 | } | ||
189 | pattern outgoingFromFinal_M2(t : Transition, f : FinalState) { | ||
190 | Transition(t); | ||
191 | FinalState(f); | ||
192 | } | ||
193 | |||
194 | ///////// | ||
195 | // State vs Region | ||
196 | ///////// | ||
197 | |||
198 | //@Constraint(severity="error", message="error", key = {region}) | ||
199 | pattern noStateInRegion_M0(region: Region) { | ||
200 | neg find StateInRegion_M0(region,_); | ||
201 | } | ||
202 | pattern noStateInRegion_M1(region: Region) { | ||
203 | neg find StateInRegion_M1(region,_); | ||
204 | } | ||
205 | pattern noStateInRegion_M2(region: Region) { | ||
206 | neg find StateInRegion_M2(region,_); | ||
207 | } | ||
208 | pattern noStateInRegion_M3(region: Region) { | ||
209 | find StateInRegion_M0(region,_); | ||
210 | } | ||
211 | |||
212 | pattern StateInRegion_M0(region: Region, state: State) { | ||
213 | Region.vertices(region,state); | ||
214 | } | ||
215 | pattern StateInRegion_M1(region: Region, state) { | ||
216 | Region.vertices(region,state); | ||
217 | } | ||
218 | pattern StateInRegion_M2(region: Region, state:State) { | ||
219 | Region(region);State(state); | ||
220 | } | ||
221 | |||
222 | ///////// | ||
223 | // Choice | ||
224 | ///////// | ||
225 | |||
226 | @Constraint(severity="error", message="error", key = {c}) | ||
227 | pattern choiceHasNoOutgoing_M0(c : Choice) { | ||
228 | neg find transition_M0(_, c, _); | ||
229 | } | ||
230 | pattern choiceHasNoOutgoing_M1(c:Vertex) { | ||
231 | neg find transition_M0(_, c, _); | ||
232 | } | ||
233 | pattern choiceHasNoOutgoing_M2(c : Choice) { | ||
234 | neg find transition_M1(_, c, _); | ||
235 | } | ||
236 | pattern choiceHasNoOutgoing_M3(c : Choice) { | ||
237 | neg find transition_M2(_, c, _); | ||
238 | } | ||
239 | pattern choiceHasNoOutgoing_M4(c : Choice) { | ||
240 | neg find transition_M3(_, c, _); | ||
241 | } | ||
242 | pattern choiceHasNoOutgoing_M5(c : Choice) { | ||
243 | neg find transition_M4(_, c, _); | ||
244 | } | ||
245 | pattern choiceHasNoOutgoing_M6(c : Choice) { | ||
246 | find transition_M0(_, c, _); | ||
247 | } | ||
248 | |||
249 | @Constraint(severity="error", message="error", key = {c}) | ||
250 | pattern choiceHasNoIncoming_M0(c: Choice) { | ||
251 | neg find transition_M0(_, _, c); | ||
252 | } | ||
253 | pattern choiceHasNoIncoming_M1(c:Vertex) { | ||
254 | neg find transition_M0(_, _, c); | ||
255 | } | ||
256 | pattern choiceHasNoIncoming_M2(c: Choice) { | ||
257 | neg find transition_M1(_, _, c); | ||
258 | } | ||
259 | pattern choiceHasNoIncoming_M3(c: Choice) { | ||
260 | neg find transition_M2(_, _, c); | ||
261 | } | ||
262 | pattern choiceHasNoIncoming_M4(c: Choice) { | ||
263 | neg find transition_M3(_, _, c); | ||
264 | } | ||
265 | pattern choiceHasNoIncoming_M5(c: Choice) { | ||
266 | neg find transition_M4(_, _, c); | ||
267 | } | ||
268 | pattern choiceHasNoIncoming_M6(c: Choice) { | ||
269 | find transition_M0(_, _, c); | ||
270 | } | ||
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql index f4bfa3c1..98a10cde 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql | |||
@@ -27,14 +27,22 @@ pattern transition(t : Transition, src : Vertex, trg : Vertex) { | |||
27 | Transition.target(t, trg); | 27 | Transition.target(t, trg); |
28 | } | 28 | } |
29 | 29 | ||
30 | pattern transitionFrom(t : Transition, src : Vertex) { | ||
31 | Transition.source(t, src); | ||
32 | } | ||
33 | |||
34 | pattern transitionTo(t : Transition, trg : Vertex) { | ||
35 | Transition.target(t, trg); | ||
36 | } | ||
37 | |||
30 | @Constraint(severity="error", message="error", key = {e}) | 38 | @Constraint(severity="error", message="error", key = {e}) |
31 | pattern incomingToEntry(t : Transition, e : Entry) { | 39 | pattern incomingToEntry(t : Transition, e : Entry) { |
32 | find transition(t, _, e); | 40 | find transitionTo(t, e); |
33 | } | 41 | } |
34 | 42 | ||
35 | @Constraint(severity="error", message="error", key = {e}) | 43 | @Constraint(severity="error", message="error", key = {e}) |
36 | pattern noOutgoingTransitionFromEntry(e : Entry) { | 44 | pattern noOutgoingTransitionFromEntry(e : Entry) { |
37 | neg find transition(_, e, _); | 45 | neg find transitionFrom(_, e); |
38 | } | 46 | } |
39 | 47 | ||
40 | @Constraint(severity="error", message="error", key = {e}) | 48 | @Constraint(severity="error", message="error", key = {e}) |
@@ -80,12 +88,12 @@ pattern StateInRegion(region: Region, state: State) { | |||
80 | 88 | ||
81 | @Constraint(severity="error", message="error", key = {c}) | 89 | @Constraint(severity="error", message="error", key = {c}) |
82 | pattern choiceHasNoOutgoing(c : Choice) { | 90 | pattern choiceHasNoOutgoing(c : Choice) { |
83 | neg find transition(_, c, _); | 91 | neg find transitionFrom(_, c); |
84 | } | 92 | } |
85 | 93 | ||
86 | @Constraint(severity="error", message="error", key = {c}) | 94 | @Constraint(severity="error", message="error", key = {c}) |
87 | pattern choiceHasNoIncoming(c: Choice) { | 95 | pattern choiceHasNoIncoming(c: Choice) { |
88 | neg find transition(_, _, c); | 96 | neg find transitionTo(_, c); |
89 | } | 97 | } |
90 | 98 | ||
91 | ///////// | 99 | ///////// |
@@ -94,27 +102,33 @@ pattern choiceHasNoIncoming(c: Choice) { | |||
94 | 102 | ||
95 | @Constraint(severity="error", message="error", key = {s}) | 103 | @Constraint(severity="error", message="error", key = {s}) |
96 | pattern synchHasNoOutgoing(s : Synchronization) { | 104 | pattern synchHasNoOutgoing(s : Synchronization) { |
97 | neg find transition(_, s, _); | 105 | neg find transitionFrom(_, s); |
98 | } | 106 | } |
99 | 107 | ||
100 | @Constraint(severity="error", message="error", key = {s}) | 108 | @Constraint(severity="error", message="error", key = {s}) |
101 | pattern synchHasNoIncoming(s : Synchronization) { | 109 | pattern synchHasNoIncoming(s : Synchronization) { |
102 | neg find transition(_, _, s); | 110 | neg find transitionTo(_, s); |
103 | } | 111 | } |
104 | 112 | ||
105 | @Constraint(severity="error", message="error", key = {s}) | 113 | @Constraint(severity="error", message="error", key = {s}) |
106 | pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 114 | pattern SynchronizedIncomingInSameRegion(s : Synchronization, t1 : Transition, t2 : Transition) { |
107 | find transition(t1, v1, s); | 115 | find SynchronizedIncomingInSameRegionHelper1(r, s, t1); |
108 | find transition(t2, v2, s); | 116 | find SynchronizedIncomingInSameRegionHelper1(r, s, t2); |
109 | t1!=t2; | 117 | t1!=t2; |
110 | Region.vertices(r, v1); | ||
111 | Region.vertices(r, v2); | ||
112 | } or { | 118 | } or { |
113 | find transition(t1, s, v1); | 119 | find SynchronizedIncomingInSameRegionHelper2(r, s, t1); |
114 | find transition(t2, s, v2); | 120 | find SynchronizedIncomingInSameRegionHelper2(r, s, t2); |
115 | t1!=t2; | 121 | t1!=t2; |
122 | } | ||
123 | |||
124 | pattern SynchronizedIncomingInSameRegionHelper1(r : Region, s : Synchronization, t1 : Transition) { | ||
125 | find transition(t1, v1, s); | ||
126 | Region.vertices(r, v1); | ||
127 | } | ||
128 | |||
129 | pattern SynchronizedIncomingInSameRegionHelper2(r : Region, s : Synchronization, t1 : Transition) { | ||
130 | find transition(t1, s, v1); | ||
116 | Region.vertices(r, v1); | 131 | Region.vertices(r, v1); |
117 | Region.vertices(r, v2); | ||
118 | } | 132 | } |
119 | 133 | ||
120 | @Constraint(severity="error", message="error", key = {s}) | 134 | @Constraint(severity="error", message="error", key = {s}) |
@@ -136,18 +150,24 @@ pattern hasMultipleIncomingTrainsition(v : Synchronization) { | |||
136 | } | 150 | } |
137 | 151 | ||
138 | @Constraint(severity="error", message="error", key = {s}) | 152 | @Constraint(severity="error", message="error", key = {s}) |
139 | pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 153 | pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, r1 : CompositeElement, r2 : CompositeElement) { |
140 | find transition(_, v1, s); | 154 | find SynchronizedRegionsAreNotSiblingsHelper1(s, r1); |
141 | find transition(_, v2, s); | 155 | find SynchronizedRegionsAreNotSiblingsHelper1(s, r2); |
142 | CompositeElement.regions.vertices(r1, v1); | ||
143 | CompositeElement.regions.vertices(r2, v2); | ||
144 | r1 != r2; | 156 | r1 != r2; |
145 | } or { | 157 | } or { |
158 | find SynchronizedRegionsAreNotSiblingsHelper2(s, r1); | ||
159 | find SynchronizedRegionsAreNotSiblingsHelper2(s, r2); | ||
160 | r1 != r2; | ||
161 | } | ||
162 | |||
163 | pattern SynchronizedRegionsAreNotSiblingsHelper1(s : Synchronization, r1 : CompositeElement) { | ||
146 | find transition(_, s, v1); | 164 | find transition(_, s, v1); |
147 | find transition(_, s, v2); | ||
148 | CompositeElement.regions.vertices(r1, v1); | 165 | CompositeElement.regions.vertices(r1, v1); |
149 | CompositeElement.regions.vertices(r2, v2); | 166 | } |
150 | r1 != r2; | 167 | |
168 | pattern SynchronizedRegionsAreNotSiblingsHelper2(s : Synchronization, r1 : CompositeElement) { | ||
169 | find transition(_, v1, s); | ||
170 | CompositeElement.regions.vertices(r1, v1); | ||
151 | } | 171 | } |
152 | 172 | ||
153 | /////////////////////////////// | 173 | /////////////////////////////// |