Dezyne Tutorial

Table of Contents

Version 16

16 December 2016

Dezyne Version 2.1.1, 2016-09-19 09:10

Next:   [Contents]

Dezyne Tutorial


Next: , Previous: , Up: Top   [Contents]

1 Introduction

This tutorial assumes that you have developed control software in C, C++, C# and/or Java. Most likely you have worked hands-on with finite state machines in some form or other, maybe with Harel state machines or UML statecharts. You’ve seen that deeply nested if-then-else control logic leads to debugging nightmares – every fix seems to break something else. You’ve experienced unhandled events, race conditions, deadlocks and live-locks, some of which are not reproducible. You know about state machine determinism and non-overlapping guards.

The tutorial also assumes that you already generally understand the benefits Dezyne brings to developing control software – see the next paragraph – and that you now want to create something realistic with it, gaining fluency with its domain-specific language and its techniques.

Benefits summary: Dezyne enables you to methodically and efficiently divide complex control problems into verified problem-free components and interfaces that you re-compose into reliable, trustworthy systems. Verified Dezyne models have no unhandled events, problematic race conditions, deadlocks or live-locks in their core state-management and communications “skeleton” logic. Source code that Dezyne auto-generates from models will be free of these same problems. For more information about Dezyne’s benefits, see the materials on the Verum’s Dezyne website or contact Verum.

Dezyne runs on all common platforms. Dezyne Models are expressed in a simple, immediately familiar C/Java-like language.


Next: , Previous: , Up: Top   [Contents]

2 Dezyne Basics

The tutorial guides you step-by-small-step, with explanations, through building and verifying a model of a single-threaded burglar-alarm system, in the Dezyne-IDE. The model is built with hierarchical components that communicate through events. You should already understand these concepts, and you need to be able to run the Dezyne-IDE see the Dezyne IDE Manual.

Tutorial goals in decreasing order of priority are 1) efficiency of learning, 2) rigor, and 3) completeness. You should go through the tutorial from beginning to end: later sections depend on earlier ones.

We will build the system from the bottom up, first as the simplest possible useful system, ultimately as a realistic system with complex behaviours. Along the way, we will always ensure our work-in-progress components and subsystems have no inherent logical errors in their states and communications.

Also along the way, we will automatically generate C++ source code that implements the verified logic, and at the end we’ll automatically generate audit-ready state tables, state charts, sequence diagrams and architectural system diagrams. Then we’ll look back and consider the obstacles that could arise when we need to extend or refactor the system – not many, it turns out.


Next: , Up: Dezyne Basics   [Contents]

2.1 Dezyne Hello World: Turning an LED On and Off

Language keywords: behaviour component import in interface on provides void

In this section we build a near-minimal Dezyne model in which one component presents one interface.

The simplest possible valid Dezyne model consists of one component that presents no interface to its outside environment.

Step 1. Create a new Dezyne model by entering or copy-pasting the below two lines of model code into a new file in your Dezyne editor.

component LED {
}

You can copy and paste any code sample in this tutorial directly into the Dezyne editor. Most Dezyne language keywords are displayed like this in the Dezyne editor and in the tutorial code samples; a few special keywords including “enum” are colored blue. You can position curly-brackets exactly as in C/C++/Java: at the end of the line, on the next line, and so forth.

Step 2. Verify this model (in Dezyne-IDE: the double-arrow green toolbar icon images/verify_icon.75).

Dezyne will respond that no component in the model has behaviour, therefore there’s nothing yet to verify.

Step 3. Add a mininum behaviour block as below. In each code sample, added or changed lines of code from the previous sample will be highlighted like this.

component LED {
  behaviour {
  }
}

In Dezyne-IDE a small red symbol appears, indicating invalid syntax and/or semantics; moving the cursor over the symbol brings up the below information.

images/multiple_markers

A well-formed, verifiable Dezyne component presents (provides) at least one defined interface to its environment, and at least one of its presented/provided interfaces has to define one or more trigger events accessible from outside as callable functions.

Step 4. Remove the behaviour {} block from the component for now. We will add it back later.

Step 5. Enter or copy-paste the new code in the below model into the Dezyne editor. This code defines a simple interface through which a caller can turn on and turn off an LED through synchronous void function calls to the providing component. The component provides (implements) this interface. Note that commenting in Dezyne works exactly as in C/C++/C#/Java.

interface ILED {
  in void turnOn();
  in void turnOff();

  behaviour {
    on turnOn: {}
    on turnOff: {}
  }
}

component LED {
  provides ILED iLed; // removed the component's behaviour block for now
}

Step 6. Verify your copy of the above model code (images/verify_icon.75) and study the following paragraphs.

The LED component is now well-formed: it has instanced a defined interface, ILED, and we have verified that it and its interface have no bugs or other problems.

An instanced interface is known as a “port” in Dezyne; each port must have a unique name (here “iLed”) within the providing component. The term “port” is not a keyword in the Dezyne modeling language.

You may have noticed that keywords and user-defined names in Dezyne are case-sensitive. You will need to select your own conventions for naming things; in this tutorial we prefix each interface name with a capital “I” and each instance of an interface with a lower-case “i”. Dezyne requires that user-defined names contain only letters, digits and the underscore character ‘_’, and that the leading character in a name is not a digit.

In the above, by not defining any behaviour inside the component, we are asserting that the outside world needs to know only that the component supports void functions named “turnOn” and “turnOff”, and that the component will quietly and correctly do its work whenever triggered by an input event, i.e., whenever one of the functions is called. This behaviourless feature turns out to be important in practice: you can use it for placeholder model components for which you will write all C/C++ source code manually, and for which you will not use automatically-generated C/C++ source coming out of the Dezyne model. For example, you might write hardware or communications abstraction components manually. In Dezyne, a component with no defined behaviour is sometimes called “hand-written”.

To “verify” in Dezyne means to trace every possible execution sequence through a component model, and to stop and report the first occurrence of a problem – either a mismatch between a providing component’s actual functional behaviour versus its contracted functional behaviour, or a non-deterministic behaviour such as an overlapping guard or unmanaged race condition, or an unhandled event, or some other issue. If no problem is found, then the model has been verified. In the Dezyne-IDE editor, if a verification problem was found, then it is reported as the entire sequence of trace steps that led to it.

Note that, by definition, a verified interface’s externally visible functional behaviour exactly matches a verified providing component’s externally visible functional behaviour for that interface. Verification proceeds through exhaustive stimulus-response of a component’s provided functions, using the applicable interface definition to decide if the providing component’s responses are complete and correct. A providing component, however, can also optionally contain additional non-visible internal behaviour that extends and refines its responses to events. And a given interface can have any number of providing components in a Dezyne project. We will revisit these matters later.

Step 7. Create a new file named “ILED.dzn”, move the ILED interface code into it, and delete the ILED interface code from the model. Add a new import line to your original file as follows:

import ILED.dzn;

component LED {
  provides ILED iLed; // removed the component's behaviour block for now
}

You can import any number of files in any order into a Dezyne file. All imports must precede other non-comment/non-whitespace contents in the file.

Step 8. Enter or copy-paste the component behaviour as shown in the code sample below. Observe the parentheses () in the component’s added code, which differ from the parallel declarations in the interface definition, and remember that if a component defines behaviour for a called function, that behaviour must exactly match the interface’s defined behaviour as seen through function calls and only in that sense. In practice, you would replicate the exact interface behaviour in the component only if you plan to refine and extend the component’s own internal management in response to events. Notice also that the component’s function names are qualified with the port name, i.e. the interface instance’s name.

import ILED.dzn;

component LED {
  provides ILED iLed; /* "provides" means implements ILED functions */

  behaviour {
    on iLed.turnOn(): {} // qualify funcs w/interface *instance* (port) name
    on iLed.turnOff(): {}
  }
}

Step 9. Verify the model. Then, simulate interface ILED and component LED via the Dezyne-IDE toolbar icon images/simulate_icon.75, which initiates traces with events. Be sure the Dezyne-IDE Sequence View is on (menu Window / Show View / Sequence View) as well as the Trace View and Watch View.

Step 10. Experiment with the Sequence Diagram view: select Next Events (“eligible events”) one by one to build up a trace, then click on transitions in the diagram and see how the corresponding code is automatically highlighted. In the below Dezyne-IDE screen shot, the turnOff call was clicked in the diagram, highlighting its source to the left:

images/eclipse_1.75

The above screen shot shows the Dezyne console output. Every verification and simulation step executes through the console command-line interface to access the Dezyne server. Enter “dzn –h” at the command prompt at the bottom for a summary of the commands.

Look also at the Verify Results tab contents, shown below, to see the categories of model verification. You can search the Dezyne help at http://dezyne.verum.com/info-center/ for details about these.

images/verify_results.75

Notice the differences between verifying versus simulating. Simulation enables interactive exploration and explanation of the detailed interface protocol – a powerful way of communicating to other people about how an interface and its implementing component(s) function.

Step 11. You can generate this component’s C or C++ source code via Dezyne-IDE’s toolbar icon images/code_icon.75 and view it. A later chapter will discuss generated source code and how to integrate with it.

The generated source as seen in the sandbox comprises 100 to 200 lines of compilable code not counting whitespace, comments, or lines consisting of only a curly-bracket. Most of the source for this small example is generic to any Dezyne-generated code. In practice, you would rarely change automatically generated code; instead, you would modify only code that supports it or interacts with it. In this way you guarantee not introducing subtle bugs into your system, and you greatly simplify matters when refactoring or adding new features later.

That’s all! We’ve created and verified our first system model. Well, not quite, only our first verifiable and verified component model and its source code. Next we’ll build our first system.

Before moving on, consider the following. In the model so far, we could have used just one function that toggles the light on and off. Why didn’t we? In this case, because we want users/callers of the LED controller to know what the light’s state is – on or off – after sending a control command to the light. If the only control was a toggle, then even in a single-threaded system a caller would have to manage initialization and perhaps poll to know the light’s current state for sure. In a multi-threaded system the light could receive a toggle from anyone any time, and polling would likely be essential. In later sections we’ll return to these and other related matters.

The Efficiency of Code-Like Dezyne Models for States and Communications Logic

In Dezyne, you define components and their interfaces through a familiar and compact C/Java-like language, then automatically verify the completeness and syntactical correctness of your logic, and then exercise sequence diagrams to check that the coded behaviour is what you intended.

Contrast this with going in the opposite direction: you’d whiteboard a sequence diagram or draw it in a graphics editor, converge on the behaviour you seek, write the code, compile and link it, and then try to test the code to ensure it’s working properly. With Dezyne, you direct the machine to test your logic and generate interactive visualizations of the behaviour.

The Dezyne approach, once mastered, is dramatically more efficient, and that efficiency translates to dramatic savings across entire projects - and with no subtle logical bugs, such as race conditions or deadlocks or livelocks, in states-and-communications logic


Next: , Previous: , Up: Dezyne Basics   [Contents]

2.2 Simplest Usable Dezyne System Model

Language keywords: requires system

Operator: <=>

We first extend the LED model by adding a switch component that switches the LED on and off. The switch requires the ILED interface in order to call the LED component and change the light’s state. Again, commenting and whitespace in Dezyne work the same as in C/C++/C#/Java.

Step 1. Enter or copy-paste the new Switch component into the complete ILED-LED model, as shown in the below code sample. You can either import the ILED interface .dzn file or include the ILED code as here, but if you import then the import statement must precede all other statements.

component Switch {
  requires ILED iLed; // "requires" means calls ILED “in” functions
}

interface ILED {
  in void turnOn();
  in void turnOff();

  behaviour {
    on turnOn: {}
    on turnOff: {}
  }
}

component LED {
  provides ILED iLed; /* "provides" means implements ILED functions */

  behaviour {
    on iLed.turnOn(): {}
    on iLed.turnOff(): {}
  }
}

You can declare components and interfaces in any order in a Dezyne model. In the above, the Switch component requires the ILED interface but the Switch component definition precedes the interface definition.

Step 2. Verify the above code. Notice that the Switch component does not show up in the list of verifiable items – because it defines no behaviour. Nothing has really changed in this Dezyne model; we’ve only added a hand-written Switch component that we intend to connect to the LED.

Step 3. “Wire” the two components into a system as shown in the below diagram and model code. A Dezyne “system” is a component that instances other components and connects their interfaces. Wiring amounts to binding each requires interface instance (port) to a corresponding provides instance (port) for the same interface, via the Dezyne <=> operator.

images/system_1
component LEDSwitchSystem {

  system {
    LED led;
    Switch switch;
    switch.iLed <=> led.iLed;
  }
}

component Switch {
  requires ILED iLed; // "requires" means calls ILED functions
}

interface ILED {
  in void turnOn();
  in void turnOff();

  behaviour {
    on turnOn: {}
    on turnOff: {}
  }
}

component LED {
  provides ILED iLed; /* "provides" means implements ILED functions */

  behaviour {
    on iLed.turnOn(): {}
    on iLed.turnOff(): {}
  }
}

Step 4. Study the following important points one by one. They are essential to your understanding.

Step 5. Bring up the System View (in Dezyne-IDE, menu Window / Show View / System View) to display the wired system as shown below. Clicking the top-left button next to the string “LEDSwitchSystem” displays or suppresses the system internal structure, as shown below. Clicking the “wire” between the Switch and LED highlights the line of model source code that binds these two ports together.

images/system_2.75

In Dezyne-generated system/subsystem diagrams like the above, the “wires” – i.e., the requires-provides connections – are drawn top down, as the blue/black arrowheads indicate. In this simple system, the LED provides the interface for the Switch to set the light state to on or off. Later we will build composite subsystems in which “wires” are actually “buses” in the electronics sense, carrying multiple connections going top-down, or equivalently outside-in, among system components. Ultimately every chain of arrows terminates in a leaf component that provides an interface.

Step 6. View the component’s State Chart, shown below (Window / Show View / State Chart View). Though you have not yet defined any state behaviour, Dezyne still tracks state as it perceives it. This component never leaves its initial state. The next section discusses state management.

images/state_1
Dezyne Diagrams and Traces Both Validate and Document a System

Consider the value of the system diagram, the sequence diagram and the event trace. Together they validate the core system as modeled. They can serve as specifications and documentation for whoever will integrate and test the Dezyne-generated source code in the whole hardware and software system.


Next: , Previous: , Up: Dezyne Basics   [Contents]

2.3 Defining and Managing Component States

Language keywords and constructs: enum illegal reply

Operators and constructs: = == [].


Next: , Up: Defining and Managing Component States   [Contents]

2.3.1 Handling States Event-by-Event: “Event-Leading”

In this section we start tracking the LED component’s on/off state. This anticipates extending or refining state behaviour inside the component, while keeping the component’s externally visible behaviour exactly the same as its provided interface or interfaces.

Step 1. Enter or copy-paste the following new state-management code in the Dezyne editor. You can continue with the system design from the previous section, or restart with only the below code.

import ILED.dzn;

component LED {
  provides ILED iLed;

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    on iLed.turnOn(): { state = State.On; }
    on iLed.turnOff(): { state = State.Off; }
  }
}

In the above component’s code, the enum line declares an enumeration type as in C/C++/Java. “Off” and “On” are unique enum values for this particular enumeration type, not strings. “State” is a case-sensitive user-defined name for the enumeration type.

The next line after the enum declaration defines a variable named “state” of type State and initializes the setting to “Off”. By convention in this tutorial we will always list the default state first when declaring an enum. Two important but non-obvious points:

Each handler line (on event) in the component’s behaviour block is followed either by one statement that ends in a semicolon, or by curly braces {} that contain zero (no-op) or one or more statements.

Step 2. View the component’s State Chart, shown below (you might have to refresh/update views first using the images/update_icon.75 icon in Dezyne-IDE, next to the verify images/verify_icon.75 icon)

images/state_2

Next: , Previous: , Up: Defining and Managing Component States   [Contents]

2.3.2 Interface States versus Component States

You can track states in an interface exactly as you can in a component. When defined in an interface, state declarations differ from the component’s only by 1) having no interface-instance prefix, and 2) having no parentheses. Here are the same states as above, but defined instead in the interface:

interface ILED {
  in void turnOn();
  in void turnOff();

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    on turnOn: { state = State.On; }
    on turnOff: { state = State.Off; }
  }
}

It is important to understand that there are at least two occasions when one might choose to declare and manage state-related enumerations in an interface:

If you define states in both an interface and in a providing component for that interface, Dezyne verification will ignore the interface’s declared states and only compare the component’s function return values with the interface’s specified function return values.

There is no direct connection between states defined in an interface’s behavioural specification and states defined in a providing component’s implemented behaviour. All that matters is that every stimulus applied to a component-implemented interface function returns a response type that matches the interface’s declared response type, i.e. that every trace through the interface matches every trace through the implementing component for events related to just this interface. For example, we will see later that a model function can be defined to return an integer within a fixed range; verification will find any case of a return outside this range, and will display, in the Trace View window, the exact sequence of steps that led to the mismatch.

Debugging a Model: Interface specification versus Implementation

Dezyne verification examines all possible sequences of execution through a provided interface. Verification finds each mismatch between implementation and specification – e.g., return types, missing events, output events, etc – and displays the entire trace of events that led to the mismatch. Thus, you can quickly and inexpensively fix buried logical errors like race conditions and deadlocks even before any source code is generated or written.


Next: , Previous: , Up: Defining and Managing Component States   [Contents]

2.3.3 Handling Events State-by-State: “State-Leading”

The component behaviour as written so far handles state changes event-by-event. It unconditionally turns the light off when directed, whether the light was on or not, and turns it on when directed.

You can invert behavioural logic to handle events state-by-state. The Dezyne language supports if-then-else but not at the first logical level within a state’s behaviour block – we’ll see this in a later section.

Top-level logic inside a behaviour block can only be one of these three different kinds:

Step 1. Enter or copy-paste the below code into your ILED-LED design and verify it.

import ILED.dzn;

component LED {
  provides ILED iLed;

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    [state == State.Off] {
      on iLed.turnOn(): { state = State.On; }
      on iLed.turnOff(): {}
    }
    [state == State.On] {
      on iLed.turnOn(): {}
      on iLed.turnOff(): { state = State.Off; }
    }
  }
}

Important rule: The Dezyne verification “compliance” check tests that a component’s behaviour with respect to a given interface handles all possible events associated with that interface. If you handle events purely state-by-state as in the above example, then for component compliance and for zero ambiguity you must explicitly handle every on-event inside each state-oriented guard block (there is one exception to this rule involving “illegal” situations, which is explained later.).

Step 2. Comment out line “on iLed.turnOff(): {}” in the above code and re-verify. You will get a compliance error even though you’ve seemingly changed nothing in the component’s visible behaviour. This error can be reported fully only via the Trace and Sequence Views:

images/verification_error_1.75

The user interface’s Console output for the above verification is shown below; the series of events that arrived at the compliance error precede the Exit Code line.

dzn$ dzn –session=22 -v verify –model=LED Intro\LED-State-Leading.dzn
..
verify: ILED: check: completeness: ok
verify: ILED: check: deadlock: ok
verify: ILED: check: livelock: ok
verify: LED: check: deterministic: ok
verify: LED: check: illegal: ok
verify: LED: check: deadlock: ok
verify: LED: check: livelock: ok
Intro/LED-State-Leading.dzn:14:5:i19: iLed.turnOn not handled
verify: LED: check: compliance: fail
iLed.turnOn
iLed.return
iLed.turnOn
Exit Code: 1
dzn$

The Dezyne “==” comparison operator works as in C/C++/C#/Java. Each [] guard must be followed by either a single statement or a curly-bracket block {} with or without statements in it; you can always remove curly brackets where they contain exactly one statement. You can optionally further abbreviate the guard equality test for states whenever there would be no ambiguity, as shown below. We will abbreviate these ways from here on wherever possible.

Step 3. Modify and verify your design using shorthand guard statements and event handler logic as shown below.

import ILED.dzn;

component LED {
  provides ILED iLed;

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    [state.Off] {
      on iLed.turnOn(): state = State.On;
      on iLed.turnOff(): {}
    }
    [state.On] {
      on iLed.turnOn(): {}
      on iLed.turnOff(): state = State.Off;
    }
  }
}

From this point on we will leave out the Step-by-Step cues and instead sometimes suggest Exercises to try out on your own before copy-pasting code into the editor. No matter how you proceed, you must always run verification on your edits!


Next: , Previous: , Up: Defining and Managing Component States   [Contents]

2.3.4 Polling for State

Sometimes a component that sets another component’s state needs to poll (query) for the current state. The below shows how to enable polling through a “getter” function.

In order to support and verify the getState reply below, we have to declare the state enumeration publicly in the interface definition, reference the interface enumeration in the component (not declare it), and replicate at least some of the component’s state behaviour in the interface behaviour.

The interface code below uses the event-first pattern to define its internal behaviour. The rule is, as before, that all states or guards must be handled by the defined behaviour. The getState handler below does the same thing in every state, thus it does not use [] boolean checks.

Exercise: simplify the below interface’s code so that none of the on-event handlers tests the state, instead each on-event handler does the same thing in all states. Answers are at the end of this section.

interface ILED {
  enum State { Off, On };
  in void turnOn();
  in void turnOff();
  in State getState();

  behaviour {
    State state = State.Off;
    on turnOn: {
      [state.Off] state = State.On;
      [state.On] {}
    }
    on turnOff: {
      [state.Off] {}
      [state.On] state = State.Off;
    }
    on getState: { reply(state); }
  }
}

component LED {
  provides ILED iLed;

  behaviour {
    ILED.State state = ILED.State.Off;
    [state.Off] {
      on iLed.turnOn(): state = ILED.State.On;
      on iLed.turnOff(): {}
      on iLed.getState(): reply(state);
    }
    [state.On] {
      on iLed.turnOn(): {}
      on iLed.turnOff(): state = ILED.State.Off;
      on iLed.getState(): reply(state);
    }
  }
}

As noted earlier and shown here again, for state-leading-only logic, every input event (“in” function) must be handled either explicitly or implicitly inside every [state] block, else your model will have unhandled-event verification errors (compliance).

Exercise answers – the first one mixes event-leading and state-leading logic:

component LED {
  provides ILED iLed;

  behaviour {
    ILED.State state = ILED.State.Off;
    // mix event-leading and state-leading
    on iLed.getState(): reply(state);
    [state.Off] {
      on iLed.turnOn(): state = ILED.State.On;
      on iLed.turnOff(): {}
    }
    [state.On] {
      on iLed.turnOn(): {}
      on iLed.turnOff(): state = ILED.State.Off;
    }
  }
}

Exercise second answer, with minimal logic:

component LED {
  provides ILED iLed;

  behaviour {
    ILED.State state = ILED.State.Off;
    // minimal model of equivalent logic
    on iLed.turnOn(): state = ILED.State.On;
    on iLed.turnOff(): state = ILED.State.Off;
    on iLed.getState(): reply(state);
  }
}

Previous: , Up: Defining and Managing Component States   [Contents]

2.3.5 States and Illegal Events: Asserts

Suppose that the LED component insists that callers track its state and never call function turnOn() when the light is already on. Our simple example wouldn’t suffer from such a call, but a wrong call in a life-critical medical device could be devastating. Dezyne’s illegal keyword expresses the concept of, “if execution reaches this line then there is a crucial defect somewhere in your logic”. An interface and its providing component must express exactly the same legal and illegal behaviour as seen by a caller. Dezyne-generated source code resolves each illegal as an assert() statement or equivalent.

interface ILED {
  in void turnOn();
  in void turnOff();

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    on turnOn: {
      [state.Off] state = State.On;
      [state.On] illegal;
    }
    on turnOff: {
      [state.On] state = State.Off;
      [state.Off] illegal;
    }
  }
}

component LED {
  provides ILED iLed;

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    [state.Off] {
      on iLed.turnOn(): state = State.On;
      on iLed.turnOff(): illegal;
    }
    [state.On] {
      on iLed.turnOn(): illegal;
      on iLed.turnOff(): state = State.Off;
    }
  }
}

In your model code, mismatches between an interface and its provider that involve illegal will show up as verification errors, but only the Trace and Sequence views can point out the exact problem. Once any such mismatches are resolved, simulation in the Dezyne-IDE editor will not allow an illegal call to be initiated as an event – such a call will not be “eligible” in Dezyne’s terminology.

As mentioned earlier, when using state-leading logic, there is one exception to the rule that each event must be declared and handled explicitly in each state in a providing component’s behaviour implementation. If a particular event is illegal in a particular state, you are allowed to omit that declaration in the component’s behaviour; Dezyne will assume that this is an illegal and will check the interface specification for confirmation. The generated code will have an assert in the same spot where the explicit declaration would have placed it. To see this exception in action, comment out one of the component’s illegals as shown below and re-verify:

