Language keywords: 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;
}

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.

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

image

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