Jonathan Jacky, Margus Veanes, Colin Campbell, Wolfram Schulte
"Model-Based Software Testing and Analysis with C#"
EmptySequence;
static readonly Set
elements = new Set(0,1,2,3,4,5);
[Action]
static void Push([Domain("elements")] int x)
{ contents = contents.AddFirst(x); }
static void PopEnabled() { return !contents.IsEmpty; }
[Action]
static void Pop() { contents = contents.Tail; }
[StateFilter]
static bool SizeLimit() { return contents.Count < 6; }
[StateProperty("Count")]
static int Count() { return contents.Count; }
}
}
If we explore this model program using the mpv tool without state grouping, we
notice that it branches quickly. However, if we use the Count property as a state
190 Analyzing Systems with Complex State
grouping, then the branching is eliminated. Instead, we explore an action only if it
leads to a state with a Count value that has not previously been seen. The idea in this
example is that the size of the stack is the interesting property and that the particular
choice of elements may be ignored for the purposes of analysis.
The mpv tool supports state grouping over state property state-property with the
/group:state-property switch. More than one /group switch may be supplied. If
grouping is specified then each state must produce a new value for at least one of
the given state properties in order to be included in the exploration.
11.3 Sampling
Up to this point we have discussed pruning techniques that eliminate some transitions
from an exhaustive search.
Pages:
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259