component LED {
  provides ILED iLed;

  behaviour {
    enum State { Off, On };
    State state = State.Off;
    [state.Off] {
      on iLed.turnOn(): state = State.On;
      // on iLed.turnOff(): illegal;
    }
    [state.On] {
      on iLed.turnOn(): illegal;
      on iLed.turnOff(): state = State.Off;
    }
  }
}

Uncluttering code by making use of implicit illegals has the downside of hiding logic from a code reviewer.


Next: , Previous: , Up: Dezyne Basics   [Contents]

2.4 Time and Timers: Making an LED Blink

Language keywords: bool extern false inevitable out true

Operator: !

Dezyne’s logical models have no inherent concept of time; instead, Dezyne only knows sequences of events and responses to events. Model verification proceeds by examining, directly or indirectly, every possible eligible-event-initiated trace path through the component and/or interface(s) being verified. Each step in an underway verification trace represents zero elapsed time in the modeled system (and takes very little computation time during verification). Any verification trace stops immediately upon finding an error, thus running to completion signals that no logic-related errors were found in the model.

Dezyne can model and verify repeating behaviour. We’ll build a timer interface that makes our LED blink on and off at constant time intervals, and that works as-is in auto-generated C++ source code. The entirely new – but nearly all familiar – code below defines a simple timer interface and a hand-written component that will implement the interface. An out function names an event that a requiring (calling) component has to handle in its behaviour.

interface ITimer {
  enum State { Idle, Running };
  in void start();
  in void cancel();
  out void timeout();

  behaviour {
    State state = State.Idle;
    [state.Idle] {
      on start: state = State.Running;
      on cancel: {}
    }
    [state.Running] {
      on start: illegal;
      on cancel: state = State.Idle;
      on inevitable: { // ALWAYS happens eventually unless cancelled first
        state = State.Idle;
        timeout;
      }
    }
  }
}

component Timer {
  provides ITimer iTimer;
}

Dezyne inevitable keyword indicates that the timeout event will always eventually happen during model verification, to test all possible execution paths, including the possibility of a timeout just before a cancel call arrives. The inevitable keyword has a companion we’ll discuss later, optional, which means “usually happens but might never happen”; both these keywords are used only in interfaces, to inform verification about certain special conditions it must check.

Note in the above the asymmetry between the Idle state and the Running state. The interface says it’s OK to cancel when the timer is idle, but it’s illegal to try to start when the timer is running. We assume the caller will manage its own state with respect to use of the timer.

The next version of the timer shows how to pass a parameter of a particular type to a model method.

interface ITimer {
  extern long_integer $long$; // source code data type will be long
  in void start(long_integer milliseconds);
  in void cancel();
  out void timeout();

  behaviour {
    enum State { Idle, Running };
    State state = State.Idle;
    [state.Idle] {
      on start: state = State.Running;
      on cancel: {}
    }
    [state.Running] {
      on start: illegal;
      on cancel: state = State.Idle;
      on inevitable: { // ALWAYS happens eventually unless cancelled first
        state = State.Idle;
        timeout;
      }
    }
  }
}

component Timer {
  provides ITimer iTimer;
}

The extern keyword above maps a model data type to an indicated data type in Dezyne-generated source, via string substitution. For example, the above sample leads to this line in generated C++ code:

std::function<void (long milliseconds)> start;

Now we integrate the timer into the LED controller. The interface definition below is complete; it uses the events-leading pattern.

interface ILED {
  in void shine();
  in void darken();
  in void blink();

  behaviour {
    enum State { Dark, Shining, Blinking };
    State state = State.Dark;
    on shine: { state = State.Shining; }
    on blink: { state = State.Blinking; }
    on darken: { state = State.Dark; }
  }
}

This interface allows a caller to reset the LED to the same state it’s already in. Below is a partial implementation of the blinkable LED component, sketching in a states-leading approach. You can create this exact component in Dezyne (though it might need a different name) and verify that it conforms to both the ILED interface and the ITimer interface, even though the interface expresses its logic in event-leading format. Also, in this component we will track the LED’s lit/dark state as part of managing the blinking state; as with state variables we have to initialize any boolean variable in its declaration.

component LED {
  provides ILED iLed;
  requires ITimer iTimer;

  behaviour {
    enum State { Dark, Shining, Blinking };
    State state = State.Dark;
    bool lit = false;
    [state.Dark] {
      on iLed.shine(): {}
      on iLed.darken(): {}
      on iLed.blink(): {}
      on iTimer.timeout(): {}
    }
    [state.Shining] {
      on iLed.shine(): {}
      on iLed.darken(): {}
      on iLed.blink(): {}
      on iTimer.timeout(): {}
    }
    [state.Blinking] {
      on iLed.shine(): {}
      on iLed.darken(): {}
      on iLed.blink(): {}
      on iTimer.timeout(): {}
    }
  }
}

In the above, we have added a new bool variable named “lit” to track the shining-darkened state changes when the LED is blinking. The light is off by default, hence variable lit is initialized to false. Booleans work in Dezyne as they do in C/C++/Java, including the negation operator !.

Filling in the event handlers for the initially dark LED:

  [state.Dark] {
    on iLed.shine(): { // -> Shining, lit
      state = State.Shining;
      lit = true;
    }
    on iLed.darken(): {} // ignore
    on iLed.blink(): { // -> Blinking, half-second timer
      lit = false;
      state = State.Blinking;
      iTimer.start($500$);
    }
    on iTimer.timeout(): {} // shouldn't occur, just ignore
  }

The Shining state event handlers are essentially the same as for Dark. Blinking state handlers are below. When Blinking, on each timer timeout the light switches between off and on and restarts the timer.

  [state.Blinking] {
    on iLed.shine(): {
      iTimer.cancel();
      state = State.Shining;
    }
    on iLed.darken(): {
      iTimer.cancel();
      state = State.Dark;
    }
    on iLed.blink(): {}
    on iTimer.timeout(): {
      lit = !lit;
      iTimer.start($500$);
    }
  }

You can use if else instead of the negation operator when handling the timeout, as below. In Dezyne, the if-else construct can appear only within on-event behaviour.

  [state.Blinking] {
    on iLed.shine(): {
      iTimer.cancel();
      state = State.Shining;
    }
    on iLed.darken(): {
      iTimer.cancel();
      state = State.Dark;
    }
    on iLed.blink(): {}
    on iTimer.timeout(): {
      if (lit) { lit = false; } else { lit = true; }
      iTimer.start($500$);
    }
  }

As an exercise you should complete the [state.Shining] event handlers, then verify and simulate.

Here is a screen shot showing some of the source and all of the Trace, Sequence and State Chart views for the completed, verified and simulated blink-able LED (the Shining event handlers are visible in it).

images/eclipse_2.75

Challenge: The above model verifies completely and it simulates with no logic errors (by definition). But it has a functional bug related to exiting the Blinking state. Can you spot it?

Hint: observe the state variable “lit” in the Watch View window when you simulate. The answer is below the sidebar.

Simulation Can Genrate Trace Inputs for Automated Regression Tests

Observe that the Trace window contains the entire trace history to date after Dezyne processes each new simulation event. When you’re debugging a complex model, your automated test framework can save an arbitrarily long returned trace history to use as a regression tesst after a bug has been fixed.

Answer to the challenge: When exiting the Blinking state you must set the “lit” variable to the indicated new state, else the state variable might not match the actual on/off state of the LED. Which brings up an essential point: The first functional test of generated code from this model using an actual LED would probably reveal the state-tracking bug within minutes. You could then go directly to the Blinking state code in the model, insert the new assigments, regenerate the source, compile, and link – and the bug would be gone. Dezyne verifies your logic and helps you quickly validate your implemented system.


Next: , Previous: , Up: Dezyne Basics   [Contents]

2.5 Possible Events: Multiplexing Sensor Inputs

Language keyword: optional

Earlier we worked with a timer, which generates an event after a specified duration unless cancelled first. Another kind of time-related event is sensor activation. An enabled sensor might signal almost immediately, or it might never signal at all. Some control systems that use sensors have to account for events that might never occur; for example, a passcode-entry component should eventually time out and reset if a user starts keying in a passcode but never finishes and never cancels.

The alarm system we’ll build later uses multiple kinds of passive sensors, i.e., sensors that do not poll but instead only respond to stimuli. In this section we address optional events – ones that might never happen – and how to multiplex identical or similar components that provide the same defined interface.

Below is a sensor interface. When the sensor is on (enabled, sensing), at some point in the future it might trigger an event, or it might never trigger an event. The interface expects a caller to be aware of the sensor state and not call wrongly (illegal). The new keyword optional is highlighted. Note that keywords inevitable and optional occur only in interface behaviour, never in component behaviour, and that the illegal declarations are all necessary, this being an interface and not a component.

interface ISensor {
  in void turnOn();
  in void turnOff();
  out void triggered();

  behaviour {
    enum State { Off, Sensing, Triggered };
    State state = State.Off;
    [state.Off] {
      on turnOn: state = State.Sensing;
      on turnOff: illegal; // tests caller's logic
    }
    [state.Sensing] {
      on turnOn: illegal;
      on turnOff: state = State.Off;
      on optional: { // could trigger soon but might never triggered;
        state = State.Triggered;
      }
    }
    [state.Triggered] {
      on turnOn: illegal;
      on turnOff: state = State.Off;
    }
  }
}

These two components provide the same iSensor interface.

component HallEffectSensor {
  provides ISensor iSensor;
}

component VibrationSensor {
  provides ISensor iSensor;
}

Next: , Up: Possible Events Multiplexing Sensor Inputs   [Contents]

2.5.1 Inevitable Events versus Optional Events

The Dezyne interface keyword inevitable means that a specified event (i.e., out function) will always eventually happen asynchronously, unless something in your logic always happens to prevent the specified event – for example a timer that never gets set during execution, or that always gets canceled before it can time out. The keyword optional means that the event might or might not ever happen asynchronously. In the practical world, nothing asynchronous always happens in a system’s lifetime: not every burglar alarm gets tripped, not every email gets eventually delivered, not every transaction eventually succeeds, not every reptile species is eventually wiped out by a meteor or asteroid strike. Thus “optional” perhaps more often models the real situation than does “inevitable”. So when and why would we ever use “inevitable” in a model?

In sum, if you care about the system’s behaviour when an event goes unheeded essentially forever, or when an awaited event still hasn’t occurred long after you expected it, then use “optional”, for example for a half-entered passcode. Otherwise, “inevitable” is simpler and will usually test the system’s logical completeness and correctness well enough.

When you use “optional”, a rule of thumb might be to push down optional behaviour as low as possible in the system, or equivalently as close as possible to the hardware on which the system runs or depends.


Previous: , Up: Possible Events Multiplexing Sensor Inputs   [Contents]

2.5.2 The Multiplexer Component

First let’s specify requirements for a multiplexer regardless of how many sensors it controls:

  1. A multiplexer can control any number of sensors, including zero.
  2. A multiplexer’s default state is Off.
  3. Turning on a multiplexer turns on all of its sensors, unless the multiplexer’s state is already Sensing or Triggered, in which case turning on is illegal (should never occur).
  4. Turning off a multiplexer turns off all of its sensors, unless the multiplexer’s state is already Off, in which case turning off is illegal.
  5. A trigger event from any of a multiplexer’s sensors sets the multiplexer’s state to Triggered and sends a triggered event to the multiplexer’s caller.
  6. If a multiplexer has triggered, it will not trigger again until its sensors have been turned off and turned back on.

The below component with zero sensors establishes the framework for multiplexing. Its behaviour is just a replica of the interface behaviour minus the optional trigger; hence, you can copy the interface’s whole behaviour block, remove the optional sub-block, reset State references to the local declaration of State, reset event (function) names to iSensor.<name>, and add parentheses to event (function) names. The Triggered state will remain dead code until the multiplexer is hooked up to at least one sensor that can be triggered (note that Dezyne verification does NOT notify you about dead code).

component SensorMultiplexer {
  provides ISensor iSensor;

  behaviour {
    enum State { Off, Sensing, Triggered };
    State state = State.Off;
    [state.Off] {
      on iSensor.turnOn(): state = State.Sensing;
      on iSensor.turnOff(): illegal; // tests caller's logic in model
    }
    [state.Sensing] {
      on iSensor.turnOn(): illegal;
      on iSensor.turnOff(): state = State.Off;
    }
    [state.Triggered] {
      on iSensor.turnOn(): illegal;
      on iSensor.turnOff(): state = State.Off;
    }
  }
}

In the below code sample we have added one sensor and highlighted all added source code.

Exercise: Will this component verify? Make a decision, then verify in Dezyne. The answer is below the code sample.

component SensorMultiplexer {
  provides ISensor iSensor;
  requires ISensor iSensor1;

  behaviour {
    enum State { Off, Sensing, Triggered };
    State state = State.Off;
    [state.Off] {
      on iSensor.turnOn(): {
        iSensor1.turnOn();
        state = State.Sensing;
      }
      on iSensor.turnOff(): illegal;
    }
    [state.Sensing] {
      on iSensor.turnOn(): illegal;
      on iSensor.turnOff(): {
        iSensor1.turnOff();
        state = State.Off;
      }
      on iSensor1.triggered(): {
        iSensor.triggered();
        iSensor1.turnOff();
        state = State.Triggered;
      }
    }
    [state.Triggered] {
      on iSensor.turnOn(): illegal;
      on iSensor.turnOff(): state = State.Off;
      on iSensor1.triggered(): illegal;
    }
  }
}

The above component does verify, in fact. One state-event case is not handled explicitly, “on iSensor1.triggered():” in [state.Off], but this is an allowed implicit illegal declared in the interface.

The below screen shot shows the simulated SensorMultiplexer’s Trace, Sequence and State Chart views. Notice that its State Chart is exactly the same as a plain sensor. Aggregated sensor behaviour and single sensor behaviour are identical from the caller’s point of view, provided that it doesn’t matter what kind of alarm happened – motion, vibration, magnetic effect, or other.

images/eclipse_3.75

In the below code we have added a second multiplexed sensor, with new code highlighted. But this code has a logic error. Exercise: Can you spot it? If you’re impatient, just verify in Dezyne to get a hint. The multiplexing logic is highly regular and really quite simple, yet you still might find the error hard to spot (you would not be alone by any means). Hint: count the instances of “1” versus instances of “2”. The answer is below the code sample.

component SensorMultiplexer {
  provides ISensor iSensor;
  requires ISensor iSensor1;
  requires ISensor iSensor2;

  behaviour {
    enum State { Off, Sensing, Triggered };
    State state = State.Off;
    [state.Off] {
      on iSensor.turnOn(): {
        iSensor1.turnOn(); iSensor2.turnOn();
        state = State.Sensing;
      }
      on iSensor.turnOff(): illegal;
      on iSensor1.triggered(), iSensor2.triggered(): illegal;
    }
    [state.Sensing] {
      on iSensor.turnOn(): illegal;
      on iSensor.turnOff(): {
        iSensor1.turnOff();
        state = State.Off;
      }
      on iSensor1.triggered(), iSensor2.triggered(): {
        iSensor.triggered();
        iSensor1.turnOff(); iSensor2.turnOff();
        state = State.Triggered;
      }
    }
    [state.Triggered] {
      on iSensor.turnOn(): illegal;
      on iSensor.turnOff(): state = State.Off;
      on iSensor1.triggered(), iSensor2.triggered(): illegal;
    }
  }
}

The defect is in [state.Sensing], on turnOff(), which turns off the first sensor but not the second.

Exercise: Repair the defect, verify and simulate, then optionally generate the C++ source and examine it.

Having gone through most Dezyne basics, we’re ready now to design, build, verify and simulate a somewhat less simple Burglar Alarm system.


Previous: , Up: Dezyne Basics   [Contents]

2.6 The Alarm System


Next: , Up: The Alarm System   [Contents]

2.6.1 Requirements

Our next alarm system has a pincode keypad, a multi-color LED, a siren, and sensors. The keypad silently discards invalid pincodes. The system has two basic sequences of events:

On power up the system is unarmed, the LED is green, and sensors are disabled.

  1. Green: unarmed.
  2. Yellow: Valid pincode entry arms the system, turns the LED yellow and enables sensors.
  3. Red: A sensor trigger disables the sensors and turns the LED red.
  4. Either Yellow: Valid pincode entry soon enough cancels the timer and returns the system to the armed state with yellow LED and enabled sensors.
  5. Or Red with siren: Timer timeout turns on the siren.
  6. Yellow: Valid pincode entry turns off the siren and returns to armed state.

Alternate sequence with no sensor trigger event:

  1. Green: Unarmed
  2. Yellow: Valid pincode entry arms the system, turns the LED yellow, and enables sensors.
  3. Green: Valid pincode entry disarms the system, turns the LED green, and disables sensors.

One might white-board the initial conceptual system like this:

images/state_3

After power-up, a valid pincode event can arrive any time at the Controller, whether appropriate or not. Once the Controller enables the sensors, they can trigger events at any moment but possibly never. The LED is configured to be a solid-color green on power-up, yellow when armed, and red whenever there is a sensor-generated alarm active. The Controller starts the timer when a sensor triggers and starts the siren upon timeout. A user must enter a valid pincode to exit the alarm state and to silence the siren if it has begun sounding.


Next: , Previous: , Up: The Alarm System   [Contents]

2.6.2 The Controller

Usually we start designing by sketching interfaces, since we can always reasonably assume that a “hand-written” component will correctly implement any given interface. The below interface captures the two main kinds of incoming events for the controller: user-entered pincodes, and sensor trigger events. Timer timeout events are different since the controller has to initiate them.

interface IController {
  in void validPincode();
  in void sensorTriggered();

  behaviour {
    on validPincode: {}
    on sensorTriggered: {}
  }
}

The above minimal interface declares implicitly that any and every incoming event is “legal”, i.e., the caller does not have to track the controller’s state and avoid inappropriate calls. Said another way, the implemented interface will not hit an assertion via an illegal event.

A minimal Controller component would start up Unarmed; go from there to Armed upon a valid pincode; go from Armed to Alarming upon getting a sensorTriggered event; return to Armed state upon valid pincode; and return to Unarmed after another valid pincode. As an exercise you might want to build the minimal controller yourself before reading the below code.

component Controller {
  provides IController iController;

  behaviour {
    enum State { Unarmed, Armed, Alarming };
    State state = State.Unarmed;
    [state.Unarmed] {
      on iController.validPincode(): state = State.Armed;
      on iController.sensorTriggered(): {}
    }
    [state.Armed] {
      on iController.validPincode(): state = State.Unarmed;
      on iController.sensorTriggered():state = State.Alarming;
    }
    [state.Alarming] {
      on iController.validPincode(): state = State.Armed;
      on iController.sensorTriggered(): {}
    }
  }
}

The above honors its interface contract by always silently accepting and ignoring a sensorTriggered event when it is not in the Armed state.


Next: , Previous: , Up: The Alarm System   [Contents]

2.6.3 Adding the LED

Next we add simple control for an LED.

interface ILED {
  // assumes green automatically on power-up
  in void setGreen();
  in void setYellow();
  in void setRed();
  behaviour { on setGreen, setYellow, setRed: {} }
}

component LED { provides ILED iLed; }

Integrating the LED would make a good exercise.

Note that the below integrated code imports the LED interface as opposed to declaring it.

import LED.dzn;

interface IController {
  in void validPincode();
  in void sensorTriggered();

  behaviour {
    on validPincode: {}
    on sensorTriggered: {}
  }
}

component Controller {
  provides IController iController;
  requires ILED iLed;

  behaviour {
    enum State { Unarmed, Armed, Alarming };
    State state = State.Unarmed;
    [state.Unarmed] {
      on iController.validPincode(): {
        state = State.Armed;
        iLed.setYellow();
      }
      on iController.sensorTriggered(): {}
    }
    [state.Armed] {
      on iController.validPincode(): {
        state = State.Unarmed;
        iLed.setGreen();
      }
      on iController.sensorTriggered(): {
        state = State.Alarming;
        iLed.setRed();
      }
    }
    [state.Alarming] {
      on iController.validPincode(): {
        state = State.Armed;
        iLed.setYellow();
      }
      on iController.sensorTriggered(): {}
    }
  }
}

Next: , Previous: , Up: The Alarm System   [Contents]

2.6.4 Adding the Sensors

Now we add sensors, removing the sensorTriggered event from the Controller and importing the sensor we constructed earlier.

import LED.dzn;
import Sensor.dzn;

interface IController {
  in void validPincode();
  behaviour { on validPincode: {} }
}

component Controller {
  provides IController iController;
  requires ILED iLed;
  requires ISensor iSensor;

  behaviour {
    enum State { Unarmed, Armed, Alarming };
    State state = State.Unarmed;
    [state.Unarmed] {
      on iController.validPincode(): {
        iSensor.turnOn();
        state = State.Armed;
        iLed.setYellow();
      }
      on iSensor.triggered(): {}
    }
    [state.Armed] {
      on iController.validPincode(): {
        iSensor.turnOff();
        state = State.Unarmed;
        iLed.setGreen();
      }
      on iSensor.triggered(): {
        iSensor.turnOff();
        state = State.Alarming;
        iLed.setRed();
      }
    }
    [state.Alarming] {
      on iController.validPincode(): {
        iSensor.turnOn();
        state = State.Armed;
        iLed.setYellow();
      }
      on iSensor.triggered(): illegal;
    }
  }
}

Next: , Previous: , Up: The Alarm System   [Contents]

2.6.5 Adding the Siren and Timer

Next we add a siren to be sounded only when a user takes too long to enter the pincode after a sensor trigger makes the LED go red. The siren interface and component are simple:

interface ISiren {
  in void turnOn();
  in void turnOff();
  behaviour { on turnOn, turnOff: {}
  }
}

component Siren { provides ISiren iSiren; }

We’ll put the siren in its own file Siren.dzn and include that file in the Controller. In the next step we turn on the siren whenever Alarming, and turn it off whenever returning to the Armed state.

import LED.dzn;
import Sensor.dzn;
import Siren.dzn;

interface IController {
  in void validPincode();
  behaviour { on validPincode: {} }
}

component Controller {
  provides IController iController;
  requires ILED iLed;
  requires ISensor iSensor;
  requires ISiren iSiren;

  behaviour {
    enum State { Unarmed, Armed, Alarming };
    State state = State.Unarmed;
    [state.Unarmed] {
      on iController.validPincode(): {
        iSensor.turnOn();
        state = State.Armed;
        iLed.setYellow();
      }
      on iSensor.triggered(): {}
    }
    [state.Armed] {
      on iController.validPincode(): {
        iSensor.turnOff();
        state = State.Unarmed;
        iLed.setGreen();
      }
      on iSensor.triggered(): {
        iSensor.turnOff();
        state = State.Alarming;
        iLed.setRed();
        iSiren.turnOn();
      }
    }
    [state.Alarming] {
      on iController.validPincode(): {
        iSensor.turnOn();
        state = State.Armed;
        iLed.setYellow();
        iSiren.turnOff();
      }
      on iSensor.triggered(): illegal;
    }
  }
}

