Output Formats

Specl supports several output formats for integration with other tools.

Default (text)

Human-readable output. This is the default.

specl check spec.specl -c N=3

Machine-readable JSON output.

specl check spec.specl -c N=3 --output json

Useful for CI pipelines, scripts, and programmatic analysis of results.

Apalache-compatible trace format.

specl check spec.specl -c N=3 --output itf

This produces traces in the ITF format used by the Apalache model checker, enabling interoperability between tools.

Generates Mermaid sequence diagrams from violation traces.

specl check spec.specl -c N=3 --output mermaid

The output can be pasted into any Mermaid-compatible renderer (GitHub markdown, Mermaid Live Editor, etc.) to visualize the sequence of actions.

Generates a full state graph in DOT format.

specl check spec.specl -c N=2 --output dot

Only practical for small state spaces (< 100 states). Render with:

specl check spec.specl -c N=2 --output dot | dot -Tpng -o states.png

Not an output format per se, but --diff modifies the default text output to show only changed variables in each trace step:

specl check spec.specl --diff

Useful for specs with many variables where full state dumps are hard to read.

--profile adds per-action firing counts and timing to the output:

specl check spec.specl -c N=3 --profile