Dezyne NEWS – history of user-visible changes

• Injected is now supported.

To install and run, do something like:

• User action processing is indicated with a 'wait' cursor.
• Sub systems can be 'blackboxed', using the 'b' key. See the help page for more information.

• A second explore view can now be opened.
• The state diagram hides/shows all interface state, toggled with `i'.

• State diagram: selecting the appropriate event sequence has been improved. See the help page for more information.
• State diagram: The magnifying glass only shows when hovering above a node.
• The color scheme used in the three views has been slightly changed. The colors can be customized by editing the following file in the installation: .npm/lib/node_modules/dzn-enterprise/js/color_scheme.js
• dzn-explore will report any parse error and exit.
• Stand-alone components can be explored now.
• The system view now shows the correct top level system.
• When the dzn-explore command is terminated, no further exploration is possible. To alert the user all three views show a red border.

• The performance of dzn-explore has been improved.

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

• A help page has bee added, accessible 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.

To install:

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

To explore, run:

.npm/bin/dzn-explore

Allows models with a larger state space to be verified.

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

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

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

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

• 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

• Fixed the combined use of async and blocking

• Full verification support based on mCRL2 (http://mcrl2.org), see https://hosting.verum.com/regression/2.8.0.
• The async feature has been officially released, see https://hosting.verum.com/doc/?searchWord=async.
• The semantics of silent modeling events is now more strict and enforced by a new well-formedness check.
• The 2.8.0-verification service is implicitly used for previous service releases.

• 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.

• 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.

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

• 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.

• 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.

• 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.

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

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

• The language features blocking, external and async are not yet available for verification, see https://hosting.verum.com/regression/2.7.1/regression.html.

• 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.

• 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.

• Performance of the code generator has been improved significantly.

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

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

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

• 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

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

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

• 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.

• 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.

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

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

• 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.

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

• 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’

• Dollar expressions can now be used at toplevel

• 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

• The queue_size option has been fixed

• 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

• Verification performance of some models has been improved

• Authentication with the dzn client is robust against parallel execution
• Handle output from model checker where lines are broken in two parts (https://zoho.verum.com/7327)
• Dollar expressions can now contain DZN keywords (https://zoho.verum.com/7310)
• Parameters in on-clauses for unused notification events are no longer removed (https://zoho.verum.com/7309)
• The ASD converter now renames variables that conflict with DZN keywords (https://zoho.verum.com/7308)
• Type declarations can now appear anywhere at the toplevel of a behaviour (https://zoho.verum.com/6747)