As an exercise, modify the above model to turn on the siren only on a 30-second timeout after the system has been triggered into the Alarming state. You will need to import the Timer component we created earlier and configure it correctly. The fragment of model code below shows only the key changes needed to the Controller event handling; if you copy and paste this partial solution into Dezyne you will still have to debug and finish it.

      on iSensor.triggered(): {
        iSensor.turnOff();
        state = State.Alarming;
        iLed.setRed();
        iTimer.start($30000$);
      }
      on iTimer.timeout(): illegal;
    }
    [state.Alarming] {
      on iTimer.timeout(): {
        iSiren.turnOn();
      }
      on iController.validPincode(): {
        iTimer.cancel();
        iSensor.turnOn();
        state = State.Armed;
        iLed.setYellow();
        iSiren.turnOff();
      }

Previous: , Up: The Alarm System   [Contents]

2.6.6 The Completed Alarm System

Below is the Dezyne-generated sequence diagram, and event trace listing, from simulating a complete round-trip exercise of the Controller component. Events included sounding the siren when the user did not enter a valid pincode soon enough after an alarm was triggered, and returning at the end to the disarmed state. (Screen shots were edited for better readability.)

images/sequence_1

We finish the alarm system by creating a top-level system component that shows how the other components interconnect through interfaces. This system component presents the iController interface to the yet larger software system into which it might be integrated. For this tutorial, the system component’s purpose is only to auto-generate the diagram shown below the code.

component AlarmSystem {
  provides IController iController;

  system {
    Controller controller;
    LED led;
    Sensor sensor;
    Siren siren;
    Timer timer;
    iController<=>controller.iController;
    controller.iLed<=>led.iLed;
    controller.iSensor<=>sensor.iSensor;
    controller.iSiren<=>siren.iSiren;
    controller.iTimer<=>timer.iTimer;
  }
}
images/system_3
Refactoring and Extending Dezyne Models

Dezyne models capture fundamental logical behaviour in perhaps a quarter of the lines it takes to write the same logic in compatible and usable C++. The five Dezyne models in the alarm system all have tens of lines of code each. Because Dezyne model representations are compact, easily edited and complete/compliant, they make refactoring ant extending as easy as it could possible be. Further, because Dezyne quickly verifies any change or addition to an existing model, the pace of refactoring and extending is as fast as it could possibly be.

Comparing Using Dezyne to Developing “By Hand”

Think about having to develop this system “in the other direction”. You’d likely start with sketched sequence diagrams, which are tedious and difficult to draw manually and modify. From there you would specify and write the C++ source code, and build and test is. Along the way you would almost certainly rebuild the sequence diagram by hand more than once.

Eventually a test/verification persom would have to manually generate event sequences to exercise paths through the system. That person could take weeks or months to do what Dezyne did in a few seconds: trace out every possible execution path through the system and ensure there are no race conditions, deadlocks, non-deterministic overlaps among guards, or other problems.

In fact, for anything but the smallest system, your test/verification staff will probably NEVER accomplish what Dezyne has done in seconds or minutes, which is attain 100% path coverage for the heart of the system, its core states-and communications logic. This is the power of Dezyne


Next: , Previous: , Up: Top   [Contents]

3 Dezyne Code Integration

In this chapter we will

We assume that you are familiar with the basics of the Dezyne modeling language and have some affinity with C++, GNU/Linux and the Raspberry Pi. It is assumed you are somewhat familiar with software designed from an event-based approach (https://en.wikipedia.org/wiki/Event-driven_programming).

The examples shown throughout this chapter will be using the Dezyne-IDE, although Dezyne can also be used as a stand-alone command line client. It is assumed that you have a Dezyne-IDE running on your system before starting this tutorial.

Furthermore, in this chapter you we will use lambda expressions and polymorphism/inheritance in C++. If you are unfamiliar with these concepts, you may find the following resources useful:


Next: , Up: Dezyne Code Integration   [Contents]

3.1 Platform choice

This section will target the Raspberry Pi as hardware platform. The Pi can run a GNU/Linux distribution that is compatible with C++11 features that are used by generated C++ Dezyne code. With some extra components, it is also capable of driving some basic GPIO. The Raspberry Pi that was used to create this section is a Raspberry Pi Model 2 B running Raspbian 8 (Jessie). The g++ version of the Raspberry Pi is 4.9.2.

The components used are as follows:

ComponentQuantity
Raspberry Pi1
RGB Led1
220 Ohm resistor3
Hardware button1
Wiring1

It is, of course, not absolutely necessary to build an actual system that performs all of the tasks. You could also just write stubs for the hardware that will be called upon and run the application on your own system. During the section we will consider actual hardware implementations, but most of the information will still apply if you are using stubs.


Next: , Previous: , Up: Dezyne Code Integration   [Contents]

3.2 Using Dezyne in your C++ environment


Next: , Up: Using Dezyne in your C++ environment   [Contents]

3.2.1 Creating the C++ environment

The first step to start integrating your Dezyne models in an actual application is to generate code from all the models. This can be done in two ways, namely through the Dezyne application or by use of the command line client. In the Dezyne application, right-click on your *.dzn files and navigate to the ‘Generate Code‘ menu item. There you can select multiple programming languages to generate code for. Select a location where the generated code should be stored and Dezyne will generate code for you. Later on in this section, we will discuss how to automate this process by use of the Dezyne command line client and a makefile in Breakdown of example makefile automating Dezyne features.

images/menu_code

Up until now, we have approached the application as an event-based system. In order to run as a program on the Raspberry, though, we must have some kind of (infinite) loop that will provide the system with events. From here on after, this loop will be referred to as the event loop. Let’s start by creating a main function to contain this event loop for our application.

int main(int argc, char* argv[]) {
  while(true) {
    // Dezyne interaction
  }
}

The above main function will run until cancelled and each iteration of the while(true) loop will perform some kind of interaction with Dezyne later on. This is the easiest way of facilitating the event loop required by the Dezyne-generated code.


Next: , Previous: , Up: Using Dezyne in your C++ environment   [Contents]

3.2.2 Including and configuring the dzn runtime

Before the generated code can be used in combination with the event loop you just created, you must also download the Dezyne runtime to use in your project. The runtime can be found in Window / Show Views / Runtime. Once there, select the programming language you want to use and right click to download the associated files. (Just like code generation, downloading the runtime can be done by use of the command line client and a makefile; see Breakdown of example makefile automating Dezyne features. This approach can be helpful in an environment that makes use of version control.)

images/explore

The minimum required components of the Dezyne runtime that must be included in your application are the actual runtime and the Dezyne locator. The Dezyne runtime is a library of primitives used by the generated code; the locator is a mechanism to inject dependencies into a Dezyne system and its components. The runtime is an example of such a dependency that can be injected into the locator.

Their respective files that must be included are runtime.hh and locator.hh, found in the dzn subfolder. The inclusion of the runtime files should be done using ‘ <> ’ include tags as opposed to ‘ ”” ’ include tags; this is because of how code is generated from Dezyne models. This has some implications for compilation but those will be covered later in Compiling your application.

When the files are included you can instantiate the Dezyne locator and runtime objects in your created main. The minimal setup that does all of the above will look as follows:

#include <dzn/runtime.hh>
#include <dzn/locator.hh>

int main(int argc, char* argv[]) {
  dzn::locator loc;
  dzn::runtime rt;

  loc.set(rt);

  while(true) {
    // Dezyne interaction
  }
}

Near the end of this section, in some extra materials you will find a section dedicated to an in-depth look at the Dezyne runtime with more information on how you can customize some of the components of the runtime to your liking: Using the Dezyne locator to distribute runtime objects.


Previous: , Up: Using Dezyne in your C++ environment   [Contents]

3.2.3 Inspecting the generated system

Up until this point you should have completed the following tasks:

Before we start on writing implementations for the various components of the Alarm System, it is important to have a closer look at the generated code from the System component.

Recall that a System component is used to specify how components within the system interact with one another and how they are connected to the environment outside of the system. This specification of connection to the outside world is why using a System component is so important; it is where and how your handwritten code will interact with the code generated from verified models.

The iteration of the Alarm System from the Dezyne Basics we will be using for this can be found at https://github.com/VerumSoftwareTools/DezyneTutorial/tree/master/Code_Integration/Ch1_Starting_Point. If you generate code from these models, you should end up with the following files:

images/generated

As the name of the System component specified in the Dezyne model is AlarmSystem, the generated files have been named AlarmSystem.cc and AlarmSystem.hh as well. Let’s start by having a look at AlarmSystem.hh. This file contains a definition of a struct AlarmSystem which shares some similarities with the System component as specified in Dezyne, which are highlighted in the snippet below:

struct AlarmSystem
{
  dzn::meta dzn_meta;
  dzn::runtime& dzn_rt;

  const dzn::locator& dzn_locator;
  Controller controller;
  LED led;

  IController& iController;

  AlarmSystem(const dzn::locator&);
  void check_bindings() const;
  void dump_tree(std::ostream& os=std::clog) const;
};

Most notably, it specifies which ports can be accessed on the AlarmSystem object (iController, in this case). This directly maps to what ports are available on the boundaries of the system. Another important factor is the definition of the AlarmSystem constructor, which requires a dzn::locator object to be passed as parameter. This is the case for all components and systems generated from Dezyne models, but luckily the System component will take care of distributing the dzn::locator for you!

images/system_4

The other file that was generated from the System component, AlarmSystem.cc, contains the implementation of functions declared in the header file. The constructor generated for the system looks as follows:

AlarmSystem::AlarmSystem(const dzn::locator& dezyne_locator) :  dzn_meta{"","AlarmSystem",0,0,{},{&controller.dzn_meta,&led.dzn_meta},{[this]{iController.check_bindings();}}}
, dzn_rt(dezyne_locator.get<dzn::runtime>())
, dzn_locator(dezyne_locator)
, controller(dezyne_locator)
, led(dezyne_locator)
, iController(controller.iController)
{
  controller.dzn_meta.parent = &dzn_meta;
  controller.dzn_meta.name = "controller";
  led.dzn_meta.parent = &dzn_meta;
  led.dzn_meta.name = "led";
  connect(led.iLed, controller.iLed);

  dzn::rank(iController.meta.provides.meta, 0);
}

The contents of this file look a lot more daunting, but again you can relate some parts of the implementation to lines in the actual Dezyne model. For instance, the binding of ports that was done by controller.iLed <=> led.iLed in Dezyne can be traced to an invocation of the connect(led.iLed, controller.iLed) function.

In the implementation of the System’s constructor most of the magic happens, as a chain of constructors of components within the system is set off and the dzn::locator container (and as such, the dzn::runtime) is spread across the system. Using a System component for this purpose ensures that every component is using the same runtime, which is essential for Dezyne’s functionality. For every Dezyne application you create, make sure to embed the components in a System component.

Interaction with the AlarmSystem object in your event loop is how the logic modeled in Dezyne will perform in your fully integrated application. Later in the section you will see how interaction with the System on its exposed ports will work, but to conclude this section on preparing the C++ environment let’s do exactly that; prepare the main loop for use by creating the System object.

Most of the initialization steps were already completed in the earlier draft of your main function; the runtime files were included and the respective objects were created. What remains is to create an object of the AlarmSystem struct type and pass the locator to it. Then, before entering the event loop, it is recommended to invoke check_bindings() on the System. This is a Dezyne functionality that ensures that all ports have been bound properly. The result will look like this:

#include <dzn/runtime.hh>
#include <dzn/locator.hh>

int main(int argc, char* argv[]) {
  dzn::locator loc;
  dzn::runtime rt;
  loc.set(rt);

  AlarmSystem as(loc);

  as.check_bindings();
  while(true) {
    // Dezyne interaction
  }
}

Next: , Previous: , Up: Dezyne Code Integration   [Contents]

3.3 Implementing and integrating foreign components

Through the course of this section of the section, you will be gradually expanding the C++ environment you prepared in the previous section into an application where foreign code and Dezyne-generated code co-operate. At the end of this section you will be able to:


Next: , Up: Implementing and integrating foreign components   [Contents]

3.3.1 Next step in integration: detecting foreign components

Let’s have a look at the situation currently at hand. If all went well, you should have a file which includes your main function, in which Dezyne runtime components were created and an instance of the Dezyne System was created. We have had a brief look at how the System controls its internal components and how to access ports on the System’s boundary.

The next step in the integration process is to implement the functionalities that could not be modeled in Dezyne such as driving hardware and manipulating data. To do this, though, you need to know two things: what needs to be implemented and where to implement it to make integration as smooth as possible.

images/system_5

The quickest way to figure out what must be implemented as foreign code is by having a look at the System view in Dezyne. You may have already noticed there are two differently colored components in the AlarmSystem; one is a darker green, whereas the other is blue. These colors can be used to quickly assess whether a component was implemented in Dezyne. A blue component in a system indicates that the component in question was defined as a component without behavior. This should set off some alarm bells (pun very intended) because no behavior means no functionality. This leads us to a first conclusion: blue components in a System view must be implemented in foreign code.

The second indicator of implementation that must be done as foreign code is the presence of ports on the boundary of a System in the System view. Such a port, as you can imagine, means that an interface is provided (or required) but there’s no entity in Dezyne that is making use of the provided interface (or implementing the functionality required by the System). This leads us to the second and last conclusion: ports on the boundary of a System must be bound in hand-written code.

So now that we’ve identified what needs to be implemented it’s time to look at where to do so. In the case of a blue component, a very specific method of implementation must be followed. You may have noticed the generation of skel_LED.cc and skel_LED.hh earlier on during the section. These ‘skeleton’ files are generated for every blue component in a System. In these files, you will find an abstract class with pure virtual function(s) in the ‘skel’ namespace. The implementation of the abstract class must be done in files called LED.hh and LED.cc and the struct/class that inherits from skel::LED must be named LED. Although this may feel restrictive, this approach has considerable upsides too: the System becomes responsible for the distribution of runtime objects in the component and through the use of abstract classes and pure virtual functions you can verify that your implementation is complete compile-time instead of discovering such things run-time. We will cover the integration process of blue components in more detail later in Implementing generated ‘skeleton' components.

In case abstract or pure virtual are unfamiliar terms to you, please refer to the introduction of this section where some links to additional information are given .

The second case we discussed was ports on System boundaries. The implementation method for this case is not as restrictive. The implementation may be done wherever you like, as long as all events on the interfaces of the unbound ports are bound eventually. This sounds a lot easier than having to deal with abstract classes and pure virtuals, and it is, but it comes with the tradeoff of bearing more responsibilities as developer.

In the next section, we will cover the implementation of events on unbound ports.

In general, it is recommended to encapsulate your application’s functionalities as components in a System. It increases the cohesion of the overall application and it makes it much easier to find the whereabouts of hand-written code in respect to the overall system. An added benefit is that all sorts of useful meta-information is automatically generated by Dezyne while your application is running which can help tremendously in tracking the behavior of your application.


Next: , Previous: , Up: Implementing and integrating foreign components   [Contents]

3.3.2 Implementation of events on interfaces

It’s time to put the information we gathered from the System view in the previous section to use. To get a feel for interacting with the generated System, let’s start with the ‘easy’ method of integrating handwritten code: binding unbound ports. The port that is currently not bound on the AlarmSystem is of type IController. From the perspective of the System, this is a provides port. The IController interface consists of two in-events, namely validPincode and sensorTriggered. If you have a look at the generated IController.hh file, you can see how this translates to generated code:

struct IController
{

  struct
  {
    std::function<void()> validPincode;
    std::function<void()> sensorTriggered;
  } in;

  struct
  {

  } out;
  // Dezyne meta information
}

For every interface in a Dezyne System, such a file is generated. As you can imagine, in-events on an interface can be found in the in struct and out-events in the out struct. These structs contain std::function objects, which can be invoked or assigned to.

In the intoduction, four event types were mentioned. These four types are the cross product of in- and out-events on provides and requires ports. There are two distinct integration steps that can be performed to cover the integration of the four event types. The following table serves as an overview of when to apply what integration step:

Port typeEvent typeUser action
Provides interface (on top of a component)InCall Dezyne function from handwritten code
OutAssign handwritten code to system function
Requires interface (on the bottom of a component)InAssign handwritten code to system function
OutCall Dezyne function from handwritten code

In case of the IController port, a provides port, both of its events are in-events. Therefore, we must call the Dezyne functions from handwritten code. You may recall that earlier in the section we examined the generated AlarmSystem and noted that its IController port can be accessed on the AlarmSystem object (Inspecting the generated system). Then, on the IController port, we can access events from the in and out structs. The calling of events should take place in the event loop which you created.

Let’s make the event loop a bit smarter, so we can use it to process some user input. If we then map the user input to triggers for the validPincode and sensorTriggered events, we can control the AlarmSystem. The following code snippet is sufficient for processing simple user input:

 std::string input;
  while(std::cin >> input) { // Loop is executed upon every newline from user input
    if(input.compare("s") == 0) {
      // s == sensorTriggered
    }
    else if(input.compare("v") == 0) {
      // v == validPincode
    }
  }

If you replace the comments with the corresponding function calls on the AlarmSystem object, the integration steps for the IController port are complete. As an exercise, replace the comments with the help of the information in this section.

Solution:

int
main(int argc, char* argv[])
{
  dzn::locator loc;
  dzn::runtime rt;

  loc.set(rt);

  AlarmSystem as(loc);

  as.check_bindings();

  std::string input;
  while(std::cin >> input) {
    if(input.compare("s") == 0) {
      as.iController.in.sensorTriggered();
    }
    else if(input.compare("v") == 0) {
      as.iController.in.validPincode();
    }
  }
}

At this stage, the AlarmSystem has no unbound ports that contain provides/out or requires/in events. Later in the section, when we add timer functionality to the AlarmSystem, you will see how this integration step is performed (Timer and Siren integration). First, let’s have a look at implementing the LED component.


Previous: , Up: Implementing and integrating foreign components   [Contents]

3.3.3 Implementing generated ‘skeleton’ components

To start implementing the LED component’s behavior, create the LED.cc and LED.hh files. The AlarmSystem you generated from the Dezyne models already includes the LED.hh file by name, which is why you are restricted in naming it. In this LED.hh file you are also required to define a struct (or class, they are the same in C++) LED that inherits from skel::LED. The LED class definition in LED.hh will look like this:

#include "skel_LED.hh"

class LED : public skel::LED {

}

By inheriting from skel::LED, the LED class is forced to implement all pure virtual functions defined in the base class. The pure virtual functions that are defined in the base class are all events that would normally be handled by the respective component’s behavior. Let’s take a look at the generated LED class in skel_LED.hh:

namespace skel {
  struct LED
  {
    // Dezyne meta information
    ILED iLed;

    LED(const dzn::locator&);
    virtual ~LED();

    // Dezyne meta informaton

    private:
    virtual void iLed_setGreen() = 0;
    virtual void iLed_setYellow() = 0;
    virtual void iLed_setRed() = 0;
    virtual void iLed_turnOff() = 0;
  };
}

As expected, the events we promised to implement in the ILED interface (setGreen, setYellow, setRed and turnOff) are pure virtual functions in the generated base class. You should add these function declarations to the LED class definition in LED.hh as an exercise.

Solution:

#include "skel_LED.hh"

class LED : public skel::LED {
  void iLed_setGreen();
  void iLed_setYellow();
  void iLed_setRed();
  void iLed_turnOff();
}

Lastly, as the LED class you’ll be creating will be constructed like any other generated Dezyne class, you will need to define a constructor for the LED that accepts a dzn::locator reference as parameter. The final version of the foreign LED class definition, from the Dezyne perspective, will look like this:

#include "skel_LED.hh"

class LED : public skel::LED {
  void iLed_setGreen();
  void iLed_setYellow();
  void iLed_setRed();
  void iLed_turnOff();

public:
  LED(const dzn::locator& loc);
}

Note that the constructor must be public; this is because the generated AlarmSystem directly calls the constructor of the LED class. The functions it implements do not have to be public; those functions are called through the LED class’ ILED port. The skel_LED.hh file already includes the necessary files from the Dezyne runtime to be able to refer to dzn::locator, so that’s taken care of as well.

With the definition out of the way, what’s left to be done is the implementation of the functions of the LED class. Driving an LED on the Raspberry Pi can be done with the WiringPi library (http://wiringpi.com). To make use of WiringPi, its setup function needs to be called and the GPIO pins connected to the LED must be initialized. This is hardware-specific setup that should be performed in the implementation of the LED’s constructor; it will be performed when the constructor is called by the generated AlarmSystem. As an exercise, write an implementation for the constructor using wiringPiSetup() and pinMode() for your hardware setup.

Solution:

#include <wiringPi.h>
#include "LED.hh"

LED::LED(const dzn::locator& loc) {
  wiringPiSetup();
  //Pin numbers are declared in LED.hh as PIN_RED, PIN_GREEN and PIN_BLUE for readability
  pinMode(PIN_RED, OUTPUT);
  pinMode(PIN_GREEN, OUTPUT);
  pinMode(PIN_BLUE, OUTPUT);
}

The solution above takes care of all the hardware setup, but that is not all we want to do with the foreign implementation of a Dezyne component. To fully integrate a foreign component in the AlarmSystem, you should call also call the constructor of the component’s base class to handle Dezyne related initialization. In C++, this is easily done by modifying the constructor to the following:

LED::LED(const dzn::locator& loc) : skel::LED(loc) {

This modification will call the constructor of LED’s base class skel::LED as well as perform the constructor you implemented in your foreign component. In skel::LED all of the Dezyne meta information and port binding is handled, so all you need to worry about in the foreign LED class is the functional behavior of the component.

To implement the setGreen, setYellow, setRed and turnOff functions you can do that like you would any other function. WiringPi provides a digitalWrite() function you can use to turn output on a GPIO pin on or off. All the colors we wish to display on the RGB LED can be created by a mixture of on and off on the three respective pins. Try implementing the remaining functions yourself as an exercise.

Solution:

void LED::iLed_setGreen() {
  digitalWrite(PIN_RED, LOW);
  digitalWrite(PIN_GREEN, HIGH);
  digitalWrite(PIN_BLUE, LOW);
}

void LED::iLed_setYellow() {
  digitalWrite(PIN_RED, HIGH);
  digitalWrite(PIN_GREEN, HIGH);
  digitalWrite(PIN_BLUE, LOW);
}

void LED::iLed_setRed() {
  digitalWrite(PIN_RED, HIGH);
  digitalWrite(PIN_GREEN, LOW);
  digitalWrite(PIN_BLUE, LOW);
}

void LED::iLed_turnOff() {
  digitalWrite(PIN_RED, LOW);
  digitalWrite(PIN_GREEN, LOW);
  digitalWrite(PIN_BLUE, LOW);
}

In summary: you now have a small but functionally complete burglar alarm program which accepts ‘s’ and ‘v’ commands from the user to denote a sensor trigger and valid password entry. Based on sequences of events, the program will display different colors on an RGB LED denoting whether the system is Unarmed, Armed or Alarming.

In the next section, you will find instructions on how to compile this application on a Raspberry Pi target so you can see it function in the real world!


Next: , Previous: , Up: Dezyne Code Integration   [Contents]

3.4 Compiling your application

To compile your application, an example makefile has been included. In this section, we will explore the features this makefile offers and help you configure it to your environment’s needs. The makefile that was used to compile the AlarmSystem project can be found at https://github.com/VerumSoftwareTools/DezyneSection/tree/master/Code_Integration/Ch3_Makefile.

The nice thing about this makefile is that it can be re-used for other C++ projects that combine foreign code with code generated from Dezyne. Additionally, the makefile has gradually grown to facilitate version control. Dzn model files are treated as source code and checked into version control. Dezyne-generated C++ is treated similar to C++-generated object files: it is not checked into version control because it can always be regenerated.


Next: , Up: Compiling your application   [Contents]

3.4.1 Breakdown of example makefile: the core

Let’s break the provided makefile down to the core so we can discuss what is actually needed to compile the AlarmSystem application. The makefile assumes you will compile the application on a Raspberry Pi. To accomplish this, you need to transfer the source files and generated files to the Pi filesystem. With all that in place, the following snippet will compile the integrated application on the Pi:

CXX = g++
CXXFLAGS = -std=c++11 -I$(RUNTIME) -I$(SRC) -lwiringPi -lrt
CPPFLAGS = -MMD -MF $(@:%.o=%.d) -MT '$(@:%.o=%.d) $@' -I$(SRC) -I$(RUNTIME)
LDFLAGS = -lpthread
TARGET = dznpi

SRC = ./src
RUNTIME = ./lib

SRCS = $(wildcard $(SRC)/*.cc)
SRCS += $(wildcard $(RUNTIME)/*.cc)

OBJS = $(subst .cc,.o,$(SRCS))

all:
	make $(TARGET)

$(TARGET): $(OBJS)
	$(CXX) $(CXXFLAGS) -o $(TARGET) $(OBJS) $(LDFLAGS)

-include $(wildcard $(SRC)/*.d $(RUNTIME)/*.d)

This makefile will search for the Dezyne runtime files in the directory pointed at by the RUNTIME variable. The C++ source files of your application should be in the directory pointed at by the SRC variable.

One of the key reasons for using a makefile, aside from not having to re-type your compilation recipe every time you make a change, is to save time by dynamically deciding what files have been changed. An unchanged file often does not need to be recompiled and in larger projects you can save a lot of time by not re-compiling every single file for every small change you make. In this makefile, this dynamic checking is realised with the -MMD -MF $(@:%.o=%.d) -MT '$(@:%.o=%.d) $@' CPPFLAGS and the -include $(wildcard $(SRC)/*.d $(RUNTIME)/*.d) line at the end of the file.

Remember when we first inspected the generated system in Inspecting the generated system? You were told that inclusion of runtime files must be done using ‘ <> ‘ tags and that this would have some implications for compiling the application. These implications are represented in the makefile by the -I$(RUNTIME) -I$(SRC) flags in CXX/CPPFLAGS. This means that for every compilation step, RUNTIME and SRC point to directories that must be searched for included dependencies. With these flags added to your compilation recipe, ‘<>’ tags can be used and the generated code can find its required headers.

The --lwiringPi and --lrt flags are required to be able to make use of the WiringPi library. Due to the --lrt flag, the pthread library must be linked to the executable post compilation; this is done with the LDFLAGS = -lpthread compilation step.

With this makefile and a properly structured filesystem containing your project, you can already compile an application consisting of foreign and generated Dezyne code. Awesome! In case you are unsure of what your filesystem should look like, you can use the Github repository as inspiration:

images/github

With this folder structure, if you type ‘make’ in a terminal window on your Raspberry Pi while inside the same folder the makefile is in, an executable called ‘dznpi’ will be created. If you run the dznpi executable on your Pi and have connected the RGB led to the GPIO pins you defined to be the Red, Green and Blue RGB pins then you should be able to control the dznpi application with sensorTriggered and validPincode events through the command line UI!


Next: , Previous: , Up: Compiling your application   [Contents]

3.4.2 Breakdown of example makefile: version control improvements

If you’ve used version control systems (VCS) before, you have probably encountered conventions for what files are allowed to be stored on the VCS. One strategy that often occurs is to not commit temporary files such as *.o files to your VCS. To facilitate for this, you can add some clean-up recipes to the makefile like the following:

RM = rm –f

clean:
	$(RM) $(OBJS) $(TARGET)

Typing ‘make clean’ on your command line within the respective project folder will remove all of the generated *.o files as well as the compiled executable. This is a good first step in cleaning up your working directory before committing your local changes to a VCS.


Previous: , Up: Compiling your application   [Contents]

3.4.3 Breakdown of example makefile: automating Dezyne features

This improvement requires you to be able to access the dzn client from your command line. To learn how to do this, refer to https://www.verum.com/supportitem/the-dezyne-command-line-tool/ or follow the instructions on how to set your PATH variable after installation of Dezyne through the Dezyne-IDE.

In a way, generated code from Dezyne models can also be seen as temporary files, just like the *.o files from the previous paragraph. The source files for the generated code are your *.dzn files, and by including the generation of code in a makefile recipe it becomes easy to compile the application with only the makefile and source code in your VCS.

The generation of code from Dezyne models and its removal before committing can both be automated in the makefile. The generated code shares a version dependency with the runtime files, so to avoid any clashes on that aspect the example makefile also has a recipe to download the runtime.

For the generation of C++ code and the downloading of the Dezyne runtime, the following recipes were added:

VERSION = 2.3.3
CURRENT := $(shell dzn query | grep '*' | sed 's,\* ,,')

ifneq ($(VERSION),$(CURRENT))
$(info current version: $(CURRENT) is not equal to selected version: $(VERSION))
endif

runtime: | $(RUNTIME)/dzn
	for f in $(shell dzn ls -R /share/runtime/c++ | sed 's,/c++/,,' | tail -n +3); do \
	dzn cat --version=$(VERSION) /share/runtime/c++/$$f > $(RUNTIME)/$$f; \
	done
	touch $ 
$(RUNTIME)/dzn:
	mkdir -p $ 
generate: $(wildcard *.dzn)
	for f in $^; do dzn -v code --version=$(VERSION) -l c++ -o $(SRC) --depends=.d $$f; done
	touch $ 

These additions check the version you’re using against the newest possible version of Dezyne so you are notified if there is a new Dezyne available. The runtime recipe checks if the required folder structure is already present; if it is not, it will be created. Then, it checks Verum’s runtime repository and downloads the respective files for the C++ runtime.

The generate recipe checks for all *.dzn files in the root directory of your project where your makefile is located and generates C++ code for all of the interfaces and components in the files. The generated code is stored in the folder specified by the SRC variable that was declared earlier in the makefile; this ensures that foreign and generated code exist in the same directory. Lastly, the --depends option ensures that extra *.dzn.d files are generated that provide information about what *.cc and *.hh files are generated from their respective *.dzn files and their dependencies. The information in these files can be used for a final step in the VCS improvements: cleaning up generated code.

clean_generated:
	$(RM) `grep -h dzn $(SRC)/*.dzn.d | sed -e 's,:.*,,' -e 's,%,.,g'`
	$(RM) $(RUNTIME)
	$(RM) runtime generate

The recipe for cleaning up generated code is a bit harder to read, but in essence what it does is it reads the contents of the *.dzn.d files (that were generated with the --depends option of dzn code generation). In these *.dzn.d files, the names of generated files can be found; the make recipe clean_generated then removes all of the files it has found from the contents of the *.dzn.d files. The recipe also removes the runtime that was downloaded.

This should cover everything that is included in the example makefile. Depending on your preferences, you can choose to include or leave out some of its features; maybe you don’t care about having generated files in your VCS for example. As long as you include the core features discussed in Breakdown of example makefile the core, you will be able to compile your application consisting of generated and foreign code.


Next: , Previous: , Up: Dezyne Code Integration   [Contents]

3.5 Expanding the AlarmSystem

In the previous section on code integration, we did not cover all possible integration steps. In this section, we will gradually expand the AlarmSystem into the final version that can be found in the introductory section, including an added functionality that lets us explore how data parameters are handled in generated and foreign code.

After this section, you will be able to:


Next: , Up: Expanding the AlarmSystem   [Contents]

3.5.1 Timer and Siren integration

One integration step you haven’t seen yet is the binding of foreign code to a System function (i.e. calling foreign code from Dezyne). This step is performed when you need to integrate an out-event on a provides port or an in-event on a requires port. Recall that the provides/requires is seen from a System perspective.

images/system_6

A good starting point for this integration step is the AlarmSystem with foreign LED component that you have already fully integrated by now. By adding the Siren and Timer from the introductory section, you can learn how to perform this last type of integration. A starting point containing the relevant Dezyne models for this section can be found on https://github.com/VerumSoftwareTools/DezyneSection/tree/master/Code_Integration/Ch4_Siren_Timer.

Note that in the System component in AlarmSystem.dzn, a requires ITimer was added as opposed to using a component without behavior that provides ITimer. The reasoning behind this is that C++ already has access to a complete Timer implementation on most GNU/Linux distributions, including Raspbian which we are running on the Raspberry Pi. In such a case, it might be simpler to integrate the existing implementation as a required port like you will see in this section.

You can start off by generating code from the models again, either through the makefile or by use of the Dezyne-IDE client. Integrating the Siren should be rather simple after having integrated the LED already. We chose to stub the Siren functionalities with simple console output messages (Siren is activated, Siren is deactivated). Start off by integrating the Siren as an exercise.

Solution:

Siren.hh:

#include "skel_Siren.hh"

class Siren : public skel::Siren {
public:
  Siren(const dzn::locator& loc);
  void iSiren_turnOn();
  void iSiren_turnOff();
};

Siren.cc:

#include <iostream>

#include "Siren.hh"

Siren::Siren(const dzn::locator& loc) : skel::Siren(loc) {
  //no op
}

void Siren::iSiren_turnOn() {
  std::cout << "SIREN >>ACTIVATED<<" << std::endl;
}

void Siren::iSiren_turnOff() {
  std::cout << "SIREN >>DEACTIVATED<<" << std::endl;
}

After you have implemented and integrated the Siren, you should be able to compile the application again with the provided makefile. However, when you try to run the dznpi executable, the application will abort upon hitting the as.check_bindings(); line that is processed before entering the event loop with the following error message:

images/error_msg

As you can see, check_bindings() discovered that iTimer’s start function has not been bound. Previously we could not see the effects of the check_bindings() statement as we did not run the application yet. Now you can clearly see the difference between the integration of a component without behaviour and the integration of an unbound port; try leaving out the declaration and implementation of iSiren_turnOn in your foreign Siren implementation. You will discover that you can’t even compile the application, whereas the fact that the iTimer port on the System was not bound couldn’t be discovered until the application was already running.

Now of course, this AlarmSystem application is rather trivial and there are few implications for running the application and hitting the check_bindings() assert. However, imagine having a much more complex, expensive system that is partly through its initialisation process when hitting the assert- sure, you can implement measures to have the application shut down gracefully but it is a situation you would like to avoid. By using components without behaviour for your foreign implementations these issues can be found while compiling before the application is ever run. This does not mean you should skip calling check_bindings() before initiating events on the System, however.

But let’s continue with the integration process. Like we mentioned earlier in this section, we can access a complete Timer implementation in C++ on the Raspberry- the alarm (https://linux.die.net/man/3/alarm) library. What remains to be done is to bind the events on the iTimer port to the controls of this alarm library. The table that was provided in the Implementation of events on interfaces section earlier in the section suggests that the necessary integration step is to assign foreign code to a System function for in-events and call Dezyne functions from foreign code for out-events.

A quick recap: a System can expose ports, these ports contain structs for in-events and out-events where the in- and out-events are represented by std::function objects. For iTimer, which is a port of type ITimer, these are the generated structs:

 struct
  {
    std::function<void(long milliseconds)> start;
    std::function<void()> cancel;
  } in;

  struct
  {
    std::function<void()> timeout;

  } out;

For the iTimer port, a timer timeout must result in calling the out.timeout() function. From the manual for the alarm library, we can see that the alarm will generate a SIGALRM signal when the time has elapsed. Handling SIGALRM can be done by implementing a signal handler and binding SIGALRM to this signal handler in C++ as follows:

#include <signal.h>

void sigalrm_handler(int signal) {
  // signal handling logic
}

// in main():
signal(SIGALRM, sigalrm_handler);

The signal handler is called when SIGALRM is raised, so when the alarm times out. In this signal handler, you should not fire the timeout event into the Dezyne system immediately; the reasoning behind this has to do with how Dezyne’s execution model works based on certain assumptions. This will be covered later in Thread safety in the Dezyne execution model. For now, consider it safe to call the Dezyne function in the signal handler, but keep in mind that this is not something you can generally assume.

To be able to call the timeout function in the signal handler, you need to declare a global std::function object. The AlarmSystem you are interacting with in your event loop has its scope limited to the main() function, but the signal handler is separated from that. You can work around this by declaring a global std::function object and setting its value to the corresponding timeout event on the AlarmSystem’s iTimer port:

#include <iostream>
#include <string>
#include <unistd.h>
#include <signal.h>

#include <dzn/runtime.hh>
#include <dzn/locator.hh>
#include "AlarmSystem.hh"

std::function<void()> timeout;

void sigalrm_handler(int signal) {
  // For now, call the global timeout() function object within this signal handler
  timeout();
}

int
main(int argc, char* argv[])
{
  dzn::locator loc;
  dzn::runtime rt;

  loc.set(rt);

  AlarmSystem as(loc);
  as.dzn_meta.name = "AlarmSystem";

  timeout = as.iTimer.out.timeout;
  signal(SIGALRM, sigalrm_handler);

  as.check_bindings();

  std::string input;
  while(std::cin >> input) {
    if(input.compare("s") == 0) {
      as.iController.in.sensorTriggered();
    }
    else if(input.compare("v") == 0) {
      as.iController.in.validPincode();
    }
  }
}

However, we still have not fully bound the iTimer port on the AlarmSystem. The in-events require an implementation in your foreign code; start(long milliseconds) and cancel() must be bound to their respective counterparts in the alarm implementation. The most efficient way to do this is by using lambda expressions. Starting and cancelling the alarm can be done by the following expressions:

To bind these implementations to their respective events on the iTimer port, a simple assignment will suffice:

#include <iostream>
#include <string>
#include <unistd.h>
#include <signal.h>

#include <dzn/runtime.hh>
#include <dzn/locator.hh>
#include "AlarmSystem.hh"

std::function<void()> timeout;

void sigalrm_handler(int signal) {
  // For now, call the global timeout() function object within this signal handler
  timeout();
}

int
main(int argc, char* argv[])
{
  dzn::locator loc;
  dzn::runtime rt;

  loc.set(rt);

  AlarmSystem as(loc);
  as.dzn_meta.name = "AlarmSystem";

  as.iTimer.in.start = [](int ms){ alarm(ms/1000); };
  as.iTimer.in.cancel = [](){ alarm(0); };
  timeout = as.iTimer.out.timeout;
  signal(SIGALRM, sigalrm_handler);

  as.check_bindings();

  std::string input;
  while(std::cin >> input) {
    if(input.compare("s") == 0) {
      as.iController.in.sensorTriggered();
    }
    else if(input.compare("v") == 0) {
      as.iController.in.validPincode();
    }
  }
}

Previous: , Up: Expanding the AlarmSystem   [Contents]

3.5.2 Handling data: password entry

The Alarm System you created in the introductory section assumed that the keypad the user entered their password with could assert whether the password was correct. This sounds like an awfully smart component, providing not completely related functionalities in capturing input and assessing the correctness of input. An easy way to split that up would be to separate these two actions; on the IController interface, change the validPassword event to a passwordEntered event with a string parameter and create a component that can be used to assess the validity of a given password.

The new IController interface would look like this:

interface IController {
  in void passwordEntered(String pw);
  in void sensorTriggered();

  behaviour {
    on passwordEntered: {}
    on sensorTriggered: {}
  }
}

The interface for a password management component would look like this:

extern String $std::string$;

interface IPWManager {
	in bool verifyPassword(String pw);

	behaviour {
		on verifyPassword: reply(true);
		on verifyPassword: reply(false);
	}
}

As checking the validity of a password cannot be done in Dezyne, create a component without behavior that provides the IPWManager interface so this can be implemented in foreign code. Additionally, extend the behavior of the Controller component to make use of this new PWManager component by replacing the on iController.validPincode(): event statements with on iController.passwordEntered(pw): statements. The parameter to this function, pw, can then be verified with the new IPWManager port on the Controller component as follows:

    [state.Unarmed] {
      on iController.passwordEntered(pw): {
      	bool valid = iPWManager.verifyPassword(pw);
      	if(valid) {
	        state = State.Armed;
	        iLed.setYellow();
        }
      }
      on iController.sensorTriggered(): {}
      on iTimer.timeout(): illegal;
    }

Implement these changes for the other two state behavior blocks as well (Armed, Alarming). Lastly, update the System component to reflect the new interfaces and components. Re-generate code from the updated Dezyne models and create the necessary files for the foreign implementation of the password manager.

As you were previously capturing user input to trigger events on the AlarmSystem, some changes will need to be made to how the user input was being processed. Instead of mapping ‘v’ to the validPassword event like we did earlier, the simplest way to accommodate for the change is to treat every user input that is not an event trigger as a password entry, like such:

  std::string input;
  while(std::cin >> input) {
    if(input.compare("s") == 0) {
      as.iController.in.sensorTriggered();
    }
    else /*user input counts as password*/ {
      as.iController.in.passwordEntered(input);
    }
  }

Note that the function prototype in C++ for the passwordEntered event accepts std::string as parameter, just like declared in the Dezyne model by using extern String $std::string$;. By calling the passwordEntered event with the input string, the data object is sent to the AlarmSystem. Within the System, the data object is passed to another component; the PWManager component in this case. Although this data object has no meaning for Dezyne model code, Dezyne can transport such data objects across components. Of course, this is a trivially easy example but it should give you an idea of how data gathered from one component can be handled in another component.

The last thing that needs to be done is the foreign implementation of the PWManager component’s behaviour. As an exercise, define and implement the PWManager. The correct password should be “Dezyne” and should only be accessible to the PWManager class itself.

Hint: in C++, you can use string::compare or the operator== to compare strings with one another (http://www.cplusplus.com/reference/string/string/compare/).

Solution:

PWManager.hh:

#include <string>
#include "skel_PWManager.hh"

class PWManager : public skel::PWManager {
  const std::string password = "Dezyne";

  bool iPWManager_verifyPassword(std::string pw);
public:
  PWManager(const dzn::locator& loc);
};

PWManager.cc:

#include "PWManager.hh"

PWManager::PWManager(const dzn::locator& loc) : skel::PWManager(loc) {
  //no op
}

bool PWManager::iPWManager_verifyPassword(std::string pw) {
  return pw.compare(this->password) == 0;
}

Next: , Previous: , Up: Dezyne Code Integration   [Contents]

3.6 Code Integration Summary

In the introduction of this section, the following tasks were mentioned:

In this section, you will find a quick summary on each of the learning goals and where they were discussed in the section.


Next: , Up: Code Integration Summary   [Contents]

3.6.1 Navigate through the essential areas of generated code

Throughout the section, code snippets from generated code were provided and key components in the generated code were highlighted. The intent is for you to be comfortable navigating through the code so that you can quickly find (and re-use!) what to implement in an inherited class or how to connect your event loop to the various System ports. In Inspecting the generated system you had a look at generated *.hh and *.cc files from a System component and in Implementation of events on interfaces and Implementing generated ‘skeleton' components you encountered generated code for behaviour components and ports.


Next: , Previous: , Up: Code Integration Summary   [Contents]

3.6.2 Create a environment for the generated code to run in

Most importantly, this means properly initializing the runtime objects, supplying an event loop and making sure that files are named correctly. Creating the C++ environment, Including and configuring the dzn runtime and Next step in integration detecting foreign components helped you in the initial steps of generating code, initializing the runtime and event loop and discovering which files need to be created. Compiling your application provided some recipes to make the overall process easier.


Next: , Previous: , Up: Code Integration Summary   [Contents]

3.6.3 Integrate every kind of event type in Dezyne with foreign code

This learning goal covers the bulk of the section, with many different examples on the various integration techniques. In Implementation of events on interfaces, the following table was provided as a reference of when to apply what action:

Port typeEvent typeUser action
Provides interface (on top of a component)InCall Dezyne function from handwritten code
OutAssign handwritten code to system function
Requires interface (on the bottom of a component)InAssign handwritten code to system function
OutCall Dezyne function from handwritten code

Calling a Dezyne function from handwritten code can be seen in the event loop where sensorTriggered and passwordEntered events were fired as well as the Timer implementation where a timeout event was fired into the System.

Assigning foreign implementations to System functions was done with lambda expressions for the Timer start and cancel. Wrapping implementations in lambda expressions is an easy way to create std::function objects which Dezyne-generated C++ uses to store event handlers.

An alternative, more cohesive way of providing foreign implementations is inheritance of skeleton components. This technique requires a bit more work to set up, but when set up properly it is both safer and it becomes easier to track the behavior of your application. Examples for this technique are the LED, Siren and PWManager components.

The idea is generally the same as in the provided table, where assigning foreign code is replaced by implementing pure virtual functions. For out-events on required ports and in-events on provided ports, the calling of a Dezyne function is performed on the respective port.


Next: , Previous: , Up: Code Integration Summary   [Contents]

3.6.4 Understand what the Dezyne runtime is and how it should be used within your own application

At this point you know enough about the runtime to successfully use it in your application; the instructions in Including and configuring the dzn runtime cover this. However, the locator and runtime can be used for various other things as well to make your life easier. This information will be discussed in the next section, Using the Dezyne locator to distribute runtime objects. What is explained there is not required to create a functional application, however there are some techniques that may prove useful for later projects.


Previous: , Up: Code Integration Summary   [Contents]

3.6.5 Compile an application consisting of foreign and generated code (in C++)

Compiling your application is, obviously, all about this specific learning goal. In this section, you can find an example makefile broken down into core features and quality of life improvements. If you followed the section from the start up until this point, you will have noticed that the provided makefile handles expansion of the application very well. You should also be able to re-use the makefile for other Dezyne C++ projects easily.


Next: , Previous: , Up: Dezyne Code Integration   [Contents]

3.7 Code integration – extra materials

During the course of this section on Dezyne code integration, you have followed the basic steps to successfully integrate code generated from a Dezyne model. In this section, you will find some additional materials regarding more advanced aspects of the code integration process. The following items will be covered:

If you are interested in learning more about features in the Dezyne modeling language, you are recommended to have a look at the next section, which discusses the usage of the external keyword in Dezyne. The current Controller model has a race condition with its usage of the Timer which you cannot find without the usage of external; in the next section you will learn more about increasing the robustness of your Dezyne models.


Next: , Up: Code integration -- extra materials   [Contents]

3.7.1 Using the Dezyne locator to distribute (runtime) objects

In one of the first sections of this section, you created instances of dzn::locator and dzn::runtime to be able to construct the generated System and its components. It was mentioned that dzn::locator can be used for more than distributing the runtime; otherwise it wouldn’t make sense to have a separate wrapper, of course.

In this section we will explore some of the default objects stored in the dzn::locator that are used by all Dezyne components as well as discuss how to use the dzn::locator to distribute your own objects throughout a System.

The way the dzn::locator works is it stores all sorts of objects by type. You can use the set() function on a locator object to store an object of a certain type T in the locator, which has two possible outcomes:


Next: , Up: Using the Dezyne locator to distribute runtime objects   [Contents]

3.7.1.1 Default runtime objects

The dzn::locator creates two objects that are used by all Dezyne components, namely an instance of std::clog (which is an object of type std::ostream) for logging purposes and a default dzn::illegal_handler:

struct locator
  {
  public:
    locator()
    {
      static illegal_handler ih;
      set(std::clog).set(ih);
    }

Next: , Previous: , Up: Using the Dezyne locator to distribute runtime objects   [Contents]

3.7.1.2 Custom dzn::illegal_handler

If you wish to not use the default dzn::illegal_handler, you can implement your own dzn::illegal_handler and store it in the locator. The default dzn::illegal_handler will then be overwritten and if an illegal assert occurs during the runtime of your application, the customized handler will be called. This is especially useful if your application consists of potentially dangerous hardware; if you can no longer guarantee the correctness of runtime software, you will want to shut down such hardware gracefully.

An alternative to using the illegal-handler to establish a safe pre-condition to terminating the application would be to write armour components to ensure that foreign code can never trigger an illegal. Armouring is a technique in Dezyne that can be used to guard control logic from spurious behaviour in foreign components; see <reference to Armouring documentation> for more information on this subject.


Next: , Previous: , Up: Using the Dezyne locator to distribute runtime objects   [Contents]

3.7.1.3 Alternative logging methods

Trace logging by all Dezyne components is hardwired to use the std::ostream object in the dzn::locator. If you wish to use your own logging rules, for instance if you would like to log to a file instead of logging straight to std::clog, you can do so by overwriting the std::clog object in the dzn::locator.

To do this, you need to create an std::ostream object that uses a file as output buffer; say we want to log to “log.txt”. std::ostream can not directly write to files, it can only write to buffers; so, you need to create a buffer that writes to “log.txt”. This can be done using std::ofstream as follows:

std::ofstream logfile("log.txt");
std::ostream outstream(nullptr);
outstream.rdbuf(logfile.rdbuf());

With std::ofstream, a filestream to “log.txt” is created. The buffer for this filestream can be accessed by calling the rdbuf() member function of logfile. The buffer that the std::ostream writes to can be set using the same rdbuf() function, on the std::ostream object this time. In the end, you will have an std::ostream object that uses a filestream as its output buffer.

If you then use set() with the custom std::ostream object, your Dezyne application will send all of the trace logging to “log.txt” instead of displaying it in the console output. This could be useful for logging remote applications where you don’t have access to console output, for example.


Previous: , Up: Using the Dezyne locator to distribute runtime objects   [Contents]

3.7.1.4 Distributing your own data

As mentioned in the introduction of this section, you can store any object in the dzn::locator, with the limitation that there can only be one object for any given type T in the locator at any point in time. Aside from overwriting runtime objects to provide a custom implementation, you can also use the locator to distribute data objects through the System, for example to be used in foreign components. Recall that foreign components are constructed by the System and their constructors require a dzn::locator by reference:

  Siren(const dzn::locator& loc);
  Sensor(const dzn::locator& loc);
  LED(const dzn::locator& loc);
  PWManager(const dzn::locator& loc);

Within the implementation of the constructor, you can retrieve objects from the locator that is passed as parameter. This can be useful for initializing hardware. In the example implementations, we used hard-coded values for the GPIO pins. With the dzn::locator, you can distribute an object containing hardware configurations gathered from command line arguments to make the application more dynamic. This would be done by using the set() function to inject a configuration object into the locator, followed by using try_get() in the constructor of a foreign component. try_get() will return a pointer to the object of type T if it is found, or null if it is not found.

Say we have the following configuration struct:

struct HWConfig {
  int GPIO_Red, GPIO_Green, GPIO_Blue;
};

In your main containing the event loop, you could initialize this struct with the use of command line parameters. If you then use set() on your locator with the initialized HWConfig struct, it will be stored in the locator. In the implementation of the LED constructor, you can do the following:

HWConfig *config = loc.try_get(HWConfig);
if(config) {
  this->PIN_RED = config->GPIO_Red;
  this->PIN_GREEN = config->GPIO_Green;
  this->PIN_BLUE = config->GPIO_Blue;
}

With this addition, the default GPIO pin definitions will be overwritten if you supplied a HWConfig struct in the dzn::locator. If you didn’t add the struct, try_get will not be able to find a HWConfig struct and will return 0, so the if-statement will not be entered. If this is the case, you can simply default to preconfigured values.


Next: , Previous: , Up: Code integration -- extra materials   [Contents]

3.7.2 Thread safety in the Dezyne execution model

The Dezyne language semantics assumes that at most one thread is active in a component at any time. If you are working in a purely single-threaded environment where no exceptions in the thread execution model of your application exist, this condition is easily met. However, most applications will probably end up containing some thread concurrency. At this point, you need to implement a thread safety mechanism to ensure that data remains valid and no concurrent (thread) access takes place while Dezyne logic is being executed.

The easiest way to do this in Dezyne is to generate a thread-safe-shell for your System component. This thread-safe-shell will wrap its internal components in such a way that every function call is placed in an event queue. This event queue is generated with the thread-safe-shell and ensures that events are handled one-by-one in a private thread. Foreign code can interact with the System on its ports like normal, but interactions are placed in the event queue and processed by the private thread.

The generation of a thread-safe-shell can be done using the command-line client and the following command:

dzn code -l c++ -s SYSTEM FILE

The above command will generate a thread-safe-shell for the System named SYSTEM that is defined in FILE. For the System, *.cc and *.hh files will be generated with some key differences to their counterparts that were generated without the --s option. In *.hh, the System struct now contains a dzn::pump object. dzn::pump is the object that represents the private thread and the associated event queue. In *.cc, the constructor for the System now also implements wrapper functions so that incoming events are handled by the dzn::pump thread instead of the calling thread. (Incoming events should be seen from the perspective of the System, so in-events on a provides port or out-events on a requires port)

Earlier in the section you were told that calling the timeout() function of the iTimer port is not safe by default (Timer and Siren integration). Calling an event from a signal handler is not safe by default. Signal handlers are similar to interrupt-service routines in the sense that they can be called while the process is involved in another function call.

With the default method of generating code from your System component, you run the risk of multiple active threads in the System. By generating a thread-safe-shell variant of the System, however, invoking the timeout event on the iTimer port will place the event in the event queue where it will be handled by the Dezyne private thread. With this change, thread safety is ensured without requiring any changes other than the code generation method. The easiest way to make the change is to add the following rule to the ‘generate’ make recipe:

generate: $(wildcard *.dzn)
	for f in $^; do dzn -v code --version=$(VERSION) -l c++ -o $(SRC) --depends=.d $$f; done
	dzn -v code --version=$(VERSION) -l c++ -o $(SRC) -s $(SYSTEMNAME) $(SYSTEMFILE) --depends=.d
	touch $ 

SYSTEMNAME and SYSTEMFILE are variables that should be defined in the makefile.


Previous: , Up: Code integration -- extra materials   [Contents]

3.7.3 Making use of private thread scheduling to poll hardware

A foreign component is able to by-pass the dzn::pump when sending events into the System. Consequently, this means it is no longer possible to guarantee the single-thread-active convention within the System. This can be avoided by interacting with the dzn::pump within the System.

To demonstrate how you can interact with the dzn::pump in a foreign component, the final component of the AlarmSystem will be implemented and integrated: the sensor. Again, a snapshot of the Dezyne models for this stage of the application can be found at <github link>.

For the Sensor, a hardware button was used that needs to be debounced for reliable input readings (https://www.arduino.cc/en/section/debounce). The debouncing algorithm provided in the Arduino section works on a polling basis, which the event loop for the AlarmSystem does not support. On top of that, polling the foreign Sensor component outside of the safe Dezyne thread can lead to undesirable effects. Both of these challenges can be solved by making use of the dzn::pump event queue in the foreign Sensor implementation. If you store the logic that requires polling in a separate poll() function and place the poll() event in the queue while the Sensor is active, the private Dezyne thread will handle the polling and thread safety remains intact.

Below you can find a foreign Sensor implementation that implements the Arduino example debouncing algorithm by the use of dzn::pump to ensure thread safety.

Sensor.hh:

#include "skel_Sensor.hh"
#include <dzn/pump.hh>

class Sensor : public skel::Sensor {
private:
  dzn::pump& pump;
  bool sensor_value;
  bool last_sensor_value;
  unsigned long last_dbnc_time;
  bool polling;

public:
  Sensor(const dzn::locator& loc);
  void iSensor_turnOn();
  void iSensor_turnOff();
  void poll();
};

Sensor.cc:

#include <dzn/locator.hh>
#include <dzn/runtime.hh>

#include <wiringPi.h>
#include "Sensor.hh"

const int DEBOUNCE_TIME = 50;
const int PIN_SENSOR = 16;

Sensor::Sensor(const dzn::locator& loc) : skel::Sensor(loc), pump(loc.get<dzn::pump>()) {
  wiringPiSetup();
  pinMode(PIN_SENSOR, INPUT);

  pullUpDnControl(PIN_SENSOR, PUD_UP);
  this->sensor_value = false;
  this->last_sensor_value = false;
  this->last_dbnc_time = 0;
  this->polling = false;
}

void Sensor::iSensor_turnOn() {
  this->polling = true;
  this->pump( [&] { this->poll(); } );
}

void Sensor::iSensor_turnOff() {
  this->polling = false;
}

void Sensor::poll() {
  int new_sensor_value = !digitalRead(PIN_SENSOR);

  if (new_sensor_value != this->last_sensor_value) {
    this->last_dbnc_time = millis();
  }

  if((millis() - last_dbnc_time) > DEBOUNCE_TIME) {

    if(new_sensor_value != this->sensor_value) {
      this->sensor_value = new_sensor_value;
      if(this->sensor_value) {
        this->pump( [&] { this->iSensor.out.triggered(); } );
      }
    }
  }
  this->last_sensor_value = new_sensor_value;
  if(this->polling) this->pump( [&] { this->poll(); } );
}

The interactions with the dzn::pump in the System are highlighted; the Sensor class has its own reference to the dzn::pump. This reference is set in the constructor by getting the System dzn::pump from the provided dzn::locator.

The usage of dzn::pump involves providing std::function objects of events that need to be handled. The easy way to do this is by wrapping functions in lambda expressions as can be seen in the above code snippet. Finally, a way to ensure that polling is continued while the Sensor is turned on is to have the poll() method store itself in the event queue recursively.


Previous: , Up: Dezyne Code Integration   [Contents]

3.8 Integrating code in other languages

In this section, we will consider the actions denoted in the table of required actions to integrate code in other languages than C++. The following languages will be covered: C#.

For reference, the relevant table is supplied:

Port typeEvent typeUser action
Provides interface (on top of a component)InCall Dezyne function from foreign code
OutAssign foreign code to system function
Requires interface (on the bottom of a component)InAssign foreign code to system function
OutCall Dezyne function from foreign code

The Dezyne models that are used in the examples can be found at https://github.com/VerumSoftwareTools/DezyneSection/tree/master/Code_Integration/Ch1_Starting_Point. Take note that we will be showing the integration steps only; we will not focus on the functional implementation.


Next: , Up: Integrating code in other languages   [Contents]

3.8.1 Integrating code in C#

Creating instances of the required runtime libraries is done similar to how it is done in C++. In C#, it is easier in the sense that no additional files must be included on a per-file basis. Preparing the runtime libraries is done as follows:

using System;

namespace MyDznApp {
  class main {
    private dzn.Locator dznLoc;
    private dzn.Runtime dznRt;

    public static void Main() {
      dznLoc = new dzn.Locator();
      dznRt = new dzn.Runtime();

      dznLoc.set(dznRt);
    }
  }
}

Take note that Locator and Runtime are located in the dzn namespace. Depending on the execution semantics of your application, you may choose to define the objects within the scope of Main or outside the scope (as can be seen above).

Creating an object to represent the System generated from Dezyne models requires you to pass the dzn.Locator object you created as parameter:

using System;

namespace MyDznApp {
  class main {
    private dzn.Locator dznLoc;
    private dzn.Runtime dznRt;
    private AlarmSystem as;

    public static void Main() {
      dznLoc = new dzn.Locator();
      dznRt = new dzn.Runtime();

      dznLoc.set(dznRt);
      as = new AlarmSystem(dznLoc);
    }
  }
}

In C#, events are generated as Action or Func objects, the C# variant of function objects. Action is used for void on events; Func is used for on events that have a return value. To reach an event on a port of a component, the following structure is applied in generated C#:

ComponentName.PortName.PortDirection.EventName, where ComponentName is the name of the data object representing the Component, PortName is the name of the Port you are trying to access, PortDirection is either inport or outport depending on the specification and EventName is the name of the on event you are trying to access.

As an example, let’s invoke the validPincode event on the provided iController port of the AlarmSystem (required action for Provides/in and Requires/out):

using System;

namespace MyDznApp {
  class main {
    private dzn.Locator dznLoc;
    private dzn.Runtime dznRt;
    private AlarmSystem as;

    public static void Main() {
      dznLoc = new dzn.Locator();
      dznRt = new dzn.Runtime();

      dznLoc.set(dznRt);
      as = new AlarmSystem(as);

      as.iController.inport.validPincode();
    }
  }
}

Here, the ComponentName is as; PortName is iController; PortDirection is import; EventName is validPincode.

Let’s assume the provided IController port has an out event void foo(). According to the table in the introduction of this section, Provides/out and Requires/in require you to assign foreign code to a System function. void foo() will be represented as an Action object, which we must assign foreign code to. To assign to an Action object, we can use a lambda expression:

using System;

namespace MyDznApp {
  class main {
    private dzn.Locator dznLoc;
    private dzn.Runtime dznRt;
    private AlarmSystem as;

    public static void Main() {
      dznLoc = new dzn.Locator();
      dznRt = new dzn.Runtime();

      dznLoc.set(dznRt);
      as = new AlarmSystem(as);
      as.iController.outport.foo = () => { /* Foreign implementation of foo() */};

      as.iController.inport.validPincode();
    }
  }
}

For more information on lambda expressions in C#, please refer to https://docs.microsoft.com/en-us/dotnet/csharp/programming-guide/statements-expressions-operators/lambda-expressions.


Previous: , Up: Integrating code in other languages   [Contents]

3.8.2 Foreign components in C#

The interface iLED is provided by the LED component, which is a foreign component and therefore not generated from your Dezyne models. The generated AlarmSystem System component does refer to an object of type LED, so you will have to make this object yourself. Take note that this object should not be contained in a namespace; the generated System refers directly to LED.

A prototype of an LED class that complies to the ILED interface is as follows:

class LED {
  public ILED iLed;

  public LED(dzn.Locator locator, String name = "", dzn.Meta parent = null) {
    iLed = new ILED();

    iLed.inport.setGreen = this.setGreen;
    iLed.inport.setYellow = this.setYellow;
    iLed.inport.setRed = this.setRed;
    iLed.inport.turnOff = this.turnOff;
  }

  public void setGreen() {}
  public void setYellow() {}
  public void setRed() {}
  public void turnOff() {}
}

The LED class has a public member named iLed of type ILED; the name of this member variable has to be the same as the name of the provided interface of the respective component in your Dezyne model. Then, in the constructor the events of ILED that are to be implemented are bound to the implementations within the LED class.


Next: , Previous: , Up: Top   [Contents]

4 Dezyne external

In this chapter we will

This chapter consists of two parts: first we will disclose some information on how simulation and verification by Dezyne works and what the effects are of using ‘external’. The second part of the tutorial will focus on designing a solution for the problems that can be found with ‘external’.

The nature of ‘external’ requires you to be able to think in terms of threads and sequencing of events across multiple threads. You will be assisted in this during the tutorial, but it helps if you are familiar with the concepts.

This chapter will build further upon the Alarm System models and foreign implementation from the previous chapters. With ‘external’, we will be able to discover interesting real-world behavior in the Alarm System that can lead to illegality in its components.


Next: , Up: Dezyne external   [Contents]

4.1 Why use external?

In this section, we will discuss a scenario of the Alarm System’s behavior where a delay in communication between two components results in a race condition that ultimately leads to illegal behavior. With this in mind, we will examine the Dezyne verification process and why standard verification does not find the race condition we discovered.

With this information, you should be able to understand when to use ‘external’ and what problems it can solve, as well as the impact of using ‘external’ in your Dezyne models.


Next: , Up: Why use external?   [Contents]

4.1.1 What can go wrong?

For the example in this section, a snapshot containing Dezyne models and C++ source code is available on https://github.com/VerumSoftwareTools/DezyneTutorial/tree/master/External/Ch1_Alarm_System.

Consider the following situation:

images/sequence_2

In the above sequence diagram, a valid password has been entered on the IController interface. This resulted in the Controller moving to the Armed state, turning on the Sensor as well.

images/watch_1

At this point the Sensor was triggered, resulting in the starting of the Timer as well as the Controller transitioning to the Alarming state. The corresponding Watch window with this sequence of events is included and it confirms that the Controller is in the Alarming state and that the Timer is Running.

Say we were to perform another passwordEntered event, with a valid password. The following sequence will occur:

images/sequence_3 images/watch_2

So far so good, right? The Dezyne model encounters no illegal behavior and the Watch window tells us that the Controller has moved back to the Armed state, ITimer is Idle again and the Sensor is Sensing.

An important remark to make at this point is that the passwordEntered event from iController led to a series of events that took an arbitrary amount of time, x. This is important to keep in mind for the next paragraph.


Next: , Previous: , Up: Why use external?   [Contents]

4.1.2 How does this translate to runtime execution?

In order to fully understand what can happen, it’s important to replay the above scenario in real-world context where time does matter. Recall that the code generated from the System required a thread-safe-shell to guarantee the single-thread-active property of the application (https://www.verum.com/supportitem/code-integration-extra-materials/). This was done by using a dzn::pump to schedule events on a First In, First Out (FIFO) basis for a private thread to handle.

After the first valid passwordEntered event, the Controller is Armed. If Armed, the triggered event from the Sensor leads to the Controller starting the timer. Let’s call this point t = 0. The timer is configured to timeout after 30 seconds as specified in the behavior, so the timeout event will be scheduled by the foreign Timer thread at t = 30.

Earlier it was noted that the execution time of the second passwordEntered event is x. Say a valid password is entered just before t = 30. It is now a possibility that during the execution x, t = 30 occurs which results in a timeout event being scheduled. However, after x, the Controller is in the Armed state. If you look at the behavior of the Controller component in the Armed state, a timeout event cannot be handled and as such is implicitly illegal:

state.Armed] {
  on iController.passwordEntered(pw): {
    bool valid = iPWManager.verifyPassword(pw);
    if(valid) {
      state = State.Unarmed;
      iLed.setGreen();
      iSensor.turnOff();
    }
  }
  on iSensor.triggered(): {
    state = State.Alarming;
    iTimer.start($30000$);
    iLed.setRed();
    iSensor.turnOff();
  }
}

Next: , Previous: , Up: Why use external?   [Contents]

4.1.3 Why does verification not catch this?

So now that we have considered a sequence of events in context of runtime behavior, we have found a trace that leads to a race condition triggering illegal behavior. Why doesn’t Dezyne show us this illegal behavior? If you verify the Controller component, it passes every test just fine. If you simulate the Controller component, you will not be able to send a timeout event during the handling of the passwordEntered event.

The reason behind this is that Dezyne verification does not account for the time it takes to execute a sequence of events. During verification, it is assumed that the execution of events occurs instantaneously. If events occur instantaneously, there can be no concurrency of events- there is no timespan in which multiple processes are active. As such, there is no time period x in the verification during which the timeout event can be scheduled. We have found a discrepancy between the behavior verified by Dezyne and the behavior of the generated code in a real-world environment: concurrency.

The absence of concurrency in the verified scenario means that only synchronous traces of events are considered. However, the scenario we found relies on asynchronous behavior of one of the foreign components. This asynchronous behavior can only come from a component that runs on its own execution thread. Using the ‘external’ keyword, you can indicate that the implementing component is active outside of the Dezyne private thread and therefore, extra behaviors must be considered by the Dezyne verification and simulation tools.


Previous: , Up: Why use external?   [Contents]

4.1.4 What does ‘external’ do and when should you use it?

The ‘external’ keyword is a modifier for requires interfaces of a component. Marking an interface as ‘external’ will increase its set of possible event sequences in the verification and simulation tools of Dezyne. More specifically, indicating that a requires interface is ‘external’ tells Dezyne that it should account for delays that can occur in communication through the interface. If the interface is stateful, this means that the two components on either end of the interface can get out of sync regarding the state of the protocol they use to communicate.

In the example with ITimer in the previous section, the Controller considers the state of Timer is Running when the cancel event is sent. However, the Timer has already timed out and has queued the timeout event accordingly. This is a textbook example of two components, Controller and Timer, being out of sync in regard to their perceived state of the protocol they use to communicate (ITimer). The result is that an unsuspecting Controller still receives a timeout it must handle even though the Controller is under the assumption that the Timer had been canceled.

If you modify the ITimer port of the Controller to requires external ITimer iTimer; and verify the Controller, you will actually find the illegal assert:

images/sequence_4

So, when should you use ‘external’? Right now, it might seem tempting to make every required port that sends out events ‘external’. However, its usage is not always warranted and as such you might be doing a lot of work for no benefit at all. The general rule of thumb:

Mark as ‘external’ any requires interface containing out-events that is delegated to the boundary of a system. Take note that the ‘external’ marking must be done in a behavior component, not a system component.

If a requires interface with out-events is implemented in a Dezyne component contained in the same system, the scheduling of said out-events will be done on the private Dezyne thread during runtime. The semantics enforced by the included Dezyne runtime simply prevent the component from scheduling any out-events while another component is executing its behaviour. Therefore, no race conditions between state and asynchronous events within the generated Dezyne framework can exist.

For more information on the Dezyne runtime semantics, please refer to https://www.verum.com/supportitem/execution-semantics/.

With proper inclusion of ‘external’ for components implemented outside of Dezyne, verification and simulation will once again consider the full scope of the possible behaviours of your application. As you saw in the previous sequence view, though, you have some work to do in the Controller component so that it can function correctly with an ‘external’ ITimer port. In the next section, we will explore some changes you can make to the implementation of a component to allow for ‘external’ behaviour.


Next: , Previous: , Up: Dezyne external   [Contents]

4.2 How to use ‘external’?

In this section, we will explore some possible changes you can make in component behaviour to support the usage of ‘external’ for required interfaces. In a few steps, you will discover:


Next: , Up: How to use ‘external'?   [Contents]

4.2.1 Responsibilities and using ‘external’ components

To make it easier to accommodate for concurrent behaviours found in ‘external’ ports, it is recommended to define another component that provides the ITimer interface and requires an external ITimer interface. Then, in the System component, bind the provided ITimer port of the new component to the required ITimer port of the Controller. From the Controller point of view, the ITimer port is no longer ‘external’. Instead, the new component (let’s call it RobustTimer) becomes responsible for translating the ‘external’ ITimer port to a regular ITimer port.

If you’ve performed the steps above, the situation should now look like this:

component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {

  }
}
images/system_7 images/system_8

Note that the required ‘external’ ITimer port on RobustTimer is coloured yellow; this is the case for all ports that are marked ‘external’. It is an easy way to identify these ports when looking at the System view. Note that the required ITimer port in Controller is no longer marked ‘external’.


Next: , Previous: , Up: How to use ‘external'?   [Contents]

4.2.2 How to start solving the problem you face with ‘external’

The RobustTimer component will be responsible for the mapping of an ‘external’ ITimer port to a regular ITimer port. The intent is to define the behaviour of the component in such a way that even if ‘external’ delays occur, communication over the provided ITimer port does not suffer from this.

The most straight-forward behaviour specification would be to map in-events on the provided ITimer port to in-events on the required ITimer port and to do the same for out-events of the required port. As a first exercise, implement the behaviour of RobustTimer this way.

Hint: make sure the states defined in the ITimer interface are followed in the RobustTimer component behaviour as well.

Solution:

component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Idle;
      }
      [state.Idle] { }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
    }
  }
}

The above solution is a first rudimentary step towards a working solution. If you verify the RobustTimer component, you will see the exact same illegal assertion as we found earlier in the previous section. However, this time it is extracted from all interleaving with other required and provided ports of the Controller component and you can focus solely on the behaviour of the required ‘external’ ITimer port. Let’s reconsider the timeline described in How does this translate to runtime execution?:

images/sequence_5

Recall that x is the time it takes for the cancel event from iTimer to be processed. During x, the timeout occurs on ext_iTimer and is queued accordingly. After x, RobustTimer is in the Idle state but still has to handle the queued timeout. This scenario is not described in the behaviour of RobustTimer and as such, it is implicitly illegal.

In the next section, we will have a look at how to implement behaviour such that these possible concurrencies discovered by ‘external’ can be handled.


Next: , Previous: , Up: How to use ‘external'?   [Contents]

4.2.3 Implementing the solution as component behaviour

Now that the RobustTimer component has been created and the rudimentary communication between the provided ITimer and required ‘external’ ITimer has been established, it is time to start working towards a functional solution that is verifiably correct.

A logical first step could be to specify that when ext_iTimer sends a timeout event to the RobustTimer while RobustTimer is not in a Running state, the timeout event is ignored (so no operation occurs). This ensures that within the RobustTimer component, possibly delayed timeouts do not trigger illegal behaviour if the cancel event had already occurred.

As an exercise, make the aforementioned change to the handling of ext_iTimer.timeout() and verify the RobustTimer again. Try to figure out what has happened in the scenario that the verifier shows you before moving on.

Solution:

component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Idle;
      }
      [state.Idle] { }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
      [state.Idle] {}
    }
  }
}
images/sequence_6

