We’re here to help you

Menu

Start-up Sequence for Two Different Devices

The goal of this Dezyne modelling example is to illustrate a way to learn the basics of Dezyne by modelling the start-up of two different devices.

The starting point for the exercise is to define an interface model to a device with the following behaviour:

image

When told to start, this device will always respond with an asynchronous notification at some future moment in time. It can either succeed or fail to start. Turning the device off is accomplished synchronously.

The second device is simpler:

image

When told to turn on, this device immediately responds with success or failure. Turning the device off is also a synchronous action.

The goal of the exercise is to design a component that will start both of these devices. The following picture shows the two use cases that the component should support:

image

In other words, the component can be told to start all devices and it asynchronously responds that “allStarted” or that “startFailed”.

The following Dezyne model defines the visible behaviour of Device1:

interface Device1IF
{
  enum Result { OK, NOK };
  in void turnon();
  in void turnoff();
  out void ok();
  out void nok();

  behaviour
  {
    enum State { Off, GoingOn, On };
    State state = State.Off;

    [state.Off]
    {
      on turnon: state = State.GoingOn;
      on turnoff: illegal;
    }
    [state.GoingOn]
    {
      on inevitable: { ok; state = State.On; }
      on inevitable: { nok; state = State.Off; }
      on turnon: illegal;
      on turnoff: illegal;
    }
    [state.On]
    {
      on turnon: illegal;
      on turnoff: { state = State.Off; }
    }
  }
}

Device 1 begins on the Off state, in which state a “turnoff” is not allowed (“illegal”). When told to “turnon” it enters the state GoingOn. When in the GoingOn state the “turnon” and “turnoff” events are illegal. The underlying component will perform whatever instructions are necessary to turn this device on – we don’t know what they are because we can only ‘see’ the externally visible behaviour of the component. But at some point in time the component will always (inevitably) notify the client whether the start succeeded “ok” or failed “nok”. If it succeeded the device is then On, if it failed it returns to Off.

When copied into Dezyne amongst others the following state chart is displayed:

image

interface Device2IF
{
  enum Result { OK, NOK };
  in Result turnon();
  in void turnoff();

  behaviour
  {
    enum State { Off, On };
    State state = State.Off;

    [state.Off]
    {
      on turnon: { reply( Result.OK ); state = State.On; }
      on turnon: { reply( Result.NOK); }
      on turnoff: illegal;
    }
    [state.On]
    {
      on turnon: illegal;
      on turnoff: { state = State.Off; }
    }
  }
}

Device 2 starts in the Off state, where a “turnoff” instruction is illegal. Synchronously and non-deterministically it replies to a “turnon” instruction with either an “Ok” or a “NOK”. If it replies with OK, the device is in the “On” state.

The interface to the component looks like this:

interface StartControlIF
{
  enum Result { OK, NOK };
  in void startAll();
  in void stopAll();
  out void allStarted();
  out void startFailed();

  behaviour
  {
    enum States { Idle, Starting, Started };
    States state = States.Idle;

    [state.Idle]
    {
      on startAll: state = States.Starting;
      on stopAll: illegal;
    }
    [state.Starting]
    {
      on startAll, stopAll: illegal;
      on inevitable: { state = States.Idle; startFailed; }
      on inevitable: { state = States.Started; allStarted; }
    }
    [state.Started]
    {
      on startAll: illegal;
      on stopAll: state = States.Idle;
    }
  }
}

image

Now on to the main action: designing a component to tie these interfaces models together and implement the required start and stop behaviour. This is the good weather behaviour:

image

However, should the initialisation of Device1 fail, it should be retried (up to four times), for example:

image

The following model implements this behaviour:

import StartControlIF.dzn;
import DeviceIF.dzn;
component StartControl
{
  provides StartControlIF startIF;
  requires Device1IF device1IF;
  requires Device2IF device2IF;

  behaviour
  {
    subint Count {0..5};
    enum States { Idle, Starting, Started };
    States state = States.Idle;
    Device2IF.Result result2 = Device2IF.Result.NOK;
    Count count = 0;

    [state.Idle]
    {
      on startIF.startAll():
      {
        count = 0;
        state = States.Starting;
        device1IF.turnon();
      }
      on device1IF.ok(), device1IF.nok(), startIF.stopAll(): illegal;
    }
    [state.Starting]
    {
      on startIF.startAll(), startIF.stopAll(): illegal;
      on device1IF.ok():
      {
        result2 = device2IF.turnon();
        if ( result2 == Device2IF.Result.OK )
        {
          state = States.Started;
          startIF.allStarted();
        }
        else
        {
          device1IF.turnoff();
          state = States.Idle;
          startIF.startFailed();
        }
      }
      on device1IF.nok():
      {
        if ( count < 5 )
        {
          count = count + 1;
          device1IF.turnon();
        }
        else
        {
          state = States.Idle;
          startIF.startFailed();
        }
      }
    }
    [state.Started]
    {
      on startIF.stopAll():
      {
        device1IF.turnoff();
        device2IF.turnoff();
        state = States.Idle;
      }
      on startIF.startAll(), device1IF.ok(), device1IF.nok(): illegal;
    }
  }
}

Note that the model starts by importing the two aforementioned interface models. An integer type, “Count”, is defined with a range from 0 to 5 and then an instance of this type in declared, “count”. A variable of type Device 2 Interface Result type is declared and set to “NOK”. The behaviour of the model is as follows:

image

These models are available as examples in Dezyne. Various things that are worth trying including commenting out a turnoff event to a Device and then verifying the model set.

As a more advanced topic, it’s worth considering what happens if the “inevitable” keyword in the StartControlIF model is changed to the “optional” keyword, as follows:

interface StartControlIF
{
  enum Result { OK, NOK };
  in void startAll();
  in void stopAll();
  out void allStarted();
  out void startFailed();

  behaviour
  {
    enum States { Idle, Starting, Started };
    States state = States.Idle;

    [state.Idle]
    {
      on startAll: state = States.Starting;
      on stopAll: illegal;
    }
    [state.Starting]
    {
      on startAll, stopAll: illegal;
      on optional: { state = States.Idle; startFailed; }
      on optional: { state = States.Started; allStarted; }
    }
    [state.Started]
    {
      on startAll: illegal;
      on stopAll: state = States.Idle;
    }
  }
}

Try verifying this model. You will see that it immediately results in a deadlock:

image

The reason for this is the subtle difference between an “inevitable” event and an “optional” event. “Inevitable” says that the event will always happen, under all circumstances. “Optional” says the one of the alternatives for this event is that it might never happen. This interface model relies on the event happening, so the introduction of the “optional” causes a deadlock because it says that the event might never happen. In the event that the event is indeed optional, the interface must be redesign to deal with that situation, perhaps by introducing a timeout.

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.