Menu

Understanding the Execution Semantics

The execution semantics of Dezyne are illustrated using different model examples and the corresponding sequence diagrams.

When interpreting the models and corresponding sequence diagrams, keep in mind that the body of an event is executed atomically in the context of its behaviour.

For an in-event all action statements are executed depth-first. All out-events are stored in event queues at the receiving components. After the completion of all action statements, just before control is passed back to the caller, a component will flush its own queue of pending out-events. Recursively all out-events are handled this way.


Direct in event

A provides port in-event (p.a) resulting in a requires port in-event (r.a) is implemented as a function calling another function.

interface I
{
  in void a();

  behaviour
  {
    on a: {}
  }
}

component direct_in
{
  provides I p;
  requires I r;

  behaviour
  {
    on p.a(): r.a();
  }
}

image


Direct out event

A requires port out-event (r.a) resulting in a provides port out-event (p.a) is implemented as a function posting an event in the component queue followed by a call to flush the queue.

interface I
{
  out void a();

  behaviour
  {
    on inevitable: a;
  }
}

component direct_out
{
  provides I p;
  requires I r;

  behaviour
  {
    on r.a(): p.a();
  }
}

image


Direct multiple out events

A requires port inevitably triggering multiple out-events (r.a, r.b) is implemented as one function call for each out-event posting in the component queue followed by a single flush call to trigger component processing of the events. Version 1 and 2 of the component below are indistinguisable looking from the outside.

interface I
{
  out void a();
  out void b();

  behaviour
  {
    on inevitable: {a; b;}
  }
}

component direct_multiple_out1
{
  provides I p;
  requires I r;

  behaviour
  {
    on r.a(): p.a();
    on r.b(): p.b();
  }
}

image

interface I
{
  out void a();
  out void b();

  behaviour
  {
    on inevitable: {a; b;}
  }
}

component direct_multiple_out2
{
  provides I p;
  requires I r;

  behaviour
  {
    on r.a(): {}
    on r.b(): {p.a(); p.b();}
  }
}

image

The third variant is left as an exercise to the reader.


Indirect out event

A requires port out-event (r.b) posted in the context of a provides port in-event (p.a) is processed before the provides port in-event (p.a) returns.

interface I
{
  in void a();
  out void b();

  behaviour
  {
    on a: b;
  }
}

component indirect_out
{
  provides I p;
  requires I r;

  behaviour
  {
    on p.a(): r.a();
    on r.b(): p.b();
  }
}

image


Indirect multiple out events

Since the provided interface is the same in the 3 cases below the externally visible behaviour is identical. The 3 different behaviour implementations of the component show the subtle differences in the internal handling of messages.

interface I
{
  in void a();
  out void b();

  behaviour
  {
    on a: b;
  }
}

import I.dzn;

component indirect_multiple_out1
{
  provides I p;
  requires I r1;
  requires I r2;

  behaviour
  {
    on p.a(): {r1.a(); r2.a();}
    on r1.b(): {}
    on r2.b(): p.b();
  }
}

image

import I.dzn;

component indirect_multiple_out2
{
  provides I p;
  requires I r1;
  requires I r2;

  behaviour
  {
    on p.a(): {r1.a(); r2.a();}
    on r1.b(): p.b();
    on r2.b(): {}
  }
}

image

import I.dzn;

component indirect_multiple_out3
{
  provides I p;
  requires I r1;
  requires I r2;

  behaviour
  {
    on p.a(): r1.a();
    on r1.b(): r2.a();
    on r2.b(): p.b();
  }
}

image


Indirect blocking out event

See section on Blocking

The in-event on the provides port (p.a) blocks until a reply on the port is handled. This happens in the handling of the requires port out-event (r.b).

interface I
{
  in void a();
  out void b();

  behaviour
  {
    on a: b;
  }
}

interface I2
{
  in void a();
  out void b();

  behaviour
  {
    bool idle = true;
    [idle] on a: idle = false;
    [!idle] on a: illegal;
    [!idle] on inevitable: {idle = true; b;}
  }
}

component indirect_blocking_out
{
  provides I p;
  requires I2 r;

  behaviour
  {
    blocking on p.a(): r.a();
    on r.b(): { p.b(); p.reply(); }
  }
}

image


External multiple out events

See section on External

The addition of external on a required interface removes the atomicity of an action list, i.e: {a; b;}.

Note: the addition of the in-event e is required to constrain the occurrence of the inevitable event in combination with external.

interface I
{
  in void e();
  out void a();
  out void b();

  behaviour
  {
    bool idle =  true;
    [idle] on e: idle = false;
    [!idle] on e: illegal;
    [!idle] on inevitable: {idle = true; a; b;}
  }
}

component external_multiple_out
{
  provides I p;
  requires external I r;

  behaviour
  {
    bool idle =  true;
    [idle] on p.e(): {idle = false; r.e();}
    [!idle] on p.e: illegal;
    on r.a(): {}
    on r.b(): {idle = true; p.a(); p.b();}
  }
}

image


Indirect blocking multiple external out events

The 2 required out-events (r1.b, r2.b) can come in any order. The message sequence chart shows only one scenario. The implementation of the component is such that the provided behaviour is the same in both cases.

interface I
{
  in void a();
  out void b();

  behaviour
  {
    on a: b;
  }
}

component indirect_blocking_multiple_external_out
{
  provides I p;
  requires external I r1;
  requires external I r2;

  behaviour
  {
    bool ready = true;
    on p.a(): blocking {ready = false; r1.a(); r2.a();}
    [!ready] on r1.b(), r2.b(): {ready = true; p.b();}
    [ready] on r1.b(), r2.b(): p.reply();
  }
}

image


Enjoy this article? Don't forget to share.