The scenario shown to you by the verifier is one where a ‘timeout’ event sent in response to the first ‘start’ is misinterpreted by RobustTimer as if it was sent in response to the second ‘start’ event; however, ext_iTimer is Running while the timeout event is processed. After propagating the timeout event to iTimer, iTimer is Idle once again, allowing for a start event to occur. While ext_iTimer is Running, start events are illegal.

Nonetheless, the length of the trace has increased, indicating that we have passed the first hurdle of illegal timeouts after the timer had already been cancelled. Progress has been made, but we’re not quite there yet.

We need to implement some way to distinguish between outdated timeout events and timeout events from the timer that was currently started. Let’s refer to the time window between a timer start and a timeout or cancel as a session. There are two ways to approach this situation: keep track of the current session and ignore others, or implement a handshake to ensure that a session is closed before starting a new one.


Previous: , Up: How to use ‘external'?   [Contents]

4.2.4 ‘The’ solution: handshake protocol

The recommended option is to implement a handshake mechanism to ensure that the current session is closed. If you recall, the original problem we discovered was that it was possible to queue a timeout event while the timer was being cancelled. The description of the problem already hints at part of the solution: apparently there exists a state where the Timer is being cancelled. This state starts when the cancel event is sent and ends at some point in time.

When the being cancelled state has ended, this means that the Timer has fully stopped and as such, no timeout events can occur anymore. If you queue a notification that this condition is fulfilled, this notification can be used to denote the end of a Timer session.

