2.3 KiB
| description | allowed-tools | ||||
|---|---|---|---|---|---|
| Run the TLC model checker on the formal specification |
|
FormSpec Verify
You are running the TLC model checker on the existing TLA+ specification and reporting results. This command is read-only — it does not modify any spec files.
Steps
1. Validate preconditions
Check that both files exist:
spec/formal/System.tlaspec/formal/System.cfg
If either is missing, tell the user to run /formspec.formalize.2 first and stop.
2. Run TLC
If spec/hooks/run-checks exists and is executable, delegate verification to it instead of running TLC locally (see /formspec.init for the hook interface). Build the request from spec/formal/traceability.md (properties and their types) and spec/formal/System.cfg (the TLC invocation hint). Present the returned results to the developer, including any dashboard URLs.
If the hook does not exist or fails, run TLC locally:
tlc spec/formal/System.tla -config spec/formal/System.cfg -workers auto -metadir /tmp/tlc-states -cleanup
Run from the project root directory. The -metadir flag directs TLC's working state files to a temporary directory, and -cleanup removes them after a successful run. Use a 5-minute timeout by default. If TLC does not complete within this limit, stop it and report the partial state (states explored so far, queue size). If the developer expects and accepts a longer runtime, the timeout may be extended — but beyond 15 minutes, always alert the developer and wait for confirmation before continuing.
3. Parse and report
Read the TLC output (or hook response) and produce a structured report:
Summary:
- States explored / distinct states
- Duration
- Overall result: PASS or FAIL
- Dashboard URL (if provided by hook)
Property results (table format):
| Property | Type | Result |
|---|---|---|
| Name | invariant/temporal | PASS/FAIL |
For any violation, include:
- The counterexample trace, simplified into domain language
- If
spec/formal/traceability.mdexists, map the violated property back to its design requirement and include that reference
4. No modifications
Do not modify System.tla, System.cfg, traceability.md, or any other file. This command is purely diagnostic. If violations are found, advise the user to run /formspec.formalize.2 to address them.