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

at the statement labeled enter , it will eventually access its critical section. 2 Lo-
cal properties of single processes may also be stated after the code section of
processes; they are verified for every instance of the corresponding process type.
The instance section of a PlusCal program determines the finite instance
of the model that will be verified by the model checker tlc. In particular, the
user must specify concrete values for all constants that have been declared in the
header section. In our example, we instantiate the constant parameters N and
maxClock by 3 and 5. This section may also contain other declarations that are
interpreted by tlc. In particular, we define a constraint that bounds the state
space for model checking by considering only such states where no clock value
exceeds maxClock .

3.2 PlusCal Statements

The syntax of PlusCal resembles that of a standard imperative programming
language, but adds non-deterministic constructs, which are useful for modeling.
The expressions of PlusCal are just TLA + expressions. By focusing on high-
level abstractions such as sets and functions, users are encouraged not to commit
to any particular implementation early. We have found that algorithm designers
quickly learn how to write TLA + expressions. This section introduces the key
statements of PlusCal.
Basic statements include assignments and the skip statement, which has no
effect. Statements can be labeled (cf. the labels ncrit , try etc. in Fig. 2). Lam-
port's PlusCal introduced the key idea that labels define the atomic unit of
execution of a PlusCal model: a group of statements appearing between two
labels is executed atomically, without interleaving by other processes. For exam-
ple, reception and processing of a message is modeled as being atomic in process
Communicator of Fig. 1. However, the compiler sometimes introduces additional
labels when translating to TLA + . For example, the first statement appearing
inside a loop or statements following a procedure call must be labeled. Our com-
piler adds any required labels, but since every label creates an additional point
of interleaving, we have added an atomic statement to PlusCal,whichwasnot
present in Lamport's language.

atomic B end atomic

The statements B in this form are executed (pseudo-)atomically, even if they
contain labels. tlc can be used to find deadlocks caused by statements inside
an atomic block being non-executable.
Case distinction is expressed by a standard if statement. There is also a when
statement that blocks until the specified condition becomes true. Less conven-
tionally, the statement

either B 1 or ... or B n end either

2 The TLA + formula P Q asserts that every state satisfying predicate P

will

eventually be followed by a state satisfying predicate Q .