Hello World! (Dezyne Reference Manual)

4.1 Hello World!

Consider the trivial Dezyne interface ihello_world

interface ihello_world
{
  in void hello ();
  out void world ();

  behavior
  {
    on hello: world;
  }
}

It defines two events, named hello and world of type void and a trivial protocol in its behavior: whenever the hello trigger is received (on hello:), it responds synchronously with a world action.

This scenario can be explored using the simulator (See Invoking dzn simulate):

$ dzn simulate doc/examples/ihello-world.dzn
(header ((client) ihello_world provides) ((sut) ihello_world interface))
(state ((client)) ((sut)))
labels: hello
eligible: hello
>

As expected, hello is the only trigger that is eligible to execute; entering hello gives

> hello
<external>.hello -> ...
... -> sut.hello
... <- sut.world
<external>.world <- ...
... <- sut.return
<external>.return <- ...
(state ((client)) ((sut)))
(trail "hello" "world" "return")
labels: hello
eligible: hello
>

The simulator can also be run non-interactively to produce a friendlier trace view or sequence diagram

client          ihello_world
  .                  :
  .                  :
  .hello             :
  .----------------->:
  .                  :
  .             world:
  .<-----------------:
  .                  :
  .            return:
  .<-----------------:

Now consider a trivial component hello_world

import ihello-world.dzn;

component hello_world
{
  provides ihello_world p;

  behavior
  {
    on p.hello (): p.world ();
  }
}

it provides the ihello_world interface, which means that it promises to behave according to the protocol specified in the interface.

The trigger p.hello is the event hello when communicated over the port p, similarly the action is named p.world. Simulation gives:

$ dzn simulate --trail=p.hello doc/examples/hello-world.dzn
(header ((p) ihello_world provides) ((sut) hello_world component))
(state ((p)) ((sut)))
<external>.p.hello -> ...
... -> sut.p.hello
... <- sut.p.world
<external>.p.world <- ...
... <- sut.p.return
<external>.p.return <- ...
(state ((p)) ((sut)))
(trail "p.hello" "p.world" "p.return")
(state ((p)) ((sut)))
(labels "p.hello")
(eligible "p.hello")

with this trace diagram

p          hello_world
.               :
.               :
.hello          :
.-------------->:
.               :
.          world:
.<--------------:
.               :
.         return:
.<--------------:

From this component an executable program can be created (See Invoking dzn code)

$ dzn code doc/examples/ihello-world.dzn
$ dzn code --model=hello_world doc/examples/hello-world.dzn
$ g++ hello-world.cc main.cc -ldzn-c++

When running this executable and feeding it the trail, we get

echo -e 'p.hello\np.world\np.return' | ./a.out
<external>.p.hello -> sut.p.hello
<external>.p.world <- sut.p.world
<external>.p.return <- sut.p.return