HandleEvent);
}
[Action]
static void ReportLostMessage()
{
StartTimer(); // wait for next time to poll
waitfor = WaitFor.Timeout;
phase = Phase.WaitForEvent;
}
// NoHandler is enabled when no other handler is enabled
static bool NoHandlerEnabled()
{
return (phase == Phase.HandleEvent
&& !ResetEnabled()
&& !PollEnabled()
&& !CalibrateEnabled()
&& !CheckMessageEnabled()
&& !ReportLostMessageEnabled());
}
[Action]
static void NoHandler()
{
phase = Phase.WaitForEvent;
}
// continued ...
Figure 5.15. Reactive system: model program (part 4).
90 Model Programs
// ... Reactive system model program, continued
// Actions and enabling conditions for environment, added for model
static bool TimeoutEnabled()
{
return (!MessageRequested
&& TimeoutScheduled
&& phase == Phase.WaitForEvent);
}
[Action]
static void Timeout()
{
cevent = ControlEvent.Timeout;
TimeoutScheduled = false;
phase = Phase.HandleEvent;
}
static bool TimeoutMsgLostEnabled()
{
return (MessageRequested
&& TimeoutScheduled
&& phase == Phase.WaitForEvent);
}
[Action]
static void TimeoutMsgLost()
{
cevent = ControlEvent.Timeout;
TimeoutScheduled = false;
phase = Phase.HandleEvent;
MessageRequested = false;
}
// continued ...
Figure 5.16. Reactive system: model program (part 5).
Systems with Finite Models 91
// ... Reactive system model program, continued
static bool TimeoutMsgLateEnabled()
{
return (MessageRequested
&& TimeoutScheduled
&& phase == Phase.
Pages:
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139