n can be allowed in all resource states where the called party D is not already engaged in a call, where there exists an idle channel in A's access route, where the properties of A and D allow them to communicate, where appropriate teleservice resources are available and where the PCS can handle another serv- ice call (no TNW congestion). Altogether, the subset of states for this transition may be 99% of all states in the state space. This subset is defined by a precondi- tion. Thus, as soon as there is a precondition defined for a transition, one knows that the originating state is an EFSM state. Postconditions have a similar purpose: to specify how the subset of the state space is affected, as the result of the activity that is performed in the transition. Thus, a postcondition indicates that the next state is also an EFSM state. Note that the result event (if any) in a transition should always identify the next resource state. This implies that transitions that terminate in different resource or EFSM states are separate transitions, even if they are initiated by the same initiating event. This paradigm characterizes a Moore state machine. For example, the provider can give two different responses to a servReq(...): the servRef identifies the state AnotInCall as the next state, or the servCnf identifies the state AandDinCall as next state. State diagrams should always be based on Moore states, since that makes a state diagram unambiguous and more useful, for analysis purposes, for product verifica- tion and for object implementation. The AML- - operation classification system sup- ports the Moore state paradigm by distinguishing between positive and negative responses. An operation classification system that hides positive and negative responses in a common response primitive (as programming languages and the modelling language UML do) cannot distinguish between different service states, without introducing response parameter tests as parts of transitions. This makes internal activities of service objects visib