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
| Name | Required | Description | Default |
|---|---|---|---|
| dot_file | No | Absolute path to the .dot state graph file generated by TLC (not needed in traces_only mode) | |
| cfg_file | No | Absolute path to the .cfg file (for invariant/property names) | |
| tlc_output_file | No | Absolute path to the TLC output file (for violation traces) | |
| tlc_output | No | Raw TLC output string (for violation traces). If both tlc_output and tlc_output_file are provided, tlc_output takes precedence. | |
| format | No | Output format: 'dot' (raw), 'structured' (adjacency list), or 'json' (full structured output with states, transitions, violations, happy paths) | json |
| traces_only | No | When true, build a minimal graph from TLC output traces alone (no DOT file needed). Returns partial: true. | |
| output_file | No | Write 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. |