In such a model, state transitions can be as small or as large as you choose (e.g. sorting an array could be a single state change or multiple ones, depending on your chosen level of abstraction). Lamport's Temporal Logic of Actions (which forms the core, or at least the most interesting part of TLA+) has the very mathematical notion of abstraction as a first-class construct, i.e., A => B iff B is an abstraction of A (where => is the logical implication operator, which in TLA also means "refines" or "implements", i.e., the converse of abstraction).