{"slug":"tla","domain":"documents","title":"TLA+ model checked by TLC","summary":"A business or a system written as a TLA+ module, checked by TLC: every state its steps can reach, each rule that breaks with its shortest trace, and the rules that hold.","help":"tla: a TLA+ model checked by TLC.\n\nUSAGE\n  tla check Name.tla [OTHER.tla ... | Name.cfg] [--json]\n\nCHECK\n  Runs SANY and TLC on the module Name.tla and prints what TLC found: parsed\n  or not (in SANY's own words where not), the states it reached, each\n  invariant that breaks with how many states break it and its shortest\n  trace, and each invariant that holds. TLC searches breadth first, so the\n  trace it gives is the shortest way to the broken rule.\n\n  The config is Name.cfg given beside the module, else a `\\* Name.cfg:`\n  comment block at the end of the module, one config line per comment line:\n\n    \\* Shop.cfg:\n    \\* INIT Init\n    \\* NEXT Next\n    \\* INVARIANTS ShipsAfterQC OneContainerPerPallet\n\n  Other modules the main one EXTENDS go beside it; the standard modules\n  (Naturals, Sequences, FiniteSets, TLC) need not. Write the module under\n  /tmp with a heredoc first. --json prints the checker's answer as it came.\n\n  Exit 0 when every invariant holds; 1 when one breaks or the model does not\n  run. A model is checked while you wait: TLC stops at 90 seconds, so keep\n  the state space small (a few customers, a few pallets).\n\n  It is the same check a workbook holding a TLA+ module gets after every\n  edit, and the module /try/business-plan writes for a business runs here\n  as it is.\n\nCOSTS\n  Free.","example_command":"tla check /tmp/Shop.tla","example_output":"TLC 1.7.4 · Shop.tla · 1.8 s\n1,204 states generated, 388 distinct, depth 9\n\nBROKEN  ShipsAfterQC — 14 states break it. Shortest trace, 5 steps:\n   1  Initial predicate\n        /\\ order = [o1 |-\u003e \"paid\"]\n   ...\n\nholds   OneContainerPerPallet","cost_class":"upstream-fetch","tier":"free","price_per_1k_calls":0,"price_is_from":false,"status":"available","commands":["tla"],"default_enabled":true,"first_seen":"2026-11-07T03:20:47.875091Z","enabled":false}