To do this we can use a state filter. A state filter is a Boolean condition that must
be satisfied in the end state of a transition in order for the transition to be included
in the exploration. State filters say which states are ???interesting??? for analysis.
We can keep the contract separate from the ???small state??? scenario limitation by
putting the state filter in a feature:
namespace Counter2
{
[Feature]
static class SmallState
{
[StateFilter]
static bool WithinCounterLimit()
{ return Contract.counter < 3; }
}
}
If you include the SmallState feature in your model program factory, then exploration
via the mpv tool will include only transitions that result in a state in which
the WithinCounterLimit method returns true.
11.2.3 Strenghening enabling conditions
Sometimes it is useful to omit certain kinds of transitions that are allowed by the
contract model program but are of less interest for a test purpose or analysis goal.
A general technique that can be used here is to strengthen enabling conditions.
With this technique, you can add additional constraints that depend on the state of
the system and the action parameters.
namespace Counter2
{
static class PreconditionLimits
{
static bool IncrementEnabled()
{ return Contract.counter < 2; }
[Action]
static void Increment() { }
}
}
188 Analyzing Systems with Complex State
Including this feature limits possible transitions by adding a state-based requirement
to the Increment action.
Pages:
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256