As an exercise, extend the ITimer interface with a Stopping state that starts when a Running timer is cancelled. Within the Stopping state, in-events should be illegal and inevitably, an out-event cancelled should be sent.

Solution:

interface ITimer {
  extern long_integer $long$;
  enum State { Idle, Running, Stopping };
  in void start(long_integer milliseconds);
  in void cancel();
  out void timeout();
  out void cancelled();

  behaviour {
    State state = State.Idle;

    [state.Idle] {
      on start: state = State.Running;
      on cancel: { }
    }

    [state.Running] {
      on start: illegal;
      on cancel: state = State.Stopping;
      on inevitable: {
        state = State.Idle;
        timeout;
      }
    }

    [state.Stopping] {
      on start: illegal;
      on cancel: illegal;
      on inevitable: {
        state = State.Idle;
        cancelled;
      }
    }
  }
}

With the above interface modification, a handshake protocol can be supported where the end of a Timer session is marked with a cancelled event. You may find yourself wondering why this is so useful.

Here’s the trick: the event that marks the end of a session travels through the same communication channel as the timeout events. The interface prohibits sending timeouts during the Stopping state and the Stopping state transitions to the Idle state where again, no timeouts can be sent. Therefore, it is guaranteed that there will be no more timeout events from the previous session after the cancelled event has been placed into the queue.

