*) only for modifier operations Fig. 7.55 Specifications must be refined to executable specifications The difference between state diagrams and event specifications is demonstrated by Fig. 7.56. The diagram is an EFSM diagram based on a state vector with two variables, X and y, X being chosen as the explicit variable. It shows five possible transitions for the event type chSeizeReq. This event type can occur in any state, but is accepted only in states {1,1} and {2,3}. The event specification for chSeize- Req shows that the main differences from state diagrams are that event specifica- tions are textual and that an event specification represents all transitions that are initiated by the same event type (ASP), regardless of state. The rationale behind this is the observation that, in many state diagrams, the same initiating event is used in many transitions, and the activity that is referred to is the same for most of these transitions. State::=SET{x{1..2},y{1..3}] chSeizeReq stateErrorRepCnf chSeizeReq chSeizeReq act: a_failed {1,1] {2, 2} act. a failed chSeizeRef chSeizeReq chSeizeRef act. a succeeded chSeizeCnf chSeizeReq act. a_succeeded chSeizeCnf Event specification for chSeizeRequest Initiating event: chSeizeRequest(s,u,v Declarative part Precondition: st: ((x=1 and y=1) or (x=2 and y=3)) Activity: State error: not st -> stateErrorReportConfirm(...) Evaluated part Activity failed: not aTR -> chSeizeRefuse(...) Activity succeeded: (x=2 and y=2) and chSeizeConfirm(...) Fig. 7.56 The event specification An event specification can be seen as a small program based on formal logic. It consists of a declarative part and an evaluated part. The declarative part consists of three headings: 7 Concepts and Notations for Process Control Systems Modelling 1. The first heading defines the initiating event, including variable names for all parameters. There are two possible type of events: external event (as in this case) and internal event. Internal events are named by identifiers. 2. The second heading, Precondition, pro