For example, we could consider the scenario where the modular counter is
incremented by even numbers and odd numbers in alternation.
FSM(0, AcceptingStates(0),
Transitions(t(0, ModularIncrement(0), 1),
t(1, ModularIncrement(1), 0),
t(0, ModularIncrement(2), 1),
t(1, ModularIncrement(3), 0),
t(0, ModularIncrement(4), 1)))
This is a contrived example, just for the purposes of demonstrating the idea.
Systems with Complex State 189
11.2.5 State grouping
State grouping is a pruning technique that limits exploration to unique representatives
of user-provided state properties. If during exploration a state is encountered
that does not produce a new value of one of the desired properties, it is pruned away.
In other words, state exploration with grouping seeks to produce distinct examples
of the abstracted state values, rather than distinct states. This can reduce the number
of states greatly while still uncovering ???interesting??? traces.
An attribute in the form [StateProperty("name")] can be placed on a method,
property or field to define a state property named name. The value of the property in
a given state is the return value of the method, or the value of the field or property in
that state. State properties are sometimes called abstraction functions because they
remove detail.
Here is an example.
namespace Stack
{
static class Contract
{
static Sequence
contents = Sequence.
Pages:
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258