ed by the arrow of the transition. A transition always defines a single initiating event that triggers the transition to the next state. No other graphical symbols but states and transitions are allowed in AML state diagrams. For example, SDL provides symbols for procedure, save, connector, start, stop task, create and deci- sion, to be used for specifying transitions. These types of symbols violate some basic principles for state machine modelling (although they might be used for specifying or describing imple- mentations). 6 Process Control System Modelling The object stays in a reactive state until an initiating event happens. When in a reactive state, the object does no processing, as far as the other object in the service relation is concerned. During a transition between reactive states, the object is in an undefined state. When an initiating event happens, the object state immediately becomes unde- fined. A transition takes time to execute. There are two types of initiating events: those that have been initiated by the other service object (e.g. the servReq(...)), and those that are invisible for the other service object (e.g. relFromOtherParty). The former are communication events, the latter are called internal initiating events (called iie: in the diagram). A transition may also define one or several result events (e.g. servCnf). Result events are always communication events. A transition may also define preconditions (symbol pre: in the diagram) and postconditions (symbol post: in the diagram). Pre- and postconditions are state- ments that refer to the service resource model. Preconditions are either true or false when the initiating event happens. If a transition has a precondition defined, it means that the transition is valid only if the initiating event happens, and the precondition is true. A postcondition is a statement that must be true for the next state. An activity (symbol act: in diagrams) is performed by the service object in a transition. However, activities performed by one object in a se