We’re here to help you

Menu

Finishing the Alarm System

In the previous chapter, you successfully implemented the behaviour of a component such that it still behaves correctly if communication over a port is potentially delayed. In this chapter, we will have a look at what needs to be done to make the rest of the Alarm System up to date and if any changes need to be made to native code.

Updating the Controller

A snapshot containing Dezyne models and native code for the current state of the Alarm System can be found here.

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:

image

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.

Exercise: Add this Rearming state to the behaviour of the Controller component.


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.

Exercise: Implement the described behaviour in the Rearming state.


[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 native implementation of the Timer, so that accurately reflects the ITimer changes as well.

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.


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


Updating the native Timer

By adding the cancelled out-event to the ITimer interface, we added a function to the System boundary (the System still requires an ITimer port) that needs to be called from native code. As we are generating a thread-safe-shell for the System, it is permitted to call the event directly from native code; queueing it in the System dzn::pump is done by default.

Exercise: Add the calling of the cancelled event to the native Timer implementation (found in main.cc).


int main(int argc, char* argv[])
{
  dzn::locator loc;
  dzn::runtime rt;
  std::ofstream logfile("log.txt");
  std::ostream outstream(nullptr);
  outstream.rdbuf(logfile.rdbuf());

  loc.set(rt).set(outstream);

  AlarmSystem as(loc);
  as.dzn_meta.name = "AlarmSystem";

  as.iTimer.in.start = [] (int ms) { alarm(ms/1000); };
  as.iTimer.in.cancel = [&] () { alarm(0); as.iTimer.out.cancelled(); };
  timeout = as.iTimer.out.timeout;
  signal(SIGALRM, sigalrm_handler);

  as.check_bindings();

  std::string input;
  while(std::cin >> input) {
    as.iController.in.passwordEntered(input);
  }
}


With this final addition in place, you will have a fully correct implementation of the ITimer interface that is verified to always correctly deal with possible race conditions that are caused by dzn::pump queue delay. If such delays occur, they are handled by the RobustTimer Dezyne component which is verifiably correct.

The final Dezyne models and Alarm System native source code can be found on GitHub

A future tutorial on the ‘blocking’ keyword will show you a way to make use of ‘external’ with even less modifications to surrounding components, if your execution model allows it. For now, let’s reflect on what we’ve learned in this tutorial in the next and final chapter.

If you have questions that weren’t answered by this Guide,
let our support team help you out.

Enjoy this article? Don't forget to share.