Running ct. Let us add another factory method CreateModelWithProbe to the
Factory class in BagModel that constrains the bag model by including the ElementRestriction
and the Probe features.
public static ModelProgram CreateModelWithProbe()
{
return new LibraryModelProgram(typeof(Contract).Assembly,
"BagModel", new Set
("ElementRestriction","Probe"));
}
Figure 12.6 shows a partially explored part of the state machine of CreateModelWithProbe
composed with ProbeScenario and AddDeleteScenario, using mpv.
Systems with Complex State 213
0
19
Add("")
2
Add("b")
9
12
CheckView(Set(""))
1
CheckView(Set("b"))
6
Add("")
20
Add("b")
14
CheckView(Set("b", ""))
4
CheckView(Set("b"))
15
Delete("b")
8
Delete("")
10
CheckView(Set("b"))
16
CheckView(Set("b"))
Delete("b")
Delete("")
Delete("")
17
Delete("b")
CheckView(Set())
Delete("")
7
Delete("b")
18
CheckView(Set(""))
Delete("")
Delete("b")
Add("b")
13
Add("")
3
CheckView(Set(""))
Delete("")
5
Delete("b")
11
CheckView(Set(""))
Delete("")
Delete("b")
Figure 12.6. Partial exploration of CreateModelWithProbe composed with ProbeScenario and
AddDeleteScenario.
214 Testing Systems with Complex State
Probes typically increase the possibility of finding errors earlier.We can see how
ct discovers the bug in the faulty bag implementation much sooner than before,
by using CreateModelWithProbe composed with ProbeScenario and AddDeleteScenario
TestResult(1, Verdict("Failure"),
"Inconsistent views of state: model:Set() iut:Set(\"b\")",
Trace(
Add("b"),
CheckView(Set("b")),
Delete("b"),
CheckView(Set())
)
)
12.
Pages:
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287