UML14 — Protocol state machines are not pre/postconditions

The text in the semantics of ProtocolStateMachine says:

The protocol transition can always be translated into pre and post
conditions of the associated operation. For example, the transition
in Figure 9-13 specifies that:

1. the operation "m1" can be called on an instance when it is in
the state S1 under the condition C1,

2. when m1 is called in the state S1 under the condition C1,
then the final state S2 must be reached under the condition
C2.

The above translation is not possible by the definition of protocol
machines. Protocol machines are a client-side view, independent of the
the internal behavior machine of the instance. This means the protocol
states are not necessarily the same as the internal states of the
intance. The protocol machine is keeping track of the operations that
have been called to enforce and order, but the internal behavior machine
may or may not be the same. If they are the same, there would be no
purpose to the protocol machine.

The spec actually makes the same point at the beginning of the semantics of
PSM:

Using pre and post conditions on operations is a technique well
suited for expressing such specifications. However, pre and post
conditions are expressed at the operation level, and therefore do
not provide a synthetic overview at the classifier level. Protocol
state machines provide a global overview of the classifier protocol
usage, in a simple formal representation.

That is, If PSM's were easiy mappable to operation pre/postcondtions,
there would be no point to having PSMs.

Suggested change to the text:

A protocol state machine could in theory be translated to pre- and
postconditions on operations, but the conditions would need to account
for the operation call history on the instance, which may or may not
be straightforwardly represented by its internal states. A protocol
machine provides a direct model of the state of interaction with the
instance, so that constraints on interaction are more easily
expressed.

see above