1.1 Purpose

The main purpose of Dezyne is to systematically support the development and evolution of programs for which the validity is determined by their detailed behavior under operational conditions (E-type programs ¹). These are also the type of program which change the most and are most negatively affected by that change.

1.2 Conditions for Using Dezyne

The distribution terms for Dezyne-generated code permit using the code in free software programs as well as in non-free or proprietary programs: The Dezyne code generator transpiles the user’s Dezyne program into a program in the target language, e.g., C++, making the resulting C++ program a derivative work of the user’s Dezyne code, inheriting its copyright and–if applicable, licensing terms.

The Dezyne runtime is distributed under the GNU Lesser General Public License (see LGPL3+), which means that it can be freely and unconditionally used in unmodified form, also if you are creating a non-free or proprietary software. If you modify the Dezyne runtime code that you distribute with your program, one condition applies: The modifications must be made available.

Note: Dezyne comes with NO WARRANTY, to the extent permitted by law.

2.1 Concurrency

Dezyne is based on a message passing programming model. Messages are explicitly represented in the language and expressed in the underlying process algebra. The approach allows reasoning about equivalences which in turn is used in verification and allows compositions to retain their individually verified properties.

Message passing is a natural way of describing concurrency, from cooperative multitasking to multi threading and multi processing. It abstracts away from cumbersome primitives like semaphores, mutexes, condition variables, critical sections, etc. It also removes the passing of time completely and focuses our reasoning on the ordering of messages. Which allows combining synchronous and asynchronous activity in a single formalism.

Multi tasking vs parallelism.

2.2 Component Based

In Dezyne programs are divided into components by means of formal interfaces isolating the components from their surroundings. Components are composed into systems by connecting their ports. Communication across port must follow the behavior as defined by their respective interfaces. An interface behavior describes the message exchange between the components on either side of the interface that separates them. A component behavior defines the interactions in terms of the messages exchanged across all of the component ports.

Message or event maps onto a function call.

2.3 Model Based

Dezyne is for applications where one encounters the problems that the operating system does not solve.

As Dezyne is typically used to operate an abstract machine, usually real world identities are represented. They are identified by name and their interaction with their environment is captured as a behavior. A behavior is the observable interaction in terms of message exchange. Interface models and component models both define behaviors.

2.4 Design by Contract

Regular lanuages have more or less support for design by contract. In C one can assert pre and post conditions. In design there is more support for this...

As interface behaviors prescribe an interaction protocol, they provide a convenient and compact way to define contracts. A contract lists both expectations and obligations. Components in turn are a convenient and compact way to implement such contracts using other sub contractors. Components distinguish two levels of hierarchy in their interface contracts: The interfaces they provide and the interfaces they require. The essential difference between the two is that an interface which is provided must be completely implemented. While an interface that is required may or may not be used completely.

2.5 Managing Complexity

The single biggest challenge, when programming at scale, is managing complexity. What do we mean by complexity? The literal meaning is derived from weaving together. In programming it refers to the resulting behavior that emerges from combined interaction. As the number of parts and their dependencies increase, the resulting behavior increases exponentially and very soon it reaches the point where it is no longer humanly possible to know and understand it. As a result making changes will inadvertently lead to unknowingly interfering with those interactions and defects are introduced. With increasing complexity existing techniques, methods and paradigms no longer suffice to enable the programmer to adequately manage it. Dezyne offers both encapsulation as well as abstraction of interaction. Interaction which is unencapsulated in other paradigms. By encapsulating and abstract Dezyne manages complexity.

3.1 Requirements

This section lists requirements when building Dezyne from source. The build procedure for Dezyne is the same as for GNU software, and is not covered here. Please see the files README and INSTALL in the Dezyne source tree for additional details.

Dezyne is available for download from its website at https://dezyne.org/download.html.

Dezyne depends on the following packages:

• GNU Guile, version 3.0.x, with readline support;
• Guile-JSON 4.x;
• GNU Make;
• mCRL2, version 202106.0,
• SCMackerel, version 0.5.3.

Optionally, for C++11

• boost, for using co-operatibbve co-routines instead of threads.

To use the code that is generated by Dezyne, which includes running the regression test:

• GCC’s g++, version 5.4 or later.

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

4.2 A Simple State Machine

The ihello_bool interface introduces stateful behavior that is somewhat more interesting

interface ihello_bool
{
  in void hello ();
  in bool cruel ();
  out void world ();

  behavior
  {
    bool idle = true;
    [idle] on hello: idle = false;
    [!idle]
      {
        on cruel: {idle = true; reply (idle);}
        on cruel: reply (idle);
        on inevitable: {world; idle = true;}
      }
  }
}

This example introduces some new language aspects

bool idle = true;

A boolean state variable, defining idle=true as the initial state,

[idle]

A guard. Only when the expression between the brackets evaluates to true the on is eligible to execute. In the initial state, the hello trigger is the only thing that can occur. The guard and the on are declarative statements. After the declarative statements follows a,

idle = false;

An imperative statement. When hello trigger occurs, the interface transitions to state !idle,

on cruel: … on cruel: …

A non-deterministic choice³. In the !idle state, cruel is accepted; it can either...

reply (true)

reply false and remain not idle, or

{idle = true; reply (idle);}

execute a compound of two imperative statements: Set the reply value to true and transition to the idle state,

inevitable

If no cruel trigger occurs, inevitably the world action will occur. inevitable is a modeling event and is not visible on the trail. The effect is that world action now has become decoupled from the caller.

The state diagram (See Invoking dzn graph) depicts this protocol graphically:

This model is already interesting enough to have the mCRL2 model-checker verify if all is well (See Invoking dzn verify and See Verification Checks and Errors)

$ dzn -v verify doc/examples/ihello-bool.dzn
verify: ihello_bool: check: deadlock: ok
verify: ihello_bool: check: unreachable: ok
verify: ihello_bool: check: livelock: ok
verify: ihello_bool: check: deterministic: ok

which is luckily the case. The model-checker can also be used to generate all possible⁴ traces (See Invoking dzn traces) for ihello_bool:

$ dzn -v traces doc/examples/ihello-bool.dzn

produces three trace files (ihello_bool.trace.0,ihello_bool.trace.1, and ihello_bool.trace.2) with these traces (the order may differ):

1. hello,return,world
2. hello,return,cruel,true
3. hello,return,cruel,false

The sequence for the first trace with the asynchronous world looks like this

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

and for the second trace where cruel happens looks like this

client          ihello_bool
  .                  :
  .                  :
  .hello             :
  .----------------->:
  .                  :
  .            return:
  .<-----------------:
  .                  :
  .                  :
  .cruel             :
  .----------------->:
  .                  :
  .              true:
  .<-----------------:

the third trace is looks like this

client          ihello_bool
  .                  :
  .                  :
  .hello             :
  .----------------->:
  .                  :
  .            return:
  .<-----------------:
  .                  :
  .                  :
  .cruel             :
  .----------------->:
  .                  :
  .             false:
  .<-----------------:

You may have noticed that the first two traces start and end in the initial state, while the third trace starts in the initial state and ends in the !idle state (also see the corresponding state diagram).

Now have a look at the component simple_state_machine

import ihello-bool.dzn;

interface iworld
{
  in void hello ();
  out void world ();
  behavior
  {
    on hello: {}
    on hello: world;
  }
}

component simple_state_machine
{
  provides ihello_bool p;
  requires ihello_bool r1;
  requires iworld r2;
  behavior
  {
    enum status {A, B, C};
    status s = status.A;
    [s.A]
    {
      on p.hello (): {s=status.B; r2.hello (); r1.hello ();}
    }
    [s.B]
    {
      on p.cruel (): {if (r1.cruel ()) s=status.A; reply (s.A);}
      on r2.world (): s=status.C;
    }
    [s.B || s.C] on r1.world (): {s=status.A; p.world ();}
    [s.C] on p.cruel (): reply (s.A);
  }
}

It introduces the following concepts:

enum status {A, B, C}

User defined enum type named status,

[s.A]

Field test of enum variable s: evaluates to true if s has field value A, it is equivalent to s == status.A,

[s.B || s.C]

Logical or || in guard expression (see See Expressions),

on r2.world (): {}

A skip statement: upon receiving the r2.world trigger, the component does “nothing” and is ready for the next event. Omitting this line would make the occurrence of r2.world illegal.

Verification suceeds

$ dzn -v verify doc/examples/simple-state-machine.dzn
verify: ihello_bool: check: deadlock: ok
verify: ihello_bool: check: unreachable: ok
verify: ihello_bool: check: livelock: ok
verify: ihello_bool: check: deterministic: ok
verify: iworld: check: deadlock: ok
verify: iworld: check: unreachable: ok
verify: iworld: check: livelock: ok
verify: iworld: check: deterministic: ok
verify: simple_state_machine: check: deterministic: ok
verify: simple_state_machine: check: illegal: ok
verify: simple_state_machine: check: deadlock: ok
verify: simple_state_machine: check: unreachable: ok
verify: simple_state_machine: check: livelock: ok
verify: simple_state_machine: check: compliance: ok

you may want to see what happens to verification or the state diagram when you comment-out a statement of your choosing in the component’s behavior.

4.3 A Camera Example

The Camera example introduces the system component (See Systems). The system diagram (See Invoking dzn graph) looks like this:

This is what the Camera system looks like in Dezyne:

component Camera
{
  provides IControl control;

  system
  {
    Driver driver;
    Acquisition acquisition;
    Optics optics;

    control <=> driver.control;
    driver.acquisition <=> acquisition.port;
    driver.optics <=> optics.port;
  }
}

It introduces the following concepts:

provides IControl control;

Similar to a regular component, it defines ports,

system

The system specification defines instances of components and their bindings,

Driver driver;

A component instance named driver of type Driver,

Acquisition acquisition;

A component instance named acquisition of type Acquisition, which is a system component itself,

Optics optics;

An instance of another system component,

control <=> driver.control;

A binding of the Camera’s port control to the port named control of the driver instance.

driver.acquisition <=> acquisition.port;

A binding between pairs of ports on component instances.

The light blue components in the system view, such as lens are foreign components (See Components); their definition looks like this:

component Lens
{
  provides ILens port;
}

A foreign component does not specify any implementation: neither a behavior nor a system; its behavior is said to be implementation elsewhere, and in a foreign language (in this case C++).

The full example is contained in the source tree at test/all/Camera/Camera.dzn or Camera.dzn.

The simplified⁵ state diagram:

4.4 The Lego Ball Sorter

The Lego Ball Sorter example demonstrates how Dezyne can be used to write the operating system for a machine. The system view is already somewhat overwhelming:

so it makes more sense to look at smaller parts of the system, such as the MaterialHandler:

The full example is contained in the source tree at
test/all/LegoBallSorter/LegoBallSorter.dzn or
LegoBallSorter.dzn.

5.1 Direct in event

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

interface I
{
 in void a ();
 behavior
 {
   on a: {}
 }
}

component direct_in
{
  provides I p;
  requires I r;
  behavior
  {
    on p.a (): r.a ();
  }
}

5.2 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 ();
  behavior
  {
    on inevitable: a;
  }
}

component direct_out
{
  provides I p;
  requires I r;
  behavior
  {
    on r.a (): p.a ();
  }
}

5.3 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. The below 2 versions of the component are indistinguishable looking from the outside.

Notice that the interface declares that a and b are executed atomically. While in the behavior of the component each event is handled or forwarded independently. However to an observer of the provides interface of the component a and b are again executed atomically.

interface I
{
  out void a ();
  out void b ();
  behavior
  {
    on inevitable: {a; b;}
  }
}

component direct_multiple_out1
{
  provides I p;
  requires I r;
  behavior
  {
    on r.a (): p.a ();
    on r.b (): p.b ();
  }
}

import direct_multiple_out.dzn;

component direct_multiple_out2
{
  provides I p;
  requires I r;
  behavior
  {
    on r.a (): {}
    on r.b (): {p.a (); p.b ();}
  }
}

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

5.4 Indirect in event

A requires port in-event (r.a) call resulting in a requires port out-event (r.b).

interface U
{
  out void unused ();
  behavior
  {
    on inevitable: unused;
  }
}


interface I
{
  in void b ();
  out void a ();
  behavior
  {
    on inevitable: a;
    on b: {}
  }
}


component indirect_in
{
  provides U p;
  requires I r;
  behavior
  {
    on r.a (): r.b ();
  }
}

5.5 Indirect out event

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

interface I
{
  in void a ();
  out void b ();
  behavior
  {
    on a: b;
  }
}

component indirect_out
{
  provides I p;
  requires I r;
  behavior
  {
    on p.a (): r.a ();
    on r.b (): p.b ();
  }
}

5.6 Indirect multiple out events

Since the provided interface is the same in the three cases below the externally visible behavior is identical.

The three different behavior implementations of the component show the subtle differences in the internal handling of messages.

interface I
{
  in void a ();
  out void b ();
  behavior
  {
    on a: b;
  }
}

component indirect_multiple_out1
{
  provides I p;
  requires I r1;
  requires I r2;
  behavior
  {
    on p.a (): {r1.a (); r2.a ();}
    on r1.b (): {}
    on r2.b (): p.b ();
  }
}

import indirect_multiple_out.dzn;

component indirect_multiple_out2
{
  provides I p;
  requires I r1;
  requires I r2;
  behavior
  {
    on p.a (): {r1.a (); r2.a ();}
    on r1.b (): p.b ();
    on r2.b (): {}
  }
}

import indirect_multiple_out.dzn;

component indirect_multiple_out3
{
  provides I p;
  requires I r1;
  requires I r2;
  behavior
  {
    on p.a (): r1.a ();
    on r1.b (): r2.a ();
    on r2.b (): p.b ();
  }
}

5.7 Indirect blocking out event

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

