# `Lockstep.Model`
[🔗](https://github.com/b-erdem/lockstep/blob/v0.1.0/lib/lockstep/model.ex#L1)

A specification of correct sequential behavior for a system under
test. Consistency checkers (`Lockstep.Checker.Linearizable`,
`Lockstep.Checker.SequentialConsistency`) consult a Model to
decide whether a candidate serial order of operations is valid.

A Model has two callbacks:

  * `init/0` — initial state.
  * `step/3` — apply an `(invoke, complete)` operation pair to
    state. Return `{:ok, new_state}` if the completion is
    consistent with the state, or `{:error, reason}` if it isn't
    (e.g. a `:read` returned a value that the model says shouldn't
    be visible).

Models are pure functions of state — no message passing, no IO.
The checker runs them many times under different orderings.

## Built-in models

  * `Lockstep.Model.Register` — read/write/cas register.

## Writing a model

    defmodule Counter do
      @behaviour Lockstep.Model

      def init, do: 0

      def step(n, %{f: :inc}, %{type: :ok, value: result}) do
        if result == n + 1, do: {:ok, n + 1}, else: {:error, :unexpected_inc}
      end

      def step(n, %{f: :read}, %{type: :ok, value: v}) do
        if v == n, do: {:ok, n}, else: {:error, :stale_read}
      end

      # Generic completion handlers
      def step(n, _invoke, %{type: :fail}), do: {:ok, n}
      def step(n, _invoke, %{type: :info}), do: {:ok, n}
    end

# `init`

```elixir
@callback init() :: any()
```

Initial state of the model.

# `step`

```elixir
@callback step(
  state :: any(),
  invoke :: Lockstep.History.Event.t(),
  complete :: Lockstep.History.Event.t()
) ::
  {:ok, any()} | {:error, any()}
```

Apply an `(invoke, complete)` pair to the model state.

Return `{:ok, new_state}` if the completion is consistent with
current state under this model, or `{:error, reason}` if it isn't.

---

*Consult [api-reference.md](api-reference.md) for complete listing*