We are delighted to announce Dezyne 2.13: The simulator function including system scope.

This replaces the simulation function that was moved from Dezyne Core in release 2.10 to Dezyne-IDE in release 2.11. The new simulator function provides a basic command-line interface in Dezyne Core and is now also integrated in the Dezyne-IDE.

The integrated Trace view of the simulator was rewritten in P5, using the new Dezyne-P5 project by Rob Wieringa which he developed as free software. The buttons for events that are outside the accepted behaviour are only greyed-out and can still be selected to inspect what happens if the event would occur.

The integrated System view was also rewritten in P5, removing the last dependency on third-party proprietary software.

Finally, verification and simulation can now be loosely integrated on the command-line and an experimental ASCII diagram is provided by dzn trace, i.e., running

    dzn verify examples/Alarm.dzn | dzn simulate Alarm.dzn \
      | dzn trace --format=diagram

gives

error: illegal action performed in model Alarm
test/all/Alarm/Alarm.dzn:136:25: error: illegal
console             Alarm              sensor siren
  //                 //                 //     //
   .                  :                  .      . error: illegal
   .                  :                  .      .
   .                  :         triggered.      .
   .                  :<-----------------.      .
   .                  :                  .      .
   .          detected:                  .      .
   .<-----------------:                  .      .
   .                  :                  .      .
   .                  :turnon            .      .
   .                  :------------------------>.
(trail sensor.triggered console.detected siren.turnon <illegal>)
(eligible)

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?

Extending the language with aspects like: implicit interface constraints, hierarchical behaviors, module-specifications and data-interfaces. Support for Model Based Testing. Releasing the Dezyne Core as free software.

Enjoy!
The Verum Team

Download

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

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

Here are the MD5 and SHA1 checksums:

90980647b88e18a103a3b2b62bb92814  dezyne-2.13.0-i686-windows.zip
aa54b6b492e464bf1075f5ac39b13d4f  dezyne-2.13.0-x86_64-linux.tar.gz
c0c62077ff26fe95c5cfb6c512f0202d  dezyne-ide-2.13.0-i686-windows.zip
e78c1abef1da7d28180681ddd57516be  dezyne-ide-2.13.0-x86_64-linux.tar.gz
64e02fbaff3a7926561108497c8e663ba04deb08  dezyne-2.13.0-i686-windows.zip
fa696b73226200a14e69cdcb500bf462dec9196f  dezyne-2.13.0-x86_64-linux.tar.gz
83de7a9930d8dcb6ee4448551c8b65906a6bf13b  dezyne-ide-2.13.0-i686-windows.zip
11f810fe5698316f8eafba2698436120ae16176a  dezyne-ide-2.13.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.13.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.13.0 since 2.12.0

• Simulation

  • Simulation now uses the dzn simulate command under the hood. This provides a simulator function including system scope and enables future language updates.
  • The --queue-size option is now supported for simulation.

• Verification

  • Detailed error messages of verification and simulation are displayed in the console.
  • The --all flag has been removed for ide verify and thus the implicit ide simulate displays the first and only error.

• Views

  • Clicking on a port in the System view highlights the port binding across system boundaries.
  • The System view now uses P5.
  • The Trace view now uses P5.

• Noteworthy bug fixes

  • The daemon now supports the -w,--http-port option.

Dezyne Core

Changes in 2.13.0 since 2.12.0

• Simulation

  • Interactive use is now supported, it is started when invoked without input trail.
  • The input trail may now be sparse, only the input needed to resolve non-deterministic choices is required.
  • The split-arrows trace format is now used by default. It includes the provides port trace.
  • The eligible events are printed at the end of the trace.
  • Invalid input (garbage) on the trail is marked as an error.

  • All verification problems are detected and reported, notably:

    • async livelock,
    • failures model refusals,
    • forking a call from one provides port to another provides port,
    • a second async req, while a previous ack is still pending,
    • a reply on a modeling event in an interface.
  • A provides port that uses silent events is now supported.

• Commands

  • The dzn trace command has two new output formats:

    • --format=json provides P5 output for integration with Dezyne-IDE,
    • --format=ascii provides an trace diagram.
  • The JSON output for the state diagram now produces actions and state as structured data.

• Verification

  • Enum literals in the verification trace now use a colon as enum-field separator. This resolves a long standing ambiguity in the trace format.
  • The verification standard output is now adds the model name next to the trace.
  • The trace is now marked with a <label> indicating the problem found during verification.
  • Verbose output is written to standard error.
  • The --json option has been removed.
  • Async livelocks, i.e., defer.ack () => defer.req () are now detected and reported.

• Code generation

  • The C# runtime now defines a generic async interface; async interfaces are no longer generated.
  • The C++ code generator has been updated to support the new enum literal representation.
  • The C# runtime has been updated to support the new enum literal representation.
  • The experimental C code generator now properly supports systems, foreign components and namespaces.

• Noteworthy bug fixes

  • A type mismatch is now also properly reported when attempting an enum field access on a boolean (#19).

  • An undefined function is now also properly reported for a function call that has arguments (#18).

  • Verification now reports a livelock with async.

  • In the simulator, for a requires out event on a model with multiple provides ports, all provides ports are now being updated.

  • In the preprocessor, an off-by-one line count error has been fixed for deeply nested imports.

  • Generating code using a calling context for a model that uses dzn.async is now supported (#20).

  • Using the same async interface with parameters more than once no longer triggers a well-formedness error.

  • The C++ and C# code generators no longer create structs or classes for async interfaces with parameters.

  • Using an early return pattern in a function now no longer reports a false positive <livelock> or <second-reply> error (#27).

  • The C++ and C# runtime and pump now queue events that are sent to a blocked port (#23).

  • The C++ and C# runtime no longer releases collaterally blocked ports early, avoiding "component already handling an event" (#23).

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.