# Tla Symbols

> This skill extracts symbols (constants, variables, operators) from a TLA+ specification and generates a TLC configuration file. It should be used when the user asks to "generate config", "create cfg file", "no config file", "what's in my spec", "extract symbols", "generate .cfg", "list symbols", "show constants", "show variables", "set up TLC config", "prepare for model checking", "show operators", "analyze my spec", "what constants does my spec have", "what variables are defined", "what operators are in my spec", "include extended modules", "symbols from imported modules", "help me create a config", "set up model checking config", or needs a .cfg file for model checking.

- Skill: `photoszzt/tla-symbols` (Agent Skill)
- Install (CLI): `npx skillmds@latest add photoszzt/tla-symbols`
- Raw SKILL.md: https://api.skillmd.com/api/skills/photoszzt/tla-symbols/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: photoszzt (https://skillmd.com/u/photoszzt)
- Updated: 2026-09-10
- Page: https://skillmd.com/skills/photoszzt/tla-symbols

---


# Extract Symbols and Generate Config

Extract symbols (constants, variables, operators) from a TLA+ specification and generate a TLC configuration file.

**IMPORTANT: Always use the MCP tools listed above. Never fall back to running Java or TLC commands via Bash.**

## Usage

Preferred (always works):

```
/tla-symbols test-specs/Counter.tla
/tla-symbols test-specs/Counter.tla --extended
```

Both forms work identically. See `skills/shared/path-normalization.md` for path normalization rules.

## What This Does

1. Validates and normalizes the spec path from the argument
2. Calls `mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_sany_parse` to check for syntax errors
3. Calls `mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_sany_symbol` to extract symbols
4. Generates a `.cfg` file with best-guess configuration

## 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 Spec**

Call `mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_sany_parse` with `fileName=<spec_path>`

If parse errors exist, print them and exit.

**Step 4: Extract Symbols**

Determine `includeExtendedModules`:

- If the argument contains `--extended`, set to `true`
- Else set to `false`

Call `mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_sany_symbol` with:

- `fileName=<spec_path>`
- `includeExtendedModules=<flag>`

If the symbol extraction fails or returns an error, print the error message and exit. Do not proceed to config generation with incomplete data.

**Step 5: Generate Config File**

From the symbol extraction result (SymbolExtractionResult schema):

Determine output filename:

- Extract spec name from path (e.g., `Counter.tla` -> `Counter`)
- If `<SpecName>.cfg` does NOT exist: write to `<SpecName>.cfg`
- Else: write to `<SpecName>.generated.cfg`

Generate config content following this template:

```cfg
\* TLC Configuration for <SpecName>
\* Generated by /tla-symbols
\*
\* To run model checking:
\*   /tla-check <spec> <this-cfg>

<BEHAVIOR_SPEC>

<INVARIANTS>

<PROPERTIES>

<CONSTANTS_STUBS>
```

Where:

**BEHAVIOR_SPEC** (use bestGuess, never invent):

- If `bestGuess.spec` exists: `SPECIFICATION <bestGuess.spec.name>`
- Else if `bestGuess.init` AND `bestGuess.next` exist:
  ```
  INIT <bestGuess.init.name>
  NEXT <bestGuess.next.name>
  ```
- Else:
  ```
  \* INIT <TODO>
  \* NEXT <TODO>
  \* SPECIFICATION <TODO>
  \* Run /tla-parse and inspect operators; update cfg accordingly.
  ```

**INVARIANTS** (use bestGuess.invariants, never invent):

- For each inv in `bestGuess.invariants`: `INVARIANT <inv.name>`
- If empty: omit

**PROPERTIES** (use bestGuess.properties, never invent):

- For each prop in `bestGuess.properties`: `PROPERTY <prop.name>`
- If empty: omit

**CONSTANTS_STUBS** (use candidates.constants, never invent values):

- If `candidates.constants` is non-empty, emit commented stubs:
  ```
  \* Constants detected by SANY; TLC requires concrete assignments before model checking.
  \* Example: CONSTANT Max = 10
  \*
  \* CONSTANT <ConstName> = <TODO>
  ```
  (Repeat last line once per constant)
- If empty: omit

**Step 6: Write File**

Use Write tool to create the config file.

Print `CFG written: <filename>`

**Step 7: Advise User**

Print:

```
Next steps:
1. Edit <cfg-file> to assign constant values
2. Run: /tla-smoke <spec> <cfg-file>
3. Fix any TLC errors
4. Run: /tla-check <spec> <cfg-file>
```

## Example Output

```
Spec path: test-specs/Counter.tla
Parse successful
Symbols extracted

Symbols found:
  Constants: MaxValue
  Variables: count
  Init: Init
  Next: Next
  Spec: Spec
  Invariants: TypeInvariant, BoundInvariant

CFG written: test-specs/Counter.cfg

Next steps:
1. Edit test-specs/Counter.cfg to assign constant values
2. Run: /tla-smoke test-specs/Counter.tla test-specs/Counter.cfg
3. Fix any TLC errors
4. Run: /tla-check test-specs/Counter.tla test-specs/Counter.cfg
```