Timeout;
static WaitFor waitfor = WaitFor.Timeout; // enable Reset
static Sensor sensor = Sensor.Error; // enable Reset
// Control state added for model
// Alternate between waiting for events and handling events
static Phase phase = Phase.WaitForEvent;
// Model the timer and the sensor
static bool TimeoutScheduled = true;
static bool MessageRequested = false;
// Data state from implementation
static string buffer = OutOfRange;
static double previous = Uninitialized;
// Constants
const string InRange = "99.9"; // for buffer
const string OutOfRange = "999.9"; // for buffer
const double Uninitialized = double.MaxValue; // for previous
// continued ...
Figure 5.12. Reactive system: model program (part 1).
Systems with Finite Models 87
// ... Reactive system model program, continued
// Actions and enabling conditions for Controller, from implementation
static bool ResetEnabled()
{
return (cevent == ControlEvent.Timeout
&& waitfor == WaitFor.Timeout
&& sensor == Sensor.Error
&& phase == Phase.HandleEvent);
}
[Action]
static void Reset()
{
ResetSensor(); // send reset command to sensor
StartTimer(); // wait for message from from sensor
waitfor = WaitFor.Message;
phase = Phase.WaitForEvent;
}
static bool PollEnabled()
{
return (cevent == ControlEvent.Timeout
&& waitfor == WaitFor.Timeout
&& sensor == Sensor.OK
&& phase == Phase.HandleEvent);
}
[Action]
static void Poll()
{
PollSensor(); // send poll command to sensor
StartTimer(); // wait for message from sensor
waitfor = WaitFor.
Pages:
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137