We’re here to help you

Menu

Using 'inevitable' and 'optional'

To specify in an interface model that the implementation behind the interface will at a certain moment perform an action requiring a response to be sent over the interface the keyword inevitable or optional can be used.

Inevitable means that when no other events occur, this event will occur. Optional means that the event may or may not occur.

Note that an Inevitable event is not guaranteed to occur always. If there are other (optional or inevitable) events that can occur, the inevitable event may or may not occur. So it is only inevitable in the absence of other events.

The difference between the two is how the event is handled by the model verification. For inevitable events, the verification only checks the cases where the event does occur, i.e. it assumes that the event will eventually occur if no other events occur. For optional events, the model verification also checks the cases where the event never happens (which could be a cause of deadlock).

If both optional and inevitable events are used in the same state, it is only guaranteed that one of the two events will occur, but it is not guaranteed that the inevitable event will always occur. In this situation there is no difference between inevitable and optional anymore since the occurance of any of the events is a correct scenario. In fact the classification of 'inevitable' may be interpreted as property of the block of events.

Syntax

Declaration of an inevitable or optional event trigger and the actions that need to be performed as a result of it:

on inevitable: action-body ; // collection of optional conditions / guards and statements
on optional: action-body ;

The declaration of inevitable and optional actions follows the declaration of Specifying actions where action-body: a collection of conditions / guards and statements (function invocations, changing variable values, changing to another state, generating another event) that define what actions to perform.

Examples

An inevitable time-out

This example shows the interface specification for a timer.

As it is up to the implementation to define exactly how the timer will expire, the (internal or implementation specific) trigger leading to that the time-out event has to be send over the Timer interface can not be specified in the interface definition. However, we define here that that inevitably the timer will expire and the time-out event has to be send.

interface iTimer
{
// interface for a basic timer

  in void createTimer();
  in void cancelTimer();
  out void timeout();

  behaviour
  {
    enum State {Idle, Busy};
    State state = State.Idle;

    [state.Idle]
    {
      on createTimer: {state = State.Busy;}
      on cancelTimer: illegal;
    }
    [state.Busy]
    {
      on createTimer: illegal;
      on cancelTimer: {state = State.Idle;}
      on inevitable:
      {
        timeout;
        state = State.Idle;
      }
    }
  }
}

An interface for a sensor with an optional event when the sensor is triggered

This example shows the interface specification for a sensor.

As it is up to the implementation to define exactly what happens when the sensor is triggered, the (internal or implementation specific) trigger leading to that the triggered event has to be send over the Sensor interface can not be specified in the interface definition. However, we define here that that optionally the sensor might be triggered and the triggered event has to be send.

// Interface to a Sensor
// The Sensor can be enabled via enable
// The Sensor can be disabled via disable
// The Sensor indicates that it is triggered via triggered
interface Sensor
{
  in void enable();
  in void disable();

  out void triggered();

  behaviour
  {
    enum States { Disabled, Enabled, Triggered };
    States state = States.Disabled;

    [state.Disabled]
    {
      on enable:        state = States.Enabled;
      on disable:       illegal;
    }
    [state.Enabled]
    {
      on enable:        illegal;
      on disable:       state = States.Disabled;
      on optional:    { triggered; state = States.Triggered; }
    }
    [state.Triggered]
    {
      on enable:        illegal;
      on disable:       state = States.Disabled;
    }
  }
}

See also:

If you have questions that weren’t answered by this Guide,
let our support team help you out.

Enjoy this article? Don't forget to share.
google-site-verification:google656c7703ab521151.html