Skip to main content
Glama
richashworth

tlaplus-mcp

by richashworth

tla_state_graph

Load and parse TLC state graph files into structured JSON, adjacency lists, or raw DOT for exploration, including violation traces and invariants.

Instructions

Load a TLC-generated DOT state graph file and return it in a structured format for exploration. Supports raw DOT, simplified adjacency list, or full JSON format with disambiguated actions, invariants, and violation traces.

Input Schema

TableJSON Schema
NameRequiredDescriptionDefault
dot_fileNoAbsolute path to the .dot state graph file generated by TLC (not needed in traces_only mode)
cfg_fileNoAbsolute path to the .cfg file (for invariant/property names)
tlc_output_fileNoAbsolute path to the TLC output file (for violation traces)
tlc_outputNoRaw TLC output string (for violation traces). If both tlc_output and tlc_output_file are provided, tlc_output takes precedence.
formatNoOutput format: 'dot' (raw), 'structured' (adjacency list), or 'json' (full structured output with states, transitions, violations, happy paths)json
traces_onlyNoWhen true, build a minimal graph from TLC output traces alone (no DOT file needed). Returns partial: true.
output_fileNoWrite JSON to this file (REQUIRED for json format) instead of returning it inline. Response will contain a compact summary. Must be omitted for dot/structured formats.
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations are provided, so the description must fully convey behavioral traits. It states it loads a DOT file and returns structured data, but omits details like error handling, file size limits, or performance implications. Minimal behavioral context beyond the basic operation.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two concise sentences covering action and format options. No wasted words; front-loaded with the core purpose.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

With 7 parameters, no output schema, and no annotations, the description is sparse. It does not explain the structure of returned data (e.g., what 'structured format' entails) or how modes like 'traces_only' and 'output_file' affect the response. Incomplete for a tool with this complexity.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, so baseline is 3. The description adds no extra semantics beyond the schema's parameter descriptions; it lists formats but does not elaborate on parameter interactions or constraints.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the action ('load a TLC-generated DOT state graph file and return it in a structured format') and distinguishes the tool from siblings like tlc_check or tlc_simulate by focusing on state graph exploration. It specifies supported formats (dot, structured, json) and mentions disambiguated actions, invariants, and violation traces.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No explicit guidance on when to use this tool versus alternatives (e.g., tlc_coverage or tlc_simulate). The description implies usage for state graph exploration, but does not provide when-not-to-use or contrast with sibling tools.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Install Server

Other Tools

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/richashworth/tlaplus-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server