Some judgment and understanding of a program??™s purpose is required
in order to identify its accepting states.
Recall that the purpose of our reactive system is to perform a calibration with a
valid temperature sample. Also recall that a temperature sample is considered valid
when it does not differ too much from the preceding sample. Therefore, the goal
of the program has been achieved when two successive within-range temperatures
have been sampled, and a Calibration action occurs. Liveness analysis requires that
we express this in terms of a state, not an action, so once again we subsitute the
action??™s enabling condition for the action itself. The accepting state condition is
CalibrateEnabled() && buffer == InRange
&& previous == double.Parse(InRange)
We wrap this expression in a static method, label it with the [AcceptingStateCondition]
attribute, and place it in the Controller class in the Reactive model program
namespace (Figure 6.11).
Now that we have defined the accepting state condition, exploration can find all
of the accepting states and dead states in the generated FSM. We command the mpv
tool to explore the reactive system model program, and to count and display unsafe
states:
mpv /r:Controller.dll Reactive.Factory.Create /livenessCheckIsOn+ ...
Figure 6.12 shows the generated FSM. We had to increase MaxTransitions to
300 to generate the true FSM.
Pages:
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169