We are delighted to announce Dezyne 2.13.3: 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 illegals, implicit temporary variables, implicit interface constraints. Releasing the Dezyne Core as free software.

Future

Looking beyond the next releases we will introduce a new keyword defer to deprecate the use of async. Full blocking support. Hierarchical behaviors, module-specifications and data-interfaces. Support for Model Based Testing.

Enjoy!
The Verum Team

Download

Here are the binary downloads and a GPG detached signature[*]:
dezyne-2.13.3-x86_64-linux.tar.gz (70MB)
dezyne-2.13.3-x86_64-windows.zip (133MB)
dezyne-ide-2.13.3-x86_64-linux.tar.gz (85MB)
dezyne-ide-2.13.3-x86_64-windows.zip (136MB)

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

Here are the MD5 and SHA1 checksums:

69a4c52cd856a971111475a51474ff24  dezyne-2.13.3-x86_64-windows.zip
0ac6eec9d18f0953a2641c08bee8b602  dezyne-2.13.3-x86_64-linux.tar.gz
81921fc1f38eddcb9fb291a9d053a784  dezyne-ide-2.13.3-x86_64-windows.zip
fbf118cd0c640e15894c465820c6af5c  dezyne-ide-2.13.3-x86_64-linux.tar.gz
70fa30b769e7327fd3acb4894907e5e050d9d6c6  dezyne-2.13.3-x86_64-windows.zip
790d2db6ab0b79bfbb71ea2101bc9d574c1866fe  dezyne-2.13.3-x86_64-linux.tar.gz
a5657a936fb1e98bd0621fb7f51c5d077d766c0c  dezyne-ide-2.13.3-x86_64-windows.zip
6e5f100a500b73daf8e88abcb2eef30c9bc8a6a3  dezyne-ide-2.13.3-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.3-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.openpgp.org \
  --recv-keys 1A858392E331EAFDB8C27FFBF3C1A0D9C1D65273 AD43109BE73D4891B77076862A611108640C1816

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.3 since 2.13.2

• Views

  • In the trace view, the order of lifelines of the ports can be changed by dragging them to a new place.
  • For verification errors that have multiple error messages or extra informational messages, such as compliance errors or range errors, in the trace view each message can be clicked to show the relevant location in the Dezyne code.

