-
Notifications
You must be signed in to change notification settings - Fork 0
/
5(ii).als
133 lines (97 loc) · 2.39 KB
/
5(ii).als
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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
// load fm signatures
open fm
one sig FM1, FM2, FMUnion, FMIntersection extends FM{}
one sig Fp, Fi, Fj, Fk extends Name{}
// == FM1
fact FM1Features {
FM1.features = Fp + Fi + Fj
}
pred FM1Semantics[config:set Name] {
--fixed
config in FM1.features
root[Fp,config]
--relations
mandatory[Fp, Fi,config]
mandatory[Fp, Fj,config]
--formulas
}
// == FM2
fact FM2Features {
FM2.features = Fp + Fi + Fj + Fk
}
pred FM2Semantics[config:set Name] {
--fixed
config in FM2.features
root[Fp,config]
--relations
orGroup[Fp, Fi + Fj + Fk,config]
--formulas
}
// == FMUnion
fact FMUnion{
FMUnion.features = Fp + Fi + Fj + Fk
}
pred FMUnionSemantics[config:set Name] {
--fixed
config in FMUnion.features
root[Fp, config]
--relations
orGroup[Fp, Fi + Fj + Fk, config]
--formulas
}
// == FMIntersection
fact FMIntersection{
FMIntersection.features = Fp + Fi + Fj + Fk
}
pred FMIntersectionSemantics[config:set Name] {
--fixed
config in FMIntersection.features
root[Fp, config]
--relations
mandatory[Fp, Fi, config]
mandatory[Fp, Fj, config]
nonselectable[Fp, Fk, config]
--formulas
}
// == Hints to generate configurations
fact configurationHints {
some c: set Name | Fp + Fi in c
some c: set Name | Fp + Fj in c
some c: set Name | Fp + Fk in c
some c: set Name | Fp + Fi + Fj in c
some c: set Name | Fp + Fi + Fk in c
some c: set Name | Fp + Fj + Fk in c
some c: set Name | Fp + Fi + Fj + Fk in c
some c: set Name | Fp in c
some c: set Name | Fp not in c
some c: set Name | Fi in c
some c: set Name | Fi not in c
some c: set Name | Fj in c
some c: set Name | Fj not in c
some c: set Name | Fk in c
some c: set Name | Fk not in c
}
// == verifications
assert isUnion1{
all c:set Name | FMUnionSemantics[c] =>
(FM1Semantics[c] or FM2Semantics[c])
}
assert isUnion2 {
no c:set Name | FM1Semantics[c] and not FMUnionSemantics[c]
}
assert isUnion3 {
no c:set Name | FM2Semantics[c] and not FMUnionSemantics[c]
}
assert isIntersection1{
all c:set Name | FMIntersectionSemantics[c] =>
(FM1Semantics[c] and FM2Semantics[c])
}
assert isIntersection2{
no c:set Name | (FM1Semantics[c] and FM2Semantics[c])
and not FMIntersectionSemantics[c]
}
check isUnion1 for 15 FM, 4 Name
check isUnion2 for 15 FM, 4 Name
check isUnion3 for 15 FM, 4 Name
check isIntersection1 for 15 FM, 4 Name
check isIntersection2 for 15 FM, 4 Name