Information Technology Reference
In-Depth Information
6.4.1
Testing with Extremal Derivatives
A
test
is simply a process in the language
rpCSP
, except that it may in addition
use special
success
actions for reporting outcomes; these are drawn from a set
ʩ
of
fresh actions not already in
Act
˄
. We refer to the augmented language as
rpCSP
ʩ
.
Formally a test
T
is some process from that language, and to apply test
T
to process
P
we form the process
T
|
Act
P
, in which
all
visible actions of
P
must synchronise
with
T
. The resulting composition is a process whose only possible actions are
˄
and the elements of
ʩ
. We will define the result
d
(
T
,
P
) of applying the test
T
to the process
P
to be a set of testing outcomes, exactly one of which results from
each resolution of the choices in
T
A
|
Act
P
. Each
testing outcome
is an
ʩ
-tuple of real
numbers in the interval [0,1], that is, a function
o
:
ʩ
ₒ
[0, 1], and its
ˉ
-component
o
(
ˉ
), for
ˉ
ʩ
, gives the probability that the resolution in question will reach an
ˉ-success state
, one in which the success action
ˉ
is possible.
We will now give a definition of
∈
d
(
T
,
P
), which is intended to be an alternative of
A
A
(
T
,
P
). Our definition has three ingredients. First of all, to simplify the presentation
we normalise our pLTS by removing all
˄
-transitions that leave a success state. This
way an
ˉ
-success state will only have outgoing transitions labelled
ˉ
.
ₒ
Definition 6.6 (
ˉ
-Respecting)
Let
be a pLTS such that the set of labels
L
includes
ʩ
. It is said to be
ˉ-respecting
whenever
s
S
,
L
,
ˉ
−ₒ
˄
.
It is straightforward to modify an arbitrary pLTS so that it is
ˉ
-respecting. Here
we outline how this is done for our pLTS for
rpCSP
.
, for any
ˉ
∈
ʩ
,
s
−ₒ
Definition 6.7 (Pruning)
Let [
·
] be the unary operator on
ʩ
-test states given by the
operational rules
ˉ
−ₒ
ʱ
−ₒ
ˉ
s
ʔ
s
−ₒ
(for all
ˉ
∈
ʩ
),
s
ʔ
(
ˉ
∈
ʩ
)
(
ʱ
∈
Act
˄
)
.
ˉ
−ₒ
ʱ
−ₒ
[
s
]
[
ʔ
]
[
s
]
[
ʔ
]
Just as
and
|
A
, this operator extends as syntactic sugar to
ʩ
-tests by distributing
[
ʔ
(
s
). Clearly, this
operator does nothing else than removing all outgoing transitions of a success state
other than the ones labelled with
ˉ
·
] over
p
↕
; likewise, it extends to distributions by [
ʔ
]([
s
])
=
ʩ
.
Next, using Definition
6.4
, we get a collection of subdistributions
ʘ
reachable
from [[[
T
∈
|
Act
P
]]]. Then, we isolate a class of special weak derivatives called
extreme
derivatives
.
˄
−ₒ
Definition 6.8 (Extreme Derivatives)
A state
s
in a pLTS is called
stable
if
s
,
and a subdistribution
ʘ
is called
stable
if every state in its support is stable. We write
ʔ
⃒
ʘ
whenever
ʔ
⃒
ʘ
and
ʘ
is stable, and call
ʘ
an
extreme
derivative
of
ʔ
.
Referring to Definition
6.4
, we see this means that in the extreme derivation of
ʘ
from
ʔ
at every stage a state must move on if it can, so that every stopping component
can contain only states that
must
stop: for
s
ʔ
k
ʔ
k
ʔ
k
∈
+
we have that
s
∈
˄
if
and now also
only if
s
−ₒ
. Moreover, if the pLTS is
ˉ
-respecting then whenever
Search WWH ::
Custom Search