It's really nice!! On Fri, May 6, 2022, 21:09 Jan Nieuwenhuizen <jann...@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 <jann...@gnu.org> | GNU LilyPond https://lilypond.org > Freelance IT https://JoyOfSource.com | Avatar® https://AvatarAcademy.com > >
