tla-reviewlisted

# TLA+ Specification Review Run a comprehensive review of your TLA+ specification including parsing, symbol extraction, smoke testing, and best practices checklist. **IMPORTANT: Always use the MCP tools listed above. Never fall back to running Java or TLC commands via Bash.** ## Usage ``` /tla-review test-specs/Counter.tla /tla-review test-specs/Counter.tla test-specs/Counter.cfg /tla-review test-specs/Counter.tla --no-smoke ``` **Note:** If you typed `@path.tla` as the first argument, this skill strips the leading `@` and validates the file exists. ## What This Does 1. Validates and normalizes the spec path from the argument 2. Runs SANY parser to check syntax and semantics 3. Extracts symbols to analyze spec structure 4. Runs smoke test (unless `--no-smoke` flag present) 5. Generates comprehensive review report with recommendations ## Implementation **Step 1: Normalize Spec Path** Take the spec file path provided as the argument to this skill. If it starts with `@`, strip the leading `@`. Print `Spec path: <spec_path>` **Step 2: Validate File** - Check path ends with `.tla` - Use the Read tool to verify the file exists on disk - If validation fails, print error and exit **Step 3: Parse Flags** Extract flags from the argument: - `--no-smoke`: Skip smoke test (default: smoke enabled) **Step 4: Determine CFG Argument** Parse the second token from the argument (split by space, take second). If it ends with `.cfg`, treat it as the CFG_ARG. **Step 5: Run SANY Pa