-
Notifications
You must be signed in to change notification settings - Fork 0
/
CKinst.pvs
35 lines (30 loc) · 882 Bytes
/
CKinst.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
CKinst: THEORY
BEGIN
IMPORTING FeatureModelSemantics
IMPORTING CKComp
IMPORTING CKInt[Name.Configuration,
Formula_,
FormulaTheory.satisfies,
FeatureModel.FM,
Name.Name,
FeatureModelSemantics.semantics,
FeatureModelSemantics.wfFM,
FormulaTheory.wt,
FeatureModelSemantics.genFE,
FeatureModelSemantics.getFeatures,
FeatureModelSemantics.addMandatory,
FeatureModelSemantics.addOptional
]{{
RightSide:=finite_sets[AssetName].finite_set,
Item:=CKComp.Item,
CK:=CKComp.CK,
exps:=CKComp.expsCK,
getExp := CKComp.getExp,
getRS := CKComp.getRS,
items := CKComp.items,
wfCK:=CKComp.wfCK,
semantics:=CKComp.semantics,
notshowupItem := CKComp.notshowupItem,
showupItem:=CKComp.showupItem
}}
END CKinst