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

3 Introducing a New Version of PlusCal

We now present in some more detail the main features of our version of PlusCal
and describe its compilation to TLA + .Fromnowon,PlusCal will denote our
version, except if explicitly stated otherwise.

3.1 Structure of an Algorithm

Figures 1 and 2 show a model of Lamport's mutual exlusion algorithm [6] in
PlusCal. This is a basic distributed algorithm and shows some of the main
ingredients of the language.
The header section indicates the name of the algorithm and lists any TLA +
modules to be imported (“extended”). These modules contain definitions of op-
erators that are used within the algorithm. Algorithm LamportMutex imports
the modules Naturals and Sequences from the TLA + standard library. Global
constant parameters ( N and maxClock in our example) are also declared in the
header section; these will later be instantiated to obtain a finite-state instance
for verification.
The following declaration section contains declarations of global variables,
procedures, and definitions. As in TLA + , variables are untyped. A variable dec-
laration may provide an initial value. In our example, we declare a global variable
network as a two-dimensional array indexed by elements of the site Site ,which
contains the identities of the processes of type Site , declared below. The variable
network represents the communication network; more precisely, network[from][to]
is a queue of messages sent from site from to site to , initially empty (

denotes
the empty sequence in TLA + ). The operators send and broadcast , defined next,
model point-to-point and broadcast communication over the network. Specifi-
cally, send computes the network obtained by sending a single message between
two processes 1 ,and broadcast computes the state of the network after site from
sends a message to all sites.
The main part of a PlusCal program consists of the process section ,which
introduces the processes that participate in the algorithm. Programs can declare
any number of process types, and processes can be nested. Since we are mainly
interested in finite-state model checking, all process instances are created at
initialization time and we do not provide a mechanism for process activation
at run time. In the example, we declare that N processes of type Site will be
run, each containing one instance of process Communicator . Processes may be
declared as being fair ; for example, we assume (weak) fairness for each instance
of process Communicator . Each process contains declarations of local variables,
procedures or definitions analogously to the global declaration section. These
declarations are properly scoped and visible only within the enclosing process. In
our example, process Site declares variables clock , reqQ ,and acks that represent
the value of its logical clock, the sequence of requests it has received (which will
be ordered by timestamp), and the set of acknowledgements it has received for

1 The short-hand @ denotes the current value of the array cell being assigned to.