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

where vars contains all state variables. Multiple assignments to the same variable
within a group of statements are handled by introducing intermediate let-bound
constants.
User-defined atomic blocks are implemented using a system-wide lock variable
that is acquired at the begin of the block and released at the end. The guards
of actions are strengthened appropriately: actions corresponding to statements
within an atomic block test whether the lock is held by the current process,
the other actions verify that the lock is free. In case some statement within an
atomic block may become non-executable during the execution of the algorithm,
tlc will signal a deadlock during verification.
After generating all actions corresponding to the individual transitions of the
PlusCal model we define the transition relation of a process as the disjunction
of the actions it may execute (including actions occurring within procedures),
and the overall next-state relation as the disjunction of the transition relations
for all process instances, and for the main code section if present. For the example
of Figs. 1 and 2 we obtain

=

Next ∨∃ self ∈ Site : Site ( self )

∨∃ self ∈ Communicator : Communicator ( self )

where Site and Communicator are sets containing the process identifiers of pro-
cesses of type Site and Communicator ,and Site and Communicator are the
actions representing the transitions of these processes. Fairness conditions are
generated from the fairness annotations present in the PlusCal model, e.g.

=

∧∀ ∈

Fairness self Communicator :WF vars ( Communicator ( self ))

∧∀ self ∈ Site : ∧ WF vars ( enter ( self ))

∧ WF vars ( crit ( self ))

∧ WF vars ( exit ( self ))

and the overall specification is obtained as

= Init

LamportMutex ∧ [ Next ] vars ∧ Fairness

Finally, the properties and the instance sections of the PlusCal model are
processed in order to generate the configuration file, which defines the finite-
state instance and indicates the properties to be verified with tlc.

3.4 Comparison with Lamport's PlusCal

The language that we have presented in this paper was inspired by Lamport's
PlusCal, to which it remains close in spirit, but it attempts to overcome some
of the deficiencies that we have identified in section 2. We briefly comment on
what we believe are the main advantages of our language.

Self-contained models. Models written for the original PlusCal language can
express only the algorithm. All additional information, such as fairness assump-
tions, correctness properties or model checking constraints have to be manually