# `ExTLA.Simulation`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/simulation.ex#L1)

Random walks over the real implementation, checked against the spec at every step.

Where Layer 2 explores every reachable state of the *specification*, this runs the
*implementation* through random message sequences and checks each transition with the
same refinement check the runtime wrapper uses. What that catches, and the model checker
cannot:

- a refinement mapping that is wrong in a state no test happened to reach;
- an implementation bug the abstract model does not contain, because the model does not
  contain the implementation;
- a temporal property that no finite behaviour of the real code satisfies.

## The default generator only offers actions the spec enables

`ExTLA.Simulation.Generator.enabled_only/3`, not `from_spec/3`. The unrestricted generator
asks a different question — *does the implementation refuse what the spec forbids in
this state* — and most servers are not written to. A `handle_call(:done, …)` clause with
no guard of its own accepts `:done` in a state where the spec's `done` is disabled, and
the step check reports `:not_enabled`, correctly: it is a true finding about the pair.
It is also a finding about nearly every server ever written, so hunting it is opt-in.

Pass `message_generator: ExTLA.Simulation.Generator.from_spec(spec, refinement, constants)`
to ask that question deliberately.

## What a simulation is not

It is sampling, not proof. A run that finds nothing has checked the traces it drew, and
`coverage` says which actions those were — a green result over a generator that never
produced `reset` says nothing about `reset`.

## The counterexample it produces is a `ExTLA.Trace`

So a simulation failure can be handed straight back to `ExTLA.Replay.counterexample/3`,
formatted with `ExTLA.Trace.format/1`, or read the same way a model-checker counterexample
is. A finding that arrives in a different shape from the model checker's would be a
second thing to learn for no reason.

# `config`

```elixir
@type config() :: %{
  optional(:traces) => pos_integer(),
  optional(:max_steps) => pos_integer(),
  optional(:message_generator) => (ExTLA.State.t() ->
                                     term() | {atom(), map(), term()} | nil),
  optional(:inject_failures) => boolean(),
  optional(:failure_rate) => float(),
  optional(:seed) => integer() | nil,
  optional(:concurrency) => pos_integer(),
  optional(:init_arg) => term(),
  optional(:timeout) => timeout(),
  optional(:against_graph) => %{graph: term(), status: atom()} | nil
}
```

# `coverage_report`

```elixir
@type coverage_report() :: %{
  actions_hit: %{required(atom()) => non_neg_integer()},
  states_visited: non_neg_integer(),
  invariants_checked: non_neg_integer(),
  actions_covered: float()
}
```

# `result`

```elixir
@type result() :: %{
  status: :ok | :violation | :error | :left_the_graph,
  traces_run: non_neg_integer(),
  total_steps: non_neg_integer(),
  violation: ExTLA.Trace.t() | nil,
  containment: ExTLA.Conformance.finding() | nil,
  detail: String.t() | nil,
  duration_ms: non_neg_integer(),
  seed: integer(),
  restarts: non_neg_integer(),
  coverage: coverage_report()
}
```

# `replay`

Drive `module` through an explicit list of concrete messages.

The reproduction path for a failing simulation whose messages are known, and the way to
write a scenario by hand. `ExTLA.Replay.counterexample/3` is the other direction: from
*abstract* actions through `concrete_message/2`.

# `run`

Run `config.traces` random traces against `module`, stopping at the first finding.

    ExTLA.Simulation.run(MyApp.TransferServer, %{traces: 1000, max_steps: 50, seed: 42})

The seed is always in the result, generated when none was given: a random run that finds
something and cannot be run again has found nothing anybody can act on.

## Options

  * `traces:` — how many traces to run. Default `100`.
  * `max_steps:` — messages per trace. Default `25`.
  * `seed:` — the random seed. Default `nil`, meaning one is generated and reported.
  * `concurrency:` — traces run at once, each against its own server. Default `1`.
  * `init_arg:` — the argument each server starts with, `GenServer.start_link(module,
    init_arg)`. Default `[]`.
  * `timeout:` — how long each message may take to be answered, in milliseconds. Default
    `5_000`.
  * `inject_failures:` — crash and restart the server at random steps, to check recovery.
    Default `false`.
  * `failure_rate:` — the chance of a crash at each step, where `inject_failures:` is on.
    Default `0.1`.
  * `message_generator:` — a function from the abstract state to the next message, or
    `nil` to end the trace. Default: `ExTLA.Simulation.Generator.enabled_only/3`, which
    offers only actions the spec enables; `ExTLA.Simulation.Generator.from_spec/3` offers
    every action.
  * `against_graph:` — `%{graph: graph, status: status}` from `ExTLA.ModelChecker.explore/2`,
    to check that every behaviour stays inside the checker's graph. Default `nil`.

Constants are not an option: the server resolves them from
`config :extla, Spec, constants: %{…}`, and the generator uses the same ones, so passing
`constants:` raises.

# `run_trace`

One trace, with the abstract behaviour it produced.

The behaviour is returned whether or not anything was found, which is what makes this
the debugging entry point: a run that passed and a run that failed are read the same
way.

---

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