CLI Reference

Usage

caelum [OPTIONS] [SPEC]
caelum <COMMAND> [OPTIONS] <SPEC>

When no subcommand is given, caelum <spec>.lum is equivalent to caelum check <spec>.lum.

Commands

check

Parse, validate, build the transition system, and check all properties.

caelum check spec.lum
caelum check --format json spec.lum
caelum check --show-trace spec.lum

parse

Parse the specification and report any syntax errors. Does not build the model or check properties.

caelum parse spec.lum
caelum parse --format json spec.lum

fmt

Parse and print the specification in normalized form.

caelum fmt spec.lum
caelum fmt --print-keywords spec.lum
caelum fmt --print-ascii-operators spec.lum
caelum fmt --print-unicode-operators spec.lum

Formatting is idempotent: formatting an already-formatted file produces identical output.

Options

Flag	Description
--format human|json	Output format (default: human)
--show-trace	Display counterexample traces on failure
--dump-graph	Print the reachable transition graph
--max-states N	Limit state exploration (default: 100,000)
--include-path DIR	Additional import search directories
--print-keywords	Format with keyword operators (always, and)
--print-ascii-operators	Format with ASCII operators ([], /\)
--print-unicode-operators	Format with Unicode operators (□, ∧) (default)

Exit Codes

Code	Meaning
0	The specification parsed and all checks passed
1	One or more properties failed
2	Parse error
3	Semantic validation error
4	Import or file loading error
5	Model construction error
6	Internal error

If multiple error classes occur, the earliest pipeline stage determines the exit code.