tlacheck

Overview ¶

Command tlacheck runs the TLA+ model checks of this repository: the declared cases of tla/CASES.tsv with their run records, the table model's suites, the replay of the table model's findings against a table.lua, and the execution replay of table.lua receipts against EpochMemberTable.

It is a bench tool: TLC needs java, the replays need redis-server, and the runs are bounded (docs/SPEC-CI.md, the tlc job). Run it on a bench, never on a working machine. The reading of TLC's results and the suites live in pkg/tlc and internal/tablemodel; this file is the command line.

example:
  tlacheck groups --root .
  tlacheck run --root . --jar /path/to/tla2tools.jar --dir /tmp/tlc-out --group tablefirstcontact
  tlacheck run --root . --dir /tmp/tlc-bench --bench any