Running the Specs

Requires Java and tla2tools.jar. From the specs/ directory:

java -DTLC -cp /path/to/tla2tools.jar tlc2.TLC <SpecName> -config <SpecName>.cfg -modelcheck

Or use the TLA+ VS Code extension.