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:
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
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.)