diff options
author | 2020-05-06 16:16:57 -0400 | |
---|---|---|
committer | 2020-05-06 16:16:57 -0400 | |
commit | e44d27fde5c3b6c933ea3de33781f6ad03d6545b (patch) | |
tree | fd4a58ed41ff3a91702cb1b7b89a9d9688fc1b4e /Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql | |
parent | Adjust classpath for Z3 in viatra2logic (diff) | |
download | VIATRA-Generator-e44d27fde5c3b6c933ea3de33781f6ad03d6545b.tar.gz VIATRA-Generator-e44d27fde5c3b6c933ea3de33781f6ad03d6545b.tar.zst VIATRA-Generator-e44d27fde5c3b6c933ea3de33781f6ad03d6545b.zip |
Adjustments to FamilyTree and Pledge Case studies
Diffstat (limited to 'Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql')
-rw-r--r-- | Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql | 27 |
1 files changed, 19 insertions, 8 deletions
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql index 1b9b6659..a204443a 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql | |||
@@ -9,14 +9,25 @@ pattern memberIsItsOwnParent(m: Member) = { | |||
9 | m == p; | 9 | m == p; |
10 | } | 10 | } |
11 | 11 | ||
12 | //@Constraint(message="parentTooYoung", severity="error", key={m, p}) | 12 | @Constraint(message="twoMembersHaveNoParent", severity="error", key={m1, m2}) |
13 | //pattern parentTooYoung(m: Member, p: Member) = { | 13 | pattern twoMembersHaveNoParent(m1:Member, m2:Member) = { |
14 | // FamilyTree.members(_, m); | 14 | neg find memberHasParent(m1); |
15 | // Member.parents(m, p); | 15 | neg find memberHasParent(m2); |
16 | // Member.age(m, mAge); | 16 | m1 != m2; |
17 | // Member.age(p, pAge); | 17 | } |
18 | // check (mAge <= (pAge + 12)); | 18 | |
19 | //} | 19 | pattern memberHasParent(m: Member) = { |
20 | Member.parents(m, _); | ||
21 | } | ||
22 | |||
23 | @Constraint(message="parentTooYoung", severity="error", key={m, p}) | ||
24 | pattern parentTooYoung(m: Member, p: Member) = { | ||
25 | FamilyTree.members(_, m); | ||
26 | Member.parents(m, p); | ||
27 | Member.age(m, mAge); | ||
28 | Member.age(p, pAge); | ||
29 | check (mAge <= (pAge + 12)); | ||
30 | } | ||
20 | 31 | ||
21 | 32 | ||
22 | 33 | ||