The PlusCal Translator

PlusCal is an algorithm language based on TLA⁺. A PlusCal algorithm is written as a comment in a TLA⁺ module.
Please note: In order to have the editor provide code folding for your PlusCal algorithm, the --algorithm or --fair must be preceded by a (* starting in column 0 on the same or a previous line. If you attempt to insert other comment blocks before the algorithm keyword, but after what you intend to be the start of your PlusCal algorithm 'block', make sure they do not start in column 0. Additionally, the closing comment of the PlusCal algorithm block should be one or more * starting in column 0 and terminating the line with a ).
The PlusCal translator writes the TLA⁺ translation of the algorithm into the module. See the PlusCal web page for more information about PlusCal, including a language manual. An overview of the language is provided by the paper The PlusCal Algorithm Language.

You run the PlusCal translator on the module in the currently selected module editor by clicking on File/Translate PlusCal Algorithm or typing CTRL t / ⌘ t
Translation errors are displayed in the same Parsing Error view where TLA⁺ parsing errors are displayed. Some errors in a PlusCal algorithm are not found by the translator, but instead produce parsing errors in the TLA⁺ module. Those are displayed as ordinary TLA⁺ parsing errors.
The translation produces two checksums which are included in the translation comment delimiters, for example:

\** BEGIN TRANSLATION PCal-5cc64096184dcd2bcb0741a5056a664a
\** END TRANSLATION TLA-6aeb9b3874fd3c001211b4a5b3da8249

If changes are made to the PlusCal code, or generated TLA code, after translation, the user will receive a warning dialog when they attempt to run model checking. If the user would like to make a change to the TLA code and not be warned, they can remove the TLA-... checksum comment text from their spec.

The Goto PCal Source command allows you to jump from a region in the TLA⁺ translation to the PlusCal code that generated it. This makes it easy to find the source in the algorithm of an error found in its translation.

The current version of Pluscal allows you to specify most translator options in an options statement within the module's .tla file. You can also set translator options by opening the Spec Explorer view (see the Manipulating Specs help page), right-clicking on the spec, choosing Properties, and entering the desired options in the PlusCal call arguments field. This is the only way to specify translator options that cannot be put in the options statement. (However, you are unlikely to want to use those options.)

↑ TLA+ Toolbox User's Guide