interface I
{
  in void a ();
  out void b ();
  behavior
  {
    on a: b;
  }
}

interface I2
{
   in void a ();
   out void b ();
   behavior
   {
     bool idle = true;
     [idle] on a: idle = false;
     [!idle] on a: illegal;
     [!idle] on inevitable: {idle = true; b;}
   }
}

component indirect_blocking_out
{
  provides blocking I p;
  requires I2 r;
  behavior
  {
    blocking on p.a (): r.a ();
    on r.b (): {p.b (); p.reply ();}
  }
}

If the keyword blocking in above example would be omitted it would lead to an erroneous situation since the provides in-event (p.a) would return before the provides out-event (p.b) would have been generated.

5.8 External multiple out events

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

The first example shows how the behavior of external J1 interface transforms into the interface behavior of I1 by forwarding the events in the external_multiple_out1 component behavior.

interface I1
{
  in void e ();
  out void a ();
  out void b ();
  behavior
  {
    enum status {IDLE, A, B};
    status state = status.IDLE;
    [state.IDLE] on e: state = status.A;
    [!state.IDLE] on e: illegal;
    [state.A] on inevitable: {state = status.B; a;}
    [state.B] on inevitable: {state = status.IDLE; b;}
  }
}

interface J1
{
  in void e ();
  out void a ();
  out void b ();
  behavior
  {
    on e: {a; b;}
  }
}

component external_multiple_out1
{
  provides I1 p;
  requires external J1 r;
  behavior
  {
    bool idle = true;
    [idle] on p.e (): {idle = false; r.e ();}
    [!idle] on p.e: illegal;
    on r.a (): p.a ();
    on r.b (): {idle = true; p.b ();}
  }
}

Two variations of the model above can be considered. Both variants provide the same interface behavior (I2 and I3 are identical), but differ in their requires interface behavior and as a result in their component behavior.

The first variant uses the requires behavior (J1 and J2 are identical) as the first example. The component takes care of joining the independently received events a and b as required by its provides interface.

interface I2
{
  in void e ();
  out void a ();
  out void b ();
  behavior
  {
    bool idle = true;
    [idle] on e: idle = false;
    [!idle] on inevitable: {idle = true; a; b;}
  }
}

interface J2
{
  in void e ();
  out void a ();
  out void b ();
  behavior
  {
    on e: {a; b;}
  }
}

component external_multiple_out2
{
  provides I2 p;
  requires external J2 r;
  behavior
  {
    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 ();}
  }
}

This variation provides the same interface as it requires. The component however, must make sure to join a and b again to implement its provides interface behavior.

interface I3
{
  in void e ();
  out void a ();
  out void b ();
  behavior
  {
    bool idle = true;
    [idle] on e: idle = false;
    [!idle] on e: illegal;
    [!idle] on inevitable: {idle = true; a; b;}
  }
}

component external_multiple_out3
{
  provides I3 p;
  requires external I3 r;
  behavior
  {
    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 ();}
  }
}

5.9 Indirect blocking multiple external out events

The two requires 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 behavior is the same in both cases.

interface I
{
  in void a ();
  out void b ();
  behavior
  {
    on a: b;
  }
}

component indirect_blocking_multiple_external_out
{
  provides blocking I p;
  requires external I r1;
  requires external I r2;
  behavior
  {
    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 ();
  }
}

5.10 Multiple provides

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

1. ihello

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

2. 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.

5.11 Blocking multiple provides

The blocking keyword can (since 2.15) also be used in combination with multiple provides ports. In our explanation we will introduce a component that does two things. First it multiplexes the provides ports events over a single requires port. Secondly it maps the synchronous behavior of the provides ihello interfaces onto the asynchronous behavior of the requires iworld interface (see the interface declarations at the end of this section).

import ihello.dzn;
import iworld.dzn;

component blocking_multiple_provides
{
  provides blocking ihello left;
  provides blocking ihello right;
  requires iworld r;

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

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

    [side.Left] blocking on right.hello(): pending = Side.Right;
    [side.Right] blocking on left.hello(): pending = Side.Left;

    on r.world():
    {
      if(side.Left) left.reply();
      if(side.Right) right.reply();
      if(!pending.None) r.hello();
      side = pending;
      pending = Side.None;
    }
  }
}

In the event sequence trace below we can see that for each provides port that asynchronous hello world transaction is encapsulated.

5.12 Blocking in system context

Blocking has a direct effect on a single event, but it also influences the rest of the system behavior. To investigate the effects of the blocking keyword in system context, we will describe two examples. In the first example we concentrate our attention on the event interleaving at the provides ports. The second example focusses on the interleaving of events that originate from the requires ports.

The indirect effect of the use of the blocking keyword is referred to as collateral blocking. Blocking an event means making the caller wait by withholding its return until some state has been reached which is indicated by another event. To achieve this, the other processes outside the component that is applying the blocking keyword must be able to make progress. Furthermore the component must be exposed to this progress to be able to resolve the blocking situation by returning to its caller.

Let us recapitulate blocking with a small example component that will be used by each of the examples in this section.

import iblock.dzn;
import iworld.dzn;

component block
{
  provides blocking iblock b;
  requires iworld w;
  behavior
  {
    blocking on b.block():
    {
      w.hello();
      //execution waits here for b.reply()
      //to occur as a result of w.world()
    }

    on w.world(): b.reply();
  }
}

Here we see component block that withholds its return on port b until it has received event r.world. Remember that a significant amount of time may pass between r.hello and r.world. During this time the rest system that contains our block component could make progress, without the component becoming aware. If we add more system context to our block component we can see how collateral blocking manifests itself. We will add component collateral as a client to block.

import ihelloworld.dzn;
import iworld.dzn;
import iblock.dzn;

component collateral
{
  provides blocking ihelloworld h;
  requires blocking iblock b;
  requires iworld w;

  behavior
  {
    bool idle = true;
    [idle] on h.hello(): {w.hello(); b.block(); idle = false;}
    [!idle] on w.world(): {h.world(); idle = true;}
  }
}

Besides being a client to component block this component is also a client to another regular non-blocking component. The event sequence trace below shows the first of the two possible scenarios implemented by the collateral component.

In this first scenario nothing is out of the ordinary, but now take a look at the second event sequence trace below.

Here we can see that during the time between b.block and b.return the world event on port w is allowed to occur. This is the result of the fact that although the collateral component is blocked on its call to b.block, it will find w.world in its queue before returning to its caller. And as a result, forwarding w.world as h.world will occur before returning to its caller, which differs from the previous scenario. Verification of component collateral will check for both scenarios and ensure that the component behavior complies with all of the inteface behavior or otherwise report the non-compliant scenario. Verification relies on the blocking annotation on port b in order to infer the collateral blocking scenario and check for it.

• Collateral blocking and multiple provides.

5.12.1 Collateral blocking and multiple provides.

We can now revisit the blocking multiple provides example. Instead of making the multiplexing component responsible for the synchronization, we can also add a level of indirection by splitting up blocking_multiple_provides into a separate component that takes care of synchronizing the asynchronous behavior and a separate multiple provides component. The latter can be expressed as component mux below:

import ihello.dzn;
import iblock.dzn;

component mux
{
  provides blocking ihello left;
  provides blocking ihello right;

  requires blocking iblock b;

  behavior
  {
    on left.hello(): b.block();
    on right.hello(): b.block();
  }
}

This component, notwithstanding the blocking annotations on its ports, behaves exactly like component multiple_provides. However, when we bring its clients into scope we get the system model below.

import mux.dzn;
import proxy.dzn;

component collateral_multiple_provides
{
  provides blocking ihello left;
  provides blocking ihello right;

  requires blocking iblock block;

  system
  {
    proxy l;
    proxy r;
    mux m;

    left <=> l.h;
    l.r <=> m.left;
    right <=> r.h;
    r.r <=> m.right;

    m.b <=> block;
  }
}

In its event sequence trace we can see another impact of collateral blocking.

Although the behavior across the mux component is non-overlapping the behavior of the client components is interleaved.

Note: In Dezyne blocking is implemented by means of coroutines. Therefore the interleaving of event sequences is a form of cooperative multi-tasking. As a result its behavior is deterministic as opposed to non-deterministic as in multi-threaded interleaving.

---

6.1 Verification Checks and Errors

A prerequisite for running the verification checks is for Dezyne code to be syntactically correct: any parse error prohibits the verification from running and must be fixed first. Apart from syntactic parse errors, the parser also checks for a number of so-called “well-formedness” errors. A “well-formedness” error is a static check, i.e. a check that the parser can perform without considering runtime behavior (see See Invoking dzn parse and See Well-formedness).

Dezyne verifies for interfaces and for components:

deadlock

A deadlock in an interface occurs when the interface reaches a state in which no in-events are specified.

A deadlock is a situation where none of the components in a system can make progress; nothing can happen and the system simply does not respond. This commonly occurs when two components each require an action from the other before they can perform any further action themselves. Another common cause is when a component is waiting for some external event which fails to occur.

In general, deadlocks can be hard to find because the entire system needs to be reviewed to discover them and freedom from deadlocks is a property of the system as a whole. For example, component A might be waiting for B which is waiting for C while C is waiting for A. Dezyne ensures that this never happens. Each component by itself can be verified as being deadlock free and within Dezyne this deadlock property is compositional, which means that components can only be composed in ways that have been proven not to cause deadlock.

Note: Dezyne can only verify what it knows; therefore, e.g., handwritten code can still cause deadlocks.

Upon violation, the following error is reported:

error: deadlock in model <name>

unreachable code

An unreachable code error occurs when there is no code path possible that ever leads to the execution of the code.

illegal

A trigger that is not handled in a certain state, results in an illegal. For components this is also verified for the use of the interfaces of its requires ports.

Upon violation, the following error is reported:

error: illegal action performed in model <name>

livelock

A livelock in an interface occurs when in a certain state an inevitable event can occur without any restriction, i.e., its state does not change. This could starve the client that is interacting with this interface.

A livelock in a component occurs when it is permanently busy with internal behavior and fails to serve a provides port. For example, due to a design error such that the design is constantly interacting with its requires ports and starving a provides port; or due to the arrival rate of unconstrained external events such that processing them starves a provides port. As seen from the outside of a component, this appears very similar to deadlock. The difference is that a deadlocked component does nothing at all whereas a livelocked component might be performing lots of actions, but none of them are visible to a component’s provides port.

Upon violation, the following error is reported: livelock in model <name>

range error

Every possible assignment to a subint variable must be within its defined range.

Upon violation, the following error is reported:

error: integer range error in model <name>

type error

A trigger of a typed (i.e., non-void) event must reply a value of the type of the event.

Upon violation, the following error is reported

error: type error in model <name>

Note that trivial cases that can be checked statically, may be reported by the parser (See Well-formedness).

In addition, Dezyne verifies for interfaces:

observable non-determinism

Interfaces may specify non-deterministic behavior, as long as this non-determinism is observable by the client of that interface: after getting the response from the interface, a client must be able to determine what state the interface is in.

The snippet below shows observable non-determinism, i.e., an example of allowed non-determinism:

…
[idle] on hello: {world; idle=false;}
[idle] on hello: cruel;
…

in the idle state, upon sending hello either world or cruel may happen. This non-deterministic choice cannot be predicted. However, when the client sees world, the state of the interface is not idle, after seeing cruel, the state is idle.

This is an example of non-observable non-determinism, which is not allowed:

…
[idle] on hello: {world;idle=false;}
[idle] on hello: world;
…

as for a client it is impossible to tell if the interface is in state idle or in state not idle.

Upon violation, the following error is reported:

error: interface <name> is unobservably non-deterministic

In addition, Dezyne verifies for components:

compliance

The component together with its required interfaces implements the component behavior. The compliance check verifies that the component together with the required interfaces implements the behavior specified in the provided interface(s), i.e., whether the component honors its contracts.

Upon violation, the following error is reported:

error: component <name> is non-compliant with interface(s)\
    of provides port(s)

determinism

Components in Dezyne are required to be deterministic. The most common cause of non-determinism in a component is the ambiguous declaration of an event, often due to overlapping guards, i.e., in one state, for an event two different imperative statements are specified. Upon violation the following error is reported:

error: component <name> is non-deterministic

The event trace will indicate where and under which condition (state) the ambiguity occurs in the component behavior. Simulation of the corresponding event trace can be used to determine the exact location of the error in the input.

queue full

a Dezyne component has a queue where notification events are stored before they are processed. During verification it is checked that that this queue does not overflow, i.e., that it remains non-blocking. The component queue size can be specified for verification with the --queue-size option. The default queue size is 3.

Upon violation, the following error is reported

error: queue full in model <name>

For interfaces, the illegal check, range error check, and type error check are reported as part of the deadlock check. For components, the range error check, the type error check, and queue full check are reported as part of the illegal check.

6.2 Verification Counter Examples

A verification error does not only show the error it has detected, it also shows where it occurs. Where an error occurs is specified by means of a counter example, or an event trace.

Verifying

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

component illegal_requires
{
  provides ihello h;
  requires ihello w;

  behavior
  {
    on h.hello (): w.world ();
  }
}

gives:

$ dzn verify doc/examples/illegal-requires.dzn
model: hello
h.hello
w.hello
<illegal>

at the end of running this trace, an illegal action occurs. This implies there is an inconsistency in the behavior of the component and its interface, the contract is violated. This can either be fixed by a change to the interface behavior contract or by changing the component behavior.

6.3 Interpreting Verification Errors

Understanding why a certain verification error occurs, or how to fix it, is not always easy. The simulator can help to interpret the error and identify what is going on (See Invoking dzn simulate): It can show the source locations where the error occurs and the state the interface(s) and/or the component(s) are in.

The simulator can interpret the counter example from the verifier:

