-
Notifications
You must be signed in to change notification settings - Fork 0
/
PartialRefTemplatesFM.pvs
153 lines (131 loc) · 6.11 KB
/
PartialRefTemplatesFM.pvs
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
PartialRefTemplatesFM : THEORY
BEGIN
IMPORTING FeatureModel
IMPORTING FeatureModelSemantics
IMPORTING CK[Configuration,
Formula_,
satisfies,
FM,
Name,
semantics,
wfFM,
FormulaTheory.wt,
FeatureModelSemantics.genFE,
FeatureModelSemantics.getFeatures,
FeatureModelSemantics.addMandatory,
FeatureModelSemantics.addOptional
]
IMPORTING PartialRefinement[Configuration,WFM,semantics,Asset,AssetName,CK,semantics]
fm1,fm2: VAR FM
P,Q,R,M: VAR Name
pl: VAR PL
c: VAR Configuration
s: VAR set[Configuration]
fs: VAR set[Formula_]
%---------------------------------------------------------------------------------------------------------------------------------------
%---------------------------------------------TRANSF OPTIONAL TO MANDATORY TEMPLATE-----------------------------------------------------
%---------------------------------------------------------------------------------------------------------------------------------------
% Predicate that compares fm1 and fm2 for this template. The fms have the same features. However, their formulas are different
% because Q is optional in fm1 and mandatory in fm2
transfOptMand(fm1,fm2,P,Q): bool =
features(fm1) = features(fm2) AND
formulae(fm2) = union(formulae(fm1),IMPLIES_FORMULA(NAME_FORMULA(P), NAME_FORMULA(Q)))
% Template syntax. We need to make sure that the features P and Q belong to the feature models.
syntaxTransfOptMand(fm1,fm2,P,Q): bool =
transfOptMand(fm1,fm2,P,Q) AND
(features(fm1))(P) AND
(features(fm1))(Q)
% The initial feature model must satisfy the formula Q => P because the feature Q is supposed to be optional
conditionsTransfOptMand(fm1,P,Q): bool = FORALL c:
(semantics(fm1))(c) => satisfies(IMPLIES_FORMULA(NAME_FORMULA(Q),NAME_FORMULA(P)),c)
% Theorem <Transforming an optional feature into mandatory, results in a wf FM and a wf PL>
wfTransfOptMand: THEOREM
FORALL (pl,fm2,P,Q):
(
(
syntaxTransfOptMand(F(pl),fm2,P,Q) AND
conditionsTransfOptMand(F(pl),P,Q)
)
=> wfFM(fm2) AND wfPL(pl2)
)
WHERE pl2=(# F:=fm2, A:=A(pl), K:=K(pl) #)
% Theorem <Transform optional to mandatory feature template represents a strong partial refinement>
transOptMandPartRefStrong: THEOREM
FORALL (pl,fm2,s,P,Q):
(
(
syntaxTransfOptMand(F(pl),fm2,P,Q) AND
conditionsTransfOptMand(F(pl),P,Q) AND
s = <>((IMPLIES_FORMULA(NAME_FORMULA(P),NAME_FORMULA(Q))),F(pl))
)
=> strongPartialRefinement(pl,pl2,s)
)
WHERE pl2=(# F:=fm2, A:=A(pl), K:=K(pl) #)
%----------------------------------------------------------------------------------------------------------------
%---------------------------------------MOVE FEATURE TEMPLATE----------------------------------------------------
%----------------------------------------------------------------------------------------------------------------
% CASE 1 - P is the parent of Q
syntaxMoveFeature1(fm1,fm2,P,Q,R): bool =
features(fm1)(P) AND
features(fm1)(Q) AND
features(fm1)(R) AND
features(fm1) = features(fm2) AND
formulae(fm1)(IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(P))) AND
formulae(fm2) = union(formulae(fm1),IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(Q)))
moveFeaturePartialRefinement1: THEOREM
FORALL (pl,fm2,s,P,Q,R):
(
(
syntaxMoveFeature1(F(pl),fm2,P,Q,R) AND
s = <>(AND_FORMULA(NOT_FORMULA(NAME_FORMULA(Q)),NAME_FORMULA(R)),F(pl))
)
=> strongPartialRefinement(pl,pl2,s)
)
WHERE pl2=(# F:=fm2, A:=A(pl), K:=K(pl) #)
% CASE 2 - Q is the parent of P (mandatory, optional is refinement)
syntaxMoveFeature2(fm1,fm2,P,Q,R,fs): bool =
features(fm1)(P) AND
features(fm1)(Q) AND
features(fm1)(R) AND
features(fm1) = features(fm2) AND
fs(IMPLIES_FORMULA(NAME_FORMULA(P),NAME_FORMULA(Q))) AND
NOT fs(IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(P))) AND
NOT fs(IMPLIES_FORMULA(NAME_FORMULA(P),NAME_FORMULA(R))) AND
formulae(fm1) = union(fs,union(IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(P)),IMPLIES_FORMULA(NAME_FORMULA(P),NAME_FORMULA(R)))) AND
formulae(fm2) = union(fs,IMPLIES_FORMULA(NAME_FORMULA(Q),NAME_FORMULA(R)))
moveFeaturePartialRefinement2: THEOREM
FORALL (pl,fm2,s,P,Q,R,fs):
(
(
syntaxMoveFeature2(F(pl),fm2,P,Q,R,fs) AND
s = <>(AND_FORMULA(NOT_FORMULA(NAME_FORMULA(R)),NAME_FORMULA(Q)),F(pl))
)
=> strongPartialRefinement(pl,pl2,s)
)
WHERE pl2=(# F:=fm2, A:=A(pl), K:=K(pl) #)
% CASE 3 - Q and P are siblings
syntaxMoveFeature3(fm1,fm2,M,P,Q,R,fs): bool =
features(fm1)(P) AND
features(fm1)(Q) AND
features(fm1)(R) AND
features(fm1)(M) AND
features(fm1) = features(fm2) AND
fs(IMPLIES_FORMULA(NAME_FORMULA(P),NAME_FORMULA(M))) AND
fs(IMPLIES_FORMULA(NAME_FORMULA(Q),NAME_FORMULA(M))) AND
NOT fs(IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(P))) AND
NOT fs(IMPLIES_FORMULA(NAME_FORMULA(P),NAME_FORMULA(R))) AND
NOT fs(IMPLIES_FORMULA(NAME_FORMULA(Q),NAME_FORMULA(R))) AND
NOT fs(IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(Q))) AND
formulae(fm1) = add(IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(P)),fs) AND
formulae(fm2) = add(IMPLIES_FORMULA(NAME_FORMULA(R),NAME_FORMULA(Q)),fs)
moveFeaturePartialRefinement3: THEOREM
FORALL (pl,fm2,s,M,P,Q,R,fs):
(
(
syntaxMoveFeature3(F(pl),fm2,M,P,Q,R,fs) AND
s = <>(AND_FORMULA(NOT_FORMULA(NAME_FORMULA(Q)),NAME_FORMULA(R)),F(pl))
)
=> strongPartialRefinement(pl,pl2,s)
)
WHERE pl2=(# F:=fm2, A:=A(pl), K:=K(pl) #)
END PartialRefTemplatesFM