# 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<sup><a id="fnr.1" class="footref" href="#fn.1" role="doc-backlink">1</a></sup> executable, Makina should
be configured with a compatible property-based testing library like [PropCheck](https://github.com/alfert/propcheck.git):

    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<sup><a id="fnr.2" class="footref" href="#fn.2" role="doc-backlink">2</a></sup>.


# Footnotes

<sup><a id="fn.1" href="#fnr.1">1</a></sup> examples of models can be found [here](https://gitlab.com/babel-upm/makina/makina-examples)

<sup><a id="fn.2" href="#fnr.2">2</a></sup> examples of properties using PropCheck can be found [here](https://gitlab.com/babel-upm/makina/makina-examples/-/blob/master/test/makina_examples_test.exs)