# Makina Library

Makina is a testing library that provides a DSL (*domain specific
language*) for writing PBT (*property-based testing models*) *models*
for *stateful* systems.

**Note:** the word *model* is used in PBT to refer to
*properties* to be checked on the system under test.

Makina has been designed to address principles of *modularity* and
*model reuse*. Similar to other PBT libraries, Makina uses the Elixir
metaprogramming facilities to generate a model in your favourite PBT
library (like [`PropCheck`](https://github.com/alfert/propcheck.git) or [`eqc_ex`](https://github.com/Quviq/eqc_ex)).

## Using Makina

- Add Makina to your dependencies in `mix.exs`
```elixir
def deps do
    [
        {:makina, "~> 0.2.2"}
    ]
end
```
- Configure your preferred PBT compatible library (e.g. `PropCheck`) in your testing environment config file `config/test.exs`:
```elixir
config :makina, checker: PropCheck
```

## Write your model

To write your tests you will need to write a model. Let's assume you
need to test a *counter system*, i.e. a module `Counter` with
functions `put`, `ìnc` and `get`. A *model* of such of a system is:

```elixir
defmodule Counter.Model do
  use Makina, implemented_by: Counter

  state value: 0 :: integer

  invariants greater_than_0: value >= 0

  command inc :: :ok | :error do
    next value: value + 1
  end

  command put(n :: integer) :: :ok | :error do
    args n: integer(0, :inf)
    next value: n
  end

  command get() :: integer do
    post result == value
  end
end
```

## Write the test

The *boilerplate* to write the *property* is like this:

```elixir
defmodule MakinaExamplesTest do
  use PropCheck
  use ExUnit.Case, async: true

  describe "Counter" do
    property "Correctness" do
      forall cmds <- commands(Counter.Model.Behaviour) do
        {:ok, _pid} = Counter.start_link(0)
        r = {_, _, result} = run_commands(model, cmds)
        Counter.stop()

        (result == :ok)
        |> when_fail(print_report(r, cmds))
        |> aggregate(command_names(cmds))
      end
    end
  end
end
```