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.

It is the one tlacheck. nova-sprint had its own copy (four verbs over its own pkg/tlc); it runs this command instead (go run on this module's tools/tlacheck, at the version its go.mod names), so the case verbs (run, groups, merge, inputs) take any checkout with a tla/CASES.tsv under --root. The table, member, replay and witnesses verbs check this repository's table model.

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