Verum Dezyne 2.16 Release

Announcements
1

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.

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 Dezyne documentation.

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 compiled.
    • 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).
  • 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 rejected.
    • The simulator now correctly displays a V-fork compliance error in a blocking trace.
    • The simulator now correctly handles a trace with foreign provides triggers.

Changes in 2.15.4 since 2.15.3

  • Code
    • In C++, C# and the experimental Scheme code generators, a formal-binding (“<-”) to assign an out-parameter is now also supported without blocking, in a synchronous out event context (#74).

Changes in 2.15.3 since 2.15.2

  • Noteworthy bug fixes
    • A bug in the C++, C#, and the experimental Scheme and JavaScript runtime and code-generators was fixed for the use of handwritten foreign components without skeleton support (this is not recommended!). This was a regression in 2.15.0 and for the experimental code generators in 2.15.2.

Changes in 2.15.2 since 2.15.1

  • Build
    • The test suite now passes on i686-linux.
  • Code
    • The c++ runtime now avoids making unnecessary copies.
    • The c++ runtime now avoids construction of trace strings when tracing is disabled.
    • The experimental c, javascript, and scheme code generators now pass the test suite for their partial supported feature set.
  • Noteworthy bug fixes
    • The parser now accepts on <event>, inevitable: and on <event>, optional:. This was a regression since 2.9.1.
    • The dzn graph command now also honors the -m,–model option for --format=json.
    • The dzn graph --backend=state command now produces sorted output.
    • The simulator no longer changes the state of the provides port without showing provides port interaction when using -C,--no-compliance.
    • The order of -I,--import options is now preserved.
    • The dzn code generator has been fixed by:
      • Adding spacing for port qualifiers,
      • Adding support for blocking port qualifier,
      • Preserving data type definitions,
      • Preserving the scope of of function types,
      • Including import statements.
    • A bug was fixed in the experimental c code generator with respect to negation in expressions.
    • The experimental javascript and scheme code generators now support reply on a synchronous out event.
    • The experimental c, javascript and scheme code generators now use a colon (:) as separator between the enum-type and enum-field, in compliance with this change in 2.13.0.
    • The experimental scheme code generator now supports non-collateral blocking, i.e., exclusively in the top component of a system.

Changes in 2.15.1 since 2.15.0

  • Build
    • Tests that produce unstable witnesses have been disabled so that the test-suite now passes with different builds of mCRL2 that, in case of multiple counter examples, leads to reporting one of them (pseudo) randomly.
  • Noteworthy bug fixes
    • Verification no longer erroneously reports a deadlock when using blocking in a synchronous context.
    • The simulator no longer prints the initiating port event arrow twice which would lead to an invalid split-arrows trace for certain compliance errors.
    • The simulator now synthesizes the missing port action in case of a compliance error, to produce a complete split-arrows trace.
    • The simulator now reports a second reply error at the return of a void event if a reply was already set.
    • The simulator now reports a deadlock when using a void reply in a non-blocking synchronous context.
    • The simulator no longer reports a deadlock when using a skip-block reply in a function.
    • The simulator now correctly postpones flushing in system context when using multiple out events on a single modelling event until all events are enqueued.