TLA+ in Practice and Theory Part 3: The (Temporal) Logic of Actions