Next: , Previous: , Up: How to use ‘external'?   [Contents]


4.2.2 How to start solving the problem you face with ‘external’

The RobustTimer component will be responsible for the mapping of an ‘external’ ITimer port to a regular ITimer port. The intent is to define the behaviour of the component in such a way that even if ‘external’ delays occur, communication over the provided ITimer port does not suffer from this.

The most straight-forward behaviour specification would be to map in-events on the provided ITimer port to in-events on the required ITimer port and to do the same for out-events of the required port. As a first exercise, implement the behaviour of RobustTimer this way.

Hint: make sure the states defined in the ITimer interface are followed in the RobustTimer component behaviour as well.

Solution:

component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

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

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Idle;
      }
      [state.Idle] { }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
    }
  }
}

The above solution is a first rudimentary step towards a working solution. If you verify the RobustTimer component, you will see the exact same illegal assertion as we found earlier in the previous section. However, this time it is extracted from all interleaving with other required and provided ports of the Controller component and you can focus solely on the behaviour of the required ‘external’ ITimer port. Let’s reconsider the timeline described in How does this translate to runtime execution?:

images/sequence_5

Recall that x is the time it takes for the cancel event from iTimer to be processed. During x, the timeout occurs on ext_iTimer and is queued accordingly. After x, RobustTimer is in the Idle state but still has to handle the queued timeout. This scenario is not described in the behaviour of RobustTimer and as such, it is implicitly illegal.

In the next section, we will have a look at how to implement behaviour such that these possible concurrencies discovered by ‘external’ can be handled.


Next: , Previous: , Up: How to use ‘external'?   [Contents]