[Top][All Lists]

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

[ANN] Dezyne 2.15.1 released

From: Jan Nieuwenhuizen
Subject: [ANN] Dezyne 2.15.1 released
Date: Thu, 02 Jun 2022 08:34:26 +0200
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux)

We are proud and relieved to announce Dezyne 2.15.1 which completes full
support for blocking: This finally marks the Grand Unification into
single threaded execution semantics.

The documentation is available here:

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

What's next?

Verification with system scope and automatically exploring possible
traces in a system.  Introducing a new keyword `defer' for asynchronous
behavior and deprecation of `async'.


Looking beyond the next releases we will introduce implicit interface
constraints.  Hierarchical behaviors, module-specifications and
data-interfaces.  Support for Model Based Testing.

The Dezyne developers.

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

Here are the SHA1 and SHA256 checksums:

bf946bd8b13e55b055f67339c33796b86f10f4a1  dezyne-2.15.1.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 .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.


* 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 modeling event until all
    events are enqueued.

* Changes in 2.15.0 since 2.14.0
** Language
  - Blocking is now fully supported, it may be used:
    + In non-toplevel components,
    + In a component with multiple provides ports, but see the
      `Blocking' section in the manual for caveats.
    + A new `blocking' qualifier for ports must be used if a port can
      block, or block collateraly.
  - Using unobservable non-determinism in interfaces is no longer
  - An action or function call can now also be used in a return
    expression ([[][#67]]).  
Note that recursive functions still cannot be
** Commands
  - The `dzn explore' command has been removed.
** Verification
  - The verifier now supports blocking for components with multiple
    provides ports.
  - The verifier now detects possible deadlock errors due to a requires
    action blocking collaterally, which could happen when a component
    deeper in the system hierarchy uses blocking.
  - The option `--no-interface-determinism' has been removed for `dzn
** Simulation
  - The simulator now supports collateral blocking.
  - In interactive mode:
    + The new ,state command show the state 
    + The new ,quit command exits the session,
    + The simulator does not exit when supplying empty input.
  - The simulator now detects possible deadlock errors due to a requires
    action blocking collaterally, which could happen when a component
    deeper in the system hierarchy uses blocking.
  - The simulator now detects livelocks in interfaces at end of trail.
  - The simulator now detects queue-full errors caused by external at
    end of trail.
  - The `dzn simulate' command now supports the `-C,--no-compliance',
    `--no-interface-livelock' and `-Q,--no-queue-full' options,
** Code
  - The C++ and C# code generators and runtime now fully support
    collaterally blocking components.
** Views
  - Returns are no longer removed from the state-diagram.  Using the new
    `--hide=returns' (or `--hide=actions') now removes void action
** Documentation
  - Blocking has been updated and extended.
  - A new section on foreign components was added.
** Noteworthy bug fixes
  - Using the construct `provides external' (which has no semantics) no
    longer confuses the simulator.
  - A bug has been fixed that would cause the well-welformness check for
    system bindings to ignore certain missing bindings.
  - A bug has been fixed when assigning a value to a formal parameter of
    a function.
  - A bug has been fixed in the vm that would cause graph or simulate to
    hang when using a foreign component that has both provides and
    requires ports (note: don't do that!).
  - The test framework can be built using gcc-11.
  - A bug has been fixed in the code generator when assiging to a local
    variable that shadows a formal parameter or member variable.
  - A bug has been fixed in the verifier when creating a new local
    variable or assigning a variable that remains otherwise unused.
  - The simulation function now supports injection of foreign
  - The trace produced by running dezyne code is now correct when using
    injected foreign components.
  - A bug has been fixed that would cause the verifier to overlook
    non-determinism in a component.
  - Using external data in binary expressions is now reported as an
    error ([[][#64]]).
  - The parser no longer reports "<unknown-type>" expected when an
    external type definition is missing.
  - The well-formedness check of the parser no longer hangs when a
    component has the same name as one of its interfaces.
  - An interface can now have the same name as its namespace.

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

Attachment: signature.asc
Description: PGP signature

reply via email to

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