This command invokes mpv on the NewsReader model program.1
mpv /r:NewsReaderUI.dll NewsReader.Factory.Create
6.2.2 Exhaustive exploration and visualization
When the mpv tool is invoked on a finite model program, it exhaustively explores
the model program, generates its true FSM, and displays its state transition graph.
For example, invoking mpv on NewsReader (as in the command earlier) displays the
graph in Figure 6.4.
The graph generated by mpv looks similar to Figure 6.2, but not exactly the same.
In Figure 6.2, each node is labeled by the values of all the state variables in that
state. This does not generalize to many state variables, so mpv simply labels each
node with a number. The initial state is always number zero but the other numbers
are arbitrary. The mpv tool provides a state viewer panel that shows all of the state
variables and their values in the selected node. This enables mpv to be used as a kind
of debugger for model program that can be run forward or backward.2
Although Figures 6.2 and 6.4 do not look exactly the same, they both represent
the same FSM. The positions of nodes and links can be quite sensitive to the choice
of display options and other factors, so graphs that appear different at first glance
can be diagrams of the same FSM. Graphs you generate (from the same model
programs) might not look much like the figures in this book.
Pages:
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153