FeatureModelSemantics.pvs

FeatureModelSemantics: THEORY
 BEGIN
  IMPORTING FormulaTheory

  fm: VAR FM
  exp: VAR Formula_
  exps: VAR set[Formula_]
  c: VAR Configuration
  Q: VAR Name

  % well-formed feature model
  wfFM(fm: FM): bool = 
    wfTree(fm) AND wfFormulae(fm)                 


  WFM : TYPE = (wfFM)

  getFeatures(fm:FM): set[Name] = features(fm);

  genFE(f:Name):Formula_ = NAME_FORMULA(f);

  % configuration only contain names from the feature model
  satImpConsts(fm: FM, c:Configuration): bool =
    FORALL (n: Name): c(n) => features(fm)(n)

  satExpConsts(fm: FM, c:Configuration): bool =
    FORALL (f: Formula_): formulae(fm)(f) => satisfies(f,c)

  % semantics of a feature model
  semantics(fm: FM): set[Configuration] =
    {c:Configuration | satImpConsts(fm,c) AND satExpConsts(fm,c)}

  % refinement notion for feature models
  refines(abs,con: WFM): bool = subset?(semantics(abs),semantics(con))

  refines2(abs,con: WFM): bool =
    FORALL (c1: Configuration): semantics(abs)(c1) 
      => EXISTS(c2: Configuration): semantics(con)(c2)

%  addMandatory(fm:FM,n1:{n: Name | features(fm)(n)},n2:{n: Name | NOT(features(fm)(n))}):FM =
  addMandatoryFM(fm:FM,n1,n2:Name):FM =
    fm WITH [features:= add(n2,features(fm)), formulae:=add(IMPLIES_FORMULA(NAME_FORMULA(n2),NAME_FORMULA(n1)),add(IMPLIES_FORMULA(NAME_FORMULA(n1),NAME_FORMULA(n2)),formulae(fm)))]    

%  addOptional(fm:FM,n1:{n: Name | features(fm)(n)},n2:{n: Name | NOT(features(fm)(n))}):FM =
  addOptionalFM(fm:FM,n1,n2:Name):FM =
    fm WITH [features:= add(n2,features(fm)), formulae:=add(IMPLIES_FORMULA(NAME_FORMULA(n2),NAME_FORMULA(n1)),formulae(fm))]    

  addMandatory(abs:WFM,con:FM, n1,n2:Name):bool =
    features(con) = add(n2,features(abs)) AND
    formulae(con) = add(IMPLIES_FORMULA(NAME_FORMULA(n2),NAME_FORMULA(n1)),add(IMPLIES_FORMULA(NAME_FORMULA(n1),NAME_FORMULA(n2)),formulae(abs))) AND
    features(abs)(n1) AND 
    (NOT features(abs)(n2)) 

  addOptional(abs:WFM,con:FM, n1,n2:Name):bool =
    features(con) = add(n2,features(abs)) AND
    features(abs)(n1) AND 
    formulae(con) = add(IMPLIES_FORMULA(NAME_FORMULA(n2),NAME_FORMULA(n1)),formulae(abs)) AND
    (NOT features(abs)(n2))

  wtFormRefinement: LEMMA
    FORALL(abs,con:FM):
      (FORALL(name:Name): features(abs)(name) => features(con)(name) ) AND
      wfTree(abs) AND wfTree(con) =>
      	(FORALL (f:Formula_): wt(abs,f) => wt(con,f))

  notMember: THEOREM
    FORALL(fm:WFM,opt:Name):
      (not(features(fm)(opt))) =>
        (FORALL (c:Configuration) : semantics(fm)(c) => NOT c(opt)) 

  teste2: LEMMA
       FORALL (F,G:Name):
       (FORALL (c:Configuration, f:Formula_):
        NOT (member(G,names(f))) =>
              (satisfies(f,
                        IF (c(G)) THEN add(F,remove(G,c))
                        ELSE c ENDIF) 
             <=> 
         satisfies(rename(f,F,G),
            IF (c(F)) THEN add(G,remove(F,c))
                        ELSE c ENDIF)))

  renameFormulae(forms:set[Formula_],F,G:Name):set[Formula_] =
    {f:Formula_ | EXISTS (f1:Formula_): forms(f1) AND f=rename(f1,F,G)}

% operacao de renaming --> ren: FM x F x F -> FM
  renameFM(fm: FM, F,G:Name): FM =
    (# features:=add(G,remove(F,features(fm))), formulae:=renameFormulae(formulae(fm),F,G) #)

  wtFormRename2: LEMMA
    FORALL(fm1:WFM, F,G:Name):
      (
        (wfTree(fm1) AND wfTree(fm2)) 
        =>
          (FORALL (f:Formula_): wt(fm1,f) => wt(fm2,rename(f,F,G)))
      )
      WHERE fm2=renameFM(fm1,F,G)

  renameFeature_WF : THEOREM
    FORALL(fm1:WFM,F,G:Name): wfFM(fm2)
    WHERE fm2=renameFM(fm1,F,G)

  satFormula3 : THEOREM
    FORALL(fm1:WFM,F,G:Name):
      (NOT features(fm1)(G)) =>
      (FORALL (c:Configuration, f:Formula_):
              semantics(fm1)(c) AND
            (NOT (member(G,names(f)))) =>
              (satisfies(f,c) => satisfies(rename(f,F,G),
                          IF (c(F)) THEN add(G,remove(F,c))
                                  ELSE c ENDIF)))
    WHERE fm2=renameFM(fm1,F,G) 

  renameFeature3 : THEOREM
    FORALL(fm1:WFM,F,G:Name): (NOT features(fm1)(G)) => refines2(fm1,fm2)
    WHERE fm2=renameFM(fm1,F,G)

  <>(fm,exp):set[Configuration]  = {c | semantics(fm)(c) AND satisfies(exp,c)}

  <>(exp,fm):set[Configuration]  = {c | semantics(fm)(c) AND not satisfies(exp,c)}

  <>(exps,fm): set[Configuration] = {c | semantics(fm)(c) AND (FORALL exp: exps(exp) => not satisfies(exp,c))}

  % This function filters formulas from an FM that do not have Q
  filterFormulae(fm,Q): set[Formula_] = {form: Formula_ | formulae(fm)(form) AND NOT member(Q,names(form))}

 END FeatureModelSemantics