9")
TimeoutMsgLate() Message("999.9")
Command()
Timeout()
Message("999.9") TimeoutMsgLost()
Command()
Message("99.9") TimeoutMsgLate()
Figure 6.12. Reactive system: True FSM showing accepting states and dead states.
links connecting outside (lower left and lower right in Figure 6.12). This indicates
that, depending on the first several actions at startup, the program permanently enters
one or the other of two modes. In one of these modes, all of the states are dead states
(lower left in Figure 6.12). Inspecting the FSM closely (magnifying and scrolling
in mpv) reveals that the program enters this mode when the first temperature sample
is out-of-range. After that the program cannot escape. This is the same behavior we
observed in the InitialOutOfRangeMessage run we found by experimenting with the
implementation, where an out-of-range temperature sample at startup is followed by
a livelock where the program resets endlessly without making progress (Chapter 3,
Section 3.4). Exploring interactively, we reproduce the InitialOutOfRangeMessage
run (Figure 6.13). The cycle including the Reset action appears in the lower right
of the diagram. Exploration finds that all of states on the frontier at lower left in
this diagram are also dead states. They offer no escape; they only lead to longer
cycles.
112 Exploring and Analyzing Finite Model Programs
0
2
Timeout()
1
Command()
3
Reset()
6
Message("999.
Pages:
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173