-
Notifications
You must be signed in to change notification settings - Fork 0
/
CKIntFMConc.pvs~
79 lines (63 loc) · 2.83 KB
/
CKIntFMConc.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
CKIntFMConc : THEORY
BEGIN
IMPORTING FeatureModel
IMPORTING FeatureModelSemantics
IMPORTING CKInt[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: VAR Name
pl: VAR PL
c: VAR Configuration
s: VAR set[Configuration]
%---------------------------------------------------------------------------------------------------------------------------------------
%---------------------------------------------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 = <>(F(pl),(IMPLIES_FORMULA (NAME_FORMULA(P),NAME_FORMULA(Q))))
)
=> strongPartialRefinement(pl,pl2,s)
)
WHERE pl2=(# F:=fm2, A:=A(pl), K:=K(pl) #)
END CKIntFMConc