-
Notifications
You must be signed in to change notification settings - Fork 0
/
FeatureModelRefinements.pvs
95 lines (83 loc) · 2.92 KB
/
FeatureModelRefinements.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
FeatureModelRefinements: THEORY
BEGIN
IMPORTING Name, FeatureModel, FeatureModelSemantics
CONVERSION+ singleton
% useful lemma
wtFormAddNode: LEMMA
FORALL(abs,con:FM, n1,n2:Name):
wfTree(abs) AND wfTree(con) AND
features(con) = union(features(abs),n2) AND
features(abs)(n1) AND
(NOT features(abs)(n2))
=>
(FORALL (f:Formula_):
wt(abs,f) => wt(con,f))
% Add Mandatory Node
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
addMandatoryNode(abs:WFM,con:FM, n1,n2:Name):bool =
features(con) = union(features(abs),n2) AND
formulae(con) = union(formulae(abs),union(IMPLIES_FORMULA(NAME_FORMULA(n2),NAME_FORMULA(n1)),IMPLIES_FORMULA(NAME_FORMULA(n1),NAME_FORMULA(n2)))) AND
features(abs)(n1) AND
(NOT features(abs)(n2))
addMandatoryWF: THEOREM
FORALL(abs:WFM, n1,n2:Name,con:FM):
(addMandatoryNode(abs,con,n1,n2)
=>
wfFM(con))
addMandatoryT: THEOREM
FORALL(abs:WFM, n1,n2:Name):
EXISTS(con:FM):
(addMandatoryNode(abs,con,n1,n2)
=>
(FORALL (c:Configuration):
semantics(abs)(c)
=> IF (c(n1)) THEN semantics(con)(union(c,n2)) ELSE semantics(con)(c) ENDIF
)
AND
(FORALL (c:Configuration):
semantics(con)(c)
=> IF (c(n2)) THEN semantics(abs)(remove(n2,c)) ELSE semantics(abs)(c) ENDIF
)
AND wfFM(con)
)
addMandatoryTWF: THEOREM
FORALL(abs:WFM, n1,n2:Name,con:FM):
(addMandatoryNode(abs,con,n1,n2)
=>
(FORALL (c:Configuration):
semantics(abs)(c)
=> IF (c(n1)) THEN semantics(con)(union(c,n2)) ELSE semantics(con)(c) ENDIF
)
AND
(FORALL (c:Configuration):
semantics(con)(c)
=> IF (c(n2)) THEN semantics(abs)(remove(n2,c)) ELSE semantics(abs)(c) ENDIF
)
AND wfFM(con))
% Add Optional Node
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
addOptionalNode(abs:WFM,con:FM, n1,n2:Name):bool =
features(con) = union(features(abs),n2) AND
features(abs)(n1) AND
formulae(con) = union(formulae(abs), IMPLIES_FORMULA(NAME_FORMULA(n2),NAME_FORMULA(n1))) AND
(NOT features(abs)(n2))
% preserva a semantica estatica
wfPreservation: LEMMA
FORALL(abs:WFM, n1,n2:Name,con:FM):
(addOptionalNode(abs,con,n1,n2)
=>
wfFM(con))
addNode: THEOREM
FORALL(abs:WFM, n1,n2:Name):
EXISTS(con:FM):
(addOptionalNode(abs,con,n1,n2)
=>
refines(abs,con) and wfFM(con))
addOptNode: THEOREM
FORALL(abs:WFM, n1,n2:Name,con:FM):
(addOptionalNode(abs,con,n1,n2)
=>
refines(abs,con) and wfFM(con))
END FeatureModelRefinements