Advanced Commands

Beyond specl check, the CLI provides several additional commands.

`specl info` — spec analysis

Analyze a spec without running the full model checker:

specl info spec.specl -c N=3

Reports actions, variables, constants, state space characteristics, and which optimizations apply.

Estimate the state space size and required resources before committing to a full run:

specl estimate spec.specl -c N=3

Generate random execution traces without exhaustive exploration:

specl simulate spec.specl -c N=3

Useful for quick smoke testing and understanding system behavior before running the full checker.

Check all .specl files in a directory using // Use: comments embedded in each file:

specl test examples/

Each spec file contains a comment like:

// Use: specl check this.specl -c N=2 --no-deadlock

The test command reads these comments and runs each spec with the specified flags. Useful for CI and regression testing.

Quick syntax and type check without running the model checker:

specl lint spec.specl

Catches parse errors and type errors without exploring any states.

Format a spec file:

specl format spec.specl --write    # format in place
specl format spec.specl            # print formatted output to stdout

Re-run the check automatically when the file changes:

specl watch spec.specl -c N=3

Convert a TLA+ specification to Specl:

specl translate spec.tla -o spec.specl

See TLA+ Comparison for details on the translation.