A Complete Template for Professional Development in Verum Dezyne
Hello everyone!
If you’re new to Verum Dezyne and looking for a robust starting point, I’d like to share a complete Automatic High Beams Switching Example. This project serves as both a practical introduction to Dezyne and a reusable template for professional development.
Why This Example is Ideal for Beginners
-
All Tools and Scripts Included:
- The project comes with everything you need to verify, build, and execute Dezyne models.
- Cross-platform scripts for Windows and Linux are included.
-
Combines Models with Hand-Written Code:
- Demonstrates how to integrate Dezyne-generated models with custom logic written in C++.
-
Deployable Application:
- The final result is a fully functional executable that triggers the model logic and is ready for further expansion.
-
Professional-Grade Design:
- Modular and well-documented, making it easy to adapt to real-world scenarios.
Features
- Generate Executable Code:
- Generate C++ code from
.dzn
models using the included verification and build scripts.
- Generate C++ code from
- Hand-Written Code Integration:
- Learn how to extend and combine generated code with custom logic.
- State-Based Behavior:
- Implements a realistic Automatic High Beams Switching System, complete with:
- Sensor inputs (light and vehicle detection).
- Manual and automatic modes.
- Timer logic for smooth transitions.
- Implements a realistic Automatic High Beams Switching System, complete with:
- Requirement Validation:
- Built-in formal validation using Dezyne’s
illegal
states for safety-critical requirements.
- Built-in formal validation using Dezyne’s
How to Get Started
Clone the repository and follow the included User Guide for setup and usage:
-
Repository Link: AutomaticLightsExample on GitHub
-
Verum Dezyne latest release: Verum Dezyne on Verum.com
-
VS Code extension for graphical toolset: Verum Dezyne extension
(make sure to set dezyne directory in the extension settings)
Key Steps
- Setup Prerequisites:
- Install the required tools and configure paths in
config.json
.
- Install the required tools and configure paths in
- Modify/extend/create new models
- Add new components
- Add new implementations (hand-written code)
- Verify Models:
- Verify single model using right-click context menu
- Run the provided verification script to validate all
.dzn
files.
- Build the Project:
- Use the build script to compile the executable.
karol@karol:~/finished_projects/AutomaticLightsExample$ python3 build_script.py
Project Name: AutomaticLightsProject
Dezyne Path: /home/karol/dezyne-2.18.3
Runtime Path: /home/karol/dezyne-2.18.3/runtime/c++
=== Detecting Compiler Environment ===
Detected GCC environment.
=== Running CMake Configuration ===
-- CMake version: 3.28.3
-- System name:
-- CMake generator: Unix Makefiles
-- C compiler: /usr/bin/cc
-- C++ compiler: /usr/bin/c++
-- Parsed project name: AutomaticLightsProject
-- Parsed Dezyne runtime path: /home/karol/dezyne-2.18.3/runtime/c++
-- Dezyne tool path: /home/karol/dezyne-2.18.3/dzn
-- Project successfully configured!
-- Configuring done (0.0s)
-- Generating done (0.0s)
-- Build files have been written to: /home/karol/finished_projects/AutomaticLightsExample/build
=== Building Target: generate_dezyne_code ===
[ 7%] Generating /home/karol/finished_projects/AutomaticLightsExample/build/AutomaticLights.cc and /home/karol/finished_projects/AutomaticLightsExample/build/AutomaticLights.hh from /home/karol/finished_projects/AutomaticLightsExample/Models/AutomaticLights.dzn
[100%] Built target generate_dezyne_code
=== Re-running CMake Configuration with Generated Files ===
-- CMake version: 3.28.3
-- System name:
-- CMake generator: Unix Makefiles
-- C compiler: /usr/bin/cc
-- C++ compiler: /usr/bin/c++
-- Parsed project name: AutomaticLightsProject
-- Parsed Dezyne runtime path: /home/karol/dezyne-2.18.3/runtime/c++
-- Dezyne tool path: /home/karol/dezyne-2.18.3/dzn
-- Project successfully configured!
-- Configuring done (0.0s)
-- Generating done (0.0s)
-- Build files have been written to: /home/karol/finished_projects/AutomaticLightsExample/build
=== Building Target: all ===
[ 34%] Built target generate_dezyne_code
[ 48%] Built target DezyneRuntime
[ 51%] Building CXX object CMakeFiles/AutomaticLightsProject.dir/FrontCameraComponent.cc.o
[ 53%] Building CXX object CMakeFiles/AutomaticLightsProject.dir/main.cpp.o
[ 56%] Building CXX object CMakeFiles/AutomaticLightsProject.dir/AutomaticLights.cc.o
[ 58%] Linking CXX executable /home/karol/finished_projects/AutomaticLightsExample/AutomaticLightsProject
[100%] Built target AutomaticLightsProject
=== Build Completed Successfully ===
- Run the Application:
- Test and extend the generated system logic.
karol@karol:~/finished_projects/AutomaticLightsExample$ ./AutomaticLightsProject
Dezyne component successfully created.
<external>.module.Initialize -> AutoLightsSystem.modeSelector.module.Initialize
AutoLightsSystem.modeSelector.config.GetLightDelay -> AutoLightsSystem.config.api.GetLightDelay
AutoLightsSystem.modeSelector.config.Result:Ok <- AutoLightsSystem.config.api.Result:Ok
<external>.module.Result:Ok <- AutoLightsSystem.modeSelector.module.Result:Ok
Automatic Lights System Initialized.
AutoLightsSystem.modeSelector.<q> <- <external>.lightSensor.LowLight
AutoLightsSystem.modeSelector.lightSensor.LowLight <- AutoLightsSystem.modeSelector.<q>
AutoLightsSystem.modeSelector.lightsTimer.Create -> AutoLightsSystem.lightsTimer.api.Create
AutoLightsSystem.modeSelector.lightsTimer.return <- AutoLightsSystem.lightsTimer.api.return
AutoLightsSystem.modeSelector.<q> <- AutoLightsSystem.lightsTimer.api.Timeout
AutoLightsSystem.modeSelector.lightsTimer.Timeout <- AutoLightsSystem.modeSelector.<q>
AutoLightsSystem.modeSelector.highBeams.TurnOn -> <external>.relay.TurnOn
HighBeamsOn set to true.
AutoLightsSystem.modeSelector.highBeams.return <- <external>.relay.return
User Guide Highlights
The repository includes a detailed guide: README.md and ALGORITHM_EXPLANATION.md
. It covers:
- Prerequisites: Tools like Python, CMake, GCC/MinGW, and the Dezyne tool.
- Scripts: Python,
.sh
, and.bat
scripts for cross-platform verification and builds. - Step-by-Step Instructions:
- How to verify
.dzn
models. - How to build and deploy the final executable.
- How to verify
- Troubleshooting:
- Solutions for common errors (e.g., compiler not found, missing Dezyne tool).
- Algorith explanation:
- Review and purpose of system interfaces and components.
Overview
Below image is an example application of automatic light switching in the BMW.
This project includes a lights sensor that monitors ambient light conditions
Why Use This Example?
This template saves time by providing:
-
A working example to explore Dezyne’s capabilities.
-
All key functionalities and concepts needed for professional development
-
Initial integration of interfaces and foreing components
-
Tools to automate verification and builds.
-
A foundation to build professional-grade systems.
Whether you’re a beginner or an experienced developer, this project is a great way to start using Verum Dezyne for real-world applications.
Combining Dezyne Models with Hand-Written Code
When working with Verum Dezyne, integrating models with hand-written code is essential for building complete systems. There are two main approaches for this integration:
- Using Foreign Components
- Implementing Interfaces with Lambda Expressions
1. Using Foreign Components
Foreign components allow you to define the behavior of certain parts of your system in hand-written code while maintaining a formal contract with the Dezyne model.
Step 1: Declare the Foreign Component
Define the foreign component in the Dezyne model without specifying its behavior. For example:
component ConfigComponent {
provides IConfig api;
}
Step 2: Skeleton Declaration
The Dezyne tool generates a skeleton for the foreign component, which serves as a template for implementation. For example:
// Generated by dzn code
#include <dzn/runtime.hh>
#include "Config.hh"
namespace skel {
struct ConfigComponent: public dzn::component {
dzn::meta dzn_meta;
dzn::runtime& dzn_runtime;
dzn::locator const& dzn_locator;
::IConfig api;
ConfigComponent(dzn::locator const& locator);
virtual ~ConfigComponent();
private:
virtual ::Result api_GetLightDelay(int& ms) = 0;
};
}
Step 3: Implement the Foreign Component
Create a class that inherits from the generated skeleton and implement the required methods:
#pragma once
#include "ConfigSkel.hh"
struct ConfigComponent : skel::ConfigComponent {
public:
ConfigComponent(dzn::locator const& locator);
private:
::Result api_GetLightDelay(int& ms) override;
};
#include "ConfigComponent.hh"
ConfigComponent::ConfigComponent(dzn::locator const& locator) :
skel::ConfigComponent(locator)
{}
::Result ConfigComponent::api_GetLightDelay(int& ms) {
ms = 3000; // Set delay to 3000ms
return Result::Ok;
}
Step 4: Use the Foreign Component in the System
Finally, bind the foreign component in your system definition:
ModeSelector modeSelector;
ConfigComponent config;
2. Implementing Interfaces with Lambda Expressions
For simpler scenarios, interfaces in Dezyne can be implemented directly as lambda expressions in hand-written code. This approach is perfect for handling events, callbacks, or state changes.
Step 1: Declare the Interface in the System
Define the interface requirement in the Dezyne model:
requires IHighBeamsRelay relay;
system {
ModeSelector modeSelector;
modeSelector.highBeams <=> relay;
}
Step 2: Implement the Interface as a Lambda
In your hand-written code, provide the behavior for the interface using lambda expressions:
bool HighBeamsOn = false;
// Capture `HighBeamsOn` by reference in the lambda
autoLightsSystem->relay.in.TurnOn = [&HighBeamsOn]() {
HighBeamsOn = true;
std::cout << "HighBeamsOn set to true." << std::endl;
};
autoLightsSystem->relay.in.TurnOff = [&HighBeamsOn]() {
HighBeamsOn = false;
std::cout << "HighBeamsOn set to false." << std::endl;
};
This approach is concise and ideal for implementing simple, isolated logic.
When to Use Each Approach
-
Foreign Components:
- Best for complex logic or behavior requiring maintainability and reusability.
- Provides a strong contract between the model and the hand-written code.
-
Lambda Expressions:
- Best for simple behaviors, like events or quick responses.
- Reduces overhead for implementing small, isolated pieces of logic.
Further Reading
For a more in-depth explanation of these approaches, check out this excellent blog post: Fatal Dimensions Blog. It provides a detailed discussion on combining Dezyne models with hand-written code, including practical examples and advanced tips.
Feel free to ask questions or share your thoughts in the comments. Let’s learn together and build amazing systems with Verum Dezyne!