Feature modules

A feature module defines the behavior (or part of the behavior) of a feature.

Linking features and modules

A feature is implemented by referencing one or more modules after the modules keyword inside the feature block:

feature Consumer
    modules consumer_impl;
endfeature

module consumer_impl
    // ...
endmodule

In this example, the Consumer is implemented by the consumer_impl module. Multiple modules can be listed after the modules keyword (separated by comma).

Note

A module can be referenced by multiple features. In this case, the module is instantiated multiple times.

Module definitions

A module consists of two parts. The variables define its possible states and commands specify the behavior by transitions between these states.

For example, the consumer may have a variable that stores the amount of remaining work to be processed:

module consumer_impl
    work : [0 .. 3] init 0;
endmodule

Note

If no initial value is defined, the initial value for the variable is chosen nondeterministically and the model has multiple initial states.

A variable can have one of the following types.

[<n> .. <m>]

A bounded integer with minimum value n and maximum value m (the upper bound is inclusive).

bool

A Boolean variable which can be either true or false.

array [<n> .. <m>] of <type>

An array with indices ranging from n to m (inclusive). The element type must be either bool or a bounded integer. An array can be initialized using an array literal:

x : array [0..2] of bool init {true, false, true};

For initializing all elements with the same value, the following short-hand notation can be used:

x : array [0..2] of bool init false;

A command comprises a guard and an update. If the guard evaluates to true in the current state the command may be executed, which updates the local variables of the module. In the following example, the command processes the remaining work by decreasing the work variable:

module consumer_impl
    work : [0 .. 3] init 0;

    [] work > 0 -> (work' = work - 1);
endmodule

Module variables are defined in the scope of its feature. Thus, other modules can refer to the work variable of the Consumer feature by Consumer.work.

Note

In contrast to the PRISM language, module variables in ProFeat do not have to be globally unique. They only must be unique within the module definition. However, the variables of two modules that implement the same feature must be distinct, since the scope is defined by the feature, not the module.

Each time a feature is instantiated, its associated feature modules are instantiated with it. In case the feature module implements a multi-feature, the id keyword refers to the index of the corresponding feature instance. Consider the following example:

feature A
    all of X[2];
endfeature

feature X
    module X_impl;
endfeature

module X_impl
    y : [0 .. 1] init id;
endmodule

The variable y is initialized with the index of the X feature instance, i.e., X[0].y is initialized with 0 and X[1].y is initialized with 1.

Synchronization

Commands can be labeled with actions. Actions can be used to force two or more modules to take their transitions simultaneously, i.e., to synchronize. Actions are placed in the square brackets before a command:

module consumer_impl
    work : [0 .. 3] init 0;

    [dequeue] work = 0 -> (work' = 3);
endmodule

In the above example, the Consumer feature synchronizes with the buffer over the dequeue action to fetch the next work package.

Actions can be indexed similar to arrays using the index operator [ ]. For instance, the above module definition can be changed such that each instance of a Consumer multi-feature has its own dequeue action by using the id as the index:

module consumer_impl
    work : [0 .. 3] init 0;

    [dequeue[id]] work = 0 -> (work' = 3);
endmodule

If a feature is not part of a feature combination, then its modules are not included in the model instance for this feature combination. This means that an inactive feature (or rather, its modules) will not block any of its actions. However, sometimes it is desired that deactivating a feature blocks some or all of its actions. For example, the dequeue action of the Consumer feature should block if the Consumer feature is not in the feature combination. Otherwise, the buffer could execute this action on its own, which effectively drops the work package. Actions that should block are listed after the block keyword in the feature block:

feature Consumer
    block dequeue[id];

    modules consumer_impl;
endfeature

Parametrization

Similar to features, modules can be parametrized. For example, a buffer implementation can be parametrized by the buffer size:

module buffer(capacity)
    cell : array [0..capacity - 1] of bool init false;

    // ...
endmodule

Arguments are provided upon instantiation of the module in a feature block:

feature SmallBuffer
    modules buffer(2);
endfeature

A features’ parameters can be used as arguments as well:

feature Buffer(capacity)
    modules buffer(capacity);
endfeature

Meta-programming

ProFeat provides the for loop construct to generate sequences of commands, stochastic updates, variable assignments and expressions. Consider the following example of the buffer module, which implements a FIFO buffer with parametrized capacity:

module buffer(capacity)
    cell : array [0..capacity - 1] of [-1..MAX_WORK] init -1;

    for c in [0..2]
        [dequeue[c]] cell[0] != -1 ->
            (cell[capacity-1]' = -1) &
            for i in [0..capacity-2]
                (cell[i]' = cell[i+1])
            endfor;
    endfor
endmodule

The outer for loop generates a command for each instance of the Consumer multi-feature. The inner loop then shifts the work items in the buffer upon dequeuing an item.

If the for construct is used in an expression, the loop body must contain exactly one ... placeholder. Intuitively, the placeholder is the position where the expression generated by the remaining iterations is inserted. Consider the following expression containing a for loop:

for i in [1..4] i + ... endfor

In the first iteration, this expression is expanded to:

1 + for i in [2..4] i + ... endfor

Unfolding the loop completely yields the expression:

1 + (2 + (3 + 4))

Note

The placeholder ... can only be used with the operators +, -, *, & and | as well as the functions min and max.