In each
state, exploration executes each action method repeatedly, using as many different
values as it can from the domains of all its parameters, so larger domains result in
more transitions and more runs. Therefore, selecting domains can limit or select
runs. In our examples in Chapter 5, each domain is coded directly into the contract
model program. In the client/server example, one particular domain Temperatures
is always used for the datum parameter of the ServerSend action method:
[Action]
static void ServerSend([Domain("Temperatures")] double datum)
...
static Set
Temperatures()
...
Systems with Finite Models 121
This code is inflexible. It is often better to separate the domains from the contract
model program, so the same model program can be configured with different domains
for different scenarios. Figure 7.5 shows how to use features to achieve this.
In the contract model program, code the action method without a domain. Then, in a
feature, code an action method with the same name, but include the domain. Leave
the body of this action method empty. To select that domain, include that feature.
When the combined action executes, the domain from the selected feature is used,
and the body of the action method in the contract model program executes with
a parameter value from that domain. (In this example the feature has no enabling
conditions; the ones in the contract model program are sufficient.
Pages:
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182