A better way to deal with this case would be to use the Feature attribute we saw
in Section 7.2. To do this, we create a new class within the same namespace:
namespace Counter
{
[Feature]
static class SmallDomain
{
readonly Set
inputs = new Set(0, 1, 2, 3, 4);
[Action]
static void ModularIncrement([Domain("inputs")] int x) { }
}
}
We can combine the SmallDomain feature with the contract model program by means
of a factory method. Factory methods were introduced in Section 6.2.1.
namespace Counter
{
public static class Factory
{
public static ModelProgram Create()
{
return new LibraryModelProgram(typeof(Factory).Assembly,
"Counter", Set.EmptySet);
}
public static ModelProgram CreateFinite()
{
return new LibraryModelProgram(typeof(Factory).Assembly,
"Counter", new Set("SmallDomain"));
}
}
}
The factory contains methods that create either of two versions of the Counter
model. The model program produced by CreateFinite includes the feature that
restricts the domain to five elements. The advantage of this approach is that it keeps
186 Analyzing Systems with Complex State
an understandable separation between scenario and contract model program. It also
makes it possible for there to be several scenarios, not just one. Also, even though it
is not explorable, the full contract model program is useful for other purposes, such
as determining whether a trace taken from a log file is valid.
Pages:
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254