makina

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