Modelling events not visible to the outside world but leading to external visible behaviour (Dezyne Reference Manual)

As mentioned, components use or provide functionality via interfaces and not by interacting directly with other components. Therefore, interface specifications can not contain component implementation details.

However, when this leads to externally visible behaviour, interfaces necessarily capture decisions that are internal to the implementation. As an example consider in the case above the completion of the connection request that will trigger the server component to return a notification connectReqRes. But how is that captured in an interface specification that should not contain implementation details?

There are two options to specify internal events (like the completion of the request initiated by connectReq), that lead to external events in interfaces:

With this knowledge the interface specification for the ProtocolStack in the example we have been using so-far could look like:

interface IProtocolStack
{
  enum Result                               // enumeration type used for the reply value of
  {                                         // the event enable
    Ok,
    Failed
  };
  in Result enable();                       // in event to enable the ProtocolStack
                                            //   the event will return if enabling was successful or not
  in void disable();                        // in event to disable the ProtocolStack
  in void connectReq();
  out void connectReqRes();
  behaviour                                 // the specification of the externally visible behaviour
  {
      enum State {OFF, ON, CONNECTING, CONNECTED};
      State state = State.OFF;
      [state.OFF]
      {
          on enable:                        // One possible response to enable is Ok
          {
             reply(Result.Ok);
             state = State.ON;
          }
          on enable: reply(Result.Failed);  // The other possible response to enable is Failed
          on disable,connectReq: illegal;
      }
      [state.ON]
      {
          on enable: illegal;
          on disable: state = State.OFF;
          on connectReq: state = State.CONNECTING;
      }
      [state.CONNECTING]
      {
          on enable, connectReq: illegal;
          on disable: state = State.OFF;
          on inevitable:                   // inevitably the connectReq request will be done and a response will be given
          {
              state = State.CONNECTED;
              connectReqRes;
          }
      }
      [state.CONNECTED]
      {
          on enable, connectReq: illegal;
          on disable: state = State.OFF;
      }
  }
}

3.1.3 Modelling events not visible to the outside world but leading to external visible behaviour