Makina

Makina is a testing library that provides a domain specific language for writing property-based testing models for stateful programs.

Installation

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

Configuration

In order to make the models¹ executable, Makina 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 basic Makina 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 Makina model you need to import the DSL using the use macro:

defmodule ModelExample do
  use Makina

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

Writing the state definition in a Makina model

Only one call to state 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.

Writing a command in a Makina model

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.

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 that 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.

Writing a property

Finally, once the model is written you need to write a property to execute the tests. We rely this work on the property-based testing library of choice².

Footnotes

¹ examples of models can be found here

² examples of properties using PropCheck can be found here