The state / transition diagram of each RM:

Why is RM a set? In TLA+, every value is a set. Even 42 and “abc” are sets. But TLA+ doesn’t say what their elements are. TLC can’t evaluate 42 ∈ “abc”.

CONSTANT RM  // The set of all RMs

The rmState[r] is the state of RM r. The set of all arrays indexed by elements of RM with values in {”working”, “prepared”, “committed”, “aborted”}.

rmState ∈ [RM -> {"working", "prepared", "committed", "aborted"}]

The array with index set RM such that [r∈RM -> "working"] [rm] = "working" for all rm in RM.

TCInit == rmState = [r ∈ RM -> "working"]

The TLA+ syntax for an array expression:

[variable ∈ set -> expression]

Defines sqr to be an array with index set 1..42. Such that sqr[i] = i² for all i in 1..42.

sqr == [i ∈ 1..42 -> i²]