$ dzn verify doc/examples/illegal-requires.dzn \
  | dzn simulate doc/examples/illegal-requires.dzn
error: illegal action performed in model illegal_requires
(header ((h) ihello provides) ((sut) illegal_requires component) ((w) ihello requires))
(state ((h)) ((sut)) ((w)))
doc/examples/illegal-requires.dzn:6:3: error: illegal
<external>.h.hello -> ...
... -> sut.h.hello
sut.w.world -> ...
... -> <external>.w.world
<illegal>
(state ((h)) ((sut)) ((w)))
doc/examples/illegal-requires.dzn:6:3: error: illegal
(trail "h.hello" "w.world" "<illegal>")
(labels "h.hello" "h.world")
(eligible)

7.1 Interface Contracts

Dezyne does not have an exception mechanism like other languages. An exception mechanism is designed to prevent accidentally ignoring missed pre- or post-conditions. Instead, in Dezyne the interfaces establish these restrictions by means of verification (See Formal Verification). So where traditional programming languages must handle protocol violations using an exception mechanism at runtime, Dezyne prevents them using the static verification checks⁷. Interfaces in Dezyne are inherently complete with respect to their event alphabet. The generated code will accept every trigger but give an illegal response.

The illegal response is mapped to std::abort () in C++. Note that for a fully verified Dezyne system, operated by clients that adhere to the interface specifications, it is impossible for an illegal response to be triggered. In other words, when an illegal is triggered, it means that some non-Dezyne code is violating a protocol (interface specification).

• Implicit interface constraints
• Shared interface variables

interface ihmi
{
  in void enable ();
  in void disable ();

  in bool set ();
  in bool resume ();
  in void cancel ();

  out void inactive ();

  behavior
  {
    enum State {Disabled,Enabled,Active};
    enum Setpoint {Unset,Set};

    State state = State.Disabled;
    Setpoint setpoint = Setpoint.Unset;

    on disable: // always allow
    {
      state = State.Disabled;
      setpoint = Setpoint.Unset; //forget about the previous setpoint
    }

    [!state.Disabled] on enable: {/* ignore when not disabled */}
    [!state.Active] on cancel: {/* ignore when not active */}
    [!state.Enabled] on set, resume: reply (false);

    [state.Disabled] on enable: state = State.Enabled;
    [state.Enabled] {
      on set, resume: reply (false);
      on set: {state = State.Active; setpoint = Setpoint.Set; reply (true);}
      on resume: {
        [setpoint.Set] {state = State.Active; reply (true);}
        [setpoint.Unset] reply (false);
      }
    }
    [state.Active]
    {
      // this may or may not happen
      on inevitable: {state = State.Enabled; inactive;}
      on cancel: state = State.Enabled;
    }
  }
}

// observe (brake and clutch) pedals
interface ipedals
{
  in bool enable ();
  in void disable ();
  out void engage ();
  out void disengage ();
  behavior
  {
    bool monitor = false;
    bool engaged = false;
    [!monitor] {
      on enable: {monitor = true; reply (engaged);}
      on enable: {monitor = true; engaged = !engaged; reply (engaged);}
    }
    [monitor] {
      on disable: {monitor = false; engaged = false;}
      on optional: {
        engaged = !engaged;
        if (engaged) engage; else disengage;
      }
    }
  }
}

// interface to the throttle actuator PID control
interface ithrottle
{
  in void setpoint ();    // close loop and calculate actuator input
  in void reset ();  // open loop
  out void unset (); // sponaneous open loop

  behavior
  {
    bool active = false;
    on setpoint: active = true;
    [active] {
      on reset: active = false;
      on optional: {active = false; unset;}
    }
  }
}

interface itimer
{
  in void start ();
  out void timeout ();
  in void cancel ();
  behavior
  {
    bool idle = true;
    [idle] on start: idle = false;
    [!idle] on inevitable: timeout;
    on cancel: idle = true;
  }
}

interface iassert
{
  out void assert ();
  behavior
  {
    on inevitable: assert;
  }
}

import cruise-control-interfaces.dzn;

component cruise_control
{
  provides ihmi hmi;
  requires ipedals pedals;
  requires ithrottle throttle;
  requires itimer timer;
  requires iassert check;
  behavior
  {
    // functional property that asserts no unwanted acceleration
    on check.assert (): {
      [!hmi.state.Active] {
        [throttle.active] illegal;
        [!timer.idle] illegal;
        [otherwise] {}
      }
      [otherwise] {
        [!throttle.active] illegal;
        [timer.idle] illegal;
        [otherwise] {}
      }
    }
    [hmi.state.Disabled] {
      on hmi.enable (): bool b = pedals.enable ();
      on hmi.disable (): {}
    }
    [!hmi.state.Disabled] {
      on hmi.enable (): {}
      on hmi.disable (): {
        if (throttle.active) throttle.reset ();
        timer.cancel ();
        pedals.disable ();
      }
    }
    [hmi.state.Enabled && timer.idle] {
      [pedals.engaged] on hmi.set (): reply (false);
      [!pedals.engaged] on hmi.set (): {
        throttle.setpoint ();
        timer.start ();
        reply (true);
      }
      on hmi.resume (): {
        [pedals.engaged || !hmi.setpoint.Set] reply (false);
        [otherwise] {
          throttle.setpoint ();
          timer.start ();
          reply (true);
        }
      }
    }
    [!hmi.state.Enabled || !timer.idle] {
      on hmi.set (), hmi.resume (): reply (false);
    }
    on timer.timeout (): {
      if (!hmi.state.Active) illegal;
      throttle.setpoint ();
    }
    on hmi.cancel (): {
      if (hmi.state.Active) {
        throttle.reset ();
        timer.cancel ();
      }
    }
    on pedals.disengage (): {/*ignore*/}
    on pedals.engage ()
      , throttle.unset (): {
      if (hmi.state.Active) {
        hmi.inactive ();
        timer.cancel ();
        if (throttle.active) throttle.reset ();
      }
    }
  }
}

7.2 Error Handling and Recovery

The errors of concern here are not programming or design errors, but behavior that may occur and must be handled appropriately. Like a file open request because of a non existing file. Therefore these errors are at least runtime errors.

For a system, which behavior emerges as a result of its function and its interaction with an unpredictable environment, the Pareto principle holds for the distribution of its main functions and its error handling across its behavior. Typically about 10%-20% of the events that signal an error, result in 90%-80% of the behavior associated with error handling. While 90%-80% of the events that relate to the main functions of the system typically result in 10%-20% percent of the overall behavior which is unrelated to error handling.

Error handling is most often a matter of redirecting the handling to the party in charge to allow them to attempt recovery by retrying, continue with reduced or gracefully degraded function, by failing safely altogether, or continue as normal treating the error as a warning.

Dezyne is very effective in allowing engineers to discover the emergent error behaviors–i.e., without having to resolve to devising test scenarios, writing test code and running tests—as well as designing the handling of the respective error conditions.

7.3 Armoring

A common programming adagium is to be liberal what you accept and strict in what you deliver. Verification clearly depends on the accuracy with which the behavior of the environment is described by its interface specifications. Any inconsistency with reality may lead the execution of the code into unverified territory. To avoid this we can apply an approach called armoring. An armor is a defensive layer of components that protects the armored components who rely on their interface contracts from any behavior which would violate those contracts. An armoring component can be developed in Dezyne itself by creating a permissive interface from the strict interface behavior and letting the armor component map one behavior onto the other making sure the permissive behavior never violates the strict behavior.

Consider this simple strict interface

interface istrict
{
  in void request ();
  in void cancel ();
  out void notify ();

  behavior
  {
    bool idle = true;
    [idle] on request: idle = false;
    [!idle]
    {
      on cancel: idle = true;
      on inevitable: {idle = true; notify;}
    }
  }
}

used by this simple proxy component

import istrict.dzn;

/*
component proxy // a proxy pre 2.17.0
{
  provides istrict p;
  requires istrict r;

  behavior
  {
    bool idle = true;
    [idle] on p.request (): {r.request (); idle = false;}
    [!idle]
    {
      on p.cancel (): {r.cancel (); idle = true;}
      on r.notify (): {p.notify (); idle = true;}
    }
  }
}
*/

component proxy // a trivial proxy post 2.17.0
{
  provides istrict p;
  requires istrict r;

  behavior
  {
    on p.request (): r.request ();
    on p.cancel (): r.cancel ();
    on r.notify (): p.notify ();
  }
}

Because the istrict interface is stateful, a problem occurs when the enviroment would erroneously issue a second p.request event before receiving an r.notify.

Now consider this permissive interface

interface ipermissive // derives from istrict
{
  in void request ();
  in void cancel ();
  out void notify ();

  behavior
  {
    on request: {}
    on cancel: {}
    on optional: notify;
  }
}

that shares its event alphabet with istrict. Being permissive means that it will accept any of the events, regardless of the history.

Using the ipermissive interface we can derive a simple top armor component

import istrict.dzn;
import ipermissive.dzn;

component top_armor
{
  provides ipermissive p;
  requires istrict r;

  behavior
  {
    bool idle = true;
    [idle]
    {
      on p.request (): {idle = false; r.request ();}
      on p.cancel (): {}
    }
    [!idle]
    {
      on p.request (): {}
      on p.cancel (): {idle = true; r.cancel ();}
      on r.notify (): {idle = true; p.notify ();}
    }
  }
}

and likewise, a bottom_armor component

import istrict.dzn;
import ipermissive.dzn;
import iwatchdog.dzn;

component bottom_armor
{
  provides istrict p;
  requires ipermissive r;
  requires iwatchdog w;

  behavior
  {
    bool idle = true;
    [idle]
    {
      on p.request (): {idle = false; w.set (); r.request ();}
      on r.notify (): {}
    }
    [!idle]
    {
      on p.cancel (): {idle = true; w.cancel (); r.cancel ();}
      on r.notify (),
         w.timeout (): {idle = true; w.cancel (); p.notify ();}
    }
  }
}

The permissive interface is to be used on both sides of the armored_system. The system connects each permissive interface to a dedicated armor component, one for the top of the system and one for the bottom. Both protecting the inside component called proxy.

import proxy.dzn;
import top_armor.dzn;
import bottom_armor.dzn;

component watchdog
{
  provides iwatchdog w;
}

component armored_system // is permissive, but armored
{
  provides ipermissive p;
  requires ipermissive r;

  system
  {
    p <=> ta.p;
    top_armor ta;

    ta.r <=> m.p;
    proxy m; // the soft but strict middle
    m.r <=> ba.p;

    bottom_armor ba;
    watchdog w;
    ba.w <=> w.w;
    ba.r <=> r;
  }
}

8.1 Integrating C++ Code

This chapter describes the C++ code that is generated by Dezyne and the integration thereof.

• Introduction
• Interfaces
• Components
• Systems
• Integration

interface some_interface
{
  in void in_event();
  out void out_event();

  behavior
  {
    on in_event: out_event;
  }
}

struct some_interface
{
  struct
  {
    dezyne::function<void ()> in_event;
  } in;
  struct
  {
    dezyne::function<void ()> out_event;
  } out;
};

void foo () {}
some_interface port;
port.out.out_event = foo;
port.in.in_event = port.out.out_event;

import some_interface.dzn;

component some_component
{
  provides some_interface provided_port;
  requires some_interface required_port;
  behavior{}
}

struct some_component
{
  some_interface provided_port;
  some_interface required_port;
  some_component ()
    : provided_port ()
    , required_port ()
  {
    provided_port.in.in_event
      = dezyne::ref (required_port.in.in_event);
    required_port.out.out_event
      = dezyne::ref (provided_port.out.out_event);
  }
};

8.1.4 Systems

Along the same lines a Dezyne system may aggregate other components and systems and bind them together by their ports. For example:

import some_component.dzn;

component some_system
{
  provides some_interface provided_port;
  requires some_interface required_port;
  system
  {
    some_component top;
    some_component middle;
    some_component bottom;
    provided_port <=> top.provided_port;
    top.required_port <=> middle.provided_port;
    middle.required_port <=> bottom.provided_port;
    bottom.required_port <=> required_port;
  }
}

or depicted in a diagram:

#include "some_system.hh"
#include "dezyne/runtime.hh"
#include "dezyne/locator.hh"
int main()
{
  dezyne::locator loc;
  dezyne::runtime rt;
  loc.set (rt);
  //construct the system
  some_system system (loc);
  //connect the outer events directed at the system
  system.provided_port.out.event = []{
    std::cout << "system.provided_port.out.event" << std::endl;
  };
  system.required_port.in.event  = []{
    std::cout << "system.required_port.in.event" << std::endl;
  };
  //and finally fire some of the external events
  system.provided_port.in.event ();
  system.required_port.out.event ();
}

interface Foo
{
  in void bar();
  behavior
  {
    on bar:{}
  }
}
component some_component2
{
  provides some_component2 provided_port;
  requires injected Foo required_port;
  behavior { /* ...  */ }
}

int main()
{
  dezyne::locator loc;
  dezyne::runtime rt;
  loc.set (rt);
  Foo foo;
  foo.in.bar = []{/*no op*/};
  loc.set (foo);
  some_component comp (loc);
  comp.provided_port.in.in_event ();
}

8.2 Foreign Component

We already saw how to connect code directly to event slots in the interface. If we desire to encapsulate this code, we can use a component without a behavior⁸ to achieve this. The code generator will generate a similar C++ representation for components with and without behavior. The only difference is that a component without behavior declares pure virtual functions which must be implemented by a struct of class which inherits from the generated C++ representation. Note that this approach is not suitable to wrap a Dezyne component or system, since it would add the Dezyne semantic constraints via the runtime library a second time. The derived struct or class must have the same name as the component in Dezyne. To avoid a naming conflict, the generated representation with the same name as the Dezyne component is placed into the skel⁹ namespace.

