We’re here to help you

Menu

Basic Principles Demo

This is a set of examples that shows the basic principles of Dezyne.

Let’s consider the following model as a starting point:

interface MyIF
{
  in void doThis();
  in void doThat();
  out void doneThis();
  out void doneThat();

  behaviour
  {
    enum States { All };
    States state = States.All;

    [state.All]
    {
      on doThis: [true] doneThis;
      on doThat: [true] doneThat;
    }
  }
}
component MyComp
{
  provides MyIF myIF;

  behaviour
  {
    enum States { All };
    States state = States.All;

    [state.All]
    {
      on myIF.doThis(): myIF.doneThis();
      on myIF.doThat(): myIF.doneThat();
    }
  }
}

This is a very simple model that has no significant behaviour, but just demonstrates the basic language elements and the relationship between an interface and a component. In all states, both the interface and the component accept all events. Useful to set a not too complicated starting point.

After this it is illustrative to add some behaviour, as follows:

interface MyIF
{
  in void doThis();
  in void doThat();
  out void doneThis();
  out void doneThat();

  behaviour
  {
    enum States { All };
    States state = States.All;

    [state.All]
    {
      on doThis: doneThis;
      on doThat: doneThat;
    }
  }
}
component MyComp
{
  provides MyIF myIF;

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on myIF.doThis(): myIF.doneThis();
    }
    [state.AllowThat]
    {
      on myIF.doThat(): myIF.doneThat();
    }
  }
}

The component has been changed to have two states that allow ‘This’ or ‘That’ but not both. The interface does not reflect these changes and so a verification error arises. The lesson is that in Dezyne it is required that a component implements the behaviour defined in its ‘Provided’ interface model. The demo also highlights the sequence trace as the means by which verification failures are presented.

image

The next step adds the same behaviour to the interface model, as follows:

interface MyIF
{
  in void doThis();
  in void doThat();
  out void doneThis();
  out void doneThat();

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on doThis: doneThis;
      on doThat: illegal;
    }
    [state.AllowThat]
    {
      on doThat: doneThat;
      on doThis: illegal;
    }
  }
}
component MyComp
{
  provides MyIF myIF;

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on myIF.doThis(): myIF.doneThis();
    }
    [state.AllowThat]
    {
      on myIF.doThat(): myIF.doneThat();
    }
  }
}

This model is conflict free and verifies. However it doesn’t do very much – there’s no way to transition from ‘AllowThis’ to ‘AllowThat’. This is apparent from the state diagram.

image

It’s also apparent from simulation, where it’s only possible to “doThis”.

image

So the next step is to add behaviour that switches the Allow state.

The simplest way to switch state is just to toggle from one state to the other on an event, as follows:

interface MyIF
{
  in void doThis();
  in void doThat();
  out void doneThis();
  out void doneThat();

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on doThis: doneThis;
      on doThat: illegal;
    }
    [state.AllowThat]
    {
      on doThat: doneThat;
      on doThis: illegal;
    }
  }
}
component MyComp
{
  provides MyIF myIF;

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on myIF.doThis(): { myIF.doneThis(); state = States.AllowThat; }
    }
    [state.AllowThat]
    {
      on myIF.doThat(): { myIF.doneThat(); state = States.AllowThis; }
    }
  }
}

Now the component has internal behaviour that toggles the Allow state on an event. See the state diagram:

image

However the changes to the component cause a problem with the interface model, namely that the interface model still does not allow for an Allow state change…

image

How the state change happens within the component is irrelevant to the interface model, it’s only necessary to say that there’s an internal modelling event that leads to the state change. This is described by the keywords ‘optional’ or ‘inevitable’. In this case we’ll use the keyword optional in the interface model, as follows:

interface MyIF
{
  in void doThis();
  in void doThat();
  out void doneThis();
  out void doneThat();

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on doThis: doneThis;
      on doThat: illegal;
      on optional: state = States.AllowThat;
    }
    [state.AllowThat]
    {
      on doThat: doneThat;
      on doThis: illegal;
      on optional: state = States.AllowThis;
    }
  }
}

We can show the modelled behaviour using the simulation feature:

image

Simply toggling between the Allow states is too simple. Now we want to be able to control the Allow state so we do this by adding ‘changeToThis’ and ‘changeToThat’ events and updating the component accordingly.

interface MyIF
{
  in void doThis();
  in void doThat();
  in void changeToThis();
  in void changeToThat();
  out void doneThis();
  out void doneThat();

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on doThis: doneThis;
      on doThat: illegal;
      on changeToThis: illegal;
      on changeToThat: state = States.AllowThat;
    }
    [state.AllowThat]
    {
      on doThat: doneThat;
      on doThis: illegal;
      on changeToThat: illegal;
      on changeToThis: state = States.AllowThis;
    }
  }
}
component MyComp
{
  provides MyIF myIF;

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on myIF.doThis(): myIF.doneThis();
      on myIF.changeToThat(): state = States.AllowThat;
    }
    [state.AllowThat]
    {
      on myIF.doThat(): myIF.doneThat();
      on myIF.changeToThis(): state = States.AllowThat;
    }
  }
}

These models are correct, but the state diagram reveals a problem …​

image

  1. and the verification an other one: a behaviour mismatch between the interface and the component:

image

The problem is pretty clear, erroneously the control flow stays in the AllowThat state after receiving a changeToThis event. The correct behaviour is:

[state.AllowThat]
{
  on myIF.doThat(): myIF.doneThat();
  on myIF.changeToThis(): state = States.AllowThis;
}

With this change the state chart shows sensible behaviour, the models verify and we can simulate to our hearts content…

image

As a final twist to the demo, it’s worth considering the following alternative structure for the component:

interface MyIF
{
  in void doThis();
  in void doThat();
  in void changeToThis();
  in void changeToThat();
  out void doneThis();
  out void doneThat();

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    [state.AllowThis]
    {
      on doThis: doneThis;
      on doThat: illegal;
      on changeToThis: illegal;
      on changeToThat: state = States.AllowThat;
    }
    [state.AllowThat]
    {
      on doThat: doneThat;
      on doThis: illegal;
      on changeToThat: illegal;
      on changeToThis: state = States.AllowThis;
    }
  }
}
component MyComp
{
  provides MyIF myIF;

  behaviour
  {
    enum States { AllowThis, AllowThat };
    States state = States.AllowThis;

    on myIF.doThis():
    {
      [state.AllowThis] myIF.doneThis();
    }
    on myIF.doThat():
    {
      [state.AllowThat] myIF.doneThat();
    }
    on myIF.changeToThis():
    {
      [state.AllowThat] state = States.AllowThis;
    }
    on myIF.changeToThat():
    {
      [state.AllowThis] state = States.AllowThat;
    }
  }
}

The previous components were constructed from a state centric point of view. This component is constructed from an event centric point of view. The behaviour is exactly the same, but in sometimes its easier to think about a design from an event rather than a state point of view. Dezyne allows engineers to work the way that best suits them or their circumstances.

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