mix tlx.check (TLX v0.5.3)

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 --constant 'quorum=2'
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), emitted as a set: CONSTANT procs = {n1, n2}
  • --constant - Bind a constant to a scalar (repeatable), emitted as CONSTANT quorum = 2. Use this when the spec compares against the constant or does arithmetic on it — TLC can neither order nor add a model value. Overrides a value declared on the constant entity, so a spec can be re-checked at a different bound without editing it.
  • --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.