diff options
author | 2020-07-16 00:23:49 +0200 | |
---|---|---|
committer | 2020-07-16 00:23:49 +0200 | |
commit | fb952906aa64f6a502a93fba3dbc521f499221dd (patch) | |
tree | a4ecdce203d2dc5239d6b223a6bd3bb0bfdf39f0 /Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries | |
parent | Fix numeric-solver-at-end (diff) | |
download | VIATRA-Generator-fb952906aa64f6a502a93fba3dbc521f499221dd.tar.gz VIATRA-Generator-fb952906aa64f6a502a93fba3dbc521f499221dd.tar.zst VIATRA-Generator-fb952906aa64f6a502a93fba3dbc521f499221dd.zip |
Clean up MODELS20 files
Diffstat (limited to 'Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries')
4 files changed, 820 insertions, 0 deletions
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql new file mode 100644 index 00000000..57b5933a --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql | |||
@@ -0,0 +1,390 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.domains.satellite.queries | ||
2 | |||
3 | import "http://www.example.org/satellite" | ||
4 | |||
5 | @Constraint(severity = "error", key = {Element}, | ||
6 | message = "A communicating element may not have two transmitting communication subsystems.") | ||
7 | pattern communicationLinkDoesNotStartAtContainingElement(Element : CommunicatingElement) { | ||
8 | find transmittingCommSubsystem(Element, Comm1); | ||
9 | find transmittingCommSubsystem(Element, Comm2); | ||
10 | Comm1 != Comm2; | ||
11 | } | ||
12 | |||
13 | private pattern transmittingCommSubsystem(Element : CommunicatingElement, Comm : CommSubsystem) { | ||
14 | CommunicatingElement.commSubsystem(Element, Comm); | ||
15 | CommSubsystem.target(Comm, _); | ||
16 | } | ||
17 | |||
18 | @Constraint(severity = "error", key = {Station}, | ||
19 | message = "The ground station network may not have outgoing communication links.") | ||
20 | pattern transmittingGroundStationNetwork(Station : GroundStationNetwork) { | ||
21 | find transmittingCommSubsystem(Station, _); | ||
22 | } | ||
23 | |||
24 | @Constraint(severity = "error", key = {Station}, | ||
25 | message = "The ground station network may not have UHF communication subsystems.") | ||
26 | pattern roundStationNetworkUHF(Station : GroundStationNetwork) { | ||
27 | CommunicatingElement.commSubsystem(Station, Comm); | ||
28 | UHFCommSubsystem(Comm); | ||
29 | } | ||
30 | |||
31 | // At least two spacecraft must have the interferometry payload configured | ||
32 | |||
33 | @Constraint(severity = "error", key = {Mission}, | ||
34 | message = "Interferometry mission needs at least two spacecraft configured with the interferometry payload.") | ||
35 | pattern notEnoughInterferometryPayloads(Mission : InterferometryMission) { | ||
36 | InterferometryMission(Mission); | ||
37 | neg find atLeastTwoInterferometryPayloads(Mission); | ||
38 | } | ||
39 | |||
40 | private pattern atLeastTwoInterferometryPayloads(Mission : InterferometryMission) { | ||
41 | find spacecraftWithInterferometryPayload(Mission, Spacecraft1); | ||
42 | find spacecraftWithInterferometryPayload(Mission, Spacecraft2); | ||
43 | Spacecraft1 != Spacecraft2; | ||
44 | } | ||
45 | |||
46 | private pattern spacecraftWithInterferometryPayload(Mission : ConstellationMission, Spacecraft : Spacecraft) { | ||
47 | ConstellationMission.spacecraft(Mission, Spacecraft); | ||
48 | Spacecraft.payload(Spacecraft, Payload); | ||
49 | InterferometryPayload(Payload); | ||
50 | } | ||
51 | |||
52 | // All spacecraft must have some communication path to the ground station | ||
53 | |||
54 | //@Constraint(severity = "error", key = {Spacecraft}, | ||
55 | // message = "Spacecraft has no communication path to the ground station.") | ||
56 | //pattern noLinkToGroundStation(Spacecraft : Spacecraft) { | ||
57 | // ConstellationMission.groundStationNetwork(Mission, GroundStation); | ||
58 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
59 | // neg find indirectCommunicationLink(Spacecraft, GroundStation); | ||
60 | //} | ||
61 | |||
62 | //@Constraint(severity = "error", key = {Spacecraft}, message = "UNSAT") | ||
63 | //pattern unsat_linkToGroundStation(Spacecraft : Spacecraft) { | ||
64 | // ConstellationMission.groundStationNetwork(Mission, GroundStation); | ||
65 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
66 | // find indirectCommunicationLink(Spacecraft, GroundStation); | ||
67 | //} | ||
68 | |||
69 | //@Constraint(severity = "error", key = {Mission}, message = "UNSAT") | ||
70 | //pattern unsat_linkToGroundStation(Mission : InterferometryMission) { | ||
71 | // InterferometryMission(Mission); | ||
72 | // neg find noLinkToGroundStation(_); | ||
73 | //} | ||
74 | |||
75 | //@Constraint(severity = "error", key = {Spacecraft}, | ||
76 | // message = "Spacecraft has no potential communication path to the ground station.") | ||
77 | //pattern noPotentialLinkToGroundStation(Spacecraft : Spacecraft) { | ||
78 | // ConstellationMission.groundStationNetwork(Mission, GroundStation); | ||
79 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
80 | // neg find indirectLinkAllowed(Spacecraft, GroundStation); | ||
81 | //} | ||
82 | |||
83 | //private pattern indirectLinkAllowed(From : Spacecraft, To : CommunicatingElement) { | ||
84 | // find linkAllowed+(From, To); | ||
85 | //} | ||
86 | |||
87 | //private pattern linkAllowed(From : Spacecraft, To : CommunicatingElement) { | ||
88 | // find matchingAntenna(From, To); | ||
89 | // neg find cubeSat3U(From); | ||
90 | //} or { | ||
91 | // find matchingAntenna(From, To); | ||
92 | // CubeSat3U(From); | ||
93 | //} or { | ||
94 | // find matchingAntenna(From, To); | ||
95 | // CubeSat3U(From); | ||
96 | // GroundStationNetwork(To); | ||
97 | //} | ||
98 | |||
99 | //private pattern matchingAntenna(From : Spacecraft, To : CommunicatingElement) { | ||
100 | // CommunicatingElement.commSubsystem(From, FromSys); | ||
101 | // CommunicatingElement.commSubsystem(To, ToSys); | ||
102 | // find matchingCommSubsystem(FromSys, ToSys); | ||
103 | //} | ||
104 | |||
105 | private pattern matchingCommSubsystem(From : CommSubsystem, To : CommSubsystem) { | ||
106 | UHFCommSubsystem(From); | ||
107 | UHFCommSubsystem(To); | ||
108 | } or { | ||
109 | XCommSubsystem(From); | ||
110 | XCommSubsystem(To); | ||
111 | } or { | ||
112 | KaCommSubsystem(From); | ||
113 | KaCommSubsystem(To); | ||
114 | } | ||
115 | |||
116 | //private pattern cubeSat3U(Sat : CubeSat3U) { | ||
117 | // CubeSat3U(Sat); | ||
118 | //} | ||
119 | |||
120 | // No communication loops may exist | ||
121 | // No spacecraft may directly communicate with itself | ||
122 | |||
123 | @Constraint(severity = "error", key = {Element}, | ||
124 | message = "Communication loop.") | ||
125 | pattern communicationLoop(Element : CommunicatingElement) { | ||
126 | find indirectCommunicationLink(Element, Element); | ||
127 | } | ||
128 | |||
129 | private pattern indirectCommunicationLink(Source : CommunicatingElement, Target : CommunicatingElement) { | ||
130 | find directCommunicationLink+(Source, Target); | ||
131 | } | ||
132 | |||
133 | private pattern directCommunicationLink(Source : CommunicatingElement, Target : CommunicatingElement) { | ||
134 | CommSubsystem.target(SourceSubsystem, TargetSubsystem); | ||
135 | CommunicatingElement.commSubsystem(Source, SourceSubsystem); | ||
136 | CommunicatingElement.commSubsystem(Target, TargetSubsystem); | ||
137 | } | ||
138 | |||
139 | // Source and target communication systems must be compatible. | ||
140 | |||
141 | @Constraint(severity = "error", key = {SourceSubsystem}, | ||
142 | message = "Two ends of a communication link must use the same band.") | ||
143 | pattern incompatibleSourceAndTargetBand(SourceSubsystem : CommSubsystem) { | ||
144 | CommSubsystem.target(SourceSubsystem, TargetSubsystem); | ||
145 | neg find matchingCommSubsystem(SourceSubsystem, TargetSubsystem); | ||
146 | } | ||
147 | |||
148 | // 3U CubeSats are assumed to only be able to downlink to Earth using an X-band trasmitter, | ||
149 | // but cross-link using UHF | ||
150 | |||
151 | @Constraint(severity = "error", key = {Sat}, | ||
152 | message = "3U CubeSats can only cross-link using UHF.") | ||
153 | pattern threeUCubeSatWithNonUhfCrossLink(Sat : CubeSat3U) { | ||
154 | CommunicatingElement.commSubsystem(Sat, SourceComm); | ||
155 | neg find commSubsystemBandUhf(SourceComm); | ||
156 | CommSubsystem.target(SourceComm, TargetComm); | ||
157 | CommunicatingElement.commSubsystem(Target, TargetComm); | ||
158 | neg find groundStationNetwork(Target); | ||
159 | } | ||
160 | |||
161 | private pattern commSubsystemBandUhf(Comm : UHFCommSubsystem) { | ||
162 | UHFCommSubsystem(Comm); | ||
163 | } | ||
164 | |||
165 | private pattern groundStationNetwork(Network : GroundStationNetwork) { | ||
166 | GroundStationNetwork(Network); | ||
167 | } | ||
168 | |||
169 | // Only a Small Satellite can be configured with a Ka-band communication system | ||
170 | |||
171 | @Constraint(severity = "error", key = {Spacecraft}, | ||
172 | message = "Only a Small Satellite can be configured with a Ka-band communication system.") | ||
173 | pattern cubeSatWithKaAntenna(Spacecraft : Spacecraft) { | ||
174 | CommunicatingElement.commSubsystem(Spacecraft, Comm); | ||
175 | KaCommSubsystem(Comm); | ||
176 | neg find smallSat(Spacecraft); | ||
177 | } | ||
178 | |||
179 | pattern smallSat(Sat : SmallSat) { | ||
180 | SmallSat(Sat); | ||
181 | } | ||
182 | |||
183 | @Constraint(severity = "error", key = {c1,c2}, message = "error") | ||
184 | pattern differentFrequency(c1 : CommSubsystem, c2 : CommSubsystem) { | ||
185 | CommSubsystem.target(c1,c2); | ||
186 | CommSubsystem.frequency(c1,f1); | ||
187 | CommSubsystem.frequency(c2,f2); | ||
188 | check(f1!=f2); | ||
189 | } | ||
190 | |||
191 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
192 | pattern tooHighFrequencyForUHF(s : UHFCommSubsystem) { | ||
193 | UHFCommSubsystem(s); | ||
194 | CommSubsystem.frequency(s,f); | ||
195 | check(f>1000);//1GHz | ||
196 | } | ||
197 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
198 | pattern tooLowFrequencyForUHF(s : UHFCommSubsystem) { | ||
199 | UHFCommSubsystem(s); | ||
200 | CommSubsystem.frequency(s,f); | ||
201 | check(f<300);//300MHz | ||
202 | } | ||
203 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
204 | pattern tooHighFrequencyForKaComm(s : KaCommSubsystem) { | ||
205 | KaCommSubsystem(s); | ||
206 | CommSubsystem.frequency(s,f); | ||
207 | check(f>40000);//40GHz | ||
208 | } | ||
209 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
210 | pattern tooLowFrequencyForKaComm(s : KaCommSubsystem) { | ||
211 | KaCommSubsystem(s); | ||
212 | CommSubsystem.frequency(s,f); | ||
213 | check(f<26500);//26.5GHz | ||
214 | } | ||
215 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
216 | pattern tooHighFrequencyForXComm(s : XCommSubsystem) { | ||
217 | XCommSubsystem(s); | ||
218 | CommSubsystem.frequency(s,f); | ||
219 | check(f>12000);//12GHz | ||
220 | } | ||
221 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
222 | pattern tooLowFrequencyForXComm(s : XCommSubsystem) { | ||
223 | XCommSubsystem(s); | ||
224 | CommSubsystem.frequency(s,f); | ||
225 | check(f<8000);//8GHz | ||
226 | } | ||
227 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
228 | pattern tooHighPathLengthForSatelite(s:CommSubsystem) { | ||
229 | CommSubsystem.pathLength(s,l); | ||
230 | CommSubsystem.target(s,ts); | ||
231 | Spacecraft.commSubsystem(_,ts); | ||
232 | check(l>250);//250km | ||
233 | } | ||
234 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
235 | pattern tooLowPathLengthForSatelite(s:CommSubsystem) { | ||
236 | CommSubsystem.pathLength(s,l); | ||
237 | CommSubsystem.target(s,ts); | ||
238 | Spacecraft.commSubsystem(_,ts); | ||
239 | check(l<150);//150km | ||
240 | } | ||
241 | @Constraint(severity = "error", key = {s,s}, message = "error") | ||
242 | pattern tooLowPathLengthForGroundStation(s:CommSubsystem) { | ||
243 | CommSubsystem.pathLength(s,l); | ||
244 | CommSubsystem.target(s,ts); | ||
245 | GroundStationNetwork.commSubsystem(_,ts); | ||
246 | check(l!=385000);//385.000km | ||
247 | } | ||
248 | //// | ||
249 | //// Metrics | ||
250 | //// | ||
251 | // | ||
252 | //// Coverage | ||
253 | // | ||
254 | //pattern coverageMetric(Coverage : java Double) { | ||
255 | // Coverage == sum find missionCoverage(_, #_); | ||
256 | //} | ||
257 | // | ||
258 | //private pattern missionCoverage(Mission : InterferometryMission, Coverage : java Double) { | ||
259 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
260 | // ObserverCount == count find spacecraftWithInterferometryPayload(Mission, _); | ||
261 | // Coverage == eval(Math.pow(1 - 2.0 / ObserverCount, 1 + 9 * (1.0 / ObservationTime)) + 0.05 * ObservationTime / 3); | ||
262 | //} | ||
263 | // | ||
264 | //// Time | ||
265 | // | ||
266 | //pattern timeMetric(Time : java Double) { | ||
267 | // Time == sum find missionTime(_, #_); | ||
268 | //} | ||
269 | // | ||
270 | //private pattern missionTime(Mission : InterferometryMission, Time : java Double) { | ||
271 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
272 | // TrasmitTime == sum find transmitTime(Mission, _, #_); | ||
273 | // Time == eval(TrasmitTime + 60.0 * ObservationTime); | ||
274 | //} | ||
275 | // | ||
276 | //private pattern transmitTime(Mission : InterferometryMission, Spacecraft : Spacecraft, TransmitTime : java Double) { | ||
277 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
278 | // find scienceData(Spacecraft, ScienceData); | ||
279 | // IncomingData == sum find incomingData(Spacecraft, _, #_); | ||
280 | // find transmitRate(Spacecraft, TransmitRate); | ||
281 | // TransmitTime == eval((ScienceData + IncomingData) / (7.5 * TransmitRate)); | ||
282 | //} | ||
283 | // | ||
284 | //private pattern incomingData(Spacecraft : Spacecraft, Source : Spacecraft, Data : java Double) { | ||
285 | // find indirectCommunicationLink(Source, Spacecraft); | ||
286 | // find scienceData(Source, Data); | ||
287 | //} | ||
288 | // | ||
289 | //private pattern scienceData(Spacecraft : Spacecraft, Data : java Double) { | ||
290 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
291 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
292 | // Data == eval(12.0 * ObservationTime); | ||
293 | //} | ||
294 | // | ||
295 | //private pattern transmitRate(Spacecraft : Spacecraft, TransmitRate : java Double) { | ||
296 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
297 | // UHFCommSubsystem(Comm); | ||
298 | // Spacecraft(Target); | ||
299 | // TransmitRate == 5.0; | ||
300 | //} or { | ||
301 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
302 | // XCommSubsystem(Comm); | ||
303 | // Spacecraft(Target); | ||
304 | // TransmitRate == 1.6; | ||
305 | //} or { | ||
306 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
307 | // XCommSubsystem(Comm); | ||
308 | // GroundStationNetwork(Target); | ||
309 | // TransmitRate == 0.7; | ||
310 | //} or { | ||
311 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
312 | // KaCommSubsystem(Comm); | ||
313 | // Spacecraft(Target); | ||
314 | // TransmitRate == 220.0; | ||
315 | //} or { | ||
316 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
317 | // KaCommSubsystem(Comm); | ||
318 | // GroundStationNetwork(Target); | ||
319 | // TransmitRate == 80.0; | ||
320 | //} | ||
321 | // | ||
322 | //private pattern spacecraftUplink(Spacecraft : Spacecraft, TargetSubsystem : CommSubsystem, Target : CommunicatingElement) { | ||
323 | // CommunicatingElement.commSubsystem.target(Spacecraft, TargetSubsystem); | ||
324 | // CommunicatingElement.commSubsystem(Target, TargetSubsystem); | ||
325 | //} | ||
326 | // | ||
327 | //// Cost | ||
328 | // | ||
329 | //pattern costMetric(Cost : java Double) { | ||
330 | // Cost == sum find missionCost(_, #_); | ||
331 | //} | ||
332 | // | ||
333 | //private pattern missionCost(Mission : InterferometryMission, Cost : java Double) { | ||
334 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
335 | // SpacecraftCost == sum find spacecraftCost(Mission, _, #_); | ||
336 | // Cost == eval(SpacecraftCost + 100000.0 * ObservationTime); | ||
337 | //} | ||
338 | // | ||
339 | //private pattern spacecraftCost(Mission : InterferometryMission, Spacecraft : Spacecraft, Cost : java Double) { | ||
340 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
341 | // find spacecraftOfKindCount(Spacecraft, KindCount); | ||
342 | // find basePrice(Spacecraft, BasePrice); | ||
343 | // find interferometryPayloadCost(Spacecraft, InterferometryPayloadCost); | ||
344 | // find additionalCommSubsystemCost(Spacecraft, AdditionalCommSubsystemCost); | ||
345 | // Cost == eval(BasePrice * Math.pow(KindCount, -0.25) + InterferometryPayloadCost + AdditionalCommSubsystemCost); | ||
346 | //} | ||
347 | // | ||
348 | //private pattern spacecraftOfKindCount(Sat : Spacecraft, Count : java Integer) { | ||
349 | // CubeSat3U(Sat); | ||
350 | // Count == count find cubeSat3U(_); | ||
351 | //} or { | ||
352 | // CubeSat6U(Sat); | ||
353 | // Count == count find cubeSat6U(_); | ||
354 | //} or { | ||
355 | // SmallSat(Sat); | ||
356 | // Count == count find smallSat(_); | ||
357 | //} | ||
358 | // | ||
359 | //private pattern basePrice(Spacecraft : Spacecraft, BasePrice : java Double) { | ||
360 | // CubeSat3U(Spacecraft); | ||
361 | // BasePrice == 250000.0; | ||
362 | //} or { | ||
363 | // CubeSat6U(Spacecraft); | ||
364 | // BasePrice == 750000.0; | ||
365 | //} or { | ||
366 | // SmallSat(Spacecraft); | ||
367 | // BasePrice == 3000000.0; | ||
368 | //} | ||
369 | // | ||
370 | //private pattern interferometryPayloadCost(Spacecraft : Spacecraft, Cost : java Double) { | ||
371 | // find spacecraftWithInterferometryPayload(_, Spacecraft); | ||
372 | // Cost == 50000.0; | ||
373 | //} or { | ||
374 | // neg find spacecraftWithInterferometryPayload(_, Spacecraft); | ||
375 | // Cost == 0.0; | ||
376 | //} | ||
377 | // | ||
378 | //private pattern additionalCommSubsystemCost(Spacecraft : Spacecraft, Cost : java Double) { | ||
379 | // find spacecraftWithTwoCommSubsystems(Spacecraft); | ||
380 | // Cost == 100000.0; | ||
381 | //} or { | ||
382 | // neg find spacecraftWithTwoCommSubsystems(Spacecraft); | ||
383 | // Cost == 0.0; | ||
384 | //} | ||
385 | // | ||
386 | //private pattern spacecraftWithTwoCommSubsystems(Spacecraft : Spacecraft) { | ||
387 | // Spacecraft.commSubsystem(Spacecraft, Subsystem1); | ||
388 | // Spacecraft.commSubsystem(Spacecraft, Subsystem2); | ||
389 | // Subsystem1 != Subsystem2; | ||
390 | //} | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/case_study_A_withRoot.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/case_study_A_withRoot.vql new file mode 100644 index 00000000..cd876200 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/case_study_A_withRoot.vql | |||
@@ -0,0 +1,338 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http:///TaxCardWithRoot.ecore" | ||
4 | |||
5 | //AttributeRemoved -> DF | ||
6 | |||
7 | //inv1-External_Allowance.amount is a derived feature (TODOcheck) | ||
8 | //inv2-Tax_Card.income.taxPayer.taxesDue is a derived feature (TODOcheck) | ||
9 | |||
10 | //inv3-multiplicity adjusted | ||
11 | @Constraint(message = "inv03", severity = "error", key = {dep}) | ||
12 | pattern inv03(dep : Dependent) { | ||
13 | find x_inv03_eligAll(dep); | ||
14 | neg find x_inv03_hasAll(dep); | ||
15 | } or { | ||
16 | Dependent.birth_year(dep, by); | ||
17 | check(2018-by > 21); | ||
18 | Dependent.continued_studies(dep, false); | ||
19 | Dependent.allowances(dep, _); | ||
20 | } | ||
21 | pattern x_inv03_eligAll(dep : Dependent) { | ||
22 | Dependent.birth_year(dep, by); | ||
23 | check(2018-by <= 21); | ||
24 | } or { | ||
25 | Dependent.continued_studies(dep, true); | ||
26 | } | ||
27 | pattern x_inv03_hasAll(dep : Dependent) { | ||
28 | Dependent.allowances(dep, _); | ||
29 | } | ||
30 | |||
31 | //inv5 - oclIsTypeOf - handled here | ||
32 | @Constraint(message = "inv05", severity = "error", key = {inc}) | ||
33 | pattern inv05(inc : Income) { | ||
34 | //income_type: None | ||
35 | neg find x_inv08_noType(inc); | ||
36 | Income.details.worked_days(inc, wd); | ||
37 | check(wd != 0); | ||
38 | } or { | ||
39 | //income_type: Not Employment_Income | ||
40 | Income.income_type(inc, type); | ||
41 | neg find x_inv08_notEI(type); | ||
42 | Income.details.worked_days(inc, wd); | ||
43 | check(wd != 0); | ||
44 | } or { | ||
45 | //income_type: Employment Income | ||
46 | Income.income_type(inc, type); | ||
47 | Employment_Income(type); | ||
48 | find x_inv05_inRange(inc); | ||
49 | } | ||
50 | pattern x_inv05_inRange(inc : Income) { | ||
51 | Income.details.worked_days(inc, wd); | ||
52 | check(wd < 1); | ||
53 | } or { | ||
54 | Income.details.worked_days(inc, wd); | ||
55 | check(wd > 25); | ||
56 | } | ||
57 | |||
58 | //inv6-Does not make sens, but directly from OCL | ||
59 | //first part of or from definition of getAge() | ||
60 | @Constraint(message = "inv06", severity = "error", key = {tp}) | ||
61 | pattern inv06(tp : Tax_Payer) { | ||
62 | Tax_Payer.dependents(tp, _); | ||
63 | Tax_Payer.birth_year(tp, TPBy); | ||
64 | check(2018 - TPBy > 2018-16); | ||
65 | } or { | ||
66 | Tax_Payer.birth_year(tp, TPBy); | ||
67 | Tax_Payer.dependents(tp, dep); | ||
68 | Dependent.birth_year(dep, DepBy); | ||
69 | check(2018-DepBy <= 2018-TPBy-16); | ||
70 | } | ||
71 | |||
72 | //inv7-OrderedSet | ||
73 | @Constraint(message = "inv07", severity = "error", key = {inc}) | ||
74 | pattern inv07(inc : Income) { | ||
75 | Income.details.distance(inc, d1); | ||
76 | Income.details.distance(inc, d2); | ||
77 | check(d1 != d2);//compare values | ||
78 | } | ||
79 | |||
80 | //user_complete_details-AttributeRemoved | ||
81 | |||
82 | //inv8 - oclIsTypeOf - handled here | ||
83 | @Constraint(message = "inv08", severity = "error", key = {inc}) | ||
84 | pattern inv08(inc : Income) { | ||
85 | //income_type: None | ||
86 | neg find x_inv08_noType(inc); | ||
87 | Income.details.distance(inc, dist); | ||
88 | check(dist != 0); | ||
89 | } or { | ||
90 | //income_type: Not Employment_Income | ||
91 | Income.income_type(inc, type); | ||
92 | neg find x_inv08_notEI(type); | ||
93 | Income.details.distance(inc, dist); | ||
94 | check(dist != 0); | ||
95 | } or { | ||
96 | //income_type: Employment Income | ||
97 | Income.income_type(inc, type); | ||
98 | Employment_Income(type); | ||
99 | find x_inv08_inRange(inc); | ||
100 | } | ||
101 | pattern x_inv08_notEI(type : Employment_Income) { | ||
102 | Employment_Income(type); | ||
103 | } | ||
104 | pattern x_inv08_noType(inc : Income) { | ||
105 | Income.income_type(inc, _); | ||
106 | } | ||
107 | pattern x_inv08_inRange(inc : Income) { | ||
108 | Income.details.distance(inc, dist); | ||
109 | check(dist < 0); | ||
110 | } or { | ||
111 | Income.details.distance(inc, dist); | ||
112 | check(dist > 100); | ||
113 | } | ||
114 | //inv9-DerivedFeature | ||
115 | |||
116 | //inv10-Ordered Sets | ||
117 | @Constraint(message = "inv10", severity = "error", key = {inc}) | ||
118 | pattern inv10(inc : Income) { | ||
119 | Income.details.amount(inc, a1); | ||
120 | Income.details.amount(inc, a2); | ||
121 | check(a1 != a2);//compare values | ||
122 | } | ||
123 | |||
124 | //inv11-attributes-handled by multiplicity | ||
125 | @Constraint(message = "inv11", severity = "error", key = {exp}) | ||
126 | pattern inv11(exp : Expense) { | ||
127 | find x_inv11_incOver100(exp); | ||
128 | find x_inv11_incNotOver100(exp); | ||
129 | } | ||
130 | pattern x_inv11_incOver100(exp : Expense) { | ||
131 | Expense.income.income_amount(exp, incVal); | ||
132 | check(incVal / 2 > 50); | ||
133 | |||
134 | } or { | ||
135 | Expense.declared_amount(exp, decl); | ||
136 | check(decl != 50); | ||
137 | } | ||
138 | pattern x_inv11_incNotOver100(exp : Expense) { | ||
139 | Expense.income.income_amount(exp, incVal); | ||
140 | check(incVal / 2 <= 50); | ||
141 | } or { | ||
142 | Expense.declared_amount(exp, decl); | ||
143 | check(decl < 50); | ||
144 | } or { | ||
145 | Expense.income.income_amount(exp, incVal); | ||
146 | Expense.declared_amount(exp, decl); | ||
147 | check(decl > incVal/2); | ||
148 | } | ||
149 | |||
150 | //inv12 | ||
151 | //exists - handled logically | ||
152 | @Constraint(message = "inv12", severity = "error", key = {tp}) | ||
153 | pattern inv12(tp : Tax_Payer) { | ||
154 | Tax_Payer.addresses(tp, hab_add); | ||
155 | Habitual_Address(hab_add); | ||
156 | neg find x_inv12_notZZ(hab_add); | ||
157 | Tax_Payer.incomes(tp, inc); | ||
158 | Local_Income(inc); | ||
159 | neg find x_inv12_notNonRes(tp); | ||
160 | } | ||
161 | pattern x_inv12_notNonRes(tp : Non_Resident_Tax_Payer) { | ||
162 | Non_Resident_Tax_Payer(tp); | ||
163 | } | ||
164 | pattern x_inv12_notZZ(hab_add : Habitual_Address) { | ||
165 | Address.country(hab_add, ::ZZ); | ||
166 | } | ||
167 | |||
168 | //inv13 - Added new containment rel Phys_Pers->Address | ||
169 | //exists - handled logically | ||
170 | @Constraint(message = "inv13", severity = "error", key = {tp}) | ||
171 | pattern inv13(tp : Tax_Payer) { | ||
172 | Tax_Payer.addresses(tp, hab_add); | ||
173 | Habitual_Address(hab_add); | ||
174 | Address.country(hab_add, ::ZZ); | ||
175 | neg find x_inv13(tp); | ||
176 | } | ||
177 | pattern x_inv13(tp : Resident_Tax_Payer) { | ||
178 | Resident_Tax_Payer(tp); | ||
179 | } | ||
180 | |||
181 | //inv14-MultiplicityChanged | ||
182 | |||
183 | //inv15-Ordered Sets in assignment if block | ||
184 | //ERROR if no household object | ||
185 | @Constraint(message = "inv15", severity = "error", key = {ea}) | ||
186 | pattern inv15(ea : External_Allowance) { | ||
187 | neg find x_inv15(ea); | ||
188 | } | ||
189 | pattern x_inv15(ea : External_Allowance) { | ||
190 | External_Allowance.person(ea, child); | ||
191 | Household.children(h, child);//only one due to multiplicity | ||
192 | Household.parents.individual_A(h, iA); | ||
193 | Tax_Payer(iA); | ||
194 | External_Allowance.reciver(ea, iA); | ||
195 | } or { | ||
196 | External_Allowance.person(ea, child); | ||
197 | Household.children(h, child);//only one due to multiplicity | ||
198 | Household.parents.individual_B(h, iB); | ||
199 | Tax_Payer(iB); | ||
200 | External_Allowance.reciver(ea, iB); | ||
201 | } | ||
202 | |||
203 | //inv16-Tax_Card.tax_card_type is a derived feature | ||
204 | |||
205 | //inv17-attribute-handled by multiplicity | ||
206 | @Constraint(message = "inv17", severity = "error", key = {lur}) | ||
207 | pattern inv17(lur : Legal_Union_Record) { | ||
208 | Legal_Union_Record.start_year(lur, sy); | ||
209 | check(sy < 1950); | ||
210 | } or { | ||
211 | Legal_Union_Record.start_year(lur, sy); | ||
212 | check(sy > 2018); | ||
213 | } | ||
214 | |||
215 | //inv18-MultiplicityChecked | ||
216 | //inv19-MultiplicityChecked | ||
217 | |||
218 | //inv20-Useless constraint since both edges are containment (TODOCheck) | ||
219 | //OclIsUndefined-Handled by multiplicity | ||
220 | @Constraint(message = "inv20", severity = "error", key = {lur}) | ||
221 | pattern inv20(lur : Legal_Union_Record) { | ||
222 | Legal_Union_Record.individual_A(lur, iA); | ||
223 | Legal_Union_Record.individual_B(lur, iB); | ||
224 | iA == iB; | ||
225 | } | ||
226 | //inv21-MultiplicityChecked | ||
227 | //inv22-MultiplicityChecked | ||
228 | //inv23-MultiplicityChecked | ||
229 | //inv24-MultiplicityChecked | ||
230 | //inv25-MultiplicityChecked | ||
231 | //inv26-MultiplicityChanged | ||
232 | //inv27-dupOfInv24 | ||
233 | //inv28-dubOfInv23 | ||
234 | //inv29-MultiplicityChanged | ||
235 | //inv30-AttributeRemoved | ||
236 | //inv31-AttributeRemoved | ||
237 | //inv32-AttributeRemoved | ||
238 | |||
239 | //inv33-attribute-handled by multiplicity | ||
240 | @Constraint(message = "inv33", severity = "error", key = {p}) | ||
241 | pattern inv33(p : Physical_Person) { | ||
242 | Physical_Person.birth_year(p, by); | ||
243 | check(2018-by < 0); | ||
244 | } or { | ||
245 | Physical_Person.birth_year(p, by); | ||
246 | check(2018-by > 100); | ||
247 | } | ||
248 | |||
249 | //inv34-attribute-handled by multiplicity | ||
250 | @Constraint(message = "inv34", severity = "error", key = {p}) | ||
251 | pattern inv34(p : Physical_Person) { | ||
252 | Physical_Person.birth_month(p, birthMonth); | ||
253 | check(birthMonth < 1); | ||
254 | } or { | ||
255 | Physical_Person.birth_month(p, birthMonth); | ||
256 | check(birthMonth > 12); | ||
257 | } | ||
258 | |||
259 | //inv35-attribute-handled by multiplicity | ||
260 | @Constraint(message = "inv35", severity = "error", key = {p}) | ||
261 | pattern inv35(p : Physical_Person) { | ||
262 | Physical_Person.birth_day(p, birthDay); | ||
263 | check(birthDay < 1); | ||
264 | } or { | ||
265 | Physical_Person.birth_day(p, birthDay); | ||
266 | check(birthDay > 28); | ||
267 | } | ||
268 | |||
269 | //inv36-AttributeRemoved | ||
270 | //inv37-AttributeRemoved | ||
271 | //inv38-AttributeRemoved | ||
272 | //inv39-AttributeRemoved | ||
273 | //inv40-AttributeRemoved | ||
274 | //inv41-AttributeRemoved | ||
275 | //inv42-AttributeRemoved | ||
276 | //inv43-AttributeRemoved | ||
277 | //inv44-AttributeRemoved | ||
278 | //inv45-AttributeRemoved | ||
279 | //inv46-AttributeRemoved | ||
280 | |||
281 | //inv47-attributes-handled by multiplicity | ||
282 | @Constraint(message = "inv47", severity = "error", key = {lur}) | ||
283 | pattern inv47(lur : Legal_Union_Record) { | ||
284 | Legal_Union_Record.end_year(lur, endY); | ||
285 | Legal_Union_Record.start_year(lur, startY); | ||
286 | neg find x_inv47(lur); | ||
287 | check(startY >= endY); | ||
288 | } or { | ||
289 | Legal_Union_Record.end_year(lur, endY); | ||
290 | Legal_Union_Record.start_year(lur, startY); | ||
291 | check(endY!= -1); | ||
292 | check(startY >= endY); | ||
293 | } | ||
294 | pattern x_inv47(lur : Legal_Union_Record) { | ||
295 | Legal_Union_Record.separation_cause(lur, ::NONE); | ||
296 | } | ||
297 | |||
298 | //inv48-attributes-handled by multiplicity | ||
299 | @Constraint(message = "inv48", severity = "error", key = {p}) | ||
300 | pattern inv48(p : Physical_Person) { | ||
301 | Physical_Person.disability_percentage(p, disPer); | ||
302 | check(disPer > 1.0); | ||
303 | } or { | ||
304 | Physical_Person.disability_percentage(p, disPer); | ||
305 | check(disPer < 0.0); | ||
306 | } or { | ||
307 | Physical_Person.disability_type(p, ::NONE); | ||
308 | Physical_Person.disability_percentage(p, disPer); | ||
309 | check(disPer != 0.0); | ||
310 | } or { | ||
311 | neg find x_inv48(p); | ||
312 | Physical_Person.disability_percentage(p, disPer); | ||
313 | check(disPer == 0.0); | ||
314 | } | ||
315 | pattern x_inv48(p : Physical_Person) { | ||
316 | Physical_Person.disability_type(p, ::NONE); | ||
317 | } | ||
318 | |||
319 | //inv49-OclKindOf-handled by multiplicity | ||
320 | @Constraint(message = "inv49", severity = "error", key = {lur}) | ||
321 | pattern inv49_A(lur : Legal_Union_Record) { | ||
322 | Legal_Union_Record.individual_A(lur, i); | ||
323 | Legal_Union_Record.individual_B(lur, i); | ||
324 | } | ||
325 | //inv49-OclKindOf-handled by multiplicity | ||
326 | @Constraint(message = "inv49", severity = "error", key = {lur}) | ||
327 | pattern inv49_B(lur : Legal_Union_Record) { | ||
328 | Legal_Union_Record.individual_A(lur, i); | ||
329 | Dependent(i); | ||
330 | } or { | ||
331 | Legal_Union_Record.individual_B(lur, i); | ||
332 | Dependent(i); | ||
333 | } | ||
334 | |||
335 | //inv50-MultiplicityChecked | ||
336 | //inv51-MultiplicityChecked | ||
337 | //inv52-MultiplicityChecked | ||
338 | //inv53-MultiplicityChecked \ No newline at end of file | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraints.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraints.vql new file mode 100644 index 00000000..fdbac640 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraints.vql | |||
@@ -0,0 +1,41 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.org/familytree" | ||
4 | |||
5 | @Constraint(message="memberIsItsOwnParent", severity="error", key={m}) | ||
6 | pattern memberIsItsOwnParent(m: Member) = { | ||
7 | FamilyTree.members(_, m); | ||
8 | Member.parents(m, p); | ||
9 | m == p; | ||
10 | } | ||
11 | |||
12 | @Constraint(message="twoMembersHaveNoParent", severity="error", key={m1, m2}) | ||
13 | pattern twoMembersHaveNoParent(m1:Member, m2:Member) = { | ||
14 | neg find memberHasParent(m1); | ||
15 | neg find memberHasParent(m2); | ||
16 | m1 != m2; | ||
17 | } | ||
18 | |||
19 | pattern memberHasParent(m: Member) = { | ||
20 | Member.parents(m, _); | ||
21 | } | ||
22 | |||
23 | @Constraint(message="negativeAge", severity="error",key={m}) | ||
24 | pattern negativeAge(m: Member) { | ||
25 | Member.age(m,mage); | ||
26 | check(mage<0); | ||
27 | } | ||
28 | |||
29 | @Constraint(message="parentTooYoung", severity="error", key={c, p}) | ||
30 | pattern parentTooYoung(c: Member, p: Member) = { | ||
31 | FamilyTree.members(_, c); | ||
32 | Member.parents(c, p); | ||
33 | Member.age(c, cAge); | ||
34 | Member.age(p, pAge); | ||
35 | check (pAge <= (cAge + 12)); | ||
36 | } | ||
37 | |||
38 | |||
39 | |||
40 | |||
41 | |||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraintsQual.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraintsQual.vql new file mode 100644 index 00000000..946451d1 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraintsQual.vql | |||
@@ -0,0 +1,51 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.org/familytree" | ||
4 | |||
5 | @Constraint(message="memberIsItsOwnParent", severity="error", key={m}) | ||
6 | pattern memberIsRecursiveParent(m: Member) = { | ||
7 | find isParent+(m, m); | ||
8 | } | ||
9 | |||
10 | pattern isParent(m: Member, p: Member){ | ||
11 | Member.parents(m, p); | ||
12 | } | ||
13 | |||
14 | |||
15 | @Constraint(message="memberIsItsOwnParent", severity="error", key={m}) | ||
16 | pattern memberIsItsOwnParent(m: Member) = { | ||
17 | FamilyTree.members(_, m); | ||
18 | Member.parents(m, p); | ||
19 | m == p; | ||
20 | } | ||
21 | |||
22 | @Constraint(message="twoMembersHaveNoParent", severity="error", key={m1, m2}) | ||
23 | pattern twoMembersHaveNoParent(m1:Member, m2:Member) = { | ||
24 | neg find memberHasParent(m1); | ||
25 | neg find memberHasParent(m2); | ||
26 | m1 != m2; | ||
27 | } | ||
28 | |||
29 | pattern memberHasParent(m: Member) = { | ||
30 | Member.parents(m, _); | ||
31 | } | ||
32 | |||
33 | @Constraint(message="negativeAge", severity="error",key={m}) | ||
34 | pattern negativeAge(m: Member) { | ||
35 | Member.age(m,mage); | ||
36 | check(mage<0); | ||
37 | } | ||
38 | |||
39 | @Constraint(message="parentTooYoung", severity="error", key={c, p}) | ||
40 | pattern parentTooYoung(c: Member, p: Member) = { | ||
41 | FamilyTree.members(_, c); | ||
42 | Member.parents(c, p); | ||
43 | Member.age(c, cAge); | ||
44 | Member.age(p, pAge); | ||
45 | check (pAge <= (cAge + 12)); | ||
46 | } | ||
47 | |||
48 | |||
49 | |||
50 | |||
51 | |||