The additional code in our several event actions (compared to ReceiveEvent) is
necessary because the model program must model the environment that generates
events, in addition to the controller.
The model program alternates between executing an event action and a handler
action. We have to define a do-nothing handler NoHandler to model what happens
when no handler is enabled in the implementation.
Traces
We write some sample traces to show how behaviors discussed in Chapter 3 are
expressed in the action vocabulary we chose. The run coded in the test method
named Typical (section 3.3) is expressed by this trace:
Timeout();
Reset();
Message("99.9");
CheckMessage();
84 Model Programs
Timeout();
Poll();
Message("100.0");
CheckMessage();
Command();
Calibrate();
Compare this trace to the test method (Figure 3.7) and the test output (Section 3.3).
The calls to ReceiveEvent in the test method are modeled by different actions for
each kind of event: Timeout, Message, and Command (the Exit event is not modeled).
The calls to DispatchHandler are modeled by the actions for each handler: Reset,
Poll, and Calibrate.
The simulation in Section 3.4 that shows an unsafe run, labeled OutOfRangeMessageWhenIdle,
is expressed by this trace:
Timeout();
Reset();
Message("99.9");
CheckMessage();
Timeout();
Poll();
TimeoutMsgLate();
ReportLostMessage();
Message("999.
Pages:
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133