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

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