Makina (Makina v0.3.2)

This module provides the macros needed to write Makina models. After macro expansion the resulting models are property-based testing state machines compatible with the main property-based testing libraries: PropCheck or eqc_ex.

Writing a model

After importing the library and configuring the project you can start writing Makina models. A Makina model must be defined inside an Elixir module. To start writing a model you need to import the DSL using the use macro:

defmodule ModelExample do
  use Makina
  ...
end

Once the library is imported you can start defining your model. A Makina model is composed by two main parts: a state and some commands that interact with the state. Makina provides the macros state and command for this purpose.

Writing the model state

Only one call to state is allowed in each model. This macro supports the following syntax:

state attribute_name: initial_value :: type, ...

where:

attribute_name could be any atom.
initial_value could be any Elixir expression.
type could be any valid Elixir type. Type definitions are optional, but recommended.

Writing the model commands

Any number of command definitions is allowed in a Makina model. To write a command, Makina provides the command macro. This macro supports the following syntax:

command command_name(argument :: type, ...) :: return_type do
  # callbacks
  ...
end

where:

command_name is the name of the command and could be any supported function name.
type and return_type could be any valid Elixir type. Type definitions are optional, but recommended.

Inside the command block the user must write the callbacks that specify the behaviour of the model. In command definitions callbacks do not need any arguments, these are automatically inserted during macro expansion. Makina commands allow the definition of the callbacks:

pre is the predicate that should be satisfied to call the command. In this callback all model state attributes are accessible.
args is the function that generates the arguments necessary to perform the test call. It can access the state attributes of the model
valid_args is a predicate used during shrinking. Checks whether a command can be called after some elements of the trace are removed. It can access the state attributes and the generated arguments.
valid this predicate can be used to check if a generated call is valid and therefore is going to modify the state of the model. It can access the state attributes and the generated arguments. The result of valid can be accessed in next and post.
call is the function that calls the system under test. It can only access the arguments of the command.
next is a function that generates the next state after calling the command. It can access the arguments, the state and the symbolic result.
post is a predicate that must be checked after the command execution. It can access the state, the command arguments and the result of the command execution.

When writing a command, callbacks pre, valid_args, next or post can be omitted. If omitted, the default implementation of the predicates pre, valid_args and post is true and the default implementation of next is the identity function. When the command does not receive any arguments, the implementation of args can be omitted. The remaining callbacks need to be obligatorily provided by the user.

There is a way to provide a default implementation of call using the option implemented_by in the module configuration:

defmodule ModelExample do
  use Makina, implemented_by: Implementation
  ...

  command command ...
end

With this option enabled, if the module Implementation contains a function with the name command, the default implementation of call will be delegated to the function defined in Implementation.

Extending a model

Models in Makina can be refined and extended using the built-in extension mechanism provided by the library. To extend a model A with some new behaviour in a model B, we need to write a new model B which extends A. The following option must be used for this purpose:

defmodule B do
  use Makina, extends: A
  ...
end

When a model B extends a model A the resulting state is the union of attributes defined in A and B. If a state attribute appears with the same name in A and B, the attribute in B overrides the definition in A.

In the same way, the resulting commands are the union of commands defined in A and B. If an attribute appears both in A and B:

pre, valid_args, valid and post are conjunctive.
call is overridden by the implementation in B.
next and args are the merge of the arguments and the updates in A and B respectively. Updates and arguments in B are prioritized.

In all these callbacks the implementation inherited from the model A can be accessed in the model B using the function super(). The super() function can optionally provided with the implicit arguments in each callback:

pre and args can access super(state).
valid_args and valid can access super(state, arguments).
call can access super(arguments).
next and post can access super(state, arguments, result).

Composing models

Models in Makina can also be composed into a new model using the built-in parallel composition mechanism provided by the library. To compose the models A0, … , AN into a new model B, we need to write a new model B that extends the composition of A0, … , AN. The following syntax is used to achieve this:

defmodule B do
  use Makina, extends: [A1, ... AN]
  ...
end

The list provided to :extends will generate a composed model where the resulting state is the union of all attributes of the models. Commands are also the union of all commands. If the same command appears in more than once:

valid_args, valid and post are conjunctive.
next is the merge of the updates in models [A1, ... AN]
args makes a random choice between the models whose pre callback is true.
pre is disjunctive.
call makes a random choice between the callbacks that implement this callback.

The resulting model B extends the composition of the models A0, … AN, and also can extend the behaviour of this composition by refining or adding new commands or state attributes.

Renaming commands

When a Makina model is extended there is an option that allows command renaming. The syntax is the following:

defmodule B do
  use Makina, extends: A, where: [old_name: :new_name]
  ...
end

This means that the command with the old_name will be visible with the name new_name in module B.