CKtInst.pvs

CKtInst: THEORY
BEGIN

  IMPORTING FeatureModelSemantics
  IMPORTING CKtrans

  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:=CKtrans.Transformation, 
  	    Item:=CKtrans.Item, 
  	    CK:=CKtrans.CK, 
	    exps:=CKtrans.exps, 
	    getExp := CKtrans.getExp,
	    getRS := CKtrans.getRS,
	    items := CKtrans.items,
  	    wfCK:=CKtrans.wfCK, 
	    semantics:=CKtrans.semantics%, 
%	    notshowupItem := ConfigurationKnowledge.notshowupItem, 
%	    showupItem:=ConfigurationKnowledge.showupItem
  }}



END CKtInst