TLA+ Mode
(1)
The code in this section is taken from the specification of a distributed banking system, which is written in the variant of tTLA+ and originally derived from a previous version of Lamport's Introduction to TLA+.