11.2 Pruning techniques
Once you have made your model program explorable by using the technique described
in the previous section, you may still notice that it has an unbounded number
of possible states. In this section we introduce some techniques for managing this
proliferation of states.
11.2.1 State and transition limits
A simple way of limiting the number of transitions is to impose a limit and then
halt exploration after the maximum number has been reached. You can do this by
providing a maxTransitions command-line argument to the mpv tool.
Although this technique is simple, it isn??™t very systematic. Still, it is a useful stop
gap when other pruning techniques haven??™t been applied yet.
11.2.2 State filters
Sometimes it??™s useful to consider only a subset of the possible states. For example,
consider the following explorable, but infinite, model program:
namespace Counter2
{
static class Contract
{
public static int counter = 0;
[Action]
static void Increment() { counter = counter + 1; }
static bool DecrementEnabled() { return counter > 0; }
[Action]
static void Decrement() { counter = counter - 1; }
}
}
Systems with Complex State 187
We might want to consider only states where the counter is 0, 1, or 2. Clearly,
this is a small subset of the possible states for this model program, but it is a good
place to start when trying to analyze the behavior of the system.
Pages:
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255