Multiple provides (Dezyne Reference Manual)

5.10 Multiple provides

For the remainder of this chapter in our explanations we will be using the following two interfaces:

ihello

interface ihello
{
  in void hello();
  behavior
  {
    on hello: {}
  }
}

iworld

interface iworld
{
  in void hello();
  out void world();
  behavior
  {
    bool idle = true;
    [idle] on hello: idle = false;
    [!idle] on inevitable: {idle = true; world;}
  }
}

So far we have seen examples with more than one requires port. This topology leads to a tree like hierarchy which is a common structure to organize or coordinate in a top down fashion. In the case of sharing a single resource between multiple parties we need the opposite. The example below demonstrates to use of two provides ports.

import ihello.dzn;

component multiple_provides
{
  provides ihello left;
  provides ihello right;
  requires ihello hello;
  behavior
  {
    on left.hello(): hello.hello();
    on right.hello(): hello.hello();
  }
}

This component simply multiplexes the hello events from its provides ports to its requires port, resulting in the following event sequence trace:

If we replace the ihello interface in our previous example with the iworld interface and correct for the behavioral changes, we get the following component:

import iworld.dzn;

component async_multiple_provides
{
  provides iworld left;
  provides iworld right;
  requires iworld world;

  behavior
  {
    enum Side {None, Left, Right};
    Side side = Side.None;
    Side pending = Side.None;

    [side.None]
    {
      on left.hello(): {side = Side.Left; world.hello();}
      on right.hello(): {side = Side.Right; world.hello();}
    }
    [side.Left]
    {
      [pending.None]
      {
        on right.hello(): pending = Side.Right;
        on world.world(): {side = Side.None; left.world();}
      }
      [pending.Right] on world.world():
      {
        side = pending; pending = Side.None;
        left.world(); world.hello();
      }
    }
    [side.Right]
    {
      [pending.None]
      {
        on left.hello(): pending = Side.Left;
        on world.world(): {side = Side.None; right.world();}
      }
      [pending.Left] on world.world():
      {
        side = pending; pending = Side.None;
        right.world(); world.hello();
      }
    }
  }
}

As we can see from the behavior and the event sequence trace below, asynchonous behavior leads to event interleaving, which requires state to manage the behavior.