To perform a simulation,
simply code a main method or a unit test that calls the methods in the model program
in the order that expresses the scenario you wish to see. Then execute it and observe
the results.
We can analyze the model program more thoroughly by a technique called exploration,
which achieves the effect of many simulation runs. It is our primary technique
for analyzing model programs. Exploration automatically executes the methods of
the model program, selecting methods in a systematic way to maximize coverage of
the model program??™s behavior, executing as many different method calls (with different
parameters) reaching as many different states as possible. Exploration records
each method call it invokes and each state it visits, building a data structure of states
linked by method calls that represents a finite state machine (FSM).3
The mpv (Model Program Viewer) tool performs exploration and displays the
results as a state-transition diagram, where the states appear as bubbles, the transitions
between them (the method calls) appear as arrows, and interesting states and
transitions are highlighted (see, e.g., Chapter 3, Figures 3.8??“3.11).
The input to mpv is one or more model programs to explore. If there is more than
one, mpv forms their composition and explores the composed program. Composition
can be used to limit exploration to particular scenarios of interest, or to formulate
temporal properties to analyze.
Pages:
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32