tla_evaluate
Evaluate constant TLA+ expressions by running TLC to compute and output the result, enabling quick checks of expressions without writing full specifications.
Instructions
Evaluate a constant TLA+ expression using TLC. Creates a temporary spec that prints the result of the expression.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| expression | Yes | TLA+ expression to evaluate (e.g., '1 + 2', '{1,2,3} \\union {4,5}') | |
| imports | No | Modules to EXTEND (e.g., ['Integers', 'Sequences']). Defaults to ['Integers', 'Sequences', 'FiniteSets', 'TLC'] | |
| output_file | No | Optional. If provided, raw TLC output is written to this file and the response contains output_file instead of raw_output. |