A High-Level Language for Modeling Algorithms and Their Properties - Formal Methods: Foundations and Applications - page 50

of operations such as the computation of successor (or predecessor) states. Most
model checkers, in particular symbolic ones, support only low-level data types
such as fixed-size integers and records. tlc [14], the model checker for the spec-
ification language TLA + [8], accepts a significant fragment of TLA + ,whichis
based on set theory; it thus provides one of the most expressive and high-level
input languages for model checking. However, TLA + models encode transition
systems via logical formulas, losing much of the (control) structure that is present
in code.
Recently, Lamport introduced the PlusCal algorithm language [9] (originally
called +Cal). While retaining the high level of abstraction of TLA + expressions,
it provides familiar constructs of imperative programming languages for describ-
ing algorithms, such as processes, assignments, and control flow. The PlusCal
compiler generates a TLA + model corresponding to the PlusCal algorithm,
which is then verified using tlc. PlusCal is a high-level language that features
set-based abstractions, non-determinism, and user-specified grain of atomicity;
it emphasizes the analysis, not the ecient execution of algorithms and aims at
bridging the gap that we described above.
Unfortunately, as we discuss in more detail in section 2, use of Lamport's
PlusCal requires good knowledge of TLA + , and even of the translation of
PlusCal to TLA + . Aiming at a simple translation in order to make the re-
sulting TLA + model human readable, Lamport imposed some limitations on
the language that can make it dicult or unnatural to express distributed algo-
rithms. After initial attempts to extend the original language and its compiler,
these limitations motivated us to develop a new version of PlusCal that retains
the basic ideas of Lamport's language but overcomes the shortcomings that we
identified. At the same time, we aim at a translation that enables the use of
reduction techniques and hence more ecient verification.
2 Evaluation of PlusCal
TLA + is a very expressive specification language that emphasizes the use of high-
level constructs such as sets and functions for expressing algorithms. A TLA +
module contains a list of declarations, assertions, and definitions. In particular,
an algorithm is specified as a formula of temporal logic that describes which
executions are permitted. PlusCal retains the logical basis and the expression
language of TLA + , but otherwise resembles a (pseudo) programming language
for multi-process programs, extended by non-deterministic constructs useful for
modeling algorithms. In our experience we found that thinking in terms of sets
is a strong point of PlusCal, as it can make the description of algorithms much
more perspicuous. However, as we explain now, we also identified a number of
shortcomings when trying to use PlusCal for modeling distributed algorithms.
Need to understand TLA + and the compilation. PlusCal models are not fully
self-contained: the algorithm is described in the PlusCal language, but Plus-
Cal can express neither the correctness properties that should be verified nor