diff options
Diffstat (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries')
2 files changed, 53 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..49fb5b2f 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 | |||
@@ -22,19 +22,33 @@ pattern multipleEntryInRegion(r : Region) { | |||
22 | e1 != e2; | 22 | e1 != e2; |
23 | } | 23 | } |
24 | 24 | ||
25 | @Constraint(severity="error", message="error", key = {sct}) | ||
26 | pattern unsat_multipleEntryInRegion(sct : Statechart) { | ||
27 | Statechart(sct); | ||
28 | neg find multipleEntryInRegion(_); | ||
29 | } | ||
30 | |||
25 | pattern transition(t : Transition, src : Vertex, trg : Vertex) { | 31 | pattern transition(t : Transition, src : Vertex, trg : Vertex) { |
26 | Transition.source(t, src); | 32 | Transition.source(t, src); |
27 | Transition.target(t, trg); | 33 | Transition.target(t, trg); |
28 | } | 34 | } |
29 | 35 | ||
36 | pattern transitionFrom(t : Transition, src : Vertex) { | ||
37 | Transition.source(t, src); | ||
38 | } | ||
39 | |||
40 | pattern transitionTo(t : Transition, trg : Vertex) { | ||
41 | Transition.target(t, trg); | ||
42 | } | ||
43 | |||
30 | @Constraint(severity="error", message="error", key = {e}) | 44 | @Constraint(severity="error", message="error", key = {e}) |
31 | pattern incomingToEntry(t : Transition, e : Entry) { | 45 | pattern incomingToEntry(t : Transition, e : Entry) { |
32 | find transition(t, _, e); | 46 | find transitionTo(t, e); |
33 | } | 47 | } |
34 | 48 | ||
35 | @Constraint(severity="error", message="error", key = {e}) | 49 | @Constraint(severity="error", message="error", key = {e}) |
36 | pattern noOutgoingTransitionFromEntry(e : Entry) { | 50 | pattern noOutgoingTransitionFromEntry(e : Entry) { |
37 | neg find transition(_, e, _); | 51 | neg find transitionFrom(_, e); |
38 | } | 52 | } |
39 | 53 | ||
40 | @Constraint(severity="error", message="error", key = {e}) | 54 | @Constraint(severity="error", message="error", key = {e}) |
@@ -80,12 +94,12 @@ pattern StateInRegion(region: Region, state: State) { | |||
80 | 94 | ||
81 | @Constraint(severity="error", message="error", key = {c}) | 95 | @Constraint(severity="error", message="error", key = {c}) |
82 | pattern choiceHasNoOutgoing(c : Choice) { | 96 | pattern choiceHasNoOutgoing(c : Choice) { |
83 | neg find transition(_, c, _); | 97 | neg find transitionFrom(_, c); |
84 | } | 98 | } |
85 | 99 | ||
86 | @Constraint(severity="error", message="error", key = {c}) | 100 | @Constraint(severity="error", message="error", key = {c}) |
87 | pattern choiceHasNoIncoming(c: Choice) { | 101 | pattern choiceHasNoIncoming(c: Choice) { |
88 | neg find transition(_, _, c); | 102 | neg find transitionTo(_, c); |
89 | } | 103 | } |
90 | 104 | ||
91 | ///////// | 105 | ///////// |
@@ -94,27 +108,33 @@ pattern choiceHasNoIncoming(c: Choice) { | |||
94 | 108 | ||
95 | @Constraint(severity="error", message="error", key = {s}) | 109 | @Constraint(severity="error", message="error", key = {s}) |
96 | pattern synchHasNoOutgoing(s : Synchronization) { | 110 | pattern synchHasNoOutgoing(s : Synchronization) { |
97 | neg find transition(_, s, _); | 111 | neg find transitionFrom(_, s); |
98 | } | 112 | } |
99 | 113 | ||
100 | @Constraint(severity="error", message="error", key = {s}) | 114 | @Constraint(severity="error", message="error", key = {s}) |
101 | pattern synchHasNoIncoming(s : Synchronization) { | 115 | pattern synchHasNoIncoming(s : Synchronization) { |
102 | neg find transition(_, _, s); | 116 | neg find transitionTo(_, s); |
103 | } | 117 | } |
104 | 118 | ||
105 | @Constraint(severity="error", message="error", key = {s}) | 119 | @Constraint(severity="error", message="error", key = {s}) |
106 | pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 120 | pattern SynchronizedIncomingInSameRegion(s : Synchronization, t1 : Transition, t2 : Transition) { |
107 | find transition(t1, v1, s); | 121 | find SynchronizedIncomingInSameRegionHelper1(r, s, t1); |
108 | find transition(t2, v2, s); | 122 | find SynchronizedIncomingInSameRegionHelper1(r, s, t2); |
109 | t1!=t2; | 123 | t1!=t2; |
110 | Region.vertices(r, v1); | ||
111 | Region.vertices(r, v2); | ||
112 | } or { | 124 | } or { |
113 | find transition(t1, s, v1); | 125 | find SynchronizedIncomingInSameRegionHelper2(r, s, t1); |
114 | find transition(t2, s, v2); | 126 | find SynchronizedIncomingInSameRegionHelper2(r, s, t2); |
115 | t1!=t2; | 127 | t1!=t2; |
128 | } | ||
129 | |||
130 | pattern SynchronizedIncomingInSameRegionHelper1(r : Region, s : Synchronization, t1 : Transition) { | ||
131 | find transition(t1, v1, s); | ||
132 | Region.vertices(r, v1); | ||
133 | } | ||
134 | |||
135 | pattern SynchronizedIncomingInSameRegionHelper2(r : Region, s : Synchronization, t1 : Transition) { | ||
136 | find transition(t1, s, v1); | ||
116 | Region.vertices(r, v1); | 137 | Region.vertices(r, v1); |
117 | Region.vertices(r, v2); | ||
118 | } | 138 | } |
119 | 139 | ||
120 | @Constraint(severity="error", message="error", key = {s}) | 140 | @Constraint(severity="error", message="error", key = {s}) |
@@ -136,18 +156,24 @@ pattern hasMultipleIncomingTrainsition(v : Synchronization) { | |||
136 | } | 156 | } |
137 | 157 | ||
138 | @Constraint(severity="error", message="error", key = {s}) | 158 | @Constraint(severity="error", message="error", key = {s}) |
139 | pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 159 | pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, r1 : CompositeElement, r2 : CompositeElement) { |
140 | find transition(_, v1, s); | 160 | find SynchronizedRegionsAreNotSiblingsHelper1(s, r1); |
141 | find transition(_, v2, s); | 161 | find SynchronizedRegionsAreNotSiblingsHelper1(s, r2); |
142 | CompositeElement.regions.vertices(r1, v1); | ||
143 | CompositeElement.regions.vertices(r2, v2); | ||
144 | r1 != r2; | 162 | r1 != r2; |
145 | } or { | 163 | } or { |
164 | find SynchronizedRegionsAreNotSiblingsHelper2(s, r1); | ||
165 | find SynchronizedRegionsAreNotSiblingsHelper2(s, r2); | ||
166 | r1 != r2; | ||
167 | } | ||
168 | |||
169 | pattern SynchronizedRegionsAreNotSiblingsHelper1(s : Synchronization, r1 : CompositeElement) { | ||
146 | find transition(_, s, v1); | 170 | find transition(_, s, v1); |
147 | find transition(_, s, v2); | ||
148 | CompositeElement.regions.vertices(r1, v1); | 171 | CompositeElement.regions.vertices(r1, v1); |
149 | CompositeElement.regions.vertices(r2, v2); | 172 | } |
150 | r1 != r2; | 173 | |
174 | pattern SynchronizedRegionsAreNotSiblingsHelper2(s : Synchronization, r1 : CompositeElement) { | ||
175 | find transition(_, v1, s); | ||
176 | CompositeElement.regions.vertices(r1, v1); | ||
151 | } | 177 | } |
152 | 178 | ||
153 | /////////////////////////////// | 179 | /////////////////////////////// |
@@ -177,6 +203,11 @@ pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Ve | |||
177 | neg find hasMultipleRegions(c); | 203 | neg find hasMultipleRegions(c); |
178 | } | 204 | } |
179 | 205 | ||
206 | //@Constraint(severity="error", message="error", key = {sct}) | ||
207 | //pattern unsat_SynchronizedRegionDoesNotHaveMultipleRegions(sct : Statechart) { | ||
208 | // Statechart(sct); | ||
209 | // neg find SynchronizedRegionDoesNotHaveMultipleRegions(_, _); | ||
210 | //} | ||
180 | 211 | ||
181 | pattern hasMultipleRegions(composite: CompositeElement) { | 212 | pattern hasMultipleRegions(composite: CompositeElement) { |
182 | CompositeElement.regions(composite,region1); | 213 | CompositeElement.regions(composite,region1); |