aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql
blob: 8d93cafbd3c90cb3fd9fd66ba54807a2a9240350 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries

import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"

private pattern supertypeEdge(type1: Type, type2: Type) {
	Type.supertypes(type1,type2);
}

pattern supertype(type1: Type, type2: Type) {
	type1 == type2;
} or {
	find supertypeEdge+(type1,type2);
}

private pattern commonSubtype(type1: Type, type2: Type, common: Type) {
	find supertype(common,type1);
	find supertype(common,type2);
}

private pattern commonSupertype(type1: Type, type2: Type, common: Type) {
	find supertype(common,type1);
	find supertype(common,type2);
}

private pattern hasHigherCommonSubtype(type1: Type, type2: Type, common: Type, higher: Type) {
	find supertype(higher,type1);
	find supertype(higher,type2);
	Type.supertypes(common,higher);
	higher != common;
}

private pattern hasLowerCommonSupertype(type1: Type, type2: Type, common: Type, lower: Type) {
	find supertype(type1,lower);
	find supertype(type2,lower);
	Type.supertypes(lower,common);
	lower != common;
}

pattern topmostCommonSubtypes(type1: Type, type2: Type, common: Type) {
	find commonSubtype(type1, type2, common);
	neg find hasHigherCommonSubtype(type1, type2, common, _);
}

pattern lowermostCommonSupertype(type1: Type, type2: Type, common: Type) {
	find commonSupertype(type1, type2, common);
	neg find hasLowerCommonSupertype(type1, type2, common, _);
}
/*pattern topmostCommonSubtypesInObject(type1: Type, type2: Type, common: Type) {
	find commonSubtype(type1, type2, common);
	neg find supertypeEdge(type1,_);
	neg find supertypeEdge(type2,_);
	neg find hasHigherCommonSubtype(type1, type2, common, _);
}
pattern topmostCommonSubtypesInType(in: Type, type1: Type, type2: Type, common: Type) {
	find commonSubtype(type1, type2, common);
	find supertypeEdge(type1,in);
	find supertypeEdge(type2,in);
	neg find hasHigherCommonSubtype(type1, type2, common, _);
}
 */

pattern lowestCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type) {
	find typeContainsAllOccuranceOfElement(element,type);
	neg find hasLowerCommonSupertypeOfAllOccuranceOfElement(element, type, _);
}

private pattern hasLowerCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type, lower: Type) {
	find typeContainsAllOccuranceOfElement(element, type);
	find typeContainsAllOccuranceOfElement(element, lower);
	find supertype(lower, type);
	type != lower;
}

private pattern typeContainsAllOccuranceOfElement(element: DefinedElement, type: Type) {
	find supertype(containerType,type);
	TypeDefinition.elements(containerType,element);
	neg find typeDoesNotCoverElementOccurance(element,type,_);
}

private pattern typeDoesNotCoverElementOccurance(element: DefinedElement, type: Type, uncoveredOccurance: TypeDefinition) {
	find supertype(containerType,type);
	TypeDefinition.elements(containerType,element);
	TypeDefinition.elements(uncoveredOccurance,element);
	neg find supertype(uncoveredOccurance,type);
}