## 3 Background in Feature Models and Validation Mechanisms
_Let \(FMF\) be a formalised feature model consisting of the tuple (F,R), where \(F\) is a set of Boolean variables \(\{f_{1},f_{2},\cdots,f_{n}\}\) that represent the features and \(R\) as a set of relations \(r_{i}\) that are a tuple (\(S\),BR), where the scope \(S\)=(\(f_{i}\), \(f_{j}\)) are the features involved in the relation and \(BR\subseteq d_{f_{i}}\times d_{f_{j}}\) are the tuples satisfying the relation and \(d_{f_{k}}\) is the domain of the values of the feature \(f_{k}\). Given a formalised feature model, \(FMF\), composed of a set of features \(F=\{f_{1},f_{2},\cdots,f_{n}\}\), and a set of relations, \(R=\{r_{1},r_{2},\cdots,r_{k}\}\), an assignment \(a_{i}\) is the association of Boolean values to all the variables (features). \[a_{i}=\prod_{f_{k}\in F}d_{f_{k}}\]  
\[a_{i}=\{f_{1}\to v_{1},f_{2}\to v_{2},\cdots,f_{n}\to v_{n}\}\]  
For instance, \(a_{i}\)=\(\{\)_PS2 true, \(A\) true, \(A1\) true, \(A2\) false,..._ \(\}\) represents an assignment for the model in Figure 1, where missed features are assigned to _false_ value. Therefore, let \(A\) be the set of all the possible assignments of a model \(FMF\). \[A_{FMF}=\bigcup_{i\in FMF}a_{i}\]  
An assignment is considered a valid assignment when satisfies all relations (\(R\)) of the model \(FMF\). \[a_{i}=\prod_{f_{k}\in F}d_{f_{k}}\rightarrow\{true,false\}\]  
\[valid(a_{i})=true\iff\{\forall r_{i}\in R|BR(a_{i})\equiv true\}\]  
Otherwise, if there exist any relation that cannot be satisfied, the assignment will be considered invalid, hence, valid predicate will return _false_ value. For instance, the previous assignment, \(a_{i}\), represents a valid assignment since satisfies the mandatory relation between \(PS2\) and \(A\) feature and the or-relation between \(A\) and \(A1\). The \(\{\)_PS2 = true, \(A=true\}\)_ assignment is invalid due to the relation between \(A\), \(A1\), and \(A2\) is unsatisfied. For our purpose, a configuration represents an assignment of \(FMF\). Thus, the previous examples of assignments represent configurations for the feature model. The configurations can be valid whether the selection of assigned features to _true_ satisfies all the relations, invalid otherwise. The set of valid and invalid assignments of \(FMF\) can be defined as the union of all valid and invalid assignments, respectively. \[A_{FMF}^{valid}=\bigcup_{a_{i}\in A_{FMF}}\{a_{i}|\quad valid(a_{i})\}\]  
\[A_{FMF}^{invalid}=\bigcup_{a_{i}\in A_{FMF}}\{a_{i}|\quad\
eg valid(a_{i})\}\]  
The union of the sets of valid and invalid assignments represent the domain of assignments for \(FMF\) model. Let \(A\) be redefined as the union of the sets of valid and invalid assignments. Figure 1.0  
The snippet code in Figure 2 presents an example of a CSP model for ChocoSolver tool [52] obtained from the model of Figure 1.1 Each variable represents a feature that can or cannot participate in the configuration, represented by the value 1 or 0 respectively. Constraints establish the relation between features such as _ifonlyif_ restriction which represents the mandatory relation. Thus, the formalisation enables inferring information by applying some operations over the model. Modelling a feature model as a CSP enables verifying the satisfaction of the model, and to obtain the number of valid software products. Definition 3: Products. Let \(FM\) be a feature model, the potential products of \(FM\) is the valid configurations of its equivalent \(FMF\). Figure 1.2  
Definition 4: Number of Products. Let \(FM\) be a feature model, the potential number of products of \(FM\) is the solution of its equivalent number of solutions of the \(FMF\). Figure 1.3  
For example, all the valid configurations obtained from the model of Figure 1 are shown in Figure 1.4 For each configuration, the selected features are shown. For example, features \(PS1\), \(A\), and \(A1\) are selected for \(Configuration1\). The final product is composed of these features.