This handler??™s enabling condition NoHandlerEnabled
returns true in states where every other handler??™s enabling condition
returns false. The handler itself does nothing but assigns phase.
The two control state variables TimeoutScheduled and MessageRequested, which
do not appear in the implementation, model the timer and the sensor. TimeoutScheduled
is in the enabling condition for every time-out event and MessageRequested is
in the enabling condition for the message event.
There is only one Timeout event in the implementation, but there are three timeout
event action methods in the model. Timeout models a time-out that arrives
when the controller is not waiting for a message; !MessageRequested appears in
its enabling condition. TimeoutMsgLost, and TimeoutMsgLate model time-outs that
arrive when a message is expected; MessageRequested appears in their enabling
conditions. TimeoutMsgLost models what happens in the implementation when the
message is lost; it assigns MessageRequested = false so the message will never be
86 Model Programs
using System; // Math for Abs in CheckMessage
using NModel;
using NModel.Attributes;
using NModel.Execution;
namespace Reactive
{
static class Controller
{
// Types from implementation
enum ControlEvent { Timeout, Message, Command, Exit }
enum WaitFor { Timeout, Message }
enum Sensor { OK, Error }
// Types added for model
enum Phase { WaitForEvent, HandleEvent }
// Control state from implementation
static ControlEvent cevent = ControlEvent.
Pages:
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136