decrementCtr method

void decrementCtr (
  1. covariant Rocket sm
)

Handler for timer expiration

Note that at this point we are not in the SamModel.present execution scope so we generate a proposal of RK.saDecrement to present to the model that will do the actual decrementing.

It is possible that the event will occur after we have changed the model state to either RK.ssAborted or RK.saPause through actions generated by pressing the buttons that trigger these actions. For this reason we ignore RK.saDecrement on the state definitions for RK.ssAborted and RK.saPause.

Implementation

void decrementCtr(covariant Rocket sm) {
  if(sm.bLog)log("_decrementCtr");
  sm.present(sm.samState,RK.saDecrement);
}