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]