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