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