The PlusCal Algorithm Language

Last modified 27 April 2015

Contents
   What is PlusCal?
   Obtaining PlusCal
   Papers About PlusCal
   Version History
   The Specification of the Translator

What is PlusCal?

PlusCal (formerly called +CAL) is an algorithm language based on TLA+. A PlusCal algorithm is translated to a TLA+ specification, which can be checked with the TLC model checker.

An algorithm language is for writing algorithms, just as a programming language is for writing programs. The introduction to the PlusCal manual (see below) explains how algorithms differ from programs, and how PlusCal differs from programming languages.

Obtaining PlusCal

PlusCal has two syntaxes. Most users will prefer the C-syntax, which is closer to that of C-based languages like C# and Java. There is also a P-syntax that uses begin/do and end instead of the braces { and }. There are separate versions of the manual for the two syntaxes, which are briefly compared in both versions.

Click HERE to download the c-version of the manual.

Click HERE to download the p-version of the manual.

Click HERE to download a TLA+ specification of the PlusCal to TLA+ translation.

The PlusCal translator is available as part of the TLA+ tool set.

Papers About PlusCal

The following papers about PlusCal and its use are available:

Version History

Version 1.6 of July 2011
- The translator now adds the BEGIN/END TRANSLATION comments.
- The translator was modified to support the Toolbox's Goto PCal Source command.

Version 1.6 of July 2011
- Small change to the syntax for specifying fairness.
- Previously defined macros may now be called inside a macro definition.

Version 1.5 of March 2011
- Added a new way of specifying fairness, with:
    * A fair keyword and + modifier for specifying weak and strong process fairness.
    * + and - label modifiers for adjusting an atomic action's fairness.
- Improved the TLA+ translation to:
    * Eliminate the pc variable if it's obviously unnecessary.
    * Eliminate stuttering-on-termination when obviously never executed.
- Added a -version option for maintining backwards compatability.

Version 1.4 of June 2010
- Added the options statement and the -lineWidth option.

Version 1.3 of February 2008
- Added await as a synonym for when.

Version 1.2 of August 2007
- Introduced defaultInitValue for uninitialized variables.

Version 1.1 of October 2006
- Added several options, including ones for adding missing labels.
- Added the c-syntax.

The Specification of the Translator

The heart of the PlusCal to TLC+ translation is formally formally specified in TLA+ by the file PlusCal.tla, which you can download by clicking HERE. The translator option “-spec PlusCal” causes the TLA+ translation to be produced by having TLC execute this specification on the input. However, this method of performing the translation does not preserve the formatting of expressions, so it does not work if the meaning of an expression depends on proper indentation. Moreover, the resulting TLA+ translation is hard to read. The TLA+ specification has not been updated to reflect changes made to the language in Version 1.5. To use the specification, you must specify the -version 1.4 option. (The -writeAST option does not work in the Toolbox.)

This page can be found by searching the Web for the 21-letter string uidlamportpluscalhomepage. Please do not put this string in any document that could wind up on the web--including email messages and Postscript and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamportpluscalhomepage".