Verum Dezyne Release 2.19

[karkob]

Dezyne 2.19: Invariants, External Returns, and Practical Enhancements

The upcoming Dezyne 2.19 release introduces important language and tool updates.
The headline feature is invariants, allowing requirements to be expressed and formally verified directly in the model.
A second key enhancement is the ability to return external types directly from events and functions, greatly simplifying interface design.

Beyond these language changes, 2.19 also delivers tooling improvements in the dzn command set, code generation, and verification performance - making it easier to integrate Dezyne into larger projects and CI pipelines.

Invariants: Direct Requirements Traceability

Invariants make it possible to embed system requirements directly in your models. They rely on two new language features:

• Predicate functions: side-effect-free boolean functions.
• Boolean implication operator (=> ).

Example: Automatic Car High Beams

Consider the tutorial example of automatic high beams in the car. The system can operate in Manual (driver in control) or Automatic mode (computer in control). Interfaces such as beamsRelay, lightSensor, and frontCamera expose state variables.

Thanks to shared states feature, invariants can directly reference the state variables of ports, making it possible to express requirements as verifiable logical conditions inside the model.
As mentioned before, invariants can be an expression of actual requirements, so let’s first specify 3 requirements that must always hold true in our system:

1. No blinding in automatic mode
   If automatic mode is enabled, the system must never blind the driver in front.

2. Respect ambient light conditions
   In automatic mode, the system must not turn on high beams if ambient light is already sufficient.

3. Auto-switch from manual to automatic
   When the system is operational and in manual mode with low light, it should attempt to enter automatic mode.

Invariants can be used in the behavior of an interface or component. All invariants are evaluated before processing a trigger. In the the main component model, in behavior scope we can specify invariants statements as follows:

    behavior {
        enum ControlMode {Automatic, Manual};
        ControlMode mode = ControlMode.Manual;
        
        // Req1: If automatic mode is enabled system should never blind driver in front
        bool never_blind_driver_in_front () =
        mode.Automatic && frontCamera.state.Detected => !beamsRelay.isTurnedOn;
        invariant never_blind_driver_in_front ();

        // Req2: In automatic mode system should not turn on high beams if light conditions are high
        bool high_beams_off_if_light_high () =
        mode.Automatic && lightSensor.state.High && !timer.armed => !beamsRelay.isTurnedOn;
        invariant high_beams_off_if_light_high ();

        // Req3: When system is operational and in manual mode and light is low, system should try enter Automatic mode
        bool enter_automatic_when_light_low () =
        module.state.Operational && mode.Manual && lightSensor.state.Low => timer.armed;
        invariant enter_automatic_when_light_low ();

We express an invariant using the implication operator =>. In first invariant (never_blind_driver_in_front) we have:

mode.Automatic && frontCamera.state.Detected => !beamsRelay.isTurnedOn

This reads as:

If the system is in Automatic mode and the front camera detects a vehicle,
then beamsRelay.isTurnedOn must always be false.

During verification, Dezyne checks all possible scenarios. If any invariant can be violated, you’ll get a counterexample trace. This provides direct traceability of requirements without writing test cases, and ensures formally proven properties.

External Type Return Values

In earlier versions, external data types could not be used as return values for events and functions.
Instead, the user had to define an “empty container” and pass it by reference, which looked like this:

extern int $int$;

# interface trigger definition
in void GetLightDelay(out int ms);

# component usage
int delay;
config.GetLightDelay(delay);

As of Dezyne 2.19, external data types can now be returned directly.
This removes the awkward out-parameter pattern and makes the model much simpler:

extern int $int$;

# interface trigger definition
in int GetLightDelay();

# component usage
int delay = config.GetLightDelay();

On top of that, function calls can now be chained, enabling more expressive code:

# chaining into another call
portA.e(config.GetLightDelay());

# or chaining nested calls
portA.e(portB.f());

Other Updates in 2.19

Beyond the headline language changes, Dezyne 2.19 refines the toolchain with several quality-of-life improvements and fixes:

New and Enhanced Commands

• dzn exec — run any external command with arguments, often inside a Docker container with dzn as the entrypoint.
  Example:

dzn exec ltsconvert hello.aut hello.dot

This runs ltsconvert inside the container while automatically feeding it Dezyne’s preprocessed output .

• dzn hash — compute a SHA1 hash of a .dzn file and its imports for caching or verification.
  Equivalent to:

dzn parse --no-directives file.dzn | sha1sum

Useful in CI/CD pipelines to detect changes in models .

• dzn --version-number — prints only the numeric version (no extra text), making it easy to script and parse in automation contexts .
• dzn hello --runtime — in addition to the classic “hello”, this now shows the installed runtime location, helping to debug environment setup .

Parser Improvements

• dzn parse -D, --no-directives — parse models while stripping preprocessor directives, removing the need for clunky grep -v ^# workarounds .

Code Generation

• Dependency files for C++ — .deps/<file>.dzn.dep are generated so build systems can track model changes automatically .
• Multiple files & directories — dzn code now accepts a list or whole directories of .dzn files, simplifying project-wide generation.
• --touch-empty-files — ensures even empty execution units get created as files, avoiding build irregularities .
• Better error handling — using --shell=model with a missing or invalid model now cleanly fails instead of silently continuing .

Verification

• Parallel verification — --threads=N forwards directly to mCRL2’s lps2lts backend, making verification of large models significantly faster on modern multicore CPUs .
• Smarter batch verification — when verifying multiple files or directories, imported models are automatically skipped to avoid duplicate runs.

Noteworthy Bug Fixes

• Fixed trivial deadlocks in dzn graph outputs for state diagrams in external/collateral blocking contexts.
• dzn verify now respects --model=MODEL even when verifying an interface, improving precision.

Stay Tuned!