For visual validation of the behavior it is useful to restrict the size of the explored
state space to a small portion of the full state space. However, if the client is
being controlled by the tester and the server is observed only by the tester, it is
important not to restrict the behavior of the server in order to use the composition
as a test oracle. Restricting the observable behavior in the composition may lead
to false negatives during testing. Testing with observable actions is the topic of
Chapter 16.
Advanced Topics 239
namespace SP
{
[Feature]
public static class CreditScenario
{
static readonly Set
C = new Set(2);
static Set M()
{
if (Credits.window.IsEmpty)
return Set.EmptySet;
else
return new Set(Credits.window.Minimum());
}
[Action("ReqSetup(m,c)")]
[Action("ReqWork(m,c)")]
static void Req([Domain("M")]int m, [Domain("C")]int c) { }
static bool ReqEnabled(int m) { return m < 3; }
[Action("ResSetup(m,c,_)")]
[Action("ResWork(m,c,_)")]
static void Res(int m, int c){}
static bool ResEnabled(int m, int c)
{
return Credits.requests.ContainsKey(m) &&
Credits.requests[m] == c;
}
}
[Feature]
public static class CancelScenario
{
static Set M()
{
if (Cancellation.mode.Keys.Count < 2)
return Set.EmptySet;
else
return new Set(Cancellation.mode.Keys.Minimum());
}
[Action]
static void Cancel([Domain("M")]int m) { }
static bool CancelEnabled(int m)
{
return Cancellation.
Pages:
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318