[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:
<https://dezyne.org/documentation.html>.
We will evaluate your reports and track them via the
[[https://gitlab.com/groups/dezyne/-/issues][Gitlab dezyne-issues
project]], see our [[https://dezyne.org/bugreport][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'.
Future
Looking beyond the next releases we will introduce implicit interface
constraints. Hierarchical behaviors, module-specifications and
data-interfaces. Support for Model Based Testing.
Enjoy!
The Dezyne developers.
Here are the compressed sources and a GPG detached signature[*]:
https://dezyne.org/download/dezyne/dezyne-2.15.1.tar.gz
https://dezyne.org/download/dezyne/dezyne-2.15.1.tar.gz.sig
Here are the SHA1 and SHA256 checksums:
bf946bd8b13e55b055f67339c33796b86f10f4a1 dezyne-2.15.1.tar.gz
c657900fcc5a081b9aa8219a983f4b486d2830b8ff009fdd6190dcdd93122d7a
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 keys.gnupg.net --recv-keys
1A858392E331EAFDB8C27FFBF3C1A0D9C1D65273
and rerun the 'gpg --verify' command.
NEWS
* 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
supported.
- An action or function call can now also be used in a return
expression ([[https://gitlab.com/dezyne/dezyne-issues/-/issues/67][#67]]).
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 show the state
([[https://gitlab.com/dezyne/dezyne-issues/-/issues/66][#66]]),
+ 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 ([[https://gitlab.com/dezyne/dezyne-issues/-/issues/64][#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 <janneke@gnu.org> | GNU LilyPond https://lilypond.org
Freelance IT https://JoyOfSource.com | AvatarĀ® https://AvatarAcademy.com
signature.asc
Description: PGP signature
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [ANN] Dezyne 2.15.1 released,
Jan Nieuwenhuizen <=