After reading about
these techniques you might even be inspired to invent a few of your own.
11.1 Explorable model programs
We say that a model program is explorable if the domain of every action parameter
is ???finite??? (feasible to enumerate).1 You might recall from Section 10.1 that a model
program may be ???large??? in several ways. Either the number of states may be large
or the number of transitions may be large, or both.
Consider the model program that uses modular arithmetic to increment a counter:
namespace Counter
{
static class Contract
1 As in the previous chapters, we use the term finite to mean the case where it is computationally
feasible to enumerate all of the values. Although the number of 32-bit integers is fixed, we don??™t
consider it feasible to enumerate all 32-bit integers during exploration.
183
184 Analyzing Systems with Complex State
{
static int counter = 0;
[Action]
static void ModularIncrement(int x)
{ counter = (counter + x) % 5; }
}
}
This model program is not explorable because the parameter x could take an ???infi-
nite??? (very large) number of values. We sometimes call a model program like this a
contract model program because it defines all possible behaviors of a system, even
when those behaviors are too complex to be encoded as a finite state machine. In
fact, many contract model programs will not be explorable.
Pages:
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252