pcal_translate
Translates PlusCal algorithms embedded in TLA+ files into TLA+ by updating the file in-place between translation markers.
Instructions
Translate PlusCal algorithm embedded in a TLA+ file to TLA+. Modifies the .tla file in-place by inserting/updating the TLA+ translation between the * BEGIN TRANSLATION and * END TRANSLATION markers.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla file containing PlusCal code | |
| fairness | No | Fairness condition: wf (weak), sf (strong), wfNext (weak on Next), nof (none) | nof |
| termination | No | Add termination detection to the spec | |
| no_cfg | No | Do not generate a .cfg file | |
| label | No | Add missing labels automatically | |
| line_width | No | Line width for the translation output | |
| output_file | No | Optional. If provided, raw pcal.trans output is written to this file and the response contains output_file instead of raw_output. (Note: this is the raw TRANSLATOR output — the translated TLA+ spec is always written in-place to tla_file, reported as translated_file.) |