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 or eqc_ex).

Using Makina

• Add Makina to your dependencies in mix.exs

  def deps do
    [
        {:makina, "~> 0.3.2"}
    ]
  end

• Configure your preferred PBT compatible library (e.g. PropCheck) in your testing environment config file config/test.exs:

  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:

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:

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