So, the modified ITimer interface complies with the handshake we want to implement to solve the ‘external’ delay problem. What remains to be done is update the RobustTimer component behaviour to make use of the newly added handshake.

The behaviour we want to add to the RobustTimer is the addition of the Stopping state. When a cancel event is sent to its provided ITimer port, this is propagated to the ‘external’ ITimer port and the RobustTimer transitions to the Stopping state. Until the ‘external’ ITimer port has replied with a cancelled event, any timeouts coming through the port while Stopping should be silently discarded. When the cancelled event is handled, the RobustTimer transitions back to the Idle state and the cancelled event is propagated to the provided ITimer.

As an exercise, add the changes listed above to the behaviour of the RobustTimer component.

Solution:

component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running, Stopping };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Stopping;
      }
      [state.Idle] { }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
      [state.Stopping] { /* discard */ }
    }

    on ext_iTimer.cancelled(): {
      [state.Stopping] {
        iTimer.cancelled();
        state = State.Idle;
      }
    }
  }
}

If you verify the behaviour in the above solution, you will still encounter one last verification error. While we were focussing on making sure possibly delayed timeouts are properly handled, we didn’t implement the handshake we designed for that purpose in the scenario where an Idle Timer receives a cancel event. Luckily, the fix for this is a pretty simple one:

interface ITimer {
  // variable and event declarations
  behaviour {
    [state.Idle] {
      on start: state = State.Running;
      on cancel: { cancelled; }
    }
    // rest of the behaviour specification
component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    // variable declarations
    on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Stopping;
      }
      [state.Idle] { iTimer.cancelled(); }
    }
    // rest of the component implementation

With these additions in place, the RobustTimer component will pass verification and you have successfully implemented a protocol that is robust against possibly delayed asynchronous events from a foreign component. By doing this in a Dezyne component, any other component that is connected to the ITimer port provided by RobustTimer can use it as if it were not ‘external’. Only the RobustTimer component is responsible for handling the ‘external’ behaviour.

In the next and final section, we will have a look at what needs to be updated in the rest of the Alarm System and afterwards we will take a step back and summarise what we’ve discovered throughout this tutorial.


Next: , Previous: , Up: Dezyne external   [Contents]

4.3 Finishing the Alarm System

In the previous section, you successfully implemented the behaviour of a component such that it still behaves correctly if communication over a port is potentially delayed. In this section, we will have a look at what needs to be done to make the rest of the Alarm System up to date and if any changes need to be made to foreign code.


Next: , Up: Finishing the Alarm System   [Contents]

4.3.1 Updating the Controller

A snapshot containing Dezyne models and foreign code for the current state of the Alarm System can be found on https://github.com/VerumSoftwareTools/DezyneTutorial/tree/master/External/Ch3_Current_State.

images/error_msg_2

Although the Controller hasn’t been changed at all, the ITimer interface that it requires has changed. If you verify the Controller, you will find that the iTimer.cancelled event is (implicitly) illegal:

What has happened is that an out-event was added to the ITimer interface that is not handled in the Controller behaviour. Therefore, it is implicitly illegal. To avoid this, the behaviour of the Controller component should be modified such that it can handle the cancelled event from its required ITimer port.

Just like we added an extra state to the behaviour of the RobustTimer to indicate that it was in between the Running and Idle states, it makes sense to add a state to the Controller that indicates it is “waiting” for its Timer port to be fully cancelled. As the cancellation of an active Timer occurs during the transition from Alarming to Armed, the suggested state to be added is Rearming. As an exercise, add this Rearming state to the behaviour of the Controller component.

Solution:

component Controller {
  provides IController iController;
  requires ISiren iSiren;
  requires ILED iLed;
  requires ITimer iTimer;
  requires IPWManager iPWManager;
  requires ISensor iSensor;

  behaviour {
    enum State { Unarmed, Armed, Alarming, Rearming };
    State state = State.Unarmed;

    [state.Unarmed] {
      on iController.passwordEntered(pw): {
        bool valid = iPWManager.verifyPassword(pw);
        if(valid) {
          state = State.Armed;
          iLed.setYellow();
          iSensor.turnOn();
        }
      }
      on iSensor.triggered(): {}
      on iTimer.timeout(): illegal;
    }
    [state.Armed] {
      on iController.passwordEntered(pw): {
        bool valid = iPWManager.verifyPassword(pw);
        if(valid) {
          state = State.Unarmed;
          iLed.setGreen();
          iSensor.turnOff();
        }
      }
      on iSensor.triggered(): {
        state = State.Alarming;
        iTimer.start($30000$);
        iLed.setRed();
        iSensor.turnOff();
      }
      on iTimer.timeout(): illegal;
    }
    [state.Rearming] {

    }
    [state.Alarming] {
      on iController.passwordEntered(pw): {
        bool valid = iPWManager.verifyPassword(pw);
        if(valid) {
          state = State.Rearming;
          iLed.setYellow();
          iSiren.turnOff();
          iTimer.cancel();
          iSensor.turnOn();
        }
      }
      on iSensor.triggered(): {}
      on iTimer.timeout(): {
        iSiren.turnOn();
      }
    }
  }
}

Of course, simply adding a state is not enough, you will also need to handle events if the Controller is in the Rearming state. If a cancelled event comes in from the ITimer port, the Controller should transition to the Armed state. While the Controller is Rearming, incoming passwords and Sensor triggers are silently discarded. As an exercise, implement the described behaviour in the Rearming state.

Solution:

[state.Rearming] {
  on iController.passwordEntered(pw): {}
  on iSensor.triggered(): {}
  on iTimer.cancelled(): state = State.Armed;
}

With the above solution in place, the Controller component will successfully pass verification when using the new ITimer interface. The last thing that then needs to be modified is the foreign implementation of the Timer, so that accurately reflects the ITimer changes as well.

As a bonus exercise, you may want to consider checking the validity of a password that was entered during the Rearming state. If the password is valid, receiving the cancelled event could make the Controller transition straight to the Unarmed state.

Solution: (take note that some unchanged pieces of code are left out for the purpose of this document)

component Controller {
  /* provides/requires interfaces */

  behaviour {
    enum State { Unarmed, Armed, Alarming, Rearming };
    State state = State.Unarmed;
    bool correctPasswordQueued = false;

    [state.Unarmed] {
      /* behaviour unchanged */
    }
    [state.Armed] {
      /* behaviour unchanged */
    }
    [state.Rearming] {
      on iController.passwordEntered(pw): correctPasswordQueued = iPWManager.verifyPassword(pw);
      on iSensor.triggered(): {}
      on iTimer.cancelled(): {
        if(correctPasswordQueued) {
          state = State.Unarmed;
          iLed.setGreen();
          correctPasswordQueued = false;
        }
        else {
          state = State.Armed;
          iLed.setYellow();
          iSensor.turnOn();
        }
      }
    }
    [state.Alarming] {
      on iController.passwordEntered(pw): {
        bool valid = iPWManager.verifyPassword(pw);
        if(valid) {
          state = State.Rearming;
          iTimer.cancel();
          iSiren.turnOff();
        }
      }
      on iSensor.triggered(): {}
      on iTimer.timeout(): {
        iSiren.turnOn();
      }
    }
  }
}

Previous: , Up: Finishing the Alarm System   [Contents]

4.3.2 Updating the foreign Timer

By adding the cancelled out-event to the ITimer interface, we added a function to the System boundary (the System still requires an ITimer port) that needs to be called from foreign code. As we are generating a thread-safe-shell for the System, it is permitted to call the event directly from foreign code; queueing it in the System dzn::pump is done by default.

As an exercise, add the calling of the cancelled event to the foreign Timer implementation (found in main.cc).

Solution:

int main(int argc, char* argv[])
{
  dzn::locator loc;
  dzn::runtime rt;
  std::ofstream logfile("log.txt");
  std::ostream outstream(nullptr);
  outstream.rdbuf(logfile.rdbuf());

  loc.set(rt).set(outstream);

  AlarmSystem as(loc);
  as.dzn_meta.name = "AlarmSystem";

  as.iTimer.in.start = [] (int ms) { alarm(ms/1000); };
  as.iTimer.in.cancel = [&] () { alarm(0); as.iTimer.out.cancelled(); };
  timeout = as.iTimer.out.timeout;
  signal(SIGALRM, sigalrm_handler);

  as.check_bindings();

  std::string input;
  while(std::cin >> input) {
    as.iController.in.passwordEntered(input);
  }
}

With this final addition in place, you will have a fully correct implementation of the ITimer interface that is verified to always correctly deal with possible race conditions that are caused by dzn::pump queue delay. If such delays occur, they are handled by the RobustTimer Dezyne component which is verifiably correct.

The final Dezyne models and Alarm System foreign source code can be found on GitHub: https://github.com/VerumSoftwareTools/DezyneTutorial/tree/master/External/Ch4_Final_State

A future tutorial on the ‘blocking’ keyword will show you a way to make use of ‘external’ with even less modifications to surrounding components, if your execution model allows it. For now, let’s reflect on what we’ve learned in this tutorial in the next and final section.


Previous: , Up: Dezyne external   [Contents]

4.4 Dezyne external Summary

In the introduction of this tutorial, the following tasks were mentioned:


Next: , Up: Dezyne external Summary   [Contents]

4.4.1 Understand when to use ‘external’ and what problems it solves

Mark as ‘external’ any requires interface containing out-events that is delegated to the boundary of a system. This was discussed at length in What does ‘external' do and when should you use it? after an analysis of the Alarm System implementation we made in earlier tutorials showed that illegal behaviour could occur.


Next: , Previous: , Up: Dezyne external Summary   [Contents]

4.4.2 Understand the impact of using the ‘external’ keyword in your Dezyne models

Coincidentally, this was discussed before the answer to the previous learning goal was given. An analysis of why Dezyne did not warn you about this illegal behaviour in Why does verification not catch this? can also be used to explain the impact of using ‘external’: an extra set of behaviours is considered during verification so that possible delays due to external communications are included.


Next: , Previous: , Up: Dezyne external Summary   [Contents]

4.4.3 Identify where to implement additional logic in your models to support the usage of ‘external’

In How to use ‘external'?, two important considerations were given as to how you should implement ‘external’ in your models. Firstly, in Responsibilities and using ‘external' components it is recommended to create a new component that maps an external requires port to a provided port of the same type. This is so that you don’t pollute other components with logic only concerning ‘external’ behaviour. Then, in ‘The' solution handshake protocol a handshake was added to the interface so that the state of the two ports can be synchronized.


Previous: , Up: Dezyne external Summary   [Contents]

4.4.4 Use the Dezyne verification & simulation tools to correctly implement a solution using the ‘external’ keyword

Information regarding this learning goal was present all throughout the tutorial. However, by implementing the solution in a Dezyne component as opposed to doing it in foreign code, you ensure that you are making full use of the Dezyne toolkit and benefit from its verification and simulation capabilities.


Next: , Previous: , Up: Top   [Contents]

5 Dezyne blocking

In this chapter, we will

We will reconsider an implementation that handles possibly delayed communication over an ‘external’ port from the previous chapter.

The behaviour described with the ‘blocking’ keyword requires you to be able to reason about your application in terms of active threads and their calling context. In the tutorial, various examples will be discussed but it helps if you are familiar with the concepts.

Usage of ‘blocking’ requires the System it is contained in to be generated with a thread-safe-shell. For more information on the thread-safe-shell, please refer to https://www.verum.com/supportitem/code-integration-extra-materials/ and https://www.verum.com/supportitem/thread-safe-shell/.


Next: , Up: Dezyne blocking   [Contents]

5.1 What can ‘blocking’ be used for?

For the examples in this section, a snapshot containing Dezyne models and C++ source code is available on https://github.com/VerumSoftwareTools/DezyneTutorial/tree/master/Blocking/Ch1_Starting_Point.

In the chapter on the usage of the ‘external’ keyword, we successfully implemented a RobustTimer component that maps an ‘external’ requires ITimer port to a regular provides ITimer port. In order to fully capture the possible behaviours that occur when considering the port to be ‘external’, an extra out-event was added to mark the end of the cancellation transaction:

—————————— Before ———————————————————— After ——————————
interface ITimer {
  extern long_integer $long$;
  enum State { Idle, Running, Stopping };
  in void start(long_integer milliseconds);
  in void cancel();
  out void timeout();
  behaviour {
    State state = State.Idle;
    [state.Idle] {
      on start: state = State.Running;
      on cancel: { }
    }
    [state.Running] {
      on start: illegal;
      on cancel: state = State.Idle;
      on inevitable: {
        state = State.Idle;
        timeout;
      }
    }
  }
}









interface ITimer {
  extern long_integer $long$;
  enum State { Idle, Running, Stopping };
  in void start(long_integer milliseconds);
  in void cancel();
  out void timeout();
  out void cancelled();
  behaviour {
    State state = State.Idle;
    [state.Idle] {
      on start: state = State.Running;
      on cancel: { cancelled; }
    }
    [state.Running] {
      on start: illegal;
      on cancel: state = State.Stopping;
      on inevitable: {
        state = State.Idle;
        timeout;
      }
    }
    [state.Stopping] {
      on start: illegal;
      on cancel: illegal;
      on inevitable: {
        state = State.Idle;
        cancelled;
      }
    }
  }
}

This addition allowed the RobustTimer component to determine whether the ‘external’ requires port was free of any delayed timeout events. This was required to ensure that a new Timer could safely be started after cancelling an older one.

However, this change also had implications for other components that require ITimer ports. Originally, one of the reasons to create the RobustTimer component was to hide the complexity paired with ‘external’ behaviours from the Controller component. Ultimately, due to the changes made to the ITimer interface to accommodate for extra behaviours, we still had to make changes to the Controller component. Handling the asynchronous cancelled event had to be added to the behaviour of the Controller.

This phenomenon where changes lower down in the chain of command influence top-level components is what we will refer to as contagious asynchronicity. Because of asynchronous behaviour that was added to one of the lower components in the System, components higher up in the System are forced to accommodate for this asynchronous behaviour as well.

This is not always a bad thing- sometimes it is actually desired to propagate such events upwards so that perceived state of a subcomponent is updated. However, there are also cases where this additional information on the state of a subcomponent is irrelevant and as such, you do not want to deal with the added asynchronous behaviour of components. This is where ‘blocking’ comes into play; using ‘blocking’, it becomes possible to convert certain asynchronous behaviour patterns to synchronous versions.

In the case of the RobustTimer, ‘blocking’ will allow you to implement the cancellation process in such a way that it appears synchronous over the provides port even though it is asynchronous with respect to its requires port. In the next section, you will learn how to perform such an implementation.


Next: , Previous: , Up: Dezyne blocking   [Contents]

5.2 Simplifying an ‘external’ implementation using ‘blocking’

In this section, we will take a look at describing an asynchronous process as if it were synchronous. We will do this by use of the ‘blocking’ keyword. The asynchronous process we will be considering is the cancelling of RobustTimer. In case you hadn’t had a look at the snapshot containing Dezyne models and C++ source code already, it is available on https://github.com/VerumSoftwareTools/DezyneTutorial/tree/master/Blocking/Ch1_Starting_Point.


Up: Simplifying an ‘external' implementation using ‘blocking'   [Contents]

5.2.1 Changing RobustTimer to provide a synchronous Timer interface

The goal is to make RobustTimer easier to use with respect to its provided port. We will still want the newer version of the ITimer interface to fully describe the behaviour of the ‘external’ requires port, but we want to translate this to a simplified version of ITimer. The original ITimer interface will suffice. As an exercise, perform the following tasks:

Solution: see https://github.com/VerumSoftwareTools/DezyneTutorial/blob/master/Blocking/Ch2_Solution/Timer.dzn

These changes will break several parts of the application, but let’s focus on RobustTimer only for now. The cancellation process was quite nasty; a cancel event on its provided ITimer port started the process, at which point the provided ITimer port was unusable until the cancelled event from ext_iTimer came in. By separating the provides and requires interfaces, you are no longer forced to describe this period of unusability in the provides interface. From the provides port point of view, the cancellation process is synchronous again; all that remains is to make sure the RobustTimer component is verifiably correct with the new provides/requires ports.

The beginning of the cancellation process is the cancel event on the provided iTimer; the mark that denotes the end of the process is the cancelled event from the required ext_iTimer. ‘blocking’ allows you to postpone the return of an incoming event from a provides port until an event comes in from a different port; this sounds exactly like the scenario of the cancellation process.

In RobustTimer, there are two locations where the cancellation process is ended, both currently marked by the iTimer.cancelled() event left over from the previous iteration of RobustTimer. If we were to denote the iTimer.cancel() event as ‘blocking’, the ending of the transaction will be in the same locations as the current iTimer.cancelled() events:

component RobustTimer {
  provides ITimer iTimer;
  requires external AsyncITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running, Stopping };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    blocking on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Stopping;
      }
      [state.Idle] { iTimer.reply(); }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
      [state.Stopping] { /* discard */ }
    }

    on ext_iTimer.cancelled(): {
      [state.Stopping] {
        state = State.Idle;
        iTimer.reply();
      }
    }
  }
}

Note that the transaction endpoints are represented as port.reply() events. An important thing to keep in mind is that with ‘blocking’, you block the calling thread of the event until the blockage is lifted- which is done with the port.reply() event. The modified RobustTimer posted above is verifiably correct and will display the following behaviour:

On iTimer.cancel, the iTimer port is blocked. If the RobustTimer is Running, the cancel event will be sent to ext_iTimer and RobustTimer will transition to the Stopping state. In the Stopping state, the asynchronous ext_iTimer.cancelled event will release the blocked iTimer port. If RobustTimer was Idle upon receiving iTimer.cancel, the blocked iTimer port is immediately released.

This immediate release of the blocked iTimer port hints at a possible optimization; if a port is released instantly then it doesn’t really have to be blocked at all. By nesting the ‘blocking’ keyword deeper into the [guard]-on event scope you can avoid this unnecessary blockage:

component RobustTimer {
  provides ITimer iTimer;
  requires external AsyncITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running, Stopping };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    on iTimer.cancel(): {
      blocking [state.Running] {
        ext_iTimer.cancel();
        state = State.Stopping;
      }
      [state.Idle] { }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
      [state.Stopping] { /* discard */ }
    }

    on ext_iTimer.cancelled(): {
      [state.Stopping] {
        state = State.Idle;
        iTimer.reply();
      }
    }
  }
}

With the changes highlighted above, the ‘blocking’ keyword is nested deeper and affects fewer behaviour traces; the net behaviour is the same. Note that when on-event behaviour is not marked as blocking, a void port.reply() event is not allowed; hence, [state.Idle] now shows as no-op instead of port.reply(). The continuation is implicit when the on-event is not ‘blocking’.

From the perspective of the iTimer port, the cancellation process is now synchronous; a cancel event sent through the iTimer port will not return until the cancellation process has been completed. RobustTimer can still make use of the asynchronous specification of AsyncITimer to facilitate the cancellation handshake. Therefore, the asynchronous behaviour has successfully been made synchronous by using the ‘blocking’ keyword.

With the changes made to the provides interface of RobustTimer, you should also repair the Controller and AlarmSystem components. The Rearming state in the Controller can be removed as the cancellation process is synchronized. In AlarmSystem, some port types will have to be renamed to reflect the new interface names. As an exercise, fix the models so they are free of errors again.

Solution: the final versions of the models in the AlarmSystem application can be found on https://github.com/VerumSoftwareTools/DezyneTutorial/tree/master/Blocking/Ch2_Final

Unlike in the ‘external’ chapter, no foreign source code will have to be changed. All of the simplifications that were made are in Dezyne models and the foreign components and ports on the boundary of the System remain unchanged. The only requirement to be able to use ‘blocking’ is that your System is generated with a thread-safe-shell (and for now, only C++ is supported). The generation of a thread-safe-shell is included in the makefile, therefore the AlarmSystem application is fully functional again.

Now that we have implemented a simplification of the asynchronous ITimer interface, let’s consider some implications this will have for the runtime behaviour of the AlarmSystem application in the next section.


Next: , Previous: , Up: Dezyne blocking   [Contents]

5.3 ‘blocking’ behaviour in runtime context

Although ‘blocking’ has allowed you to make the Controller model much simpler, ‘blocking’ may not always be as useful or runtime semantics might prevent you from using ‘blocking’ at all in an application. In this section, we will consider the runtime behaviour of the changes we made to RobustTimer and consider some limitations to the usage of ‘blocking’.


Next: , Up: ‘blocking' behaviour in runtime context   [Contents]

5.3.1 Blocking Runtime behaviour

For simplicity’s sake, we will consider two active threads in this analysis: the main thread, running the event loop, and the Dezyne private thread, consuming events from dzn::pump.

The behaviour we described as ‘blocking’ is the cancellation process of the Timer. This process is started when in the Alarming state, a valid password is entered. Password entry is done through the passwordEntered event on the IController port of the AlarmSystem. This is where the call stack begins: invoking passwordEntered from the main thread.

Because AlarmSystem is generated with a thread-safe-shell, invoking the passwordEntered event is done with the dzn::shell functionality from the Dezyne runtime libraries. This means the main thread will be blocked until the Dezyne private thread has completed processing the event. Important: this is not because of ‘blocking’! This behaviour is fully because of the thread-safe-shell.

Once the event is scheduled in dzn::pump, at some point in time it will be picked up by the Dezyne private thread. Part of the processing of the passwordEntered event is the ‘blocking’ iTimer.cancel call:

images/sequence_7

The processing of the passwordEntered event is done on the Dezyne private thread, but remember that the main thread is blocked until the related return statement is sent (signaling that the event has been fully processed). Now, when the Dezyne private thread invokes the iTimer.cancel event, it will encounter ‘blocking’ as the implementation of iTimer.cancel in RobustTimer is ‘blocking’:

images/sequence_8

The Dezyne runtime libraries provide support for ‘blocking’ in the sense that an execution on the Dezyne private thread can be suspended and released again, which ‘blocking’ makes use of. Invoking a ‘blocking’ event suspends the execution of the current event from the dzn::pump and starts execution of the next available event. This subtle implementation in the Dezyne runtime is how the blocked execution can be released again; the release will occur from another event scheduled in dzn::pump. In the figure above, this other event is ext_iTimer.cancelled. When the execution is released, the Dezyne private thread can continue processing the iTimer.cancel event which eventually returns and both threads are released again.


Previous: , Up: ‘blocking' behaviour in runtime context   [Contents]

5.3.2 Implications of ‘blocking’ for Dezyne applications

Obviously, a big concern regarding whether you can use ‘blocking’ in your Dezyne models is that your foreign code running on the main thread must not suffer from being blocked. The Sensor polling implementation could just as easily have been handled in the event loop instead of through dzn::pump; however, then the debouncing algorithm could suffer from not polling consistently. The current event loop only handles the entering of passwords; this is so trivial that blockage is not a concern. However, when more execution takes place on the main thread you will have to make sure that it is allowed to be postponed until the blocking call returns.

A second concern is that the execution semantics of your platform of choice must support some way to schedule events outside of normal main thread activity. If the main thread is blocked and the private Dezyne thread is waiting for events in dzn::pump, the only way to continue is to have some sort of activity outside of the two existing threads. This activity can then release the Dezyne private thread, which can release the main thread again. Examples of such activity are Interrupt Service Routines (ISRs) or raising a signal like in the foreign Timer implementation.

Another consideration you should make is whether the asynchronous process you’re simplifying with ‘blocking’ even benefits from it. RobustTimer could be simplified even more by having a ‘blocking’ start event that returns upon timeout. This would make the components requiring ITimer even simpler, perhaps, but it would no longer be possible to cancel the timer.

In a way, we even removed functionality from Controller by synchronizing the cancellation process; at the end of the ‘external’ chapter, we implemented a “queue” to allow passwords entered during the cancellation to be stored and handled when the process ends. By hiding this process from Controller, such interactions are no longer necessary. Sometimes you can make clever use of the asynchronous period and if that is the case, you will have to consider whether the simplified models outweigh the clever usage.

All in all, there are some hard and some soft constraints to using the ‘blocking’ keyword: hard constraints are the execution model on your main thread and whether it can handle being blocked for an arbitrary amount of time; soft constraints mostly consist of design decisions and whether you can make use of the asynchronous process or not.


Previous: , Up: Dezyne blocking   [Contents]

5.4 Summary of Dezyne blocking

In the introduction of this chapter, the following tasks were mentioned:


