ExTLA.Simulation (ExTLA v0.6.0)

Copy Markdown View Source

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.

Summary

Types

config()
coverage_report()
result()

Functions

replay(module, messages, config \\ %{})

Drive module through an explicit list of concrete messages.

run(module, config \\ %{})

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

run_trace(module, config \\ %{})

One trace, with the abstract behaviour it produced.

Types

config()

@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()

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

result()

@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()
}

Functions

replay(module, messages, config \\ %{})

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(module, config \\ %{})

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(module, config \\ %{})

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.