Automatic Lights: A Complex System with One-Button Deployment

[karkob]

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

1. 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.

2. Combines Models with Hand-Written Code:

   • Demonstrates how to integrate Dezyne-generated models with custom logic written in C++.

3. Deployable Application:

   • The final result is a fully functional executable that triggers the model logic and is ready for further expansion.

4. 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.
• 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.
• Requirement Validation:
  • Built-in formal validation using Dezyne’s illegal states for safety-critical requirements.

---

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

1. Setup Prerequisites:
   • Install the required tools and configure paths in config.json.
2. Modify/extend/create new models
   • Add new components
   • Add new implementations (hand-written code)
3. Verify Models:
   • Verify single model using right-click context menu
   • Run the provided verification script to validate all .dzn files.
4. 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 ===

5. 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:

1. Prerequisites: Tools like Python, CMake, GCC/MinGW, and the Dezyne tool.
2. Scripts: Python, .sh, and .bat scripts for cross-platform verification and builds.
3. Step-by-Step Instructions:
   • How to verify .dzn models.
   • How to build and deploy the final executable.
4. Troubleshooting:
   • Solutions for common errors (e.g., compiler not found, missing Dezyne tool).
5. 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:

1. Using Foreign Components
2. 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!