Next: , Up: Summary of Dezyne blocking   [Contents]

5.4.1 Understand what ‘blocking’ allows you to do in Dezyne

Using ‘blocking’, it becomes possible to describe certain asynchronous behaviour patterns as if they were synchronous. By hiding the asynchronicity of a process, components higher up in a system are simplified. This was discussed in What can ‘blocking' be used for?


Next: , Previous: , Up: Summary of Dezyne blocking   [Contents]

5.4.2 Simplify an ‘external’ implementation with usage of ‘blocking’

In Changing RobustTimer to provide a synchronous Timer interface, changes were made to RobustTimer to provide a blocking synchronous cancel event. This event starts an asynchronous process in RobustTimer where the end of the process signals the return of the ‘blocking’ event.


Next: , Previous: , Up: Summary of Dezyne blocking   [Contents]

5.4.3 Identify when ‘blocking’ may be used and when it may not be used

Following an analysis of a ‘blocking’ process in Blocking Runtime behaviour, some hard constraints were identified in Implications of ‘blocking' for Dezyne applications: the main thread must not suffer from being blocked and the target platform must support some way to provide activity when the main thread is blocked.


Previous: , Up: Summary of Dezyne blocking   [Contents]

5.4.4 Reason about design decisions when using the ‘blocking’ keyword

Besides hard constraints, Implications of ‘blocking' for Dezyne applications also provides example situations where the usage of ‘blocking’ may or may not be warranted. Considerations to take into account are whether the period of asynchronicity can be used for other purposes. Due to contagious asynchronicity, other components may be simplified by usage of ‘blocking’, which could have implications for the layer of a system you wish to implement ‘blocking’ in.


Next: , Previous: , Up: Top   [Contents]

6 Dezyne async

In this chapter, we will

The behaviour described with the ‘async’ keyword requires you to be able to reason about your application in terms of active threads and their calling context and synchronous / asynchronous calling concepts. In the tutorial, various examples will be discussed but it helps if you are familiar with these concepts. It is best to be familiar with the ‘blocking’ keyword before studying this chapter. Usage of ‘async’ requires the availability of an event pump in the System it is contained in. An event pump is generated automatically with the generation of a thread-safe-shell. For more information read an article about the event pump and one about the thread-safe shell.


Next: , Up: Dezyne async   [Contents]

6.1 What is the Bare Function of ‘async’?

In the chapter on the usage of the ‘blocking’ keyword, we implemented a situation where a synchronous event call was mapped on an asynchronous reply. The use of the ‘async’ keyword is to support the reciprocal situation: an asynchronous event call is mapped on a synchronous reply. As you can imagine this requires some dedicated internal processing. In normal situation an asynchronous event call returns and a new external trigger is required to eventually generate the asynchronous reply. In this ‘async’ case the caller of the event should not notice it gets an immediate response. By some runtime magic the asynchronous reply event is generated automatically without requiring an external trigger. This may sound a bit puzzling still but in the next example it will become clear what is happening. The interface declares an asynchronous input event e and a (related) asynchronous output event a. The fact of the void reply value of the input event already indicates it cannot return anything synchronously. In the component at the highlighted line a special internal port is declared as dzn.async. The name of the port is ‘defer’. The type dzn.async is defined inside Dezyne and it has a number of predefined functions. In this example we use:

In the declaration of the internal port we added a parameter ‘t’ of type ‘T’ that can be used in all functions of the port.

extern T $int$;

interface i
{
  in void e(T t);
  out void a(T t);
  behaviour {
    bool idle = true;
    [idle] on e: idle=false;
    [!idle] {
      on inevitable: {idle=true;a;}
      on e: illegal;
    }
  }
}

component async_hello
{
  provides i p;
  behaviour {
    requires dzn.async(T t) defer;
    bool idle = true;
    [idle] on p.e (t): {idle=false; defer.req (t);}
    [!idle] on defer.ack (t): {idle=true; p.a (t);}
  }
}

In this example the ‘defer.req’ puts an event in the queue. After all processing has completed (this may also involve handling input and output events to other components), the event call returns and subsequently the defer.ack event fires. This will trigger the actions listed at the ‘on defer.ack’ and as a result the output event a is called. From the perspective of the caller, the event handling is asynchronous. Still this was all handled by the called component without the need for an external event. Therefore, the asynchronous protocol has successfully been made seemingly synchronous by using the ‘async’ keyword. As you can see in the example the ‘defer.ack’ event is treated in the code as any other event.

image

The type dzn.async has one more function we did not discuss yet and we will show that in the next example:

In the example below the defer.clr is called as result from an event c. The situation where a clr needs to be called will typically be defined in the interplay between multiple components.

extern T $int$;

interface i
{
  in void e(T t);
  in void c(T t);
  out void a(T t);
  out void b();
  behaviour {
    bool idle = true;
    [idle] {
      on e: idle=false;
      on c: illegal;
    }
    [!idle] {
      on c: idle=true;
      on inevitable: {idle=true;a;b;}
      on e: illegal;
    }
  }
}
component async_cancel
{
  provides i p;
  behaviour {
    requires dzn.async(T t) defer;
    bool idle = true;
    [idle] on p.e (t): {idle=false; defer.req (t);}
    [!idle] on p.c (t): {idle=true; defer.clr ();}
    [!idle] on defer.ack (t): {idle=true;p.a (t);p.b();}
  }
}

We have now covered all the basics of the async keyword. In Applications of ‘async' we will visit a few typical situations where the async pattern comes in handy.


Next: , Previous: , Up: Dezyne async   [Contents]

6.2 Applications of ‘async’

An effect of queuing the async event, as if it were an external event, is that it creates a kind of context switch. The current chain of event processing is completed and all Dezyne component queues are emptied before the ack event is fired. This means some interactions become possible which previously were not allowed because of potential circular reference problems. Two such situations are presented in the first 2 examples. In other situations it is just very handy to schedule some actions at a moment you are sure all event processing has finished. The last examples shows this.


Next: , Up: Applications of ‘async'   [Contents]

6.2.1 Communication across two provided ports

image

Without async it is not allowed in Dezyne to call an out-event in another provided port than the provided port that was the origin of the event. The following example shows how this can be done using async.

component Async_ForkProvidedIn
{
  provides IA ppa;
  provides IA ppb;

  behaviour
  {
    bool outstanding_a = false;
    bool outstanding_b = false;
    requires dzn.async reflector_a;
    requires dzn.async reflector_b;

    [!outstanding_a] on ppa.ia(): {outstanding_a = true; reflector_a.req();}
    [!outstanding_b] on ppb.ia(): {outstanding_b = true; reflector_b.req();}
    [outstanding_a] {
      on ppa.ia(): {} // ignore second ia
      on reflector_a.ack(): {outstanding_a = false; ppb.oa();}
    }
    [outstanding_b] {
      on ppb.ia(): {} // ignore second ia
      on reflector_b.ack(): {outstanding_b = false; ppa.oa();}
    }
  }
}
interface IA
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

In this example an in-event on one port results in an out-event on the other port. The async only decouples the resulting out-event from the context of the in-event.

image

A provides in-event on one provides port generates an out-event on the other provides port


Next: , Previous: , Up: Applications of ‘async'   [Contents]

6.2.2 Fork a required event across two provided ports

image

Async can also be used to fork an event to two different provides ports. A similar argument applies here that without async circular references could be the result. The code is shown below:

component Async_ForkRequiredOut
{
  provides IA ppa;
  provides IA ppb;
  requires IB rp;

  behaviour
  {
    requires dzn.async() reflector;

    on ppa.ia(): rp.ib();
    on ppb.ia(): rp.ib();
    on rp.ob(): {reflector.req(); ppb.oa();}
    on reflector.ack(): ppa.oa();
  }
}

interface IA
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}
interface IB
{
  in void ib();
  out void ob();

  behaviour
  {
    bool is_active = false;
    on ib: is_active = true;
    [is_active] on inevitable: {ob; is_active = false;}
  }
}

At the reception of an out-event in the required port directly one of the out-events to a provided port is generated together with the sync.req. At the subsequent firing of the sync.ack the out-event to the other provided port is generated.

image

Forking an event over two provides interfaces triggered by a requires out-event


Previous: , Up: Applications of ‘async'   [Contents]

6.2.3 Armour for a missing synchronous out-event

image

A Dezyne component has a requires port where a synchronous out-event is expected in response to an in-event. The type of this port is the strict interface IStrict. We armour for the situation where the foreign component that implements this interface potentially violates this requirement by defining a robust interface IRobust that is more forgiving. You can see in the code below that the IRobust interface has one additional statement to describe the situation that the in-event does not result in a synchronous out-event. The Armour component maps the IRobust on the IStrict by simply ignoring the error.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
  }
}

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
    on ia: {}
  }
}

extern str $char*$;
interface ILogger
{
  in void Log(str msg);

  behaviour {
    on Log: {}
  }
}

component ArmourMSOE {
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
    requires dzn.async p;

    on pStrict.ia(): blocking {rRobust.ia(); p.req();}
    on rRobust.oa(): {pStrict.reply(); pStrict.oa(); p.clr();}
    on p.ack(): {pStrict.reply(); pStrict.oa(); iLog.Log($"Foreign comp does not send sync out-event oa"$);}
  }
}

component Dezyne {
  provides IA pp;
  requires IStrict rStrict;

  behaviour {
    on pp.ia(): blocking {rStrict.ia();}
    on rStrict.oa(): {pp.reply(); pp.oa();}
  }
}

interface IA
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
  }
}

component Foreign {
  provides IRobust pRobust;
  requires IRobust r;
}

component ArmouredSystemMSOE {
  provides IA pp;
  requires IRobust ir;

  system {
    Dezyne re;
    ArmourMSOE am;
    Foreign n;

    pp <=> re.pp;
    re.rStrict <=> am.pStrict;
    am.rRobust <=> n.pRobust;
    n.r <=> ir;
  }
}

We use both the blocking and async keyword in this example in order to detect the situation that the synchronous out-event is missing. The blocking keyword is used to guarantee that the armour only gives control back to the caller after it is sure that a potential violation is captured and dealt with. With the async we raise an internal event req’. It fires after all processing of the current context has been completed. So before it fires, a synchronous out-event may happen. In the normal case where the synchronous out-event happens we pass it on through the IStrict interface and cancel the async event. This is the happy flow. If no such synchronous out-event fires in the armour then eventually the ‘ack’ event fires and the interface violation can be dealt with. In this example the armour simply logs the error and generates a synchronous out-event on its own to satisfy the IStrict requirement. The reply statement in both situations lifts the blocking situation so after completion of the statement block control is passed back to the caller.

image

Handling the interface violation in the Armour component


Next: , Previous: , Up: Dezyne async   [Contents]

6.3 ‘async’ Behaviour in Runtime Context

Although the async feature makes use of an event-pump it does not have any specific effect on the interaction with foreign code. The only requirement to be able to use ‘async’ is that you have an event-pump. A system generated with a thread-safe-shell will get an event pump implicitly but you could also build one in foreign code. In this description we simply refer to the Dezyne runtime in combination with code generated with the option to generate a thread-safe-shell. For more information read an article about the event pump and one about the thread-safe shell.


Up: ‘async' Behaviour in Runtime Context   [Contents]

6.3.1 Async Runtime behaviour

In the execution semantics of Dezyne events are handled in a fixed order. For an in-event all action statements are executed depth-first. All out-events are stored in event queues at the receiving components. After the completion of all action statements, just before control is passed back to the caller, a component will flush its own queue of pending out-events. Recursively all out-events are handled this way. This process is repeated for all components involved in handling the external event. As last action in the row, just before the Dezyne private thread would switch to a ‘waiting for next event’ mode, the queue of async events would be handled.

image

DZN Pump

In the diagram above an external event could lead to actions in Component1 and Component2. First all processing as a result of the external event is handled; this might include raising async events which are stored in the Async Event Queue. Then, before the next external event is picked up from the External Event Queue the contents of Async Event Queue is handled. There could be several components between the component where the async is handled and the component where the external event fires after being picked up by the event pump. At the level of the ‘async’ component there could be more input events resulting from the original external event that would be processed before the async queued event gets activated. The component simulator cannot see whether multiple events entering a component belong to a tree of actions resulting from one external event or from multiple external events. So the simulator cannot see whether an external event has been completely handled and async events can already be activated. As a consequence the simulator will offer more choices in the next eligible events than could happen in practice at system level.

image

Next eligible events

In the example above events ‘a’ and ‘b’ could be resulting from the same external event e.g. ‘e1’ or they could be resulting from 2 different external events ‘e1’ and ‘e2’. The blocking keyword creates a dependency on an event external to the component to eventually lift the blocking situation. Obviously this introduces a risk if the external event never comes. See the description at the blocking keyword. The async feature in fact removes the dependency of an event external to the component. So in its use no risks are introduced, in fact there is one dependency less.


Previous: , Up: Dezyne async   [Contents]

6.4 Summary of Dezyne async

In the introduction of this chapter, the following tasks were mentioned:

In this section, you will find a quick summary on each of the learning goals and where they were discussed in the tutorial.


Next: , Up: Summary of Dezyne async   [Contents]

6.4.1 Understand what ‘async’ allows you to do in Dezyne

Using ‘async’, it becomes possible to support asynchronous communication behaviour patterns in a synchronous process. This was discussed in What is the Bare Function of ‘async'?


Next: , Previous: , Up: Summary of Dezyne async   [Contents]

6.4.2 Identify when ‘async’ may be used and when it may not be used

The analysis of a ‘async’ process in ‘async' Behaviour in Runtime Context, completes the picture of what is happening behind the scenes in the example cases presented in Applications of ‘async'.


Previous: , Up: Summary of Dezyne async   [Contents]

6.4.3 Reason about design decisions when using the ‘async’ keyword

The section Applications of ‘async' provides example situations where the usage of ‘async’ may or may not be warranted including the application of the standard events in ‘async’.


Next: , Previous: , Up: Top   [Contents]

7 Armouring

 In this chapter, we will


Next: , Up: Armouring   [Contents]

7.1 Definition and usage of armouring

In the chapter on the usage of the ‘async’ keyword, we already reviewed a situation where we did not fully trust a foreign component and called that an armour. In this tutorial we will generalize this concept of armouring: An Armour protects a system built in Dezyne during runtime against interface violations by foreign code. Between Dezyne components such violations can never occur after passing the verification. However, the integration with foreign code cannot be formally verified and hence the foreign code could be misbehaving. Typically if the foreign code is not fully understood it may be suspected of not being fully interface compliant.

An Armour component shields the Dezyne system by capturing misbehavior and ensuring that the Dezyne components only perceive good behaviour. We call the interface between the Armour and the Dezyne component the Strict interface. We call the interface between the armour and the Foreign code the Robust interface. The Robust interface does not enforce the restrictions of the Strict interface and so, in a sense, allows misbehaviour. Depending on the situation the Armour could simply correct the violations such that the Dezyne components never notice anything.

The Armour could also raise an error condition which must be handled by the Dezyne components first before normal behaviour is continued. The Armour examples provided in this chapter all come in two flavours representing the situation with and without error handling. In all cases the error is logged for diagnostics purposes. The list is exhaustive in the sense that for any single possible interface violation an example is provided. The list may appear surprisingly small but many problems are static in nature and are detected by the compiler. Off course in practice multiple violations to an interface may occur and then multiple Armour patterns would need to be combined.

As an example of the situation without error handling look at the often used example of a device that is always switched on and off in alternation. The interface would specify that it is illegal to send an on-command if it is already on and similarly illegal to send an off -command if it is already off. In the implementation there is not a real problem to accept an on-command if it already on so that is not the reason to be strict in the interface. However, if we want to verify whether this device is used in a proper alternating way then having these strict interfaces supports such a verification. In this situation an Armour would need to log the error situation but probably the system could simply continue to execute.

In more complex situations an Armour cannot solve a violation independently. Since the behaviour is unexpected by the Dezyne components appropriate handling is not available and a general error status would need to be raised in the Dezyne components. Also the foreign component generating the erroneous event must be reset to a known situation. This means a generic pattern of error status handling must be present in the Dezyne components to be prepared for interaction with Armour components. In the Armour patterns provided we assume that the Dezyne component directly communicating with the Armour takes full responsibility for this error handling and hides this completely for other components making use of the functionality. This may not be applicable in all situations and then the error should be passed on. This is just one example how such error handling is situation dependent. This means that many different patterns of error handling are possible; in this tutorial and the given examples we consistently apply the pattern described below.


Next: , Up: Definition and usage of armouring   [Contents]

7.1.1 Pattern of error handling behaviour

If the Armour detects a violation it sends an event RaiseError to the Dezyne component. The Dezyne component must go to a controlled state and will eventually send a Reset event to the Foreign component (the Armour will pass this on). As a consequence the Foreign component will go to a known state. The Foreign component is expected to send an output event Recovered as result. As a consequence the Armour and Dezyne components will move to normal mode of operation again.

image

The overall state behaviour related to this pattern is a state machine with 3 states: {noError, raisedError, resetError}. Often it will be possible to reduce this to 2 error states only. The Robust interface supports the same events as the Strict interface without its limitations. The Armour maps the Robust interface to the Strict interface. It passes on all events in normal operation. It triggers on deviations of the allowed behaviour and then enters an error state. It logs the error using a Log interface via an injected port. Also it raises the error with the Dezyne component and prevents any further regular interaction with the Foreign component until the error is handled as described above.


Next: , Previous: , Up: Definition and usage of armouring   [Contents]

7.1.2 Foreign component below required interface

This is the ‘natural’ way Foreign components are connected. A logging component connected through an injected port logs the error information. The variant with error handling is an extension of the variant without error handling and extends the Armour and Strict interface with the error handling state behaviour described above. The Dezyne component and Robust interface error handling does only deal with 2 states, in error or not.

image

Next: , Previous: , Up: Definition and usage of armouring   [Contents]

7.1.3 Foreign component above required interface

This may happen in special cases. The armouring concept is slightly more complex here. On the other hand in the variant with error handling all components and interfaces only have a 2–state error handling mechanism, in error or not. The Dezyne component needs the async feature to automatically send the asynchronous Reset event as a response to the RaiseError event. The Foreign component might send a Recovered event before it is being Reset. In that case the asynchronous Reset event will not be sent anymore by the clr of the async.

image

Previous: , Up: Definition and usage of armouring   [Contents]

7.1.4 Combinations of armours

In case a strict interface has multiple conditions which a foreign component might violate it is necessary to build an armour that is a mixture of several of these patterns. This might result in rather complex code. A simplistic but also very effective approach might be to put the various armours in a sequential fashion where the transformation from strict to robust interface (and vice versa) is achieved in steps.

We have now covered all the basics of armouring. In Armouring patterns we will review all possible individual armouring situations.


Next: , Previous: , Up: Armouring   [Contents]

7.2 Armouring patterns

Here we discuss the exhaustive list of Armour patterns separated in armouring either a provides interface or a requires interface. They all come in 2 flavours, with or without error handling. The names were inspired by the error messages that the Dezyne verifier generates.


Next: , Up: Armouring patterns   [Contents]

7.2.1 In Provides interface


Next: , Previous: , Up: Armouring patterns   [Contents]

7.2.2 In Requires interface


Previous: , Up: Armouring patterns   [Contents]

7.2.3 Might be expected but not possible Armour cases

Due to the semantics of the Dezyne Modeling Language some situations are syntactically or semantically impossible


Next: , Previous: , Up: Armouring   [Contents]

7.3 Individual Armour cases

We will now discuss all possible armour cases individually but only in the simplistic variant where the error is logged and subsequently ignored. The complex variant, with the error handling procedure, is also available in Dezyne code but not discussed in this tutorial.


Next: , Up: Individual Armour cases   [Contents]

7.3.1 ArmourIBVIRR (IllegalBooleanValueInRequiresReply)

A reply value from a required interface can contain a boolean value that is not allowed. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourIBVIRR

We only deal with one in-event returning a boolean result value. The Strict interface specifies that only a boolean value of ’true’ can be replied.

interface IStrict
{
  in bool ia();

  behaviour
  {
    on ia: reply (true);
  }
}

The Robust interface allows both boolean reply values of ’true’ and ’false’.

interface IRobust
{
  in bool ia();

  behaviour
  {
    on ia: reply (true);
    on ia: reply (false);
  }
}

In the armour the result from the requires interface is captured in a local bool b. If it is false we log it as an error. In all cases we simply return the boolean value ’true’ to the provides interface.

component ArmourIBVIRR // IStrict to IRobust
{
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
    on pStrict.ia(): {
        bool b = rRobust.ia();
        if (!b) iLog.Log($"Reply value false from ia not allowed by port"$);
        reply(true);
    } // armour ignore (false) case
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIBVIRR
Example with error handling: ArmourIBVIRRError


Next: , Previous: , Up: Individual Armour cases   [Contents]

7.3.2 ArmourIIPRB (IllegalInProvidesReturnsBool)

A provided interface may have an illegal in-event with a bool return type. The system diagram shows the armour at the provides port of the Dezyne component:

ArmourIIPRB

We only deal with one bool in-event and one void out-event. The Strict interface specifies that the in-event is illegal.

interface IStrict
{
  in bool ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

The Robust interface allows both an in-event and an out-event’. In the case of the in-event it always replies ’false’.

interface IRobust
{
  in bool ia();
  out void oa();

  behaviour
  {
    on ia: {reply(false);}
    on inevitable: oa;
  }
}

In the armour the occurrance of an illegal in-event is logged and ’false’ is replied. An out-event from the requires port is simply passed to the provides port.

component ArmourIIPRB // IStrict to IRobust
{
  provides IRobust pRobust;
  requires IStrict rStrict;
  requires injected ILogger iLog;

  behaviour {
    on pRobust.ia(): {reply(false); iLog.Log($"In-event ia is illegal in port"$);} // armour illegal ia
    on rStrict.oa(): pRobust.oa();
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIIPRB
Example with error handling: ArmourIIPRBError


Next: , Previous: , Up: Individual Armour cases   [Contents]

7.3.3 ArmourIIPRE (IllegalInProvidesReturnsEnum)

A provided interface may have an illegal in-event with a myEnum return type. The system diagram shows the armour at the provides port of the Dezyne component:

ArmourIIPRE

We only deal with one in-event returning an enumerated and one void out-event. The Strict interface specifies that the in-event is illegal.

interface IStrict
{
  in myEnum ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

The Robust interface allows both an in-event and an out-event’. In the case of the in-event it always replies ’No’.

interface IRobust
{
  in myEnum ia();
  out void oa();

  behaviour
  {
    on ia: {reply(myEnum.No);}
    on inevitable: oa;
  }
}

In the armour the occurrance of an illegal in-event is logged and ’No’ is replied. An out-event from the requires port is simply passed to the provides port.

component ArmourIIPRE // IStrict to IRobust
{
  provides IRobust pRobust;
  requires IStrict rStrict;
  requires injected ILogger iLog;

  behaviour {
    on pRobust.ia(): {reply(myEnum.No); iLog.Log($"In-event ia is illegal in port"$);} // armour illegal ia
    on rStrict.oa(): pRobust.oa();
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIIPRE
Example with error handling: ArmourIIPREError


Next: , Previous: , Up: Individual Armour cases   [Contents]

7.3.4 ArmourIIPRV (IllegalInProvidesReturnsVoid)

A provided interface may have an illegal in-event with a void return type. The system diagram shows the armour at the provides port of the Dezyne component:

ArmourIIPRV

We only deal with one void in-event and one void out-event. The Strict interface specifies that the in-event is illegal.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

The Robust interface allows both an in-event and an out-event’. In the case of the in-event there is no associated action.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on inevitable: oa;
  }
}

In the armour the occurrance of an illegal in-event is logged. An out-event from the requires port is simply passed to the provides port.

component ArmourIIPRV // IStrict to IRobust
{
  provides IRobust pRobust;
  requires IStrict rStrict;
  requires injected ILogger iLog;

  behaviour {
    on pRobust.ia(): {iLog.Log($"Input event ia is illegal in port"$);} // armour illegal ia
    on rStrict.oa(): pRobust.oa();
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIIPRV
Example with error handling: ArmourIIPRVError


Next: , Previous: , Up: Individual Armour cases   [Contents]

7.3.5 ArmourISOE (IllegalSynchronousOutEvent)

The context is expected to not generate a synchronous out-event via the requires port but may still do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourISOE

We only deal with one void in-event and one void out-event. The Strict interface specifies that the in-event does not lead to a synchronous out-event.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on inevitable: oa;
  }
}

The Robust interface allows that in-event either results in a synchronous out-event or no out-event at all.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on ia: oa;
    on inevitable: oa;
  }
}

In the armour we use the async keyword to discriminate between out-events that are triggered by an out-event from a requires port from a synchronous out-event. On the receival of an in-event we set a bool and put a request in the async queue. If the async acknowledge triggers and we have not had an out-event from the requires port in between we know the behaviour is according to the strict interface. If we receive an out-event from the requires port in the context of the provides in-event (we know by inspecting the boolean value) then we know it is an error and we deal with it. Otherwise we pass the out-event as normal allowed behaviour.

component ArmourISOE {
    provides IStrict pStrict;
    requires IRobust rRobust;
    requires injected ILogger iLog;

    behaviour {
        requires dzn.async p;

        bool requested = false;
        on pStrict.ia(): {
            rRobust.ia();
            if (!requested) {p.req(); requested = true;}
        }
        on rRobust.oa(): {
            if (!requested) pStrict.oa();
            else {
                requested = false; p.clr();
                iLog.Log($"Foreign comp does sync out-event oa where async oa was expected"$);
            }
        }
        on p.ack(): requested = false;
    }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourISOE
Example with error handling: ArmourISOEError


Next: , Previous: , Up: Individual Armour cases   [Contents]

7.3.6 ArmourMAOE (MissingAsynchronousOutEvent)

The foreign component is expected to generate an out-event asynchronously via the requires port but may not do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourMAOE

We only deal with one void in-event and one void out-event. The Strict interface specifies that an in-event must lead to an asynchronous out-event. As a consequence a next in-event is only allowed after such an asynchronous out-event has happened.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    bool ia_called = false;

    [!ia_called] on ia: {ia_called = true;}
    [ia_called] {
        on ia: illegal;
        on inevitable: {oa; ia_called = false;}
    }
  }
}

The Robust interface allows any occurrance of in-events and asynchronous out-events. We do allow to use multiple in-events without asynchronous out-events in between but the Dezyne component on top (the armour) will not issue multiple in-events.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

In the strict sense we can never determine that an out-event is not coming anymore but a practical solution is to use a timeout period. After an in-event we start waiting for the asynchronous out-event from the requires port but we only wait for a given timeout period. If the timeout occurs we consider it an error; we log it and generate the missing out-event. If the out-event occurs within the deadline we pass it on and reset the armour top wait for a next in-event.

component ArmourMAOE {
    provides IStrict pStrict;
    requires IRobust rRobust;
    requires ITimer it;
    requires injected ILogger iLog;

    behaviour {
        bool waiting_for_oa = false;

        on it.timeout(): {
            iLog.Log($"timeout on expected oa"$);
            pStrict.oa(); waiting_for_oa = false;
        }
        [waiting_for_oa]
            on rRobust.oa(): {pStrict.oa(); it.cancel(); waiting_for_oa = false;}
        [!waiting_for_oa]{
            on pStrict.ia(): {rRobust.ia(); it.start(); waiting_for_oa = true;}
            on rRobust.oa(): {}
        }
    }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourMAOE
Example with error handling: ArmourMAOEError


Next: , Previous: , Up: Individual Armour cases   [Contents]

7.3.7 ArmourMSOE (MissingSynchronousOutEvent)

The context is expected to generate out-event via requires interface but may not do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourMSOE

We only deal with one void in-event and one void out-event. The Strict interface specifies that an in-event must lead to a synchronous out-event.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
  }
}

The Robust interface allows that an in-event either or not sends a synchronous out-event.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
    on ia: {}
  }
}

