We are delighted to announce Dezyne 2.12: The first release to include a complete state diagram for interfaces, components and systems.

Dezyne introduces a new command to explore models (dzn explore) that can generate an LTS in Aldebaran format a state diagram in DOT format for interfaces, components and systems.

This release also introduces language packs, and re-introduces C# as a separate language pack.

Dezyne-IDE re-introduces a state view: ide state. Unlike previous versions of the state diagram, this one displays the values of each state variable involved in constraining the behavior, i.e. for components this includes the interface state variables of its ports, and for systems this also includes the state variables of its inner components.

The documentation is available here: download.verum.com/documentation.html.

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?

In the upcoming release(s) we aim to integrate the new system simulator in Dezyne-IDE. In the core of Dezyne we aim to extend the language with aspects like: implicit interface constraints, hierarchical behaviors, data-interfaces, as well as release the Dezyne language core as free software.

Enjoy!
The Verum Team

Download

Here are the binary downloads and a GPG detached signature[*]:
dezyne-2.12.0-x86_64-linux.tar.gz (55MB)
dezyne-2.12.0-i686-windows.zip (118MB)
dezyne-ide-2.12.0-x86_64-linux.tar.gz (74MB)
dezyne-ide-2.12.0-i686-windows.zip (157MB)

Here are the GPG detached signatures[*]:
dezyne-2.12.0-x86_64-linux.tar.gz.sig
dezyne-2.12.0-i686-windows.zip.sig
dezyne-ide-2.12.0-x86_64-linux.tar.gz.sig
dezyne-ide-2.12.0-i686-windows.zip.sig

Here are the MD5 and SHA1 checksums:

6cd5093963972a544e91b84939fdcd57  dezyne-2.12.0-i686-windows.zip
34faedd5fd72f2e5af82157feb6da95c  dezyne-2.12.0-x86_64-linux.tar.gz
11928b91f4384c346dd92d78fc006f3e  dezyne-ide-2.12.0-i686-windows.zip
4a9c5caa57e360b83e8e3799f685d12e  dezyne-ide-2.12.0-x86_64-linux.tar.gz
f69cc22c390968661e4df945afbe30f82764aec8  dezyne-2.12.0-i686-windows.zip
45611b9706a74b4175a2775a545231efc7723cf4  dezyne-2.12.0-x86_64-linux.tar.gz
1a1a591c6d8b0d99fb97d78195254b938f288e62  dezyne-ide-2.12.0-i686-windows.zip
656c361e0836a4f0dcafc2f390d6f53a5b00206f  dezyne-ide-2.12.0-x86_64-linux.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.12.0-x86_64-linux.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.

Get informed, get involved

See gitlab.com/dezyne/dezyne-issues
Join #dezyne on irc.libera.chat.

NEWS

Dezyne-IDE

Changes in 2.12.0 since 2.11.0

• Commands

  • A new command ide state provides a state diagram for interfaces, components and systems. The state comprises all variables, the behaviour . Under the hood, it uses the new dzn explore command. Note that there is no convenient way to display models with a large state space yet. Also note that the trace view still uses the component simulator.
  • ide commands no longer spawn a browser.

• Views

  • The views now reconnect automatically when the connection to the daemon is lost.

• Build

  • Building with Guile 3.0.5 is now supported.

• Noteworthy bug fixes

  • The implicit --all flag was removed from ide verify. As the current trace view can only show one verify result, running with --all can lead to confusion (#13).

  • The system view now handles every go-to-location click (#14).

  • Click events now carry the working directory of a command. Even when the daemon was started in another directory than the current working directory of a command, click events should continue to work (#15).

  • The LSP client is now robust against non-existent imports (#16).

  • On Windows, ide verify would hang for a model with a longer compliance error trace (#17).

  • On Windows, ide browse uses the user-defined default browser instead of trying chromium first.

Dezyne core

Changes in 2.12.0 since 2.11.0

• Commands

  • A new command dzn explore can be used to create LTSs and accurate state diagrams of interfaces, components and systems.
  • A new command dzn simulate provides a basic system simulator.
  • Code completion now supports boolean expressions in (partial) guards and (partial) enum field tests.

• Parser

  • The dzn parse command has a new option: --list-models.
  • The import file-name now supports relative directories.

• Verification

  • The verification pipeline was refactored and opened-up:

    • The actual pipeline commands are shown when running dzn -d verify ..., ready for use on the command line.
    • The dzn verify command now has a new --out=FORMAT option to produce intermediate verification output of a certain FORMAT.

• Code generation

  • Code generation has been cleaned-up.

    • Language packs are now supported.
    • The code generators produce less gratuitous whitespace.
    • The code indenter cleans-up orphan parentheses when generating Scheme code.
  • The C# code generator (language CS) has been resurrected.
  • The generated code now provides basic provenance by adding a Generated by dzn code from <file-name> comment, removing any question of copyright. Protip: for reproducible output, use a relative dezyne file name.
  • The json code generator (for the system diagram) now strips behaviours and leaf-locations.

• Language

  • Lookup of imports is now supported.
  • Completion of guard expressions and field-tests are now supported.

• Build

  • Building with Guile 3.0.5 and guile-json-4 is now supported.

• Noteworthy bug fixes

  • Unresolved imports are handled (#6).

  • Duplicate imports when using different directory prefixes (#7).

  • A regression has been fixed that caused parsing of a system with many imports (> 20) to become very slow (#8).

  • c++ thread_pool support is now off by default, like it should be (#10).

  • Using a synchronous callback in the context of a thread safe shell has been fixed for c++ and scheme.

  • A bug has been fixed in parsing verification traces with flushes occurring in a namespace (#11).

  • Triggering an illegal using a synchronous callback in the context of dzn.async has been fixed (#12).

  • In dzn language, any line-column separator can be used with the --point= option; using a comma no longer gives unexpected results.

About Dezyne

In Dezyne, you define components and their interfaces through a familiar and compact C/Java like-language. The Dezyne language is targeted at the logic or event-driven behaviour of an application. The interfaces are the specification and the components are the implementation.

Dezyne automatically verifies semantic correctness of the logic behaviour and proves that the components correctly implement the interfaces. A user can simulate the behaviour to validate whether this is as intended. Diagrams and logical views are generated automatically from the language description. As a final step code can be generated in a number of standard programming languages.

Without having to rely on a process Dezyne automatically highlights problems areas, stimulates communication about these and enforces that components work together.

About Verum

verum.com is a leading developer of software design tools to create, simulate, mathematically verify and automatically generate code for embedded and cyber-physical systems.

At Verum, we help our customers and partners solve the most challenging software issues of today and tomorrow. We support customers with our product Dezyne, a software engineering toolset that enables engineers to specify, design, validate and formally verify software components for embedded systems combined with consultancy services.