The type of each parameter of enabling
condition method must match the type of the corresponding parameter in the action
method.
A static enabling condition method may be used for an instance-based action
method. If the static enabling condition method takes parameters, the first parameter
must represent the this parameter:
class Bar
{
static void FooEnabled(Bar obj)
{
return obj != null && obj.mode == Mode.Start;
}
static void FooEnabled(Bar obj, int x)
{
return x > 0;
}
[Action]
void Foo(int x)
{
this.mode = Mode.Running;
}
}
A.1.5 Parameter domains
Model programs may be given finite domains for exploration. This is done using the
[Domain] attribute applied to method parameters. The form of the domain attribute
is
[Domain("name")]
Appendices 289
where name is a string naming a method, property, or field in the containing class.
An example of its use is
[Action]
static void Foo([Domain("SomeInts")] int x)
{
/* ... */
}
static readonly Set
SomeInts = new Set(1, 2, 3, 4);
If a method name is given as the domain name and the action method is static,
then the domain method must also be static. For an instance-based action method,
domain methods may be either static or instance-based. Domain methods must
take no parameters. Their return type must be a Set, where T is the type of the
parameter being attributed.
Only types with finite domains have default domains.
Pages:
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377