[pron]

The state transitions can be partially ordered, but the way this works in TLA is that every computation is a set of legal behaviors (sequences of states).