Specify service states and the transitions that are actually atomic

Consider a service that allocates a fixed number of one-unit reservations. State includes a free-unit counter and a status for each stable request identifier: new, held, committed, or cancelled. Committed reservations consume units permanently in this small model; cancellation refunds only a held reservation. The initial state gives every identifier status new and sets free capacity to the declared total. Preserve terminal statuses instead of reusing identifiers, because forgetting an earlier commitment changes how retries behave. This model deliberately excludes replenishment, variable-size requests, and garbage collection.

A state is a valuation of all declared variables, not an informal diagram label. Specify their domains and the relationship between the counter and request statuses. If a response or durable record affects the promised contract, represent it rather than assuming it follows automatically from an internal status change. An abstract committed state can be useful, but a separate refinement argument must connect it to the actual storage and response boundary. Writing down the variables often reveals that two engineers meant different things by 'the request succeeded.'

Reserve(r) requires a new identifier and at least one free unit; it changes that identifier to held and subtracts one free unit. Commit(r) changes held to committed without changing free capacity. Cancel(r) changes held to cancelled and returns one unit. State explicitly that all unrelated statuses remain unchanged. The next-state relation permits any enabled action, so concurrent clients appear as different possible interleavings of these atomic transitions. A model does not prefer the helpful action unless a separate scheduling or fairness condition says so.

Duplicate calls need a defined result. A retry of an already committed identifier may return its recorded result while leaving state unchanged; it must not reserve another unit. Reusing the same identifier with a different payload should have a declared rejection or conflict rule. In TLA-style specifications, primed variables denote successor-state values, and stuttering permits a step that changes no modeled variable. PlusCal can generate such a specification from labeled algorithm steps, but its labels determine atomic boundaries that still need review against the intended service mechanism.

If the implementation checks capacity and updates it in different transactions, split those operations into separate model actions with intermediate state. Otherwise two workers can both observe one free unit before either decrements it, a behavior excluded by the atomic Reserve action. Likewise distinguish volatile and durable state when restart can erase one but preserve the other. Model message loss, duplication, or delay only where the environment permits them. Stronger environmental assumptions can simplify a model, but they narrow what the resulting analysis says about the deployed service.

Use the queue instrument to see why aggregate state is an incomplete service specification. Reset, set arrival λ=0 and service μ=2, predict that its initial backlog four becomes two after one second, then take two Steps. Separately Reset, set λ=2 and μ=2, predict backlog four after one second, then take two Steps. This fluid counter contains no identifiers, reservation ownership, durable records, or atomic transactions. Matching its aggregate count cannot establish the reservation contract; the missing state distinctions must be represented in the actual specification.