[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[ANN] Dezyne 2.16.0 released

From: Jan Nieuwenhuizen
Subject: [ANN] Dezyne 2.16.0 released
Date: Thu, 18 Aug 2022 17:18:27 +0200
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux)

We are happy to announce Dezyne 2.16 which introduces the `defer'
keyword: A new language concept for implementing an asynchronous
interface.  With defer, the basic semantics are complete.

* About

Dezyne[0] is a programming language and a set of tools to specify,
validate, verify, simulate, document, and implement concurrent control

The Dezyne language has formal semantics expressed in mCRL2[1] developed
at the department of Mathematics and Computer Science of the Eindhoven
University of Technology (TUE[2]).  Dezyne requires that every model is
finite, deterministic and free of deadlocks, livelocks, and contract
violations.  This achieved by means of the language itself as well as by
builtin verification through model checking.  This allows the
construction of complex systems by assembling independently verified

* Summary

Defer replaces dzn.async ports feature that cannot be used in systems
collateral blocking.  The use of dzn.async ports is now deprecated.

Also new in this release: Cleanups to the code generators and model to
model transformations.

See also the documentation <>.

We will evaluate your reports and track them via the Gitlab
dezyne-issues project[3], see our guide to writing helpful bug

* What's next?

In the next releases we like to see implicit interface constraints,
shared interface state and verification with system scope for
automatically exploring possible traces in a system.

* Future

Looking beyond the next releases: Module-specifications and
data-interfaces.  Hierarchical behaviors.  Support for Model Based

The Dezyne developers.

* Download

  git clone git://

Here are the compressed sources and a GPG detached signature[*]:

Here are the SHA1 and SHA256 checksums:

  91e8d61cdd9333edbd2768c26c187c35ba7e8a6c  dezyne-2.16.0.tar.gz

[*] Use a .sig file to verify that the corresponding file (without the
.sig suffix) is intact.  First, be sure to download both the .sig file
and the corresponding tarball.  Then, run a command like this:

  gpg --verify dezyne-2.16.0.tar.gz.sig

If that command fails because you don't have the required public key,
then run this command to import it:

  gpg --keyserver --recv-keys 

and rerun the 'gpg --verify' command.

Alternatively, Dezyne can be installed using GNU Guix[5]:
  guix pull
  guix install dezyne


* Changes in 2.16.0 since 2.15.4
** Language
  - A new keyword `defer' has been introduced.
  - The `dzn.async' ports are now deprecated.
  - Complex boolean and integer expressions are now supported.
** Build
  - The tests for the experimental Scheme code generator are now being
  - The tests for the experimental Scheme and JavaScript code generators
    now also execute out-of-the-box in a container.
** Code
  - The C++, C#, and experimental Scheme code generators support `defer'.
  - The experimental Scheme code generator now also supports collateral
    blocking and thus has full blocking support.
  - The C++ and C# runtime now has a more elegant and efficient
    implementation for collateral blocking.
  - The code generators now produce expressions with `&&' and `||' using
    courtesy parentheses.  This avoids compiler warnings.
  - The code generators no longer produce unnecessarily parenthesized
    and complex expressions.  This also avoids CLANG compiler warnings.
  - The code generators now preserve the top level comment.
** Commands
  - The `dzn' command has a new option: `-t,--transform=TRANS'.  This
    makes dzn->dzn transformation avaiable from the command line.
    + New transformations have been added:
      `add-determinism-temporaries`, `inline-functions',
      `simplify-guard-expressions', and `split-complex-expressions'.
    + The `add-explicit-temporaries' transformation now supports complex
      boolean and integer expressions (#67[6]).
** Noteworthy bug fixes
  - Some warnings in the C++ runtime have been fixed and side-stepped.
  - The mCRL2 code generator now generates correct code for an unused
    assignment from an action or function call as only statement in a
    branch of an if-statement.
  - Shadowing of a variable in a branch of an if-statement is no longer
  - The simulator now correctly displays a V-fork compliance error in a
    blocking trace.
  - The simulator now correctly handles a trace with foreign provides

* Links


Jan Nieuwenhuizen <>  | GNU LilyPond
Freelance IT | AvatarĀ®

reply via email to

[Prev in Thread] Current Thread [Next in Thread]