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:

\* 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