It may not be obvious that we may run into a conflict when we put our foreign component in a file with the same name as the component. The reasons for this are as follows. Names introduced in Dezyne are also used by the generated code to refer to component representations. If a component is not defined locally Dezyne import is mapped to a #include. This means that the actual implementation of a foreign component must be in a file with the name derived from the component name. Therefore the component representation in the skel namespace is not written to the same file, the code generator simply refuses this. The solution is to put foreign component definitions into another file, for instance in the file of the system instantiating the component.

When implementing the foreign component the compiler must also be able to see the representation in the skel namespace. The code generator makes sure that the actual implementation inheriting the skel representation is included directly after it. Therefore we do not have to include anything into the header file of our foreign implementation. However, if we put the actual definition into a separate source file, we must include both the header file of the actual foreign component as well as the header file declaring the skel representation.

An example will help clarifying:

// hello_foreign.dzn

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

  behavior
  {
    on hello: world;
  }
}

component foreign
{
  provides ihello p;
}

component hello
{
  provides ihello p;
  requires ihello r;

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

component hello_foreign
{
  provides ihello p;

  system
  {
    p <=> h.p;
    hello h;
    h.r <=> f.p;
    foreign f;
  }
}

// end of hello_foreign.dzn

Here we see an interface ihello, a foreign component, a regular component hello and a system hello_foreign being defined.

For C++ the code generator produces a hello_foreign.hh and a hello_foreign.cc file. Since hello_foreign instantiates the component foreign, it will #include a file called foreign.hh. The contents of this file might look something like this:

#ifndef FOREIGN_HH
#define FOREIGN_HH

struct foreign: public skel::foreign
{
  foreign (const dzn::locator &locator)
    : skel::foreign (locator)
  {}
  void p_hello ()
  {
    p.out.world ();
  }
};

#endif

Note the absence of an #include statement.

If we want to move all member function definitions from the header file to a source file, we might write foreign.cc like this.

#include "hello_foreign.hh"

foreign::foreign (const dzn::locator &locator)
  : skel::foreign (locator)
{}

void foreign::p_hello ()
{
  p.out.world ();
}

Note the presence of #include "hello_foreign.hh" and remember this already includes foreign.hh.

8.3 Thread-safe Shell

A Dezyne Thread-safe Shell guarantees safe use of a Dezyne system component in a multi-threaded environment. It also implements the use of the blocking and the defer keywords.

• Shell Syntax
• Semantics
• Shell Example
• See also:

  dzn code -l c++ -s SYSTEM FILE    (1)

component SYS {
  provides IA pp;
  requires IA rp;
  system {
    BHV bhv;
    pp <=> bhv.pp;
    bhv.rp <=> rp;
  }
}
component BHV {
  provides IA pp;
  requires IA rp;
}
extern int $int$;
interface IA {
  in void iv(int i);
  out void o(int i);
  behavior {
    on iv: {}
    on optional: o;
  }
}

#ifndef SYS_HH
#define SYS_HH
#include #include #include #include #include "BHV.hh"
#include "IA.hh"
#include "IA.hh"
namespace dzn {struct locator;}
struct SYS
{
  dzn::meta dzn_meta;
  dzn::runtime dzn_runtime;
  dzn::locator dzn_locator;
  BHV bhv;
  IA pp;
  IA rp;
  dzn::pump dzn_pump;
  SYS (dzn::locator const&);
};
#endif // SYS_HH

#include "SYS.hh"
SYS::SYS (dzn::locator const& locator)
: dzn_meta{"","SYS",0,{&bhv.dzn_meta},{}}
, dzn_locator (locator.clone ().set (dzn_runtime).set (dzn_pump))
, bhv(dzn_locator)
, pp (bhv.pp)
, rp (bhv.rp)
, dzn_pump ()
{
  pp.in.iv = [&] (int i) {
    return dzn::shell (dzn_pump, [&,i] {return bhv.pp.in.iv (i);});
  };
  rp.out.o = [&] (int i) {
    return dzn_pump ([&,i] {return bhv.rp.out.o (i);});
  };
  bhv.pp.out.o = std::ref (pp.out.o);
  bhv.rp.in.iv = std::ref (rp.in.iv);
  bhv.dzn_meta.parent = &dzn_meta;
  bhv.dzn_meta.name = "bhv";
}

8.4 Integrating Scheme Code

Note: The Scheme code generator is still considered experimental; use with caution.

To enable the Scheme code generator, configure by doing something like

./configure --enable-languages=scheme --with-courage

Dezyne comes with a code generator for GNU Guile see Guile reference manual. Scheme is an interesting language for using with Dezyne. It supports a functional programming style that can be applied in handwritten code.

Program code written in a purely functional style is more reasonable than imperative code and especially so for concurrent programs (see Modularity Objects and State in Structure and Interpretation of Computer Programs). The Scheme code for Dezyne components that is generated by the code generator (See Invoking dzn code) can still use assignments to store state in an imperative way, but that is not a problem as this code is verified: the most tricky aspects of the software are left to Dezyne!

• Namespace to Module

9.1 Invoking dzn

The dzn command is a front-end to Dezyne functions, such as verification, code generation, simulation, etc. Those functions all have their own sub command:

dzn dzn-option… command command-option… FILE...

Running dzn without a sub command shows a brief help text and the list of available dzn commands.

The dzn-options can be used with every dzn command and can be among the following:

--debug

-d

Enable debug output.

--help

-h

Display help on invoking dzn, and then exit.

--skip-wfc

-p

Skip well-formedness checking.

The well-formedness checking of a large program can take a significant amount of time. As the well-formedness check does not change a correct AST in any way, it can be safely skipped when parsing a previously checked and unmodified program (See Invoking dzn parse).

--timings

-T

Show detailed Scheme and mCRL2 timing information.

--transform=trans

-c trans

Apply transformation trans after parsing. Use dzn --help --verbose to show all transformations. This option can be used more than once. For example,

dzn code -l dzn -t add-explitic-temporaries -t -o- normalize:compounds test.dzn
dzn code -l dzn -t 'inline-functions(f)' -t -o- normalize:compounds test.dzn

will inline function f and remove redundant compound-statements created by the inlining.

--verbose

-v

Be more verbose, show progress.

--version

-V

Display the current version of dzn, and then exit.

Note: The dzn-options are placed between dzn and the sub command, e.g. to increase verbosity when using dzn verify, use

dzn -v verify file.dzn

9.2 Invoking dzn code

While the simulator (See Invoking dzn simulate) can interpret Dezyne code directly, to create an executable program Dezyne uses a code generator.

This code generator, the command dzn code, generates compilable or runnable code for a Dezyne file, such as C++. Usually—i.e., except for trivial cases—this generated Dezyne code is combined with “handwritten” code in the target language to create a Dezyne application, See Code Integration.

dzn dzn-option… code option… FILE

The options can be among the following:

--calling-context=type

-c type

Generate an extra parameter of type for every event.

--help

-h

Display help on invoking dzn code, and then exit.

--import=dir

-I dir

Add directory dir to the import path.

--init=PROCESS

When generating mCRL2 code, use init PROCESS. For other language backends, this options is ignored.

--language=language

-l language

Generate code for language language.

--model=model

-m model

Generate a trivial main for model. This “generated main” can execute an event trace read from stdin, and writes a code trace to stderr. See Getting Started.

--no-constraint

-C

Do not use a constraining process.

--no-unreachable

-U

Do not generate tags for the unreachable code check.

--output=dir

-o dir

Write output to directory dir (use - for standard output).

--queue-size=size

-q size

When generating mCRL2 code, use component queue size size for verification, the default is 3. For other language backends, this options is ignored.

--queue-size-defer=size

When generating mCRL2 code, use defer queue size size for verification, the default is 2. For other language backends, this options is ignored.

--queue-size-external=size

When generating mCRL2 code, use extternal queue size size for verification, the default is 1. For other language backends, this options is ignored.

--shell=model

-s model

Generate thread-safe system shell for model model. This option can be used multiple times. See Thread-safe Shell.

9.3 Invoking dzn graph

The dzn graph command can be used to generate different graphs from a Dezyne model.

dzn dzn-option… graph option… FILE

The options can be among the following:

--backend=type

-b type

Generate a diagram using backend type; one of dependency, lts, state, or system and write it to standard output. The default is system.

The state diagram can simplified using options --hide and --remove.

Under the hood, lts and state use the Dezyne VM. LTSs can be queried and manipulated using dzn lts (Invoking dzn lts) and the mCRL2 tooling.

Note: Generating an LTS for a large component or system using the VM can be very time-consuming. For generating an LTS using the verification engine, see (Invoking dzn verify) and (Invoking dzn traces).

--format=format

-f format

Print trace in format format; one of aut, dot, or json. For --lts the default is aut, for other formats the default is dot.

Note: The json can be processed by Dezyne-P5 to draw state and system diagrams in a browser.

--help

-h

Display help on invoking dzn graph, and then exit.

--hide=hide

-H hide

Generate a state diagram and hide hide from the transitions; one of labels (hide everything), actions or returns.

--import=dir

-I dir

Add directory dir to the import path.

--model=model

-m model

Generate graph for model model. The default is to use the most “interesting” model.

--queue-size=size

-q size

Use component queue size size for exploration, the default is 3.

--queue-size-defer=size

Use defer queue size size for exploration, the default is 2.

--queue-size-external=size

Use external queue size size for exploration, the default is 1.

--remove=vars

-R vars

Generate a state diagram and remove variables from nodes remove; one of ports or extended.

ports Hides the state of the component’s or system’s ports, extended hides the interface’s or component’s extended state, i.e., all but the main (first) state variable and implies ports.

9.4 Invoking dzn hello

The dzn hello command can be used to test your installation; it echos “hello” to standard output.

dzn dzn-option… hello

The options can be among the following:

--help

-h

Display help on invoking ide hello, and then exit.

9.5 Invoking dzn language

The dzn language command produces Dezyne language completion results and location information. It can be used by an editor or IDE to create a rich editing experience.

dzn dzn-option… language option… FILE

The options can be among the following:

--complete

-c

Show completion result; this is the default action.

--help

-h

Display help on invoking dzn language, and then exit.

--import=dir

-I dir

Add directory dir to the import path.

--offset=offset

Use offset offset to determine context.

--line=line,column

--point=line,column

-p line,column

Calculate offset from line line and column column.

--lookup

-l

Show lookup result.

--verbose

-v

Display input, parse tree, offset, context and completions.

9.6 Invoking dzn lts

The dzn lts command can be used to manipulate and query a labeled transition system (lts) in Aldebaran (aut) format (See Invoking dzn graph, See Invoking dzn verify, See Invoking dzn traces).

dzn dzn-option… lts option… [FILE]…

The options can be among the following:

--cleanup

-c

Rewrite mCRL2 labels to Dezyne, optionally remove prefix as specified with --prefix.

--deadlock

-d

Detect deadlock in lts (after introduction of failures) and produce a witness.

--exclude-illegal

Remove edges leading to illegal (in combination with --failures).

--failures

-f

Introduce a failure for each ’optional’ event into the lts.

--help

-h

Display help on invoking dzn lts, and then exit.

--illegal

-i

Detect whether lts contains <illegal> labels.

--livelock

-l

Detect tau-loops in lts and produce a witness.

--deterministic-labels=label[,label…]

-n label[,label…]

Detect whether lts is deterministic by detecting multiple edges of label from a single state, and produce a witness.

--prefix=prefix

Optional prefix for --cleanup

--tau=event[,event…]

-t event[,event…]

Hide all events from lts.

--exclude-tau=event[,event…]

Exclude given events from ’--tau’ list.

--single-line

-s

Report each error including its trace (witness) on a single line.

9.7 Invoking dzn parse

The dzn parse command parses a Dezyne file and reports any errors, both syntax errors as well as “well-formedness” errors. The Dezyne parser consists of three stages:

1. The PEG parser creates a raw parse-tree¹⁰,
2. The parse-tree is converted into the abstract syntax tree (AST),
3. A number of so-called “well-formedness” checks are performed on the AST that ascertain type correctness and detect semantic errors (See Well-formedness),
4. After parsing, some commands perform a normalization on the AST.

The well-formedness checking of a large program can take a significant amount of time. As the well-formedness check does not change a correct AST in any way, it can be safely skipped when parsing a previously checked and unmodified program (See Invoking dzn).

Usually, the parser is invoked implicitly by commands like dzn verify and dzn code. It can be useful to do an explicit check for errors, for example after saving a Dezyne file (See The Perfect Setup). Its syntax is:

dzn dzn-option… parse option… FILE

The options can be among the following:

--preprocess

-E

Resolve imports and produce a content stream. This pre-processed content can also be processed later by the parser and it has the advantage of being independent of the file-system.

--help

-h

Display help on invoking dzn parse, and then exit.

--import=dir

-I dir

Add directory dir to the import path.

--list-models

List the Dezyne models defined in the file, with their type.

--locations

-L

Show locations in output ast.

--model=model

-m model

Only output ast for model model.

--parse-tree

-t

Write the raw peg parse tree, skip generating a full ast,

--output=file

-o file

Write ast to file, use “-” for standard output.

9.8 Invoking dzn simulate

The dzn simulate command starts a simulation run.

Under the hood, dzn simulate uses the Dezyne VM. The simulator can be used to explore Dezyne models (interfaces, components, and systems), and to interpret error traces (witnesses) from the verification engine (See Getting Started). It shows code locations, state, and state transitions and produces friendly error messages. The simulator and verification both report the same errors (See Formal Verification). The simulator, however, only reports errors that it encounters while interpreting a specific event trace. The verifier performs an exhaustive search for errors but only produces a witness and does not report any context information. Its syntax is:

dzn dzn-option… simulate option… FILE

The options can be among the following:

--format=format

-f format

Print trace in format format; one of diagram, event, or trace. The default is trace.

--help

-h

Display help on invoking dzn simulate, and then exit.

--import=dir

-I dir

Add directory dir to the import path.

--internal

-i

Display internal events when using the diagram trace format.

--locations

-l

Display locations in the trace, this implies --format=trace.

--model=model

-m model

Start simulating model. The default is the most “interesting” model.

--no-compliance

-C

Do not run the compliance check.

--no-deadlock

-D

Do not run the deadlock check at the end of the trail (EOT).

--no-interface-determinism

Do not run the observable non-determinism check on interfaces.

--no-interface-livelock

Do not run the interface livelock check at the end of the trail (EOT).

--no-queue-full

-Q

Do not run the external queue-full check at the end of the trail (EOT).

--no-refusals

-R

Do not run the compliance check for the failures model refusals check at the end of the trail (EOT).

--queue-size=size

-q size

Use component queue size size for simulation, the default is 3.

--queue-size-defer=size

Use defer queue size size for simulation, the default is 2.

--queue-size-external=size

Use external queue size size for simulation, the default is 1.

--strict

-s

Use strict matching of trail, i.e., the trail must contain all observable events.

--trail=trail

-t trail

Use trail trail. The default is to read from stdin.

--verbose

-v

Display non-communication steps in the trace, this implies --format=trace, --locations.

9.9 Invoking dzn trace

The dzn trace command is a pseudo-filter to convert between different trace formats:

event trace (trail)

An event trace or trail is a list of event names observable by interacting with a Dezyne model, for example, for doc/examples/hello-world.dzn:

p.hello
p.world
p.return

event trace (character separated)

Some tools, such as the simulator also read an event trace separated by a comma or a space:

 p.hello,p.world,p.return
"p.hello p.world p.return"

code trace (arrow trace)

The Dezyne executable code can produce a trace showing the sender and the receiver of an event on the same line:

<external>.p.hello -> sut.p.hello
<external>.p.world <- sut.p.world
<external>.p.return <- sut.p.return

simulator trace (split-arrow trace)

The simulator produces a trace showing the sender and the receiver of an event both on their own line:

<external>.p.hello -> ...
... -> sut.p.hello
... <- sut.p.world
<external>.p.world <- ...
... <- sut.p.return
<external>.p.return <- ...

which is especially useful when the lines are prefixed with location information.

The dzn trace command reads arrow traces and converts them to a code trace (the default) or an event trace. A split-arrow trace can also be converted to an ASCII sequence diagram. Its syntax is:

dzn dzn-option… trace option… [FILE]

The options can be among the following:

--format=format

-f format

Display trace in format format, one of diagram, event, json, or sexp. The default is code.

Note: The json can be processed by Dezyne-P5 to draw a trace diagram in a browser.

--help

-h

Display help on invoking dzn trace, and then exit.

--internal

-i

Show communication between components in the system. When using the option --format=diagram on a system trace, the communication between components in the system is hidden by default.

--locations

-L

Show locations in output.

--meta

-m

When using format=event also show meta-events, such as <defer> and <illegal>.

--trace=trace

-t trace

Use trace trace. The default is to read from standard input.

9.10 Invoking dzn traces

The dzn traces command generates an exhaustive set of event traces or trails for a behavioral Dezyne model. It can also be used to generate an lts in Aldebaran format (See Invoking dzn lts, See Invoking dzn graph, See Invoking dzn verify).

Under the hood, dzn traces uses dzn code and mCRL2.

dzn dzn-option… traces option… FILE

The options can be among the following:

--flush

-f

Include <flush> events in trace.

--help

-h

Display help on invoking dzn traces, and then exit.

--illegal

-i

Include traces that lead to an illegal.

--import=dir

-I dir

Add directory dir to the import path.

--lts

-l

Instead of generating trace files, generate an lts in Aldebaran format.

--model=model

-m model

Generate traces for model model.

--no-constraint

-C

Do not use a constraining process.

--output=dir

-o dir

Write trace files to directory dir.

--queue-size=size

-q size

Use component queue size size for generation, the default is 3.

--queue-size-defer=size

Use defer queue size size for trace generation, the default is 2.

--queue-size-external=size

Use external queue size size for trace generation, the default is 1.

--traces

-t

Generate trace files, this is the default. Using --traces will generate trace files even when --lts is used.

9.11 Invoking dzn verify

The dzn verify command exhaustively checks a Dezyne file for verification errors in Dezyne models. See Formal Verification.

dzn dzn-option… verify option… FILE

The options can be among the following:

--all

-a

Show all errors, i.e., keep going after finding an error. By default, verification stops after finding a verification error.

--help

-h

Display help on invoking dzn verify, and then exit.

--import=dir

-I dir

Add directory dir to the import path.

--model=model

-m model

Limit verification to model, and for a behavioral component model, to its interfaces.

Note: Verification cannot be limited to system component models; verifying a system model is a no-op¹¹.

--no-constraint

-C

Do not use a constraining process.

--no-interfaces

Do not verify interfaces.

--no-unreachable

-U

Disable the unreachable code check. For large models the unreachable code check may have a serious performance impact.

--out=format ¶

Run a partial verification pipeline to produce format.

Interesting formats are mcrl2, aut, aut-dpweak-bisim, aut-weak-trace, and aut+provides-aut. Use --out=help for a full list.

The verification pipeline starts by generating mCRL2 code, which is converted into an lps and then into an lts (See Invoking dzn lts). The lts is then manipulated further.

Using the --debug on dzn (See Invoking dzn) shows the pipelines with all their commands that are being used, ready for use on the command line.

--queue-size=size

-q size

Use component queue size size for verification, the default is 3.

--queue-size-defer=size

Use defer queue size size for verification, the default is 2.

--queue-size-external=size

Use external queue size size for verification, the default is 1.

10.1 Lexical Analysis

Dezyne is a C-like language. This means that identifiers must be separated by either whitespace, delimiters or operators and is otherwise whitespace invariant. The Dezyne parser is defined using a partial expression grammar or “PEG” (see PEG Parsing in GNU Guile Reference Manual).

• Identifiers
• Keywords
• Operators
• Delimiters
• Lexical Scoping
• Comments

identifier ::= [a-zA-Z_][a-zA-Z0-9_]*

p, hello, Alarm, turn_on, VALUE_123, _

behavior        blocking        bool            component
defer           else            extern          external
enum            false           if              illegal
import          inevitable      injected        inout
interface       in              namespace       on
optional        otherwise       out             provides
reply           requires        return          subint
system          true

+       -       !
<       >       <=      >=      ==      !=      <=>

(       )       {       }       $

,       .       ;       =

reference ::= scope* identifier
scope ::= identifier "."

/* This is an example of multi-line comment.
 * The line below is ignored also:
 * this component implements...
 */
component hello
{
  provides ihello p; // a single-line comment
}

10.2 Dezyne Files

Dezyne types, interfaces, and components are organized in files. A file, with extension ’.dzn’ by convention, may contain zero or more of type definitions, interfaces, and/or components.

The toplevel Dezyne program text is defined as follows:

text ::= root
root ::= (import | data-expression
           | namespace | type | interface | component)*

An interface can refer to a global type definition. A component can refer to types, interfaces and other components. An explicit import clause is needed when the referred information is defined in another file.

• Import

import    ::= "import" (file-name "/")* file-name ";"
file-name ::= [a-zA-Z0-9_+.-]+

import file-name.dzn;
import ../global-types.dzn;
import some/directory/prefix/library.dzn;

10.3 Types and Expressions

In Dezyne all variables and constants are typed. A number of type constructs are available.

type      ::= bool / enum / subint / void
data-type ::= extern

types are used for event reply types, variables, function parameters, function, function return types, and function call arguments. data-types are used for event parameters, action arguments, and variables.

• void
• bool
• enum
• subint
• extern data
• Expressions

in void hello ();

void foo ()
{
  world;
}

in bool test ();

bool idle = true;

bool negate (bool input)
{
  return !input;
}

enum   ::= "enum" identifier "{" fields "}" ";"
fields ::= identifier ("," identifier)* ","?

enum result {FALSE,TRUE,ERROR};

subint  ::= "subint" identifier "{" range "}" ";"
range   ::= integer ".." integer
integer ::= ("-")? [0-9]+

subint int {-1..2};

extern          ::= "extern" identifier data-expression ";"
data-expression ::= "$" (!"$")* "$" | data-variable
data-variable   ::= identifier | port "." identifier

extern string $std::string$;

expression ::= bool-expression | data-expression | enum-expression
                | integer-expression

bool-expression ::= bool-literal
                     | bool-variable
                     | action
                     | call
                     | field-test
                     | "!" bool-expression
                     | "(" bool-expression ")"
                     | bool-expression bool-operator bool-expression
                     | int-expression comparison-operator int-expression
bool-variable   ::= identifier | port "." identifier
bool-literal    ::= "false" | "true"
field-test      ::= enum-variable "." enum-field
enum-variable   ::= identifier | port "." identifier
bool-operator   ::= "==" | "!=" | "&&" | "||"
comparison-operator
                ::= "==" | "!=" | "<" | "<=" | ">" | ">="

enum-expression ::= enum-literal
                     | enum-variable
                     | action
                     | call
enum-literal    ::= enum "." field
enum-variable   ::= identifier | port "." identifier

int-expression  ::= int-literal
                      | subint-variable
                      | action
                      | call
                      | "-" int-expression
                      | "(" int-expression ")"
                      | int-expression int-operator int-expression
subint-variable ::= identifier | port "." identifier
int-literal     ::= "-"? [0-9]+
int-operator    ::= "+" | "-"

10.4 Interfaces

Interfaces describe the interaction between two components: the events (or messages) that can and cannot be communicated, i.e., the interaction protocol.

interface ::= "interface" identifier "{" types-and-events behavior "}"
type-and-events
          ::= (type | event)*
behavior  ::= "behavior" "{" behavior-statement* "}"

Each event has a direction specified by the in or out keywords. An event labeled with in (in-event) is received by the implementation providing the interface. Conversely, an event labeled with out (out-event) is emitted by the implementation providing the interface. Note that from the point of view of an implementation requiring an interface the interpretation of in and out is inverted.

The interface protocol is specified in the behavior section.

$include <string>;$
interface ihello
{
  enum result {FALSE,TRUE,ERROR};
  extern string $std::string$;
  in result hello (string greeting);
  out void world ();
  behavior { … }
}

• Events
• Behavior
• Declarative Statements
• Imperative Statements
• Functions

event     ::= direction type identifier "(" parameter-list? ")" ";"
direction ::= "in" | "out"
parameter-list
          ::= parameter ( "," parameter)*
parameter ::= parameter-direction? data-type identifier
parameter-direction
          ::= "in" | "out" | "inout"

in void e ();

in enum_type e2 ();

out void e3 (some_id in_id, out some_id out_id);

out void e4 (some_string s);

behavior ::= "behavior" "{" behavior-statement* "}"
behavior-statement
         ::= type | variable | function | declarative-statement

variable ::= (type identifier = expression
                | data-type identifier = data-expression
                | data-type identifier) ";"

bool idle = true;

declarative-statement ::= guard | on | "{" declarative-statement "}"

transition   ::= prefix imperative-statement
prefix       ::= <guards> <on>

on        ::= "on" trigger ("," trigger)* ":" statement
trigger   ::= event-name | "inevitable" | "optional"
statement ::= declarative-statement | imperative-statement | illegal
imperative-statement
          ::= action | assign | call | if | reply | return | variable
                | imperative-compound
                | empty-statement
illegal   ::= "illegal"
imperative-compound
          ::= "{" (imperative-statement ";")+ "}"
empty-statement
          ::= ";" | "{" "}"

on hello: {}
on inevitable: {world; idle = true;}

on hello: world;
on hello: cruel;

on hello: {}
on hello: idle = true;

guard ::= "[" bool-expression "]" statement

[idle]  on hello: idle = false;
[!idle]
{
  on hello: idle = true;
  on inevitable: {world; idle = true;}
}

on inevitable: imperative-statement;
on optional:   imperative-statement;

interface inevitable_optional
{
  in bool hello ();
  in void bye ();
  out void world ();
  out void cruel ();

  behavior
  {
    enum status {IDLE, WORLD, CRUEL};
    status state = status.IDLE;

    [state.IDLE]
    {
      on hello: {state = status.WORLD; reply (true);}
      on hello: {state = status.CRUEL; reply (false);}
    }
    [state.WORLD] on inevitable: {state = status.IDLE; world;}
    [state.CRUEL]
    {
      on optional: {state = status.WORLD; cruel;}
      on bye: state = status.IDLE;
    }
  }
}

action ::= event-name ";"

world;

assign ::= variable "=" expression ";"

idle = true;
idle = !b;
idle = negate (idle);

call          ::= identifier "(" argument-list ")"
argument-list ::= (expression ",")*

foo ();
bar (true, 12);

bool b = bool_function ();
b = bool_function ();

if (bool_function ()) …;
if (!bool_function ()) …;
if (!bool_function () && b) …;
if (enum_function () == result.FALSE) …;
if (enum_function () != result.TRUE || b) …;
reply (enum_function ());
reply (enum_function () != result.ERROR);

empty-statement ::=  ";" | "{" "}"

on hello: {}
on cruel: ;

if ::= ("if" "(" bool-expression ")" imperative-statement)
         | ("if" "(" bool-expression ")" imperative-statement
              "else" imperative-statement)

if (idle)
  {world; idle = false;}
else
  cruel;

if (bool_function ()) …;
if (!bool_function ()) …;
if (!bool_function () && b) …;
if (enum_function () == result.TRUE) …;
if (enum_function () != result.ERROR || b) …;

if (b1) if (b2) then-statement else else-statement

if (b1)
{ if (b2) then-statement else else-statement }

illegal ::= "illegal" ";"

on hello: illegal;

reply ::= "reply" "(" expression ")" ";"

on hello: reply (true);

return ::= "return" ";"
             | "return" expression ";"

void foo ()
{
  if (idle) return;
  world;
}

bool negate (bool b)
{
  return !b;
}

variable ::= (type identifier = expression
               | data-type identifier = data-expression
               | data-type identifier) ";"

bool b = true;
bool not_idle = !idle;
bool c = negate (idle);

function ::= type identifier "(" parameter-list ")"
               "{" imperative-statement* "}"

void foo ()
{
  bye;
  cruel;
  world;
}

bool bar (bool b, int i)
{
  if (b)
    world;
  idle = i == 12;
  return idle;
}

10.5 Components

Components are the building blocks in a Dezyne. They allow composition into bigger components called system components.

A component has a list of ports and optionally a behavior or a system block.

component ::= "component" "{" port+ (behavior | system)? "}"
behavior  ::= "behavior" "{" behavior-statement* "}"
system    ::= "system" "{" system-statement* "}"

• Ports
• Component Behavior
• Component Types
• Component Declarative Statements
• Component Imperative Statements
• Multiple Provides Ports

port      ::= ("provides" interface-type identifier ";")
              | ("requires" qualifier? interface-type identifier ";")
qualifier ::= "blocking" | "external" | "injected";

provides ihello p;
provides blocking ihello p;      // (1)
requires ihello r;
requires blocking ihello r;      // (2)
requires external itimer t;  // (3)
requires injected ilogger l; // (4)

requires injected ilogger l;

requires external itimer t;

extern double $double$;

interface itimer
{
  in void create (double seconds);
  in void cancel ();
  out void timeout ();
  behavior
  {
    bool is_armed = false;
    [!is_armed] on create: is_armed = true;
    on cancel: is_armed = false;
    [is_armed] on inevitable: {timeout; is_armed = false;}
  }
}

component remote_timer_proxy
{
  provides itimer pp;
  requires external itimer rp;
  behavior
  {
    bool is_armed = false;
    on pp.create (s):
      [!is_armed] {rp.create (s); is_armed = true;}
    on pp.cancel (): {rp.cancel (); is_armed = false;}
    on rp.timeout ():
      [is_armed] {pp.timeout (); is_armed = false;}
  }
}

behavior           ::= "behavior" "{" behavior-statement* "}"
behavior-statement ::= type | variable | function | declarative-statement

component hello
{
  provides ihello p;
  requires ihello r;
  requires itimer t;
  behavior
  {
    on p.hello (): t.create ();
    on t.timeout (): r.hello ();
    on r.world (): p.world ();
  }
}

component timer
{
  provides itimer t;
}

component timer_system
{
  provides ihello p;
  requires ihello r;
  system
  {
    hello h;
    timer t;
    p <=> h.p;
    h.t <=> t.t;
    h.r <=> r;
  }
}

component-declarative-statement ::= declarative-statement | blocking

transition  ::= prefix imperative-statement
prefix      ::= <blocking?> <guards> <on>

on            ::= ("on" triggers ":" statement)
                  | ("on" illegal-triggers ":" illegal)
triggers      ::= trigger ("," trigger)*
trigger       ::= port-name "." event-name "(" formal-list? ")"
formal-list   ::= formal ("," formal)*
formal        ::= identifier | (identifier formal-binding)
statement     ::= declarative-statement | imperative-statement | illegal
imperative-statement
              ::= action | assign | call | if | reply | return | variable
                  | imperative-compound
                  | defer-statement
                  | empty-statement
illegal       ::= "illegal"
imperative-compound
              ::= "{" (imperative-statement ";")* "}"
defer-statement
              ::= "defer" argument-list? imperative-statement
argument-list ::= "(" ")" | "(" expression ("," expression)* ")"
empty-statement
              ::=
illegal-triggers
              ::= illegal-trigger ("," illegal-trigger)*
illegal-trigger
              ::= port-name "." event-name

on p.hello (greeting): w.hello (greeting);
on p.cruel, r.hello: illegal; // Note this is optional since 2.14.0.

on p.hello (): w.hello ();
on p.hello (): ;

blocking ::= "blocking" statement

on trigger (): blocking imperative-statement;         (1)

blocking on trigger (): imperative-statement;         (2)

on trigger (): blocking [guard] imperative-statement; (3)

on trigger ():
{
  blocking [guard] imperative-statement1;             (4)
  [guard] imperative-statement2;
}

trigger        ::= port-name "." event-name "(" formal-list? ")"
formal-list    ::= formal ("," formal)*
formal         ::= identifier | (identifier formal-binding)
formal-binding ::= "<-" identifier

extern int $int$;
component blocking_binding
{
  provides ihello h;
  requires iworld w;

  behavior
  {
    int g = $123$;
    bool busy = false;
    [!busy] on h.hello (n <- g): blocking {w.hello (); busy = true;}
    [busy] on w.world (): {g = $456$; h.reply (); busy = false;}
    [busy] on w.cruel (): {h.reply (); g = $456$; busy = false;}
  }
}

on hello: world;
on hello: cruel;

extern int $int$;
component synchronous_out_event_binding
{
  provides ihello h;
  requires iworld w;

  behavior
  {
    int g = $123$;

    on h.hello (n <- g): w.hello ();
    on w.world (): {g = $456$; h.reply (true);}
    on w.cruel (): {h.reply (true); g = $456$; ;}
  }
}

extern int $int$;
component synchronous_out_event_binding
{
  provides ihello h;
  requires iworld w;

  behavior
  {
    int g = $123$;

    on h.hello (n <- g): w.hello ();
    on w.world (): g = $456$;
  }
}

interface starter
{
  in void start_and_wait ();
  behavior
  {
    on start_and_wait: {}
  }
}

interface runner
{
  in void start ();
  out void finished ();
  behavior
  {
    bool running = false;
    on start: running = true;
    [running] on inevitable: {running = false; finished;}
  }
}

component join
{
  provides blocking starter ref;
  requires runner one;
  requires runner two;

  behavior
  {
    subint Runners {0..2};
    Runners running = 0;

    blocking on ref.start_and_wait ():
      {running = 2; one.start(); two.start ();}
    [running != 1] on one.finished (), two.finished ():
      running = running - 1;
    [running == 1] on one.finished (), two.finished ():
      {running = 0; ref.reply ();}
  }
}

Next: Multiple Provides Ports, Previous: Component Declarative Statements, Up: Components   [Contents][Index]

10.5.5 Component Imperative Statements

• Component action
• Component if
• Component illegal
• Component reply
• Component defer

---

Next: Component if, Up: Component Imperative Statements   [Contents][Index]

10.5.5.1 Component action

When handling the response of a trigger, a component can send one or more events over its ports. The sending of a provides-out-event or a requires-in event is referred to as an action.

action        ::= port-name "." event-name argument-list
argument-list ::= "(" ")" | "(" expression ("," expression)* ")"

where port-name is the name of a port defined in the component, and event-name is the name of an event defined in the interface associated with the port.

Note that the event in an action statement must be of type void. For a typed action the reply value may not be ignored. A variable definition or an assign are the appropriate ways to handle a reply value:

bool b = r.bool_event ();
b = r.bool_event2 ();

or it can be used directly in a simple expression, optionally in combination with ==, !=, !, &&, or || (since 2.14.0)

if (r.bool_event ()) …;
if (!r.bool_event ()) …;
if (!r.bool_event () && b) …;
if (r.enum_event () == result.FALSE) …;
if (r.enum_event () != result.TRUE || b) …;
reply (r.enum_event ());
reply (r.enum_event () != result.ERROR);

or in any expression (since 2.16.0).

Note: The restriction of using only one action or call in an expression has been lifted (since 2.16.0).

---

Next: Component illegal, Previous: Component action, Up: Component Imperative Statements   [Contents][Index]

10.5.5.2 Component if

In a component an illegal can be used as an imperative statement in the branch of an if as any other imperative statement (See Component illegal).

if ::= ("if" "(" bool-expression ")" then-statement)
         | ("if" "(" bool-expression ")" then-statement
            "else" else-statement)
then-statement := imperative-statement | illegal
else-statement := imperative-statement | illegal

For example:

if (error) illegal;

Since 2.14.0, one typed action or typed call may be used in an if-expression.

Since 2.16.0, arbitrarily complex expressions may be used.

For example:

if (r.bool_event ()) …;
if (!r.bool_event ()) …;
if (!r.bool_event () && b) …;
if (r.enum_event () == result.FALSE) …;
if (r.enum_event () != result.TRUE || b) …;
if (bool_function ()) …;
if (!bool_function ()) …;
if (!bool_function () && b) …;
if (enum_function () == result.TRUE) …;
if (enum_function () != result.ERROR || b) …;

---

Next: Component reply, Previous: Component if, Up: Component Imperative Statements   [Contents][Index]

10.5.5.3 Component illegal

A trigger can be explicitly marked as illegal. In that case, illegal must be the only imperative statement for that trigger.

on      ::= "on" illegal-triggers ":" illegal
illegal-triggers
        ::= illegal-trigger ("," illegal-trigger)*
illegal-trigger
        ::= port-name "." event-name
illegal ::= "illegal" ";"

Note that in this case the trigger’s formal parameter list may be omitted.

For example:

on p.hello,r,world: illegal;

Note: A trigger with an illegal response can also be omitted since an illegal response is the default behavior for every trigger.

In a component an illegal can be used as an imperative statement in the branch of an if as any other imperative statement (See Component if).

---

Next: Component defer, Previous: Component illegal, Up: Component Imperative Statements   [Contents][Index]

10.5.5.4 Component reply

A typed trigger event requires an appropriate return value in its response handling, the reply only determines the value not the moment of returning it:

  reply (typed_expression);

reply is also used to release a blocked call (See blocking), or set the reply value from a synchrous context like so:

  port.reply ();
  port.reply (expression);

---

Previous: Component reply, Up: Component Imperative Statements   [Contents][Index]

10.5.5.5 Component defer

defer is a keyword that may be placed in front of an imperative statement.

defer-statement
              ::= "defer" argument-list? imperative-statement
argument-list ::= "(" ")" | "(" expression ("," expression)* ")"

defer indicates that the execution of the corresponding statement must be postponed at least until after returning back to the caller. Note that in order for the deferred statement to execute, the surrounding system must have reached an overall state where it can accept new activating events, i.e., this state is a system wide run to completion state.

The primary goal of defer is to decouple the execution of an imperative statement from the caller. This allows implementing an asynchronous interface almost as concisely as implementing it synchronously, as demonstrated by the example below.

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

component synchronous_asynchronous
{
  provides ihelloworld h;
  behavior
  {
    bool synchronous = false;
    [synchronous] on h.hello (): h.world ();
    [!synchronous] on h.hello (): {
      synchronous = true;
      defer {
        synchronous = false;
        h.world ();
      }
    }
  }
}

Here we can observe the difference between synchronous and asynchronous behavior once more. When the synchronous boolean equals true the world action occurs in the context, e.g. between the hello and its return. When synchronous equals false the world action occurs after the return. This behavior is clearly depicted by the following state diagram.

Perhaps the idle state might seem superfluous in the example above, however it is not. Besides resulting in component behavior which is not compliant with its interface, removing the idle state and the corresponding guard would allow a client to do multiple consecutive h.hello’s, which results in an overflow of the defer queue.

Besides state playing a role in avoiding defer queue overflow, there is another aspect related to state and the use of defer. In order for the deferred statement to execute, the component must remain in the same state as it was at the time of invoking defer. Anything that changes the state of the component after invoking defer but before the deferred statement executes will remove it from the queue, and thereby implicitly cancel it. This is demonstrated by the example below. Note that a data member variable is not part of the component state, and changing its value does not cancel the deferred statement.

interface ihellocruelworld
{
  in void hello ();
  in void cruel ();
  out void world ();
  behavior
  {
    bool idle = true;
    [idle] on hello: idle = false;
    [!idle] on inevitable: {
      idle = true;
      world;
    }
    on cruel: idle = true;
  }
}
component defer_cancel
{
  provides ihellocruelworld h;
  behavior
  {
    bool idle = true;
    [idle] on h.hello (): {
      idle = false;
      defer {
        idle = true;
        h.world ();
      }
    }
    on h.cruel (): idle = true;
  }
}

Here we see that the cruel event makes the component idle again and in compliance with the interface this implies that the world event can no longer occur. The corresponding component state diagram is depicted below.

The ability to cancel a deferred statement is not always desirable. The way to influence the skip behavior is to add an argument list of state variables to the defer keyword. This limits the scope of the state which is observed by defer in deciding when to skip the execution. The two extreme cases are:

• The full list of variables, which is equivalent to defer without an arument list.
• The empty list of variables, which removes ability to cancel entirely.

We can see an example of a defer argument list below.

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

interface icruel
{
  in void cruel();
  behavior
  {
    on cruel: {}
  }
}

component defer_selection
{
  provides ihelloworld h;
  provides icruel c;
  behavior
  {
    bool synchronous = false;
    bool cruel = false;
    on c.cruel(): cruel = !cruel;
    [synchronous] on h.hello (): h.world ();
    [!synchronous] on h.hello (): {
      synchronous = true;
      defer(synchronous) {
        synchronous = false;
        h.world ();
      }
    }
  }
}

Here the execution of the deferred statement must remain unaffected by the change to the cruel state variable. We can achieve this by only observing the state variable as the example shows or not observing any state at all. The latter case is left as an exercise to the reader.

---

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

component v_fork
{
  provides ihello left;
  provides ihello right;
  behavior
  {
    on left.hello():
    {
      right.world(); //is non-compliant with interface(s) of provides port(s)
    }
    on right.hello(): {}
  }
}

component y_fork
{
  provides ihello left;
  provides ihello right;
  requires ihello r;
  behavior
  {
    on left.hello(), right.hello(): {}
    on r.world():
    {
      left.world();
      right.world(); //is non-compliant with interface(s) of provides port(s)
    }
  }
}

10.6 Systems

A system component, or system is a component which is composed from one or more sub components. The system block instantiates each of the sub components and either connects their ports together or exposes them as its own, such that all ports are bound.

system-component ::= "component" "{" port* system "}"
system           ::= "system" "{" system-statement* "}"
system-statement ::= (instance | binding)
instance         ::= component-name identifier ";"
binding          ::= end-point "<=>" end-point ";"
end-point        ::= port-name
                     | wildcard
                     | (instance-name "." port-name)
                     | (instance-name "." wildcard)
wildcard         ::= "*"

Note: A binding can have only one wildcard, See Using Injection.

For example:

interface i
{
  in void event();
  behavior {}
}

component c
{
  provides i pp;
  requires i rr;
}

component top_middle_bottom
{
  provides i p;
  requires i r;
  system
  {
    c top;
    c middle;
    c bottom;
    p <=> top.pp;
    top.rr <=> middle.pp;
    middle.rr <=> bottom.pp;
    bottom.rr <=> r;
  }
}

The system description shows the instantiation of the two component instances ci1 and ic2 and two connections or bindings between ports.

• Component Instances
• Binding

instance ::= component-name identifier ";"

hello h1;
hello h2;

binding   ::= end-point "<=>" end-point ";"
end-point ::= port-name
              | wildcard
              | (instance-name "." port-name)
              | (instance-name "." wildcard)
wildcard  ::= "*"

interface ilog
{
  ...
}
component logger
{
  provides ilog log;
  ...
}

...
component some_component12
{
  provides some_interface12 p;
  requires injected ilog l;
  ...
}
component some_component13 {
  provides some_interface13 p;
  requires injected ilog l;
  ...
}
...

component some_system
{
  ...
  system
  {
    logger clog;
    ...
    some_component12 c12;
    some_component13 c13;
    ...
    clog.log <=> *;
  }
}

component some_sub_system
{
  ...
  system {
    ...
    some_component12 c12;
    some_component13 c13;
    ...
  }
}

component some_system
{
  ...
  system
  {
    logger clog;
    some_sub_system subsys;
    ...
    clog.log <=> subsys.*;
  }
}

10.7 Namespaces

All component, interface, and type definitions are defined in a namespace, which provides name scoping. The scope is used as a prefix when referring to the name from another scope.

namespace      ::= "namespace" compound-identifier "{" namespace-root "}"
namespace-root ::= (namespace | type | interface | component)*
compound-identifier
               ::= scope* identifier
scope          ::= identifier "."

For example:

namespace space
{
  extern string $std::string$;
  interface ihello
  {
     enum result {FALSE, TRUE, ERROR};
     in result hello (string s);
     out void world ();
     behavior
     {
       on hello (s): reply (result.TRUE);
    }
  }
}

• Namespace Extension
• Referencing

namespace space
{
  extern string $std::string$;
  interface ihello { ...  }
}

namespace space
{
  extern string $std::string$;
}
namespace space
{
  interface ihello { ...  }
}

namespace foo {
  interface I {
    enum Bool {F,T};
    in Bool e();
    out void a();
    behavior {
      on e: {a; reply (Bool.T); }
    }
  }
}
namespace inner {
  namespace foo {
    interface I {
      enum Bool {f,t};
      in Bool e();
      out void a();
      behavior { }
    }
  }
  component space {
    provides foo.I inner;
    provides .foo.I fooi;
    behavior {
      foo.I.Bool inner_state = foo.I.Bool.t;
      .foo.I.Bool foo_state = .foo.I.Bool.T;
      on inner.e(): { }
      on fooi.e(): { }
    }
  }
}
namespace bar {
  component c {
    provides foo.I i;
    behavior {
      foo.I.Bool state = foo.I.Bool.T;
      on i.e(): { }
    }
  }
}

11.1 Well-formedness Checks Categories

Well-formedness checks on the behavior part of a model come in a number of categories:

Top level

Interface, event and component definitions.

Directional

triggers and actions are expected at different places depending on the direction of their event.

Nesting

The imperative part of the language (assigns, actions, function calls) are only allowed in an imperative statement or in a function body,

Mixing

The use of statements within compounds is restricted,

Reply

The usage of reply,

Valued Actions and Calls

The use of non-void actions and calls,

Injection

The use of injected ports,

Functions

A function body should be imperative, and have a well-defined return.

Data Parameters

The use of data parameters,

Injection

The use of injected ports,

System

All ports should be bound correctly.

Note: A trigger is an event that occurs and is prefixed by on in the behavior, an action is an event that is emitted inside the imperative body of a trigger.

11.2 List of Well-formedness Checks

The well-formedness checks in alphabetical order:

See action in member variable initializer,
See action outside on,
See action value discarded,
See assign outside on,
See call in member variable initializer,
See call value discarded,
See Cannot bind external port to non-external port,
See Cannot bind port to port,
See Cannot bind two wildcards,
See Cannot bind wildcard to requires port,
See Cannot use blocking in an interface,
See Cannot use event as action,
See Cannot use event as trigger,
See Cannot use illegal in function,
See Cannot use illegal in if-statement,
See Cannot use illegal with imperative statements,
See Cannot use inout-parameter on out-event,
See Cannot use otherwise guard more than once,
See Cannot use otherwise guard with non-guard statements,
See Cannot use out-parameter on out-event,
See Cannot use return outside of function,
See Cannot use statement after recursive call,
See Component with behavior must define a provides port,
See Component with behavior must have a trigger,
See Declarative statement expected,
See Formal binding is not a data member variable,
See Imperative statement expected,
See injected port has out-events,
See instance in in a cyclic binding,
See Interface must define a behavior,
See Interface must define an event,
See Missing return,
See Must specify provides-port with reply,
See Must specify provides-port with reply on out-trigger,
See Nested blocking used,
See Nested on used,
See out-event must be void,
See port is bound more than once,
See port not bound,
See port not bound – of instance,
See System composition is recursive,
See Type mismatch: parameter expected extern.

11.3 Well-formedness – Top level

These checks are concerned about interface, event and component definitions.

• Interface must define an event
• Interface must define a behavior
• out-event must be void
• Component with behavior must have a trigger
• Component with behavior must define a provides port

interface interface_without_event
{
  behavior {}
}

interface-without-event.dzn:1:1: error: interface must define an event

interface interface_without_behavior
{
  in void hello ();
}

interface-without-behavior.dzn:3:3: error: event `hello' is not used in
    behavior of interface `interface_without_behavior'
interface-without-behavior.dzn:1:1: error: interface must define a
    behavior

interface typed_out_event
{
  out bool world ();
  behavior {on optional:bool b = world;}
}

typed-out-event.dzn:3:3: error: out-event `world' must be void, found
    `bool'

interface iworld
{
  out void world ();
  behavior {on optional:world;}
}

component component_provides_without_trigger
{
  provides iworld p;
  behavior {}
}

component-provides-without-trigger.dzn:7:1: error: component with
    behavior must have a trigger

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

component component_requires_without_trigger
{
  requires ihello r;
  behavior {}
}

component-requires-without-trigger.dzn:7:1: error: component with
    behavior must define a provides port
component-requires-without-trigger.dzn:7:1: error: component with
    behavior must have a trigger

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

component component_without_provides
{
  requires iworld r;
  behavior {}
}

component-without-provides.dzn:7:1: error: component with behavior must
    define a provides port
component-without-provides.dzn:7:1: error: component with behavior must
    have a trigger

11.4 Well-formedness – Directional

triggers and actions are expected at different places, depending on the direction of their event.

• Cannot use event as action
• Cannot use event as trigger

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

interface-trigger-used-as-action.dzn:6:15: error: cannot use in-event
    `hello' as action
interface-trigger-used-as-action.dzn:3:3: info: event `hello' defined
    here

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

component component_trigger_used_as_action
{
  provides ihello p;
  requires ihello r;
  behavior
  {
    on p.hello ():
    {
      p.hello ();
      r.world ();
    }
  }
}

component-trigger-used-as-action.dzn:16:7: error: cannot use provides
    in-event `hello' as action
component-trigger-used-as-action.dzn:10:3: info: port `p' defined here
component-trigger-used-as-action.dzn:3:3: info: event `hello' defined
    here
component-trigger-used-as-action.dzn:17:7: error: cannot use requires
    out-event `world' as action
component-trigger-used-as-action.dzn:11:3: info: port `r' defined here
component-trigger-used-as-action.dzn:4:3: info: event `world' defined
    here

interface interface_action_used_as_trigger
{
  out void world ();
  behavior
  {
    on world: {}
  }
}

interface-action-used-as-trigger.dzn:6:8: error: cannot use out-event
    `world' as trigger
interface-action-used-as-trigger.dzn:3:3: info: event `world' defined
    here

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

component component_action_used_as_trigger
{
  provides ihello p;
  requires ihello r;
  behavior
  {
    on p.world (): {}
    on r.hello (): {}
  }
}

component-action-used-as-trigger.dzn:14:8: error: cannot use provides
    out-event `world' as trigger
component-action-used-as-trigger.dzn:10:3: info: port `p' defined here
component-action-used-as-trigger.dzn:4:3: info: event `world' defined
    here
component-action-used-as-trigger.dzn:15:8: error: cannot use requires
    in-event `hello' as trigger
component-action-used-as-trigger.dzn:11:3: info: port `r' defined here
component-action-used-as-trigger.dzn:3:3: info: event `hello' defined
    here

11.5 Well-formedness – Nesting

Dezyne statements are either declarative or imperative. One or more declarative statements must be used as a prefix to the imperative statement (See Declarative Statements). Imperative statements cannot be used without a “declarative prefix”, and declarative statements cannot be used inside an imperative statement

• assign outside on
• action outside on
• Nested on used
• Nested blocking used
• Cannot use blocking in an interface

interface assign_outside_on
{
  in void hello ();
  behavior
  {
    bool b = true;
    [true] b = false;
    on hello: {}
  }
}

assign-outside-on.dzn:7:12: error: assign outside on

interface action_outside_on
{
  out void world ();
  behavior
  {
    [true] world;
  }
}

action-outside-on.dzn:6:12: error: action outside on

interface nested_on
{
  in void hello ();
  in void cruel ();
  out void world ();
  behavior
  {
    on hello: on cruel: world;
  }
}

nested-on.dzn:8:15: error: nested on used
nested-on.dzn:8:5: info: within on here

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

component nested_blocking
{
  provides blocking ihello p;
  behavior
  {
    blocking on p.hello (): [true] blocking p.reply ();
  }
}

nested-blocking.dzn:15:36: error: nested blocking used
nested-blocking.dzn:15:5: info: within blocking here

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

blocking-in-interface.dzn:6:5: error: cannot use blocking in an
    interface

11.6 Well-formedness – Mixing

A behavior description introduces a sequence of statements. A statement itself can be a compound, which is a sequence of statements between curly braces.

In order to be able to define clear semantics, there are some restrictions on the mix of statements in such a sequence.

• Declarative statement expected
• Imperative statement expected
• Cannot use otherwise guard more than once
• Cannot use otherwise guard with non-guard statements
• Cannot use illegal with imperative statements
• Cannot use illegal in if-statement
• Cannot use illegal in function

interface mixing_declarative
{
  in void hello ();
  behavior
  {
    [true]
    {
      on hello: {}
      if (true);
    }
  }
}

mixing-declarative.dzn:9:7: error: declarative statement expected
mixing-declarative.dzn:9:7: error: if outside on
mixing-declarative.dzn:9:16: error: imperative compound outside on

interface mixing_imperative
{
  in void hello ();
  behavior
  {
    bool b = true;
    on hello:
    {
      b = false;
      [b] b = false;
    }
  }
}

mixing-imperative.dzn:10:7: error: imperative statement expected

interface second_otherwise
{
  in void hello ();
  in void cruel ();
  in void world ();
  behavior
  {
    bool b = true;
    [b] on hello: b = false;
    [otherwise] on world: b = true;
    [otherwise] on cruel: {}
  }
}

second-otherwise.dzn:11:5: error: cannot use otherwise guard more than
    once
second-otherwise.dzn:10:5: info: first otherwise here

interface otherwise_without_guard
{
  in void hello ();
  in void cruel ();
  behavior
  {
    on hello: {}
    [otherwise] on cruel: {}
  }
}

otherwise-without-guard.dzn:8:5: error: cannot use otherwise guard with
    non-guard statements
otherwise-without-guard.dzn:7:5: info: non-guard statement here

interface imperative_illegal
{
  in void hello ();
  behavior
  {
    bool b = false;
    on hello:
    {
      b = true;
      illegal;
    }
  }
}

imperative-illegal.dzn:10:7: error: cannot use illegal with imperative
    statements
imperative-illegal.dzn:9:7: info: imperative statement here

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

component component_if_illegal
{
  provides ihello p;
  behavior
  {
    bool b = true;
    on p.hello():
    {
      b = false;
      if (b)
        illegal;
    }
  }
}

interface interface_if_illegal
{
  in void hello ();
  behavior
  {
    bool b = false;
    on hello:
    {
      if (b)
        illegal;
    }
  }
}

interface-if-illegal.dzn:10:9: error: cannot use illegal in if-statement

interface interface_function_illegal
{
  in void hello ();
  behavior
  {
    void f ()
    {
      illegal;
    }
    on hello: f ();
  }
}

interface-function-illegal.dzn:8:7: error: cannot use illegal in
    function

11.7 Well-formedness – Reply

A reply is required in the handling of a typed (i.e. non-void) trigger. It is also required in case a trigger (which in this case might be void) is used in blocking mode; in that case the occurrence of the reply might be postponed. In general this is hard to check statically. What can be checked is described below.

• Must specify provides-port with reply on out-trigger
• Must specify provides-port with reply

interface ihello
{
  in bool hello ();
  behavior
  {
    on hello: reply (true);
    on hello: reply (false);
  }
}

interface iworld
{
  in void hello ();
  out void world ();
  behavior
  {
    on hello: world;
  }
}

component requires_reply_needs_provides_port
{
  provides ihello left;
  provides ihello right;
  requires iworld r;
  behavior
  {
    on left.hello (): reply (true);
    on right.hello (): reply (false);
    on r.world (): reply ();
  }
}

requires-reply-needs-provides-port.dzn:30:20: error: must specify a
    provides-port with reply on requires out-trigger: `r.world'

interface ihello
{
  in bool hello ();
  behavior
  {
    on hello: reply (true);
    on hello: reply (false);
  }
}

component function_reply_needs_provides_port
{
  provides ihello left;
  provides ihello right;
  behavior
  {
    void f (bool b)
    {
      left.reply (b);
    }
    void g (bool b)
    {
      reply (b);
    }
    on left.hello (): f (true);
    on right.hello (): g (false);
  }
}

function-reply-needs-provides-port.dzn:23:7: error: must specify a
    provides-port with reply

11.8 Well-formedness – Valued Actions and Calls

Both actions and function calls can be typed, and as such are considered to be expressions. They can only be called are from the imperative statement. The reason is that actions and function calls (at least the functions that contain actions) cause a side effect.

This means that actions or function calls cannot be used to initialize the value of a global variable in a behavior, neither can it be used in a guard statement.

• action in member variable initializer
• call in member variable initializer
• action value discarded
• call value discarded

interface ihello
{
  in bool hello ();
  behavior
  {
    on hello: reply (true);
  }
}

component action_in_member_definition
{
  provides ihello p;
  requires ihello r;
  behavior
  {
    bool b = r.hello ();
  }
}

action-in-member-definition.dzn:16:14: error: action in member variable
    initializer

interface ihello
{
  in bool hello ();
  behavior
  {
    on hello: reply (true);
  }
}

component call_in_member_definition
{
  provides ihello p;
  requires ihello r;
  behavior
  {
    bool f () {return false;}
    bool b = f ();
  }
}

call-in-member-definition.dzn:17:14: error: call in member variable
    initializer

interface ihello
{
  in bool hello ();
  behavior
  {
    on hello: reply (true);
  }
}

component action_discard_value
{
  provides ihello p;
  requires ihello r;
  behavior
  {
    on p.hello (): r.hello ();
  }
}

action-discard-value.dzn:16:20: error: action value discarded

interface call_discard_value
{
  in void hello ();
  behavior
  {
    bool f ()
    {
      return true;
    }

    on hello: f ();
  }
}

call-discard-value.dzn:11:15: error: call value discarded

11.9 Well-formedness – Injection

Not every port can be injected.

• injected port has out-events

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

component injected_with_out_event
{
  provides ihello p;
  requires injected ihello r;
  behavior
  {
  }
}

injected-with-out-event.dzn:14:3: error: injected port `r' has out
    events: world
injected-with-out-event.dzn:4:3: info: port defined here

11.10 Well-formedness – Functions

• A function body can only contain imperative statements, including actions. See the sections on ’Mixing’ and ’Direction’ above,
• A typed function is required to have an explicit return,
• A return is only allowed in a function body,
• A recursive function is required to be tail recursive.

• Missing return
• Cannot use return outside of function
• Cannot use statement after recursive call

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

component function_missing_return
{
  provides ihello p;
  behavior
  {
    bool a = true;
    bool b = false;
    bool c = true;
    bool func ()
    {
      if (a && b)
        return true;
      else if (c)
        illegal;
    }
  }
}

function-missing-return.dzn:22:12: error: missing return

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

return-outside-function.dzn:6:15: error: cannot use return outside of
    function

interface function_not_tail_recursive
{
  in void hello ();
  behavior
  {
    void f ()
    {
      bool b = false;
      if (b)
      {
        f ();
        b = true;
      }
    }
    on hello: f ();
  }
}

function-not-tail-recursive.dzn:11:9: error: cannot use statement after
    recursive call
function-not-tail-recursive.dzn:12:9: info: statement after call

11.11 Well-formedness – Data Parameters

The restrictions on data parameters are summarised here.

• Type mismatch: parameter expected extern
• Cannot use out-parameter on out-event
• Cannot use inout-parameter on out-event
• Formal binding is not a data member variable

extern int $int$;
interface event_with_bool_porameter
{
  in void hello (bool b);
  behavior {on hello:{}}
}

event-with-bool-parameter.dzn:4:18: error: type mismatch: parameter `b';
    expected extern, found: `bool'

extern int $int$;
interface out_parameter_on_out_event
{
  out void world (out int value);
  behavior {on optional:world;}
}

out-parameter-on-out-event.dzn:4:19: error: cannot use out-parameter on
    out-event `world'

extern int $int$;
interface inout_parameter_on_out_event
{
  out void world (inout int value);
  behavior {on optional:world;}
}

inout-parameter-on-out-event.dzn:4:19: error: cannot use inout-parameter
    on out-event `world'

extern int $int$;
interface ihello
{
  in void hello (int i);
  in void cruel (int i);
  behavior
  {
    on hello:;
    on cruel:;
  }
}

component parse_out_binding
{
  provides blocking ihello p;
  behavior
  {
    bool b = false;
    int data;
    blocking on p.hello (i <- data): {}
    blocking on p.cruel (b <- data): {}
    blocking on p.cruel (data <- i): {}
    blocking on p.cruel (k <- b): {}
  }
}

out-binding-reversed.dzn:22:26: error: formal binding `i' is not a data
    member variable
out-binding-reversed.dzn:23:26: error: formal binding `b' is not a data
    member variable

11.12 Well-formedness – System

In a system, the component’s ports and all sub component’s ports must be bound correctly.

Bindings in which ‘’wildcards” are involved will be described at the end of this section.

• port not bound
• port not bound – of instance
• port is bound more than once
• Cannot bind port to port
• Cannot bind two wildcards
• instance in in a cyclic binding
• Cannot bind wildcard to requires port
• System composition is recursive
• Cannot bind external port to non-external port

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

component port_not_bound
{
  provides ihello p;
  system {}
}

port-not-bound.dzn:9:3: error: port `p' of type `ihello' not bound

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

component hello
{
  provides ihello p;
  behavior {}
}

component instance_port_not_bound
{
  system
  {
    hello h;
  }
}

instance-port-not-bound.dzn:17:5: error: port `p' of type `ihello'
    not bound

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

component hello
{
  provides ihello p;
  behavior {}
}

component instance_port_not_bound
{
  provides ihello p;
  system
  {
    hello h;
    hello i;
    p <=> h.p;
    p <=> i.p;
  }
}

port-bound-twice.dzn:20:5: error: port `p' is bound more than once
port-bound-twice.dzn:21:5: error: port `p' is bound more than once

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

component hello
{
  provides ihello p;
  requires ihello r;
  behavior {}
}

component world
{
  provides ihello p;
  behavior {}
}

component instance_port_not_bound
{
  provides ihello p;
  system
  {
    hello h;
    world w;
    p <=> h.r;
    h.p <=> w.p;
  }
}

binding-mismatch-direction.dzn:27:5: error: cannot bind provides port
    `p' to requires port `r'
binding-mismatch-direction.dzn:22:3: info: port `p' defined here
binding-mismatch-direction.dzn:10:3: info: port `r' defined here
binding-mismatch-direction.dzn:28:5: error: cannot bind provides port
    `p' to provides port `p'
binding-mismatch-direction.dzn:16:3: info: port `p' defined here
binding-mismatch-direction.dzn:9:3: info: port `p' defined here

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

component hello
{
  provides ihello p;
  requires injected ihello r;
  behavior {}
}

component logger
{
  provides ihello p;
  behavior {}
}

component binding_two_wildcards
{
  provides ihello p;
  system
  {
    hello h;
    logger log;

    p <=> h.p;
    log.* <=> *;
  }
}

binding-two-wildcards.dzn:29:5: error: cannot bind two wildcards
binding-two-wildcards.dzn:26:5: error: port `p' of type `ihello' not
    bound

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

component hello
{
  provides ihello p;
  requires ihello r;
  behavior {}
}

component binding_cycle
{
  system
  {
    hello h;
    h.p <=> h.r;
  }
}

binding-cycle.dzn:18:5: error: instance `h' is in a cyclic binding

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

component hello
{
  provides ihello p;
  requires ihello r;
  behavior {}
}

component world
{
  provides ihello p_left;
  provides ihello p_right;
  requires ihello r_left;
  requires ihello r_right;
  behavior {}
}

component binding_cycle
{
  provides ihello p_left;
  provides ihello p_right;
  requires ihello r_left;
  requires ihello r_right;
  system
  {
    hello h1;
    hello h2;
    world w1;
    world w2;

    p_left <=> w1.p_left;
    p_right <=> w2.p_left;

    w1.r_left <=> h1.p;
    w1.r_right <=> h2.p;

    w2.r_left <=> w1.p_right;
    w2.r_right <=> r_right;

    h1.r <=> r_left;
    h2.r <=> w2.p_right;
  }
}

binding-cycle-elaborate.dzn:32:5: error: instance `h2' is in a cyclic
    binding
binding-cycle-elaborate.dzn:33:5: error: instance `w1' is in a cyclic
    binding
binding-cycle-elaborate.dzn:34:5: error: instance `w2' is in a cyclic
    binding

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

component hello
{
  requires injected ihello r;
}

component logger
{
  requires ihello r;
}

component binding_wildcard_requires
{
  system
  {
    hello h;
    logger log;

    log.r <=> *;
  }
}

binding-wildcard-requires.dzn:24:5: error: cannot bind wildcard to
    requires port `r'
binding-wildcard-requires.dzn:14:3: info: port `r' defined here

component c1 {
  system {
    c2 ci2;
    c3 ci3;
  }
}

component c2 {
  system {
    c5 ci5;
  }
}

component c3 {
  system {
    c4 ci4;
    c2 ci2;
  }
}

component c4 {
  system {
    c1 ci1;
  }
}

component c5 {
  system { } // an empty system
}

recursive-system.dzn:1:1: error: system composition of `c1' is recursive
recursive-system.dzn:14:1: error: system composition of `c3' is
    recursive
recursive-system.dzn:21:1: error: system composition of `c4' is
    recursive

interface i {
  in void e ();
  behavior {
    on e: {}
  }
}

component c1 {
  provides i p;
  requires external i r1;
  requires external i r2;
  behavior {
    on p.e (): {}
  }
}

component c2 {
  provides i p;
  behavior {
    on p.e (): {}
  }
}

component s1 {
  provides i p;
  requires i r;
  system {
    c1 ci1;
    c2 ci2;
    p <=> ci1.p;
    ci1.r1 <=> r;
    ci1.r2 <=> ci2.p;
  }
}

component s2 {
  provides i p1;
  provides i p2;
  requires external i r1;
  requires external i r2;
  system {
    s1 si1;
    p1 <=> si1.p;
    p2 <=> r2;
    r1 <=> si1.r;
  }
}

binding-mismatch-external.dzn:45:5: error: cannot bind non-external port
    `r' to external port `r1'
binding-mismatch-external.dzn:26:3: info: port `r' defined here
binding-mismatch-external.dzn:39:3: info: port `r1' defined here

12.1 Building from Git

If you want to hack Dezyne yourself, it is recommended to use the latest version from the Git repository:

git clone git://git.savannah.nongnu.org/dezyne

To setup a development environment, we use GNU Guix (see The GNU Guix Manual); run

guix shell

If you are unable to use Guix when building Dezyne from a Git checkout, the following are the required packages in addition to those mentioned in the installation instructions (see Requirements).

• GNU Autoconf;
• GNU Automake;
• GNU Gettext;
• GNU Libtool;
• GNU Texinfo;
• GNU Help2man (optional).

Run ./autogen.sh to generate the build system infrastructure using Autoconf and Automake.

Then, run ./configure and make as usual.

12.2 Running Dezyne Before It Is Installed

After making changes you will want to test them. To that end, all the command-line tools can be used even if you have not run make install. To do that, you first need to have an environment with all the dependencies available (see Building from Git), and then simply prefix each command with ./pre-inst-env. As an example, here is how you would verify the trivial the hello test:

$ ./pre-inst-env dzn -v verify test/all/hello/hello.dzn

See the file HACKING for some developer tips and tricks.

12.3 The Perfect Setup

The Perfect Setup to hack on Dezyne is basically the perfect setup used for GNU Guile hacking (see Using Guile in Emacs in GNU Guile Reference Manual). To work on real-life Dezyne projects, you need more than an editor: you need an IDE, see the Verum-Dezyne Manual.

GNU Emacs

To edit .DZN files, use emacs/dzn-mode.el.

...

...

12.4 Coding Style

In general our code follows the GNU Coding Standards (see GNU Coding Standards)¹⁵. However, they do not say much about Scheme, so here are some additional rules.

• Programming Paradigm
• Data Types and Pattern Matching
• Formatting Code

(if test? trivial-case
    the-more-elaborate-case)

12.5 Submitting Patches

Development is done using the Git distributed version control system. Thus, access to the repository is not strictly necessary. We welcome contributions in the form of patches as produced by git format-patch sent to the dezyne-devels@nongnu.org mailing list (see Submitting patches to a project in Git User Manual).

Please write commit logs in the ChangeLog format (see Change Logs in GNU Coding Standards); you can check the commit history for examples.