Information Technology Reference
In-Depth Information
Fig. 3.
The compilation phases for the new version of PlusCal
where
B
denotes the guarded command corresponding to
B
. Any nested guarded
commands resulting from this translation are subsequently flattened. Procedure
calls and returns are handled using an explicit run-time stack.
This translation may require additional labels, in particular for translating
loops and returns from procedure calls, and the translator adds those as neces-
sary, and signals labels added in this way to the user.
Generation of TLA
+
code.
The final phase of compilation generates the actual
TLA
+
model from the list of guarded commands obtained from the preceding
phase. A guarded command
λ
:
branch
P
1
then
x := t; y[self] := u; pc[self] :=
μ
...
P
n
then
...
end branch
is essentially translated to the TLA
+
action
λ
(
self
) =
∧
pc
[
self
]=
λ
∧∨∧
P
1
∧
x
=
t
∧
y
=[
y
except ![
self
]=
u
]
∧
pc
=[
pc
except ![
self
]=
μ
]
∧
unchanged
vars
\{
x, y, pc
}
∨
...
∨∧
P
n
∧
...
Search WWH ::
Custom Search