The actions can be method calls with arguments, which can also have a great
many values. In that case, the number of states and transitions defined by the model
program is effectively ???infinite???: much too large to write down, or even to store in a
computer. Then it is not possible to completely explore the true FSM.We will write
and analyze such infinite model programs in Part III. In Chapter 11, we will showhow
to configure nonexhaustive exploration of infinite model programs, in order to perform
analyses that are incomplete, but still useful (we will finitize the analysis instead
of the model). But here in Part II, we only consider model programs where we can
completely explore the true FSM. That is why we emphasized finitizing the model
programs in Chapter 5.
6.2 Exploration
Recall that exploration automatically generates an FSM from a model program. The
FSM can then be used for visualization, analysis, and offline test generation. In the
following subsections we explain how to explore a model program with the library
and tools.
6.2.1 Accessing the model program
To work with the library or any tool created from it (including mpv, otg, or ct), a
model program must provide a factory method that creates a LibraryModelProgram
object from the compiled model program assembly. All tools access the model
program indirectly, by invoking the methods of this object.
Pages:
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151