mix tlx.check (TLX v0.5.2)

Copy Markdown

Emit a TLA+ spec and run TLC model checker.

Usage

mix tlx.check MyApp.MySpec
mix tlx.check MyApp.MySpec --tla2tools path/to/tla2tools.jar
mix tlx.check MyApp.MySpec --model-values 'procs=n1,n2'
mix tlx.check MyApp.MySpec --no-deadlock

When the spec declares refines, the abstract modules it instantiates are emitted alongside it so TLC can resolve the INSTANCE references. This is applied transitively — an abstract spec that itself refines another spec pulls in that module too.

Options

  • --tla2tools - Path to tla2tools.jar
  • --model-values - Comma-separated model values per constant (repeatable)
  • --workers - TLC worker threads (default: auto)
  • --no-deadlock - Disable TLC deadlock checking. Useful for specs with terminal states, where having no successor is intended rather than a bug.