9");
NoHandler();
Command();
Calibrate();
In this trace, two different time-out actions appear: Timeout and TimeoutMessageLate.
The NoHandler action here indicates that no handlers are enabled after the
second message.
State variables
In this example, the parts of the model program that model the Controller class are
similar to the implementation. The model program has these control state variables,
which also occur in the implementation: cevent, the most recent event; waitfor, the
kind of event the controller is waiting for; and sensor, the inferred sensor status.
The model program has additional control state variables that are not in the
implementation. TimeoutScheduled and MessageRequested model the timer and the
sensor to ensure that events are modeled realistically. They are tested by the enabling
conditions for the event actions, and are updated by the event actions. Finally, the
phase variable controls the alternation of events and handlers.
Systems with Finite Models 85
The model program has two data state variables, which also appear in the implementation:
buffer and previous, the most recent temperature sample and the
preceding temperature sample. These are numbers, so they could generate an ???in-
finite??? state space. To finitize our model, we limit both variables to just two values
that represent temperatures that are within-range and out-of-range (by the criteria
explained in Chapter 3, Section 3.
Pages:
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134