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

4.3.2 Updating the foreign 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 foreign code. As we are generating a thread-safe-shell for the System, it is permitted to call the event directly from foreign code; queueing it in the System dzn::pump is done by default.

As an exercise, add the calling of the cancelled event to the foreign Timer implementation (found in


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


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


  std::string input;
  while(std::cin >> 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 foreign 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 section.