In
our sandbox implementation, simulated events were generated by the user (through
the Simulator class, Figures 3.5 and 3.6) or by the test fixture (Figure 3.7). In the
model, we cannot use a .NET timer as we did in the simulator, because the time-out
events must be scheduled by the tools.
Actions
There is an action in the model program for every event handler in the implementation??™s
Controller class: Reset, Poll, and so on. The enabling conditions
for these actions are the same as the guards in the implementation: ResetEnabled,
PollEnabled, and so on. There is no action in the model corresponding to the implementation??™s
DispatchHandler method; its control structure is implicit in the enabling
conditions.
There is also an action for each kind of event that the reactive program handles. In
the implementation, there is a single method ReceiveEvent with a cevent parameter
that indicates what kind of event occured. Our several event actions correspond
to different invocations of ReceiveEvent with different values for cevent. In the
model, it turns out to be simpler to define a different action for each type of event,
because each has a different enabling condition and makes different updates to the
model state. In fact, there are more of these action methods than event types. For the
Timeout event, we have the actions Timeout, TimeoutMsgLost, and TimeoutMsgLate.
Pages:
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132