Menu

Defining and Managing Component States

Language keywords and constructs: enum illegal reply

Operators and constructs: = == [].

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 ser-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:

  • You are required to initialize an enumeration-type variable in its declaration

  • You cannot split this declaration-assignment line into the two lines, e.g.“State state; state = State.Off” – this equals sign is a special initialization operator, not a generic assignment (try it).

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 image icon in Eclipse, next to the verify image icon)

image

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:

  • When the providing component or components are hand-written, i.e. have no behaviour blocks and therefore no declared state behaviour, yet enumerated state behaviour is of interest to requiring (calling) components.

  • When an interface function will synchronously return enumerated results that inform the caller of a new state arrived at (at least momentarily) as a consequence of the function call.

    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 hat 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, etc – and displays the entire trace of events that led to the mismatch. Thus, you van quickly and inexpensively fix buried logical errors like race conditions and deadlocks even before any source code is generated or written.

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:

  • Declaration plus initialization of an enum or a variable.

  • An on-event block.

  • A [boolean-test] “guard” block as used below.

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:

image

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 IntroLED-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!

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 hidden below.

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


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); }
  }
}


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.On;
      [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 Eclipse 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.

Enjoy this article? Don't forget to share.