namespace SP
{
[Feature]
public static class ReqParams
{
readonly static Set
C = new Set(3);
readonly static Set M() { return Credits.window; }
[Action("ReqSetup(m,c)")]
[Action("ReqWork(m,c)")]
static void Req([Domain("M")]int m, [Domain("C")]int c){ }
}
}
The model program SP[Credits,Commands,SetupModel,ReqParams] is explorable
for controllable actions but not for observable actions. Nevertheless, it is possible to
run ct with the following options, where SP.OTFTest.Make is a factory method for
this model program.
/r:SPImpl.dll /r:SP.dll SP.OTFTest.Make /iut:SPImpl.Stepper.Make
/o:ResWork /o:ResSetup
The following is a sample output that shows a conformance failure similar to the
one shown in Figure 16.1. Notice that the reason in the failure has been extracted
from the requirement attribute of the ResEnabled1 condition in Section 14.2.1 that
268 Reactive Systems
refers to the part of the natural language document that specifies the condition that
clients must not starve.
TestResult(7, Verdict("Failure"),
"Action ??™ResWork(1, 0, Status(\"Completed\"))??™ not enabled in the model
Section ...: Client must have enough credits",
Trace(
ReqSetup(0, 3),
ResSetup(0, 1, Status("Completed")),
ReqWork(1, 3),
ResWork(1, 0, Status("Completed"))
)
)
16.5 Adaptive on-the-fly testing
Recall the test execution algorithm from Section 12.
Pages:
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352