Re: [ANN] Dezyne 2.15.0 released as Free Software

[Nala Ginrut]

It's really nice!!

On Fri, May 6, 2022, 21:09 Jan Nieuwenhuizen <janneke@gnu.org> wrote:

> We are thrilled to announce Dezyne 2.15: Dezyne is now being released as
> Free Software (FLOSS).
>
> * About
>
> Dezyne[0] is a programming language and a set of tools to specify,
> validate, verify, simulate, document, and implement concurrent control
> software.
>
> 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
> components.
>
> * Summary
>
> This release completes full support for blocking: This finally marks
> the Grand Unification into single threaded execution semantics.
>
> The documentation has seen a major rewrite and is available here:
> <https://dezyne.org/documentation.html>.
>
> We will evaluate your reports and track them via the
> Gitlab dezyne-issues project[3], see our guide to writing
> helpful bug reports[4].
>
> * 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'.
>
> * Future
>
> Looking beyond the next releases we will introduce implicit interface
> constraints.  Hierarchical behaviors, module-specifications and
> data-interfaces.  Support for Model Based Testing.
>
> Please do not hesitate to forward this announcement to other fora
> interested in formal methods and verification!
>
> Enjoy!
> The Dezyne developers.
>
> * Download
>
>   git clone git://git.savannah.nongnu.org/dezyne.git
>
>   Here are the compressed sources and a GPG detached signature[*]:
>     https://dezyne.org/download/dezyne/dezyne-2.15.0.tar.gz
>     https://dezyne.org/download/dezyne/dezyne-2.15.0.tar.gz.sig
>
>   Here are the SHA1 and SHA256 checksums:
>
>     395ff05e4f2c17bcee895fd9436d696fb0aab93d  dezyne-2.15.0.tar.gz
>     982d8f7cca9de23225e2f06b4c8524c0b57acfba81beaaff1a0c045c1e6409ea
> dezyne-2.15.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.15.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 keys.gnupg.net --recv-keys
> 1A858392E331EAFDB8C27FFBF3C1A0D9C1D65273
>
>   and rerun the 'gpg --verify' command.
>
>   Alternatively, Dezyne can be installed using GNU Guix[5]:
>     guix pull
>     guix install dezyne
>
> * NEWS
>
> * 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
>     supported.
>   - An action or function call can now also be used in a return
>     expression (#67[5]).  Note that recursive functions still cannot be
>     valued.
> ** 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
>     verify'.
> ** Simulation
>   - The simulator now supports collateral blocking.
>   - In interactive mode:
>     + The new `,state' command shows the state (#66[6]),
>     + 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
>     returns.
> ** 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
>     components.
>   - 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[7]).
>   - 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.
>
> * Links
>
> [0] https://dezyne.org
> [1] https://mcrl2.org
> [2] https://tue.nl
> [3] https://gitlab.com/groups/dezyne/-/issues
> [4] https://dezyne.org/bugreport
> [5] https://gitlab.com/dezyne/dezyne-issues/-/issues/67
> [6] https://gitlab.com/dezyne/dezyne-issues/-/issues/66
> [7] https://gitlab.com/dezyne/dezyne-issues/-/issues/61
>
> --
> Jan Nieuwenhuizen <janneke@gnu.org>  | GNU LilyPond https://lilypond.org
> Freelance IT https://JoyOfSource.com | Avatar® https://AvatarAcademy.com
>
>