Records are like structs or objects - they group named fields together. In TLA+, records are simply functions whose domain is a set of strings (the field names), but because this pattern occurs so frequently, TLA+ provides dedicated syntax for them.
[name |-> "Alice", age |-> 30]Use dot notation:
person.name \* "Alice"
person.age \* 30[name: {"Alice", "Bob"}, age: 0..120]
This is the set of all records with a name field from the given set and an age field from 0..120. Useful for TypeOK invariants.
Just like functions, use EXCEPT:
person' = [person EXCEPT !.age = @ + 1]Under the hood, a record is a function from field names (strings) to values:
[name |-> "Alice", age |-> 30]is the same as:
[x \in {"name", "age"} |-> IF x = "name" THEN "Alice" ELSE 30]
The spec models user accounts with a small maximum balance so the reachable state space is finite. Deposit checks the limit before changing a balance; a type invariant alone would only detect an out-of-range balance, not prevent it.
When every account is inactive, Finished permits an unchanged terminal state. This deliberate stuttering step models a completed system rather than an unexpected deadlock.
TLC completes without errors for two users and MaxBalance = 3. Try removing the upper-bound guard from Deposit; TypeOK then fails when a balance exceeds MaxBalance.