-
Notifications
You must be signed in to change notification settings - Fork 0
/
5(viii).als
154 lines (118 loc) · 3.32 KB
/
5(viii).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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
// load fm signatures
open fm
one sig FM1, FM2, FMUnion, FMIntersection extends FM{}
one sig Fp, Fi, Fj, Fk, Fm, Fn extends Name{}
// == FM1
fact FM1Features {
FM1.features = Fp + Fi + Fj + Fk
}
pred FM1Semantics[config:set Name] {
--fixed
config in FM1.features
root[Fp,config]
--relations
alternative[Fp, Fi + Fj + Fk, config]
--formulas
}
// == FM2
fact FM2Features {
FM2.features = Fp + Fi + Fj + Fm + Fn
}
pred FM2Semantics[config:set Name] {
--fixed
config in FM2.features
root[Fp,config]
--relations
alternative[Fp, Fi + Fj + Fm + Fn, config]
--formulas
}
// == FMUnion
fact FMUnion{
FMUnion.features = Fp + Fi + Fj + Fk + Fm + Fn
}
pred FMUnionSemantics[config:set Name] {
--fixed
config in FMUnion.features
root[Fp, config]
--relations
alternative[Fp, Fi + Fj + Fk + Fm + Fn, config]
--formulas
}
// == FMIntersection
fact FMIntersection{
FMIntersection.features = Fp + Fi + Fj + Fk + Fm + Fn
}
pred FMIntersectionSemantics[config:set Name] {
--fixed
config in FMIntersection.features
root[Fp, config]
--relations
alternative[Fp, Fi + Fj, config]
nonselectable[Fp, Fk, config]
nonselectable[Fp, Fm, config]
nonselectable[Fp, Fn, 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 + Fm in c
some c: set Name | Fp + Fn 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 + Fm in c
some c: set Name | Fp + Fj + Fm in c
some c: set Name | Fp + Fi + Fn in c
some c: set Name | Fp + Fj + Fn in c
some c: set Name | Fp + Fi + Fj + Fk in c
some c: set Name | Fp + Fi + Fj + Fm in c
some c: set Name | Fp + Fi + Fj + Fn in c
some c: set Name | Fp + Fi + Fk + Fm in c
some c: set Name | Fp + Fi + Fk + Fn in c
some c: set Name | Fp + Fj + Fk + Fm in c
some c: set Name | Fp + Fj + Fk + Fn in c
some c: set Name | Fp + Fi + Fj + Fk + Fm in c
some c: set Name | Fp + Fi + Fj + Fk + Fn in c
some c: set Name | Fp + Fi + Fk + Fm + Fn in c
some c: set Name | Fp + Fj + Fk + Fm + Fn in c
some c: set Name | Fp + Fi + Fj + Fk + Fm + Fn 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
some c: set Name | Fm in c
some c: set Name | Fm not in c
some c: set Name | Fn in c
some c: set Name | Fn 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 35 FM, 5 Name
check isUnion2 for 35 FM, 5 Name
check isUnion3 for 35 FM, 5 Name
check isIntersection1 for 35 FM, 5 Name
check isIntersection2 for 35 FM, 5 Name