55 lines
2.4 KiB
Markdown
55 lines
2.4 KiB
Markdown
---
|
|
description: Run the TLC model checker on the formal specification
|
|
argument-hint: [property-name]
|
|
allowed-tools: [Read, Glob, Grep, Bash]
|
|
---
|
|
|
|
# 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.tla`
|
|
- `spec/formal/System.cfg`
|
|
|
|
If either is missing, tell the user to run `/formspec.2.formalize` 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.0.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:
|
|
|
|
```bash
|
|
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.md` exists, 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.2.formalize` to address them.
|