Depends on what you mean by "actual transaction". Every TLA+ behavior is describable as a series of "next-states", where _usually_ (not always, but _usually_) o

Depends on what you mean by "actual transaction". Every TLA+ behavior is describable as a series of "next-states", where _usually_ (not always, but _usually_) one action is true. In which case you'd model the transaction by determining the changes that the overall transaction makes and then declaring them all as part of a single action.