Announcement: discontinuation of service 2.7.x

Service 2.7.x has been discontinued as of November 2018. With the full verification support in 2.8.0, the 2.7.x service was declared deprecated. Service series 2.7.x was intended as a verification preview release series while working on the transition to mCRL2 based verification.

The 'development' service is based on service 2.8.1 and not on 2.8.2. The 'development' service contains work in progress and is not intended for evaluation or production use.

On the 20th of November 2018 service 2.8.2 replaced service 2.8.1 as Default with the following code generation fixes and improvements:

  • Solution for generating C++ code with a shell for system components that are defined in a namespace - solution for problem reported in Ticket 7505

  • Fix: "local variables within blocking cause a failure in the code generator" - solution for problem reported in Ticket 7509

  • Fix: "System with component with multiple injected interfaces generates double component instantiations" - solution for problem reported in Ticket 7518

  • Solution for shadowing a member variable with an interface declared event parameter

Service 2.8.1 replaced service 2.8.0 as Default with the following fixes and improvements:

  • The combined use of async and blocking is fixed as it regards verification.

On the 19th of June 2018 service 2.8.0 replaced service 2.7.2 as Default with the following fixes and improvements:

  • The Dezyne verification engine is based on mCRL2, see with full feature support, see

  • There is full support for the async feature. For more information click on and press Enter.

  • The semantics of silent modeling events, i.e. state transitions associated with on inevitable or on optional without externally visible events, is now more strict and enforced by a new well-formedness check.

  • The 2.8.0 dzn service version is used when verifying your models using previous dzn service versions.

  • Code generation is improved as follows:

    • The C++ code and runtime embed the service version.

    • There are several fixes for usage of native (sometimes referred as foreign) components.

    • The INTERFACE_ONLY macro has been removed from the C++ code generators.

    • Skeleton code for native components is now generated inline; no longer in a separate skel_ file.

If you have native components in your project please consider the following points:

  • For the handwritten code create a separate .hh and .cc file for every native component named exactly as the native component names in Dezyne (these files are included by Dezyne generated code)

  • Include the generated file (e.g. dezynefile.hh) that contains the skeleton (pure abstract) struct definition

  • If the native component is in a Dezyne file with the same name as the component we run the risk to overwrite handwritten code, therefore code generation for that file is refused, even though code generation is, incorrectly, reported as successful

  • The ASD converter now fixes an issue with shadowing of member variables.

  • Several namespace usage related bugs have been fixed. For an overview of supported namespace-usage see the following models in

    • hello_interface_namespace.dzn

    • hello_namespace_enum.dzn

    • foreign.dzn

    • inner_space.dzn

    • namespace_assert.dzn

    • name_space.dzn

  • Several bugs have been fixed in the --glue=dzn code generator.

Note: Due to changes in the Dezyne runtime you have to replace the old Dezyne runtime in your projects with the new one.

Additionally, a new version of the Dezyne command line client, a.k.a. dzn, is released with the following extensions/improvements:

  • The --version dzn command option accepts also the following constructions: --version=MAJOR and/or --version=MAJOR.MINOR.

  • The dzn query command also displays MAJOR and MAJOR.MINOR service versions.

Important:The c, c#, java, java7, python and scheme code generators are not available in this release; for these languages please use 2.4.1 or earlier

Note: To switch between dzn service version 2.8.x/Default and 2.4.1 or earlier, choose in the Dezyne Eclipse plugin/GUI the Window-Preferences menu item, click on Dezyne, select the desired 'dzn service version', and click 'Apply' or 'Apply and Close' (if you use a pre 2.6.0 version of the Dezyne Eclipse based GUI/plugin you have to click first on Log Out and then Log In).

On the 3rd of July 2018 Dezyne Eclipse plugin/GUI 2.8.0 is released with the following fixes/improvements:

  • Feature: Resolve "add option to create component model from interface model" - solution for problem reported in Ticket 7200

  • Feature: Resolve "Auto connect system ports"

  • Fix: Resolve "Already bound ports in system code completion"

  • Fix: Resolve "Suggestions not updated" - solution for problem reported in Ticket 7406

  • Fix: Resolve "System template generates the binding with error"

  • Fix: "Indent formatter on ASD import doesn’t respect space preference" - solution for problem reported in Ticket 7321

  • Feature: Provide option not to show popup on completion code generation - solution for problem reported in Ticket 7414

  • Feature: Verify all models in the project with a single invocation - solution for problem reported in Ticket 7442.
    Select the project folder in the Project Explorer and press F6 or select the 'Start Dezyne Model Verification' from the Toolbar.

  • Fix: Resolve "NPE on Sequence View and Watch View"

Next to the improvements mentioned above

  • The text of the DZN files in the regression test matrix can now be downloaded. To see the results of our regression tests and the models used in the respective tests feel free to visit the Results of Dezyne regression tests.

  • On GitHub there is a repository where Dezyne users may, and are invited to, share ideas and examples related to Dezyne. Feel free to visit the Dezyne Community repository and let us know how you use Dezyne.

This version is free for non-commercial use.

If you are interested in a license for commercial evaluation or commercial usage, please contact

Known issues

  • Those who install Dezyne on Ubuntu versions greater or equal than 18.04 and do not have the 'libgconf-2-4' library installed will receive the 'could not create any browser' message. Please ensure that you have installed the 'libgconf-2-4' library.

  • In some corner cases, nested function calls will cause a failing verification.

  • Not all old(er) versions of the Dezyne Eclipse GUI/plugin notify you that a new version is available. Please empty the 'dezyne_folder/p2/org.eclipse.equinox.p2.repository/cache' folder and restart Dezyne, or simply download the new version and use it with your (old) workspace.

  • Views (i.e. system views, state charts, state and event tables) are not cleared if they can not be updated due to an error in the model or due to missing data

For a complete list of known issues click on the following link: Known issues in Dezyne

Your free copy of Dezyne is waiting for you, and we encourage you to put Dezyne 2.8.x to good use and provide us with all your feedback.

Good Dezyning!

The Verum team.