Information Technology Reference
In-Depth Information
can be used to express non-deterministic choice between
n
possible branches. In
fact, the
if
,
when
,and
either
constructs are just special cases of the primitive
form
branch
P
1
then
B
1
P
2
then
B
2
...
P
n
then
B
n
else
B
end branch
inspired by Dijkstra's guarded commands [3]. The first
n
branches consist of a
condition
P
i
and a block of statements
B
i
, the final
else
branch is optional. The
effect of a
branch
statement is to non-deterministically choose some
i
such that
P
i
evaluates to true and execute the corresponding block
B
i
.Ifno
P
i
is true
then the
else
branch is executed if it is present, otherwise execution blocks (and
another process may be executed).
Non-deterministic choice over the elements of a set (rather than a fixed number
of alternatives) is expressed by the statement
with
x
∈
S
do
B
end with
which executes the statements
B
for some element of the set
S
, and blocks if
S
is empty. Since the expression
S
may contain program variables, executing the
code of other processes may unblock a
with
statement.
PlusCal offers three iteration constructs. Beyond the standard
while
loop
while
P
do
B
end while
which is already present in Lamport's PlusCal, we added the statement
loop
B
end loop
for expressing infinite loops; this simply abbreviates
while
true
do
B
.More
importantly, we added a loop of the form
for
x
∈
S
do
B
end for
for iterating over the elements of a set
S
.(Incontrast,the
with
statement men-
tioned above executes its body for a single, nondeterministically chosen element
of
S
.) The order in which the elements of
S
are processed is unspecified but
fixed. Exploring only one iteration order helps mitigate state space explosion,
but the correctness of the algorithm should not depend on any particular order.
3
We extended PlusCal by the ability to express fairness assumptions for
algorithms inside the language rather than through TLA
+
formulas that the user
must add to the generated model. Fairness assumptions are fundamental for the
3
We plan to add a compile-time option to a future version of the PlusCal compiler
that will cause the model checker to explore all possible iteration orders.
Search WWH ::
Custom Search