Dezyne NEWS – history of user-visible changes

Dezyne Enterprise preview

Changes in dzn-explore dd. June 21, 2019

  • The performance of dzn-explore has been improved.

Changes in dzn-explore dd. June 13, 2019

  • State diagram: event descriptions related to foreign components now include their full path.

Changes in dzn-explore dd. June 4, 2019

  • A help page has bee added, accessable through the 'h' key.
  • You no longer have to specify the server on the command line.
  • A magnifying glass has been added to the state diagram.
  • The trace view header is now always visible at startup.
  • When navigating, the state diagram is not centered when the target state is already in view.
  • A trace can be truncated now.
  • The enterprise daemon has been rewritten in Dezyne, so incidental crashes are avoided.

Initial release of dzn-explore at https://development.verum.com

To install:

npm install -g https://development.verum.com/download/npm/dzn-enterprise.tar.gz

To explore, run:

.npm/bin/dzn-explore

Changes in development since 2.9.1

It contains work in progress and is not intended for evaluation or production use.

Changes in 2.9.1 (since 2.9.0)

Verification: reduce memory usage by one order of magnitude:

Allows models with a larger state space to be verified.

Verification: improved error reporting:

Internal errors and out of memory error are now reported as such.

Verification: fix for issue 7547:

Compliance now succeeds when using async in the middle of two provides out events on a single modeling event in the interface.

Code: fix for issue 7529:

C++: a reply with a port prefix can be used anywhere, not just in a blocking context.

Code: fix for issue 7527:

C++: parameterized events can be used with dzn::shell

Changes in 2.9.0 (since 2.8.1)

Reintroduction of C#.

For C++ fix the use of injected in combination with thread safe shell.

Announcement: discontinuation of 2.7.x

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

Changes in 2.8.2 (since 2.8.1)

Code generation

  • C++: fixed 7505 Namespaces and system components
  • C++: fixed 7509 local variables within blocking cause a failure in the code generator
  • C++: fixed 7518 System with component with multiple injected interfaces generates double component instantiations
  • fixed shadowing a member variable with an interface declared event parameter

Changes in 2.8.1 (since 2.8.0)

Verification

  • Fixed the combined use of async and blocking

Changes in 2.8.0 (since 2.7.2)

Verification

Service selection

  • The dzn COMMAND –version option now also accepts –version=MAJOR and –version=MAJOR.MINOR.
  • dzn query command now also shows MAJOR and MAJOR.MINOR service versions.

Code generation

  • C++ code and runtime now embed the service version.
  • Several fixes for usage of foreign components.
  • INTERFACE_ONLY has been removed from the C++ code generators.
  • Skeleton code for foreign components are now generated inline; no longer in a separate skel_ file.

ASD Converter

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

Noteworthy bug fixes

  • Several namespace bugs have been fixed, supported usage includes tests in https://hosting.verum.com/regression/2.8.0
    • 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.

Changes in 2.7.2 (since 2.7.1)

Verification

  • The verification performance has been improved by a factor 3-4, especially for large models. For an interface, the deadlock and livelock checks are performed in parallel. For a component, the determinisctic, illegal, deadlock, and livelock checks are performed in parallel.
  • The verification results view reports per check the number of states and transitions that have been considered.

Known issues

  • In some corner cases, nested function calls will cause a failing verification.
  • The language features blocking, external and async are not yet available for verification, see https://hosting.verum.com/regression/2.7.2/regression.html.
  • For verification, when selecting version 2.7.0 or 2.7.1, version 2.7.2 is used instead.

Changes in 2.7.1 (since 2.7.0)

Verification

  • The dezyne verification now supports models with multiple provides ports.
  • Functions with parameters are verified correctly now.

Code generation

  • Code generation for c++-msvc11 has been fixed.

Known issues

Changes in 2.7.0 (since 2.6.1)

Verification

  • The Dezyne verification engine has been replaced by mCRL2, see http://mcrl2.org.
  • Interface completeness verification is performed as part of the deadlock check.
  • Verification counter examples may differ from previous versions.

Known issues

  • The language features multiple provides, blocking, external and async are not yet available for verification, see https://hosting.verum.com/regression/2.7.0/regression.html.
  • The verification feature has been discontinued for all older releases.
  • Verification performance has not been fully optimized.

Code generation

  • Performance of the code generator has been improved significantly.

Changes in 2.6.1 (since 2.6.0)

Code generation

  • The c++ code now avoids triggering some Visual Studio compiler warnings.
  • Calling context has been enhanced.

ASD Converter

  • The ASD converter now forwards user-defined includes to DZN.

Changes in 2.6.0 (since 2.5.3)

  • The interpreter now shows the content of the queues in the watch-window.

Command line client

  • The ‘dzn hello’ command now returns with a dedicated exit status 3 in case no server connection could be made

Model verification

  • All models in a DZN file are now verified by default, unless the explicit ‘-m,–model=MODEL’ option is used.
  • The –queue_size option (broken since 2.5.0) has been fixed

Verification view

  • The new verification view displays for each check the number of states and transitions the verification engine had to consider.

Documentation

  • The text of the DZN files in the regression test matrix can now be downloaded.

Changes in 2.5.3 (since 2.5.2)

Noteworthy bug fixes

  • Globally declared enums which are not used as event reply type no longer cause a crash in verification (bug introduced in 2.5.0)
  • dzn convert now has a ‘–glue’ option. The glue namespace is only added when this option is used.

Code generation

  • c++* only depends on pump when blocking or async are used
  • this relaxes the boost dependency on 1.58+ for coroutine to any previous version supporting bind, function and tuple.

Changes in 2.5.2 (since 2.5.1)

Code generation

  • c++* fix void event in thread safe shell

Changes in 2.5.1 (since 2.5.0)

Code generation

  • c++* thread safe shell now supports enum and subint reply types

Changes in 2.5.0 (since 2.4.1)

Code generation

  • The javascript code generator now uses file2file mode.
  • The c++ code generator passes ASD construction parameters via glue.
  • The c++ code generator skips retrieving the pump pointer when async is not used.
  • The c++03 code generator now supports thread safe shell, but only if there is enough c++11 support available in the compiler.
  • 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.

ASD Converter

  • The ASD converter produces ‘.map’ files for Components with construction parameter information that is used by the glue code generator.

Known issue:

  • Global declared enum not referenced as a reply type not supported in verification.
  • The queue_size option gives an error: ‘gdzn: no such option: -q’

Changes in 2.4.1 (since 2.4.0)

DZN language

  • Dollar expressions can now be used at toplevel

Code generation

  • The c++03 runtime now uses a boost-compatible workaround for lacking move semantics
  • Using ‘reply()’ in a function called from a ‘blocking’ context has been fixed

Verification

  • The queue_size option has been fixed

Changes in 2.4.0 (since 2.3.4)

Code generation

  • The c++ code generators use file2file mode by default Generating code for a DZN file ‘model.dzn’ now produces ‘model.hh’ and ‘model.cc’
  • The c# runtime now has a ‘check_bindings’ function
  • The interface of the c++ and c++03 runtime has been modified
  • The container interface the c++ languages (‘container.hh’) has been changed
  • The c++03 code generator now supports ‘blocking’
  • The c++03 code now depends on boost 1.58 or newer

Model verification

  • Verification performance of some models has been improved

Noteworthy bug fixes

Author: Nix build user

Created: 2019-06-21 Fri 09:15

Validate