Dezyne 2.13.2 Release

Announcements
1

With release 2.13 the previous simulator has been replaced with a new simulator function, which includes system scope validation, a major improvement. The system scope simulator provides more insight in the working of a system by combining multiple components and multiple interfaces. This is an important feature that is of support to the parties involved in the software engineering process: software engineer, test engineer, software architect and system engineer.

Dezyne-IDE

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.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 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 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 or 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).