-
Notifications
You must be signed in to change notification settings - Fork 0
/
FMint.pvs
34 lines (29 loc) · 1.24 KB
/
FMint.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
FMint[
Configuration:TYPE,
FeatureExpression:TYPE,
sat: [FeatureExpression,Configuration -> boolean]
]: THEORY
BEGIN
IMPORTING FeatureExpression[Configuration]{{
FeatureExpression:=FeatureExpression,
sat:=sat
}}
% Assumption <Feature model semantics>
FMi: TYPE
Feature : TYPE
[||] : [FMi -> set[Configuration]]
% ----Filter configurations that do not satisfy an expression exp and belong to a feature model fm
% <>(fm:FMi,e:FeatureExpression):set[Configuration] = {c:Configuration | ([||](fm))(c) AND NOT sat(e,c)}
% <>(e:FeatureExpression,fm:FMi):set[Configuration] = {c: Configuration | ([||](fm))(c) AND sat(e,c)}
% <>(fm:FMi, exps:set[FeatureExpression]):set[Configuration] =
%{c: Configuration | ([||](fm))(c) AND FORALL (e:FeatureExpression): exps(e) => NOT sat(e,c)}
wf(fm:FMi):boolean
wt(fm:FMi, f:FeatureExpression):boolean
genFeatureExpression(f:Feature):FeatureExpression
getFeatures(fm:FMi):set[Feature]
addMandatory(fm1:FMi, fm2:FMi, p:Feature, f:Feature):bool
addOptional(fm1:FMi, fm2:FMi, p:Feature, f:Feature):bool
addOR(fm1:FMi, fm2:FMi, p:Feature, f:Feature):bool
addAlternative(fm1:FMi, fm2:FMi, p:Feature, f:Feature):bool
% sat(f:FeatureExpression, c:Configuration): boolean
END FMint