The PlusCal Algorithm Language

Last modified 2 January 2009

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.

New in Version 1.1

Several options have been added with Version 1.1. The two most important are:

You can let the translator add missing labels. In particular, if you omit all labels from a sequential algorithm, then the translator will act as if the necessary labels were there.
There are now two alternate syntaxes: the original, somewhat prolix p-syntax and a new, more compact c-syntax. The c-syntax is closer to that of C-based languages like C# and Java, using braces { and } instead of begin/do and end. There is a separate version of the manual for each syntax; the two syntaxes are briefly compared in both versions.

Obtaining PlusCal

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

Click HERE to download the c-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:

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.

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".