diff options
author | 2019-10-25 04:15:39 -0400 | |
---|---|---|
committer | 2020-06-07 19:43:49 -0400 | |
commit | 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f (patch) | |
tree | 0e67f50df5b4d9a42f0075e1e19be988eae59bf9 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.tar.gz VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.tar.zst VIATRA-Generator-32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries')
2 files changed, 102 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql new file mode 100644 index 00000000..5b04960e --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql | |||
@@ -0,0 +1,17 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries | ||
2 | |||
3 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/AlloyLanguage" | ||
4 | |||
5 | pattern directSubset(x: ALSSignatureDeclaration, y: ALSSignatureDeclaration) { | ||
6 | ALSSignatureBody.declarations(b,y); | ||
7 | ALSSignatureBody.supertype(b,x); | ||
8 | } or { | ||
9 | ALSSignatureBody.declarations(b,y); | ||
10 | ALSSignatureBody.superset(b,x); | ||
11 | } | ||
12 | |||
13 | pattern subset(x: ALSSignatureDeclaration, y: ALSSignatureDeclaration) { | ||
14 | x == y; | ||
15 | } or { | ||
16 | find directSubset+(x,y); | ||
17 | } | ||
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql new file mode 100644 index 00000000..9847b60a --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql | |||
@@ -0,0 +1,85 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries | ||
2 | |||
3 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" | ||
4 | |||
5 | private pattern supertypeEdge(type1: Type, type2: Type) { | ||
6 | Type.supertypes(type1,type2); | ||
7 | } | ||
8 | |||
9 | pattern supertype(type1: Type, type2: Type) { | ||
10 | type1 == type2; | ||
11 | } or { | ||
12 | find supertypeEdge+(type1,type2); | ||
13 | } | ||
14 | |||
15 | private pattern commonSubtype(type1: Type, type2: Type, common: Type) { | ||
16 | find supertype(common,type1); | ||
17 | find supertype(common,type2); | ||
18 | } | ||
19 | |||
20 | private pattern commonSupertype(type1: Type, type2: Type, common: Type) { | ||
21 | find supertype(common,type1); | ||
22 | find supertype(common,type2); | ||
23 | } | ||
24 | |||
25 | private pattern hasHigherCommonSubtype(type1: Type, type2: Type, common: Type, higher: Type) { | ||
26 | find supertype(higher,type1); | ||
27 | find supertype(higher,type2); | ||
28 | Type.supertypes(common,higher); | ||
29 | higher != common; | ||
30 | } | ||
31 | |||
32 | private pattern hasLowerCommonSupertype(type1: Type, type2: Type, common: Type, lower: Type) { | ||
33 | find supertype(type1,lower); | ||
34 | find supertype(type2,lower); | ||
35 | Type.supertypes(lower,common); | ||
36 | lower != common; | ||
37 | } | ||
38 | |||
39 | pattern topmostCommonSubtypes(type1: Type, type2: Type, common: Type) { | ||
40 | find commonSubtype(type1, type2, common); | ||
41 | neg find hasHigherCommonSubtype(type1, type2, common, _); | ||
42 | } | ||
43 | |||
44 | pattern lowermostCommonSupertype(type1: Type, type2: Type, common: Type) { | ||
45 | find commonSupertype(type1, type2, common); | ||
46 | neg find hasLowerCommonSupertype(type1, type2, common, _); | ||
47 | } | ||
48 | /*pattern topmostCommonSubtypesInObject(type1: Type, type2: Type, common: Type) { | ||
49 | find commonSubtype(type1, type2, common); | ||
50 | neg find supertypeEdge(type1,_); | ||
51 | neg find supertypeEdge(type2,_); | ||
52 | neg find hasHigherCommonSubtype(type1, type2, common, _); | ||
53 | } | ||
54 | pattern topmostCommonSubtypesInType(in: Type, type1: Type, type2: Type, common: Type) { | ||
55 | find commonSubtype(type1, type2, common); | ||
56 | find supertypeEdge(type1,in); | ||
57 | find supertypeEdge(type2,in); | ||
58 | neg find hasHigherCommonSubtype(type1, type2, common, _); | ||
59 | } | ||
60 | */ | ||
61 | |||
62 | pattern lowestCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type) { | ||
63 | find typeContainsAllOccuranceOfElement(element,type); | ||
64 | neg find hasLowerCommonSupertypeOfAllOccuranceOfElement(element, type, _); | ||
65 | } | ||
66 | |||
67 | private pattern hasLowerCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type, lower: Type) { | ||
68 | find typeContainsAllOccuranceOfElement(element, type); | ||
69 | find typeContainsAllOccuranceOfElement(element, lower); | ||
70 | find supertype(lower, type); | ||
71 | type != lower; | ||
72 | } | ||
73 | |||
74 | private pattern typeContainsAllOccuranceOfElement(element: DefinedElement, type: Type) { | ||
75 | find supertype(containerType,type); | ||
76 | TypeDefinition.elements(containerType,element); | ||
77 | neg find typeDoesNotCoverElementOccurance(element,type,_); | ||
78 | } | ||
79 | |||
80 | private pattern typeDoesNotCoverElementOccurance(element: DefinedElement, type: Type, uncoveredOccurance: TypeDefinition) { | ||
81 | find supertype(containerType,type); | ||
82 | TypeDefinition.elements(containerType,element); | ||
83 | TypeDefinition.elements(uncoveredOccurance,element); | ||
84 | neg find supertype(uncoveredOccurance,type); | ||
85 | } \ No newline at end of file | ||