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.

Installation and configuration

Makina can be installed by adding this git repository to your list of dependencies in mix.exs:

def deps do
  [
    {:makina, git: "https://gitlab.com/babel-upm/makina/makina.git", branch: "master"}
  ]
end

In order to make the models executable, the project should be configured with a compatible property-based testing library like PropCheck.

config :makina, checker: PropCheck

Once the project is configured, tests and properties can be written and executed using the default mechanisms provided by the property-based library.

You also need to setup the Makina compilation tracer:

def project do
  [
    elixirc_options: [{:tracers, [Makina.Tracer]}]
  ]

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-a-state-definition

Writing a state definition

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

state attribute_name: initial_value :: type, ...

where:

• attribute_names could be any atom.
• initial_values could be any Elixir expression.
• types could be any valid Elixir type. Type definitions are optional, but recommended.

todo-writing-invariants

TODO Writing invariants

writing-a-command-definition

Writing a command definition

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.
• 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, args, valid_args, call and next in A are overridden by definitions in B.
• post is conjunctive, this means that the predicate defined in B either the predicate in A must be satisfied during execution.

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 should be provided with the implicit arguments in each callback:

• pre and args can access super(state).
• valid_args can access super(state, arguments).
• call can access super/n where n is the number of arguments in the command.
• 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 and post are conjunctive.
• next is the functional composition of the next callbacks of the models. The order of application is taken from the order of the models in the composition.
• 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.