Information Technology Reference
In-Depth Information
Fig. 5.4
Collecting results
1
1
V
f
(
ʔ
s
)
=
2
·{
1, 0
}+
2
·{
1
}
that, since there are only two possible choices, evaluates
1
further to
{
2
,1
}
. Similarly
V
f
(
t
1
)
= V
f
(
t
2
)
={
0, 1
}
and we calculate that
1
4
·{
3
4
·{
0,
1
4
,
3
V
f
(
ʔ
t
)
=
0, 1
}+
0, 1
}={
4
,1
}
.
Definition 5.2
|
Act
P
]] .
With this definition we now have two testing preorders for
pCSP
, one based on
may
testing
,
P
pmay
Q
, and the other on
must testing
,
P
pmust
Q
.
Comparing the results-gathering function
For any process
P
∈
pCSP
and test
T
, let
A
(
T
,
P
)
= V
f
[[
T
V
f
in definition
5.1
with the one given
in Sect. 4.2, we notice that the former only records those testing outcomes obtained
by using static resolutions of a pLTS while the latter records the outcomes of all
resolutions. Here, we prefer to use the former that is simpler because we are dealing
with scalar testing and as a matter of fact applying convex closure to subsets of the
one-dimensional interval [0, 1] (such as those arisen from applying scalar tests to
processes) has no effect on the Hoare and Smyth orders between these subsets.
Lemma 5.1
Suppose X
,
Y
ↆ
[0, 1]
. Then
1. X
≤
Ho
Y , if and only if
X
≤
Ho
Y .
2. X
≤
Sm
Y , if and only if
X
≤
Sm
Y .
Proof
We restrict attention to the first clause; the proof of the second one goes
likewise. It suffices to show that (i)
X
≤
Ho
X
and (ii)
X
≤
Ho
X
. We only prove (ii)
=
i
∈
I
p
i
x
i
for a finite set
I
with
since (i) is obvious. Suppose
x
∈
X
, then
x
i
∈
I
p
i
=
X
. Let
x
∗
=
1 and
x
i
∈
max
{
x
i
|
i
∈
I
}
, then
p
i
x
∗
=
x
∗
∈
x
=
p
i
x
i
≤
X.
i
∈
I
i
∈
I
Search WWH ::
Custom Search