The mpv tool finds 239 transitions and 121 states, including
4 unsafe states. The unsafe states are marked but they are hard to find in Figure 6.9.
They are easier to find in the mpv session, where we can magnify and scroll the
graph.
To check that the unsafe states found by exploration include the one we expect,
we explore interactively. We reproduce the OutOfRangeMessageWhenIdle run we
found by experimenting with the implementation (Chapter 3, Section 3.4). The
FSM we generate shows a path to one of the unsafe states (Figure 6.10). This FSM
contains the second trace we wrote in Chapter 5, Section 5.7.1. The unsafe state is
the state labeled 105 near the bottom of the diagram, where Calibrate is enabled.
4 Here we apply De Morgan??™s Law, which shows how to negate expressions involving and and
or: !(p && q) == !p || !q.
108 Exploring and Analyzing Finite Model Programs
0
2
Timeout()
1
Command()
71
113
Calibrate()
99
103
Calibrate()
11
13
Calibrate()
32
36
Calibrate()
105
107
Calibrate()
117
119
Calibrate()
3
Reset()
22
NoHandler()
Timeout()
Command()
4
Command()
6
Message("999.9")
8
TimeoutMsgLost()
7
Message("99.9")
5
TimeoutMsgLate()
52
NoHandler()
9
CheckMessage()
19
NoHandler()
10
CheckMessage()
14
NoHandler()
17
Message("99.9")
16
Message("999.9")
15
Command()
CheckMessage() CheckMessage()
18
NoHandler()
Message("99.
Pages:
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164