Skip to content

fPromela

There are two kinds of approaches to implement (models of) SPLs. Compositional methods capture the effect of features in isolated modules. A given product is then obtained by composing the right set of modules. On the contrary, annotative approaches directly adorn models with constraints over the features, e.g.,feature expressions. These annotations express that parts of the model are exclusive to the set of products satisfying the formulae.

fPromela falls into the latter category. It is an executable language based on Promela, Spin’s input syntax. In an fPromela model, the behaviour of each process is described in a \texttt{proctype} structure. Within a process, executable statements are expressed using constructs inspired by imperative programming. fPromela extends Promela by its capability to distinguish features from normal variables. We focus here on how to declare features and associate them to Promela statements.

Boolean features

Features are declared in a specific user-defined data structure called features. For instance, to declare a Boolean feature b and its child feature c, one must write:

// Declare list of features inside the special type "features"
typedef features {
bool b;
bool c
};
// Declare an instance of this type
features f;

In an fPromela model, the behaviour of each process is described in a proctype structure. Within a process, executable statements are expressed using constructs inspired by imperative programming. Statements can be guarded by feature expressions, i.e., formulae over the features and their attributes. Then, a product can execute a statement if and only if it satisfies the formula that guards this statement.

To specify a guarded statements, we use the keywords gd ... dg. Between these keywords, we specify the feature expression as well as the guarded statements. The following code specifies that the products with feature c increments variable i, whereas the others decrements it:

active proctype p() {
int i = 1;
gd
:: f.c; i = i+1;
:: else; i = i-1;
dg
}

In ProVeLines, however, fPromela is not limited to Boolean features; multi-features and numeric features are also supported.

Multi-features

To declare a multi-feature with a maximum cardinality of n, simply declare it in an n-sized array. For instance, the following code declares that b is a multi-feature with at most two instances:

typedef features {
bool b[2]
};
features f;

Due to ambiguity in the semantics of multi-features, the above addition compels a hierarchical declaration of child features. For instance, let us assume that every instance of b may have one child feature named c. To uniquely define each instance of c, we declare this feature in a new user-defined data structure, which will be the new type of b. Hence, we write:

typedef B {
bool is_in;
bool c
};
typedef features {
B b[2]
};
features f;

The first field of such a data structure is always is_in. It acts as a Boolean variable that informs whether the feature is enabled or disabled. Should c also have child features, its type would be another user-defined data structure. fPromela supports finitely-sized arrays only; it is thus impossible to represent multi-features with infinite cardinality.

To guard statements with a precise instance of a feature, one must refererence the appropriate data structures. For instance, the following code specifies that the products equipped with the child feature c of the first instance of b increment variable i whereas the other decrement it:

active proctype p() {
int i = 1;
gd
:: f.b[0].c; i = i+1;
:: else; i = i-1;
dg
}

Note that if one want to constraint a statement with a non-terminal feature like b, she can either reference the field is_in of this instance, or the instance directly. In other words, f.b[0].is_in and f.b[0] are two equivalent expressions.

The number of instances of a feature can also constrain the executability of statements. For this purpose, one uses the keyword card. The following excerpt specifies that products with more than one instance of b increments variable i whereas the other decrements it:

active proctype p() {
int i = 1;
gd
:: card(f.b > 1); i = i+1;
:: else; i = i-1;
dg
}

Numeric features

In feature modelling, numeric features are often represented as numeric attributes of another feature. We also do so in fPromela. As for non-terminal multi-features, a feature with an attribute must be declared in a specific data structure. For example, let us assume that in addition to a child feature c, feature b has also an integer attribute named a. Then, we write:

typedef B {
bool is_in;
bool c;
int a
};
typedef features {
B b
};
features f;

As before, the first field of the data structure is Boolean and called is_in. One may then use constraints over numeric features to guard statements, even in loop conditions. For instance, the following excerpt specifies that variable i eventually receives the same value as the numeric child-feature a of b‘s second instance:

active proctype p() {
int i = 0;
do
:: f.b[1].a > i; i = i+1;
:: else; break;
od
}

Such guard is potentially dangerous since it may lead to an infinite state-space model. To prevent such cases, please specify a maximum attribute value for the numeric feature in TVL or fPromela.