• Noteworthy bug fixes

  • The ide lsp command has been greatly improved (#38,#41,#51,#52):

    • Redundant parsing has been eliminated: The callbacks for reading a file and for parsing are now called only once per file; greatly improving performance on larger projects,
    • The lsp server can no longer be flooded with "didChange" messages, leading to a denial of service: superseeded "didChange" messages are now dropped; also cancel-requests are honored,
    • Error messages no longer contain the skipped text; this makes the root cause of the error easier to spot,
    • An import statement refering to a non-existing file is now reported as a syntax error,
    • A syntax check is now also performed when a file is opened, any errors are reported,
    • When a file is opened using the "textDocument/didOpen" command, the text from the message is used instead of accessing the file system,
    • The "textDocument/didOpen" command now also works even if the file is not present on the file system,
    • Two problems with unbounded recursion and several crashes have been fixed.
    • The goto definition function now also considers the identifier to the left of the cursor if the cursor is on punctuation, catering for users that use a caret instead of a cursor in their editor.

  • A second ide simulate session for another model from the same file now corretly simulates and presents the newly selected model,

  • The System view now automatically updates after running a new ide system command (#56).

  • A bug has been fixed in the System view that could cause stack-overflow in JavaScript.

Changes in 2.13.2 since 2.13.1

• Views

  • An SVG image of a view can be saved by pressing Control-S.

• Noteworthy bug fixes

  • Verify and simulate now always show a trace view (#34):

    • The alert sign with messages is shown even when there is no trace,
    • An invalid trace is handled gracefully; the valid prefix of the trace is shown along with an error message,
    • Pressing [F12] now always produces the browser's console.

  • User experience (#37):

    • Source code locations of some arrows have been fixed,

    • All error messages are now also shown in the browser,

    • The placement of the alert sign and the last arrow leading up to the alert sign has been fixed,

    • The color scheme of an interface trace is now consistent,

    • Performance: built with GNU Guile 3, Windows 64 bit.

Changes in 2.13.1 since 2.13.0

• Noteworthy bug fixes

  • Simulation now reports well-formedness errors instead of merely exiting with a non-zero status.

  • The well-formedness check is now skipped on subsequent simulation runs.

  • When verifying a correct model that is defined in a namespace, a crash has been fixed that prevented the simulation function to start.

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. Its performance requires more work.
  • 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.3 since 2.13.2

• Parser

  • Using newlines in dollar-expressions and toplevel dollar-statements is no longer reported as an error.

• Verification

  • The length of the command-line used by the verification pipeline has been reduced, allowing Windows users to verify larger models (still up to the arbitrary 8191 command-line limit) (#31):

    • The dzn lts command now has a new --exclude-tau option that is used in the verification pipeline. This reduces the length of the command-line by about 2/3rds,
    • The ltscompare command as used in the verification pipeline no longer contains duplicate or unused events. This reduces the length of the command-line in some cases by an order of magnitude.

• Noteworthy bug fixes

  • The default model selection for a command no longer considers imported models (#46).

  • Verification and simulation now have a new check that dissallows non-deterministic behavior in interfaces which is not directly but indirectly observable by the client.

  • The new option --no-interface-determinism can be used to disable this check on dzn verify and dzn simulate.

  • Stateful models with a livelock performed poorly in explore. Therefore state diagrams or LTSses for models with a livelock are now truncated.

  • On dzn explore, the --queue-size parameter now works.

  • The deadlock check in the simulator no longer performs a full (expensive) run of all events, greatly improving the performance for some models.

  • A bug in the simulator was fixed that lead to quadratic duplication of identical traces for each extra event on the input, with dramatic impact on performance (#52).

  • A bug in the simulator was fixed that lead to unbounded retry of silent event execution. This regression was introduced in 2.13.2.

  • A bug in the simulator was fixed that could cause a reply value in a port to be overwritten by the reply value of its component, leading to a wrong and incomprehensible output trace.

  • A bug in the simulator was fixed that would skip a block when an earlier reply was mistaken for a release.

  • A bug in the simulator was fixed that would skip a block when flushing the queue.

  • A bug in the verifier since 2.8.0 was fixed. It caused back-to-back function calls to produce invalid mCRL2 code.

  • A bug in the parser has been fixed that allowed using parentheses on actions in an interface; this is now an error (improves #39).

  • An oversight since 2.10 in the c++ code generator was fixed. Component constructors now default initialize reply values.

  • The dzn language command has been greatly improved (#38,#41):

    • Incomplete or garbled parse-trees are handled more gracefully,

    • Lookup was rewritten to breadth-first and to allow memoization for better performance,

    • Lookup now supports bool, subint and extern variables, arguments, event type, formals, expresions, blocking out-bindings, component instances, system bindings, and namespaces,

    • Completion was rewritten to use type resolving based on context accessors,

    • Completion now supports bool, subint and extern variables, arguments, assignments, formals, if and else, imports, optional and inevitable, otherwise, port-qualifiers, reply, return, system bindings, and namespaces,

    • Completion now includes the full type signature when completing triggers (#51),

    • Completion now better handles incomplete or garbled parse trees,

    • Two bugs were fixed where completion would enter unbounded recursion,

    • The --line option was added as an alias for --point,

    • When using the -d,--debug option on dzn, the relevant parse tree element is shown,

    • A new --stress option was added to test completion in an automated and exhaustive way,

    • 126 new tests for lookup and completion were added.

Changes in 2.13.2 since 2.13.1

• Noteworthy bug fixes

  • The simulator would produce an invalid split-arrows trace for certain combinations of blocking and external (#34).

  • In the simulator, events on the input trail now determine when an external event is executed, i.e., taken out of the queue.

  • On the split-arrows trace, external q-in events are now hidden.

  • Six new regression-tests on the external feature where added along with fixes for the simulator.

  • The simulator's major performance bottle necks have been addressed (#36).

  • The simulator now prioritizes errors in the same order as verification does; a possible error trace is always shown.

  • On dzn simulate, the --queue-size parameter now works.

  • dzn explore:

    • A bug that left some states without a label has been fixed,

    • The "tau" label on tau-transitions has been removed,

    • Duplicate transitions due to non-determinism are merged.

Changes in 2.13.1 since 2.13.0

• Parser

  • The well-formedness check now reports an error when the ports of a binding have different types.

• Simulation

  • The 'dzn simulate' command now supports using --format="diagram" directly. It also supports the -i,--internal option from `dzn trace' for this.
  • In interactive mode, the `dzn simulate' command now uses GNU Readline.
  • When simulating interactively and an async ack is pending, show first observable action triggered by the async ack as eligible event.
  • In interactive mode, the simulator now prints the action where input is needed to resolve a non-deterministic choice.

• Noteworthy bug fixes

  • The C++ and C# runtime has an updated pump that fixes the collateral blocked release that was previously only handled during pump destruction (#23).

  • The C++ code generator now correctly sets async ranking for thread safe shells.

  • A bug in verification has been fixed that would sometimes cause invalid mCRL2 code, resulting in a backtrace.

  • A bug in verification has been fixed that would attempt to add missing void returns to valued functions.

  • The well-formedness check now reports two more cases of missing returns in a valued function: An else branch without return, and the empty function body.

  • In the simulator, the location of <q-out> events has been fixed.

  • In the simulator, a crash related to injected has been fixed in the default split-arrows trace output.

  • In the simulator, two bugs with respect to scoping function variables have been fixed.

  • The simulator now skips the (expensive) deadlock check when input is needed to resolve a non-deterministic choice.

  • A bug in the simulator's trace output has been fixed that caused some eligible event names to be prefixed with "sut." when simulating an interface.

  • The simulator now updates the provides ports right after flushing async.

  • The simulator now skips the deadlock check for illegal traces.

  • The simulator now shows complete split-arrows trace for deadlock errors.

  • The simulator now supports systems with dangling injected ports, which may happen when simulating a sub system that relies on an injected instance from an outer system.

  • A bug in the simulator was fixed where a trace needing input leading up to a non-deterministic choice would already include one of the possible choices at the end.

  • A bug in the simulator was fixed that generated duplicate traces.

  • The ASCII trace diagram now supports interface traces.

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.