.. _sec-modules: 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. .. _sec-module-definitions: 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 :ref:`multiple initial states `. A variable can have one of the following types. ``[ .. ]`` 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 [ .. ] of `` 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 :ref:`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 .. _sec-meta-programming: 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`` :ref:`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``.