, it checks the operation property EFFECT and finds that the operation is of the modifier type. 7.6 The General State Machine Model 2. PO will therefore initiate a devRepCnf(<Request_event>) towards the event object (EO). EO detects the event. Confirm 8 1 Request ES Event specification os Operation specification SVS State vector specification TRS Transaction specification AO Activity object EO Event object PO Provider port object SO State object Fig. 7.58 Successful execution of a modifier operation in the state machine of a virtual object 3. EO reads the operation name and accesses the corresponding event specification (ES). EO reads the precondition declaration from the ES and initiates a pre- Req(<precondition>) towards the state object (SO). 4. SO checks if the actual value of the state vector lies within the subset of states that is defined by the precondition. Assuming that it is, SO responds with preCnf(OK!). 5. EO detects the preCnf(OK!) and reads the ES again, in order to find out what activity to perform. EO accesses the corresponding transaction specification (TRS) and executes it. During the execution, a number of interactions with activity objects (AO) occur. When the transaction ends, it returns some parame- ters, among them an indication that (in this scenario) the transaction succeeded. 6. EO checks the result of the transaction. Assuming that the activity has suc- ceeded, EO again reads the ES to find out what the next state will be (defined under the heading "Activity succeeded"). EO then orders the SO to change state with the event postOrder(<postcondition>) SO changes the value of the state vector (SVS). 7. EO again looks in the ES to find out if a result event is required (it is in this sce- nario). EO therefore initiates a gevOrd(<result_event>) towards the PO. 8. PO uses the os to create the external response (a Confirm event in this case). The user now knows that the state machine is in a defined resource state and ready for new external events. The next scenario describes how the machine 