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