In the armour we use a combination of async and blocking. We need blocking to make sure all the lower level handling can be done semi-asynchronously and still we can reply in a synchronous way. The in-event is passed to the requires port and we raise an async request. If the async ackowledges we know all the processing in the context of the original in-event has completed and hence the required synchronous out-event is missing; we log the error, and create such an out-event in the armour. If the requires port receives an out-event this is happening in the context of the the original in-event (since the async acknowledge did not fire yet). Hence this is a synchronous reply and everything is fine. We cancel the async to avoid the error trigger.

component ArmourMSOE {
    provides IStrict pStrict;
    requires IRobust rRobust;
    requires injected ILogger iLog;

    behaviour {
        requires dzn.async p;
        bool xxxx = false;

        on pStrict.ia(): blocking {rRobust.ia(); p.req();}
        on rRobust.oa(): {pStrict.reply(); pStrict.oa(); p.clr();}
        on p.ack(): {pStrict.reply(); pStrict.oa(); iLog.Log($"Foreign comp does not send sync out-event oa"$);}
    }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourMSOE
Example with error handling: ArmourMSOEError


Next: , Previous: , Up: Individual Armour cases   [Contents]

7.3.8 ArmourOENABP (OutEventNotAllowedByPort)

The required interface is not allowed to send an out-event but may still do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourOENABP

We only deal with one void in-event and one void out-event. The Strict interface specifies that an in-event must not lead to any out-event.

interface IStrict
{
  in void ia();
  out void oa(); // nb not part of completeness check

  behaviour
  {
    on ia: {}
  }
}

The Robust interface allows optional out-events.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

In the armour an in-event at the provides port is passed to the requires port. If an out-event is received from the requires port it is logged as an error and suppressed.

component ArmourOENABP // IStrict to IRobust
{
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
    on pStrict.ia(): rRobust.ia();
    on rRobust.oa(): {iLog.Log($"Out-event oa is not allowed by port"$);} // armour potential oa
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourOENABP
Example with error handling: ArmourOENABPError


Previous: , Up: Individual Armour cases   [Contents]

7.3.9 ArmourREIR (RangeErrorInRequiresReply)

The reply of a requires interface event could have a range error (a mis-mapping between two subints). The system diagram shows the armour at the requires port of the Dezyne component:

ArmourREIR

We only deal with one in-event areturning an integer value. We defined 2 integer ranges. The Strict interface use the most restricted one so we only allow a very limited set of reply values.

interface IStrict
{
  in SubCount ia();

  behaviour
  {
    SubCount c=0;
    on ia: reply(0);
    on ia: reply(1);
    on ia: reply(2);
  }
}

The Robust interface allows the more relaxed set of reply values. In the model code we do not have to describe all possible reply values as long as we at least define one good case and one bad case that the verifer can investigate.

interface IRobust
{
  in AllCount ia();

  behaviour
  {
    on ia: reply (-1);  // -1 triggers an error
    on ia: reply (0);   // 0 is ok behaviour
  }
}

In the armour an in-event at the provides port is passed to the requires port. If the reply value from the requires port is outside the strict range it is logged as an error and either the lower or upper boundary of the restricted range is returned.

component ArmourREIR // IStrict to IRobust
{
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
    AllCount c = 0;

    on pStrict.ia(): {
        c = rRobust.ia();
        if (c<0) {
            iLog.Log($"Reply value from ia outside range (too small)"$);
            reply(0);
        }
        else if (c>2) {
            iLog.Log($"Reply value from ia outside range (too large)"$);
            reply (2);
        }
        else reply(c+0);
    } // armour on boundary values
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourREIR
Example with error handling: ArmourREIRError


Previous: , Up: Armouring   [Contents]

7.4 Summary of Armouring

In the introduction of this chapter, the following tasks were mentioned:

In this section, you will find a quick summary on each of the learning goals and where they were discussed in the tutorial.


Next: , Up: Summary of Armouring   [Contents]

7.4.1 Understand what ‘armouring’ means in Dezyne and what it is used for

You can use armouring to protect a Dezyne generated system against misbehaving foreign code. This was discussed in Definition and usage of armouring


Next: , Previous: , Up: Summary of Armouring   [Contents]

7.4.2 Identify how to apply ’armouring’ in Dezyne

To understand how to apply armouring you must study the contents of Definition and usage of armouring and at least one example in Armouring patterns.


Previous: , Up: Summary of Armouring   [Contents]

7.4.3 Understand the different ’armouring’ patterns

The section Armouring patterns provides an example for all possible invidual armour cases.


Previous: , Up: Top   [Contents]

Appendix A GNU Free Documentation License

Version 1.3, 3 November 2008
Copyright © 2000, 2001, 2002, 2007, 2008 Free Software Foundation, Inc.
http://fsf.org/

Everyone is permitted to copy and distribute verbatim copies
of this license document, but changing it is not allowed.
  1. PREAMBLE

    The purpose of this License is to make a manual, textbook, or other functional and useful document free in the sense of freedom: to assure everyone the effective freedom to copy and redistribute it, with or without modifying it, either commercially or noncommercially. Secondarily, this License preserves for the author and publisher a way to get credit for their work, while not being considered responsible for modifications made by others.

    This License is a kind of “copyleft”, which means that derivative works of the document must themselves be free in the same sense. It complements the GNU General Public License, which is a copyleft license designed for free software.

    We have designed this License in order to use it for manuals for free software, because free software needs free documentation: a free program should come with manuals providing the same freedoms that the software does. But this License is not limited to software manuals; it can be used for any textual work, regardless of subject matter or whether it is published as a printed book. We recommend this License principally for works whose purpose is instruction or reference.

  2. APPLICABILITY AND DEFINITIONS

    This License applies to any manual or other work, in any medium, that contains a notice placed by the copyright holder saying it can be distributed under the terms of this License. Such a notice grants a world-wide, royalty-free license, unlimited in duration, to use that work under the conditions stated herein. The “Document”, below, refers to any such manual or work. Any member of the public is a licensee, and is addressed as “you”. You accept the license if you copy, modify or distribute the work in a way requiring permission under copyright law.

    A “Modified Version” of the Document means any work containing the Document or a portion of it, either copied verbatim, or with modifications and/or translated into another language.

    A “Secondary Section” is a named appendix or a front-matter section of the Document that deals exclusively with the relationship of the publishers or authors of the Document to the Document’s overall subject (or to related matters) and contains nothing that could fall directly within that overall subject. (Thus, if the Document is in part a textbook of mathematics, a Secondary Section may not explain any mathematics.) The relationship could be a matter of historical connection with the subject or with related matters, or of legal, commercial, philosophical, ethical or political position regarding them.

    The “Invariant Sections” are certain Secondary Sections whose titles are designated, as being those of Invariant Sections, in the notice that says that the Document is released under this License. If a section does not fit the above definition of Secondary then it is not allowed to be designated as Invariant. The Document may contain zero Invariant Sections. If the Document does not identify any Invariant Sections then there are none.

    The “Cover Texts” are certain short passages of text that are listed, as Front-Cover Texts or Back-Cover Texts, in the notice that says that the Document is released under this License. A Front-Cover Text may be at most 5 words, and a Back-Cover Text may be at most 25 words.

    A “Transparent” copy of the Document means a machine-readable copy, represented in a format whose specification is available to the general public, that is suitable for revising the document straightforwardly with generic text editors or (for images composed of pixels) generic paint programs or (for drawings) some widely available drawing editor, and that is suitable for input to text formatters or for automatic translation to a variety of formats suitable for input to text formatters. A copy made in an otherwise Transparent file format whose markup, or absence of markup, has been arranged to thwart or discourage subsequent modification by readers is not Transparent. An image format is not Transparent if used for any substantial amount of text. A copy that is not “Transparent” is called “Opaque”.

    Examples of suitable formats for Transparent copies include plain ASCII without markup, Texinfo input format, LaTeX input format, SGML or XML using a publicly available DTD, and standard-conforming simple HTML, PostScript or PDF designed for human modification. Examples of transparent image formats include PNG, XCF and JPG. Opaque formats include proprietary formats that can be read and edited only by proprietary word processors, SGML or XML for which the DTD and/or processing tools are not generally available, and the machine-generated HTML, PostScript or PDF produced by some word processors for output purposes only.

    The “Title Page” means, for a printed book, the title page itself, plus such following pages as are needed to hold, legibly, the material this License requires to appear in the title page. For works in formats which do not have any title page as such, “Title Page” means the text near the most prominent appearance of the work’s title, preceding the beginning of the body of the text.

    The “publisher” means any person or entity that distributes copies of the Document to the public.

    A section “Entitled XYZ” means a named subunit of the Document whose title either is precisely XYZ or contains XYZ in parentheses following text that translates XYZ in another language. (Here XYZ stands for a specific section name mentioned below, such as “Acknowledgements”, “Dedications”, “Endorsements”, or “History”.) To “Preserve the Title” of such a section when you modify the Document means that it remains a section “Entitled XYZ” according to this definition.

    The Document may include Warranty Disclaimers next to the notice which states that this License applies to the Document. These Warranty Disclaimers are considered to be included by reference in this License, but only as regards disclaiming warranties: any other implication that these Warranty Disclaimers may have is void and has no effect on the meaning of this License.

  3. VERBATIM COPYING

    You may copy and distribute the Document in any medium, either commercially or noncommercially, provided that this License, the copyright notices, and the license notice saying this License applies to the Document are reproduced in all copies, and that you add no other conditions whatsoever to those of this License. You may not use technical measures to obstruct or control the reading or further copying of the copies you make or distribute. However, you may accept compensation in exchange for copies. If you distribute a large enough number of copies you must also follow the conditions in section 3.

    You may also lend copies, under the same conditions stated above, and you may publicly display copies.

  4. COPYING IN QUANTITY

    If you publish printed copies (or copies in media that commonly have printed covers) of the Document, numbering more than 100, and the Document’s license notice requires Cover Texts, you must enclose the copies in covers that carry, clearly and legibly, all these Cover Texts: Front-Cover Texts on the front cover, and Back-Cover Texts on the back cover. Both covers must also clearly and legibly identify you as the publisher of these copies. The front cover must present the full title with all words of the title equally prominent and visible. You may add other material on the covers in addition. Copying with changes limited to the covers, as long as they preserve the title of the Document and satisfy these conditions, can be treated as verbatim copying in other respects.

    If the required texts for either cover are too voluminous to fit legibly, you should put the first ones listed (as many as fit reasonably) on the actual cover, and continue the rest onto adjacent pages.

    If you publish or distribute Opaque copies of the Document numbering more than 100, you must either include a machine-readable Transparent copy along with each Opaque copy, or state in or with each Opaque copy a computer-network location from which the general network-using public has access to download using public-standard network protocols a complete Transparent copy of the Document, free of added material. If you use the latter option, you must take reasonably prudent steps, when you begin distribution of Opaque copies in quantity, to ensure that this Transparent copy will remain thus accessible at the stated location until at least one year after the last time you distribute an Opaque copy (directly or through your agents or retailers) of that edition to the public.

    It is requested, but not required, that you contact the authors of the Document well before redistributing any large number of copies, to give them a chance to provide you with an updated version of the Document.

  5. MODIFICATIONS

    You may copy and distribute a Modified Version of the Document under the conditions of sections 2 and 3 above, provided that you release the Modified Version under precisely this License, with the Modified Version filling the role of the Document, thus licensing distribution and modification of the Modified Version to whoever possesses a copy of it. In addition, you must do these things in the Modified Version:

    1. Use in the Title Page (and on the covers, if any) a title distinct from that of the Document, and from those of previous versions (which should, if there were any, be listed in the History section of the Document). You may use the same title as a previous version if the original publisher of that version gives permission.
    2. List on the Title Page, as authors, one or more persons or entities responsible for authorship of the modifications in the Modified Version, together with at least five of the principal authors of the Document (all of its principal authors, if it has fewer than five), unless they release you from this requirement.
    3. State on the Title page the name of the publisher of the Modified Version, as the publisher.
    4. Preserve all the copyright notices of the Document.
    5. Add an appropriate copyright notice for your modifications adjacent to the other copyright notices.
    6. Include, immediately after the copyright notices, a license notice giving the public permission to use the Modified Version under the terms of this License, in the form shown in the Addendum below.
    7. Preserve in that license notice the full lists of Invariant Sections and required Cover Texts given in the Document’s license notice.
    8. Include an unaltered copy of this License.
    9. Preserve the section Entitled “History”, Preserve its Title, and add to it an item stating at least the title, year, new authors, and publisher of the Modified Version as given on the Title Page. If there is no section Entitled “History” in the Document, create one stating the title, year, authors, and publisher of the Document as given on its Title Page, then add an item describing the Modified Version as stated in the previous sentence.
    10. Preserve the network location, if any, given in the Document for public access to a Transparent copy of the Document, and likewise the network locations given in the Document for previous versions it was based on. These may be placed in the “History” section. You may omit a network location for a work that was published at least four years before the Document itself, or if the original publisher of the version it refers to gives permission.
    11. For any section Entitled “Acknowledgements” or “Dedications”, Preserve the Title of the section, and preserve in the section all the substance and tone of each of the contributor acknowledgements and/or dedications given therein.
    12. Preserve all the Invariant Sections of the Document, unaltered in their text and in their titles. Section numbers or the equivalent are not considered part of the section titles.
    13. Delete any section Entitled “Endorsements”. Such a section may not be included in the Modified Version.
    14. Do not retitle any existing section to be Entitled “Endorsements” or to conflict in title with any Invariant Section.
    15. Preserve any Warranty Disclaimers.

    If the Modified Version includes new front-matter sections or appendices that qualify as Secondary Sections and contain no material copied from the Document, you may at your option designate some or all of these sections as invariant. To do this, add their titles to the list of Invariant Sections in the Modified Version’s license notice. These titles must be distinct from any other section titles.

    You may add a section Entitled “Endorsements”, provided it contains nothing but endorsements of your Modified Version by various parties—for example, statements of peer review or that the text has been approved by an organization as the authoritative definition of a standard.

    You may add a passage of up to five words as a Front-Cover Text, and a passage of up to 25 words as a Back-Cover Text, to the end of the list of Cover Texts in the Modified Version. Only one passage of Front-Cover Text and one of Back-Cover Text may be added by (or through arrangements made by) any one entity. If the Document already includes a cover text for the same cover, previously added by you or by arrangement made by the same entity you are acting on behalf of, you may not add another; but you may replace the old one, on explicit permission from the previous publisher that added the old one.

    The author(s) and publisher(s) of the Document do not by this License give permission to use their names for publicity for or to assert or imply endorsement of any Modified Version.

  6. COMBINING DOCUMENTS

    You may combine the Document with other documents released under this License, under the terms defined in section 4 above for modified versions, provided that you include in the combination all of the Invariant Sections of all of the original documents, unmodified, and list them all as Invariant Sections of your combined work in its license notice, and that you preserve all their Warranty Disclaimers.

    The combined work need only contain one copy of this License, and multiple identical Invariant Sections may be replaced with a single copy. If there are multiple Invariant Sections with the same name but different contents, make the title of each such section unique by adding at the end of it, in parentheses, the name of the original author or publisher of that section if known, or else a unique number. Make the same adjustment to the section titles in the list of Invariant Sections in the license notice of the combined work.

    In the combination, you must combine any sections Entitled “History” in the various original documents, forming one section Entitled “History”; likewise combine any sections Entitled “Acknowledgements”, and any sections Entitled “Dedications”. You must delete all sections Entitled “Endorsements.”

  7. COLLECTIONS OF DOCUMENTS

    You may make a collection consisting of the Document and other documents released under this License, and replace the individual copies of this License in the various documents with a single copy that is included in the collection, provided that you follow the rules of this License for verbatim copying of each of the documents in all other respects.

    You may extract a single document from such a collection, and distribute it individually under this License, provided you insert a copy of this License into the extracted document, and follow this License in all other respects regarding verbatim copying of that document.

  8. AGGREGATION WITH INDEPENDENT WORKS

    A compilation of the Document or its derivatives with other separate and independent documents or works, in or on a volume of a storage or distribution medium, is called an “aggregate” if the copyright resulting from the compilation is not used to limit the legal rights of the compilation’s users beyond what the individual works permit. When the Document is included in an aggregate, this License does not apply to the other works in the aggregate which are not themselves derivative works of the Document.

    If the Cover Text requirement of section 3 is applicable to these copies of the Document, then if the Document is less than one half of the entire aggregate, the Document’s Cover Texts may be placed on covers that bracket the Document within the aggregate, or the electronic equivalent of covers if the Document is in electronic form. Otherwise they must appear on printed covers that bracket the whole aggregate.

  9. TRANSLATION

    Translation is considered a kind of modification, so you may distribute translations of the Document under the terms of section 4. Replacing Invariant Sections with translations requires special permission from their copyright holders, but you may include translations of some or all Invariant Sections in addition to the original versions of these Invariant Sections. You may include a translation of this License, and all the license notices in the Document, and any Warranty Disclaimers, provided that you also include the original English version of this License and the original versions of those notices and disclaimers. In case of a disagreement between the translation and the original version of this License or a notice or disclaimer, the original version will prevail.

    If a section in the Document is Entitled “Acknowledgements”, “Dedications”, or “History”, the requirement (section 4) to Preserve its Title (section 1) will typically require changing the actual title.

  10. TERMINATION

    You may not copy, modify, sublicense, or distribute the Document except as expressly provided under this License. Any attempt otherwise to copy, modify, sublicense, or distribute it is void, and will automatically terminate your rights under this License.

    However, if you cease all violation of this License, then your license from a particular copyright holder is reinstated (a) provisionally, unless and until the copyright holder explicitly and finally terminates your license, and (b) permanently, if the copyright holder fails to notify you of the violation by some reasonable means prior to 60 days after the cessation.

    Moreover, your license from a particular copyright holder is reinstated permanently if the copyright holder notifies you of the violation by some reasonable means, this is the first time you have received notice of violation of this License (for any work) from that copyright holder, and you cure the violation prior to 30 days after your receipt of the notice.

    Termination of your rights under this section does not terminate the licenses of parties who have received copies or rights from you under this License. If your rights have been terminated and not permanently reinstated, receipt of a copy of some or all of the same material does not give you any rights to use it.

  11. FUTURE REVISIONS OF THIS LICENSE

    The Free Software Foundation may publish new, revised versions of the GNU Free Documentation License from time to time. Such new versions will be similar in spirit to the present version, but may differ in detail to address new problems or concerns. See http://www.gnu.org/copyleft/.

    Each version of the License is given a distinguishing version number. If the Document specifies that a particular numbered version of this License “or any later version” applies to it, you have the option of following the terms and conditions either of that specified version or of any later version that has been published (not as a draft) by the Free Software Foundation. If the Document does not specify a version number of this License, you may choose any version ever published (not as a draft) by the Free Software Foundation. If the Document specifies that a proxy can decide which future versions of this License can be used, that proxy’s public statement of acceptance of a version permanently authorizes you to choose that version for the Document.

  12. RELICENSING

    “Massive Multiauthor Collaboration Site” (or “MMC Site”) means any World Wide Web server that publishes copyrightable works and also provides prominent facilities for anybody to edit those works. A public wiki that anybody can edit is an example of such a server. A “Massive Multiauthor Collaboration” (or “MMC”) contained in the site means any set of copyrightable works thus published on the MMC site.

    “CC-BY-SA” means the Creative Commons Attribution-Share Alike 3.0 license published by Creative Commons Corporation, a not-for-profit corporation with a principal place of business in San Francisco, California, as well as future copyleft versions of that license published by that same organization.

    “Incorporate” means to publish or republish a Document, in whole or in part, as part of another Document.

    An MMC is “eligible for relicensing” if it is licensed under this License, and if all works that were first published under this License somewhere other than this MMC, and subsequently incorporated in whole or in part into the MMC, (1) had no cover texts or invariant sections, and (2) were thus incorporated prior to November 1, 2008.

    The operator of an MMC Site may republish an MMC contained in the site under CC-BY-SA on the same site at any time before August 1, 2009, provided the MMC is eligible for relicensing.

ADDENDUM: How to use this License for your documents

To use this License in a document you have written, include a copy of the License in the document and put the following copyright and license notices just after the title page:

  Copyright (C)  year  your name.
  Permission is granted to copy, distribute and/or modify this document
  under the terms of the GNU Free Documentation License, Version 1.3
  or any later version published by the Free Software Foundation;
  with no Invariant Sections, no Front-Cover Texts, and no Back-Cover
  Texts.  A copy of the license is included in the section entitled ``GNU
  Free Documentation License''.

If you have Invariant Sections, Front-Cover Texts and Back-Cover Texts, replace the “with…Texts.” line with this:

    with the Invariant Sections being list their titles, with
    the Front-Cover Texts being list, and with the Back-Cover Texts
    being list.

If you have Invariant Sections without Cover Texts, or some other combination of the three, merge those two alternatives to suit the situation.

If your document contains nontrivial examples of program code, we recommend releasing these examples in parallel under your choice of free software license, such as the GNU General Public License, to permit their use in free software.