A record corresponds to a struct in C.

[ptof -> "Fred", num -> 42] = [num -> 42, prof -> "Fred"]

f.prof is an abbreviation for f["prof"].

Represents a Prepared message sent by r to the TM.

[type -> "Prepared", rm -> r]

Each record represents a message sent by the TM to all RMs.

{[type -> "Commit"], [type -> "Abort"]}

Describes the receipt of a Prepared message from RM r by TM. Add r to tmPrepared.