TLX.Simulator (TLX v0.5.2)

Copy Markdown

Random walk state exploration for TLX specs.

Evaluates guards and transitions in Elixir without TLC, checking invariants at each state. Useful for fast development feedback.

Summary

Functions

Run random walk simulations on a compiled spec module.

Functions

simulate(module, opts \\ [])

Run random walk simulations on a compiled spec module.

Options:

  • :steps — max steps per run (default: 100)
  • :runs — number of random walks (default: 1000)
  • :seed — random seed for reproducibility

Returns {:ok, stats} or {:error, violation, trace}.