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+.