Information Technology Reference
In-Depth Information
Definition 6.10
Let
P
be a
rpCSP
process and
T
an
ʩ
-test. Then
d
(
T
,
P
):
A
={
$
ʘ
|
[[[
T
|
Act
P
}
]] ]
⃒
ʘ
}
.
The role of pruning in the above definition can be seen via the following example.
Example 6.7
ˉ.
0
). The pLTS generated by
applying
T
to
P
can be described by the process
˄.
(
˄.
0
Let
P
=
a.b.
0
and
T
=
a.
(
b.
0
ˉ.
0
). Then [[
T
|
Act
P
]] has
a unique extreme derivation [[
T
|
Act
P
]]
⃒
[[
0
]], and [[[
T
|
Act
P
]]] also has a unique
d
(
T
,
P
) shows that
process
P
passes test
T
with probability 1, which is what we expect for state-based
testing, which we use in this topic. Without pruning we would get an outcome saying
that
P
passes
T
with probability 0, which would be what is expected for action-based
testing.
Using the two standard methods for comparing two sets of outcomes, the Hoare-
and Smyth preorders, we define the may- and must-testing preorders; they are
decorated with
extreme derivation [[[
T
|
Act
P
]] ]
⃒
[[
ˉ.
0
]]. The outcome in
A
ʩ
·
for the repertoire
ʩ
of testing actions they employ.
Definition 6.11
pmay
Q
if for every
ʩ
-test
T
,
A
d
(
T
,
P
)
≤
Ho
A
d
(
T
,
Q
).
1.
P
pmust
Q
if for every
ʩ
-test
T
,
d
(
T
,
P
)
d
(
T
,
Q
).
2.
P
A
≤
Sm
A
These preorders are abbreviated to
P
pmay
Q
and
P
pmust
Q
, when
|
ʩ
|=
1.
Example 6.8
Consider the process
Q
1
=
rec
x.
(
˄.x
2
↕
a.
0
), which was already
discussed in Sect.
6.1
. When we apply the test
T
a.ˉ.
0
to it we get the pLTS
in Fig. 4.3b, which is det
er
ministic and unaffected by pruning; from part (ii) of
Lemma
6.7
it follows that
s
0
has a unique extreme derivative
ʘ
. Moreover,
ʘ
can
be calculated to be
=
1
2
k
·
s
3
,
k
≥
1
{
ˉ
which simplifies to the distribution
s
3
. Thus it gives the same set of results
gained
by applying
T
to
a.
0
on its own; and in fact it is possible to show that this holds for
all tests, giving
}
Q
1
pmay
a.
0
Q
1
pmust
a.
0
.
Consider the process
Q
2
=
rec
x.
((
x
2
↕
a.
0
)
(
0
2
↕
a.
0
)) and the
Example 6.9
application of the same test
T
a.ˉ.
0
to it, as outlined in Fig. 4.4a and b.
C
onsider any extreme derivative
ʔ
from [[[
T
=
|
Act
Q
2
]]], which we have abbreviated
to
s
0
; note that here again pruning actually has no effe
ct
. Using the notation of
Definition
6.4
, it is clear th
at
ʔ
0
and
ʔ
0
must be
ʵ
and
s
0
respectively. Similarly,
ʔ
1
and
ʔ
1
must be
ʵ
and
s
1
respectively. But
s
1
is a nondeterministic state, having
two possible transitions:
Search WWH ::
Custom Search