PlusCal is an algorithm language based on TLA+. A PlusCal algorithm is written as a comment in a TLA+ module. 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 Control+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 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.)