Information Technology Reference
In-Depth Information
when the subprocess (
b
c
) is being tested the subtest (
a.ˉ
3
↕
(
b.ˉ
2
↕
c.ˉ
)) will
give probability 0. In other words
min
(
0. When applying
T
2
to
R
2
,
things can never be as bad. The worst probability will occur when
T
2
is applied to
the subprocess (
a
2
↕
b
), namely probability
A
(
T
2
,
R
1
))
=
1
6
. We leave the reader to check that
0,
6
,
3
,
2
,
3
}
1
6
,
3
,
2
,
3
}
formally
A
(
T
2
,
R
1
)
={
and
A
(
T
2
,
R
2
)
={
.
Example 5.8
The axiom
P
(
Q
p
↕
R
)
=
(
P
Q
)
p
↕
(
P
R
) is unsound.
Let
R
1
=
a
(
b
2
↕
c
),
R
2
=
(
a
b
)
2
↕
(
a
c
) and
T
be the test
a.
(
ˉ
2
↕
0
)
b.ˉ
.
1
1
1
2
,1
1
1
2
,0
1
4
,
2
,
4
}
A
={
2
}
A
=
2
{
}+
2
{
}={
One can check that
(
T
,
R
1
)
and
(
T
,
R
2
)
.
Therefore, we have
R
2
pmay
R
1
and
R
1
pmust
R
2
.
Example 5.9
The axiom
P
(
Q
R
)
=
(
P
Q
)
(
P
R
) is unsound.
Let
R
1
=
(
a
2
↕
b
)
(
c
d
),
R
2
=
((
a
2
↕
b
)
c
)
((
a
2
↕
b
)
d
) and
T
be the
0,
4
,
2
,
4
,1
test (
a.ˉ
2
↕
c.ˉ
)
(
b.ˉ
2
↕
d.ˉ
). This time we get
A
(
T
,
R
1
)
={
}
and
1
4
,
4
}
A
(
T
,
R
2
)
={
.So
R
1
pmay
R
2
and
R
2
pmust
R
1
.
=
Example 5.10
The axiom
P
(
Q
R
)
(
P
Q
)
(
P
R
) is unsound.
Let
R
1
=
(
a
2
↕
b
)
((
a
2
↕
b
)
0
) and
R
2
=
((
a
2
↕
b
)
(
a
2
↕
b
))
((
a
2
↕
b
)
0
).
1
1
2
,
4
}
One obtains
A
(
a.ˉ
,
R
1
)
={
2
}
and
A
(
a.ˉ
,
R
2
)
={
.So
R
2
pmay
R
1
. Let
R
3
and
R
4
result from substituting
a
2
↕
b
for each of
P
,
Q
and
R
in the axiom above. Now
1
2
,
4
}
3
4
}
A
(
a.ˉ
,
R
3
)
={
and
A
(
a.ˉ
,
R
4
)
={
.So
R
4
pmust
R
3
.
Example 5.11
The axiom
P
p
↕
(
Q
R
)
=
(
P
p
↕
Q
)
(
P
p
↕
R
) is unsound.
Let
R
1
=
c
).
R
1
is an instance of the left-hand side of the axiom, and
R
2
an instance of the right-hand
side. Here we use
R
3
as a tool to reason about
R
2
, but in Sect.
5.11.2
we will need
R
3
in its own right. Note that [[
R
2
]]
a
2
↕
(
b
c
),
R
2
=
(
a
2
↕
b
)
(
a
2
↕
c
) and
R
3
=
(
a
b
)
2
↕
(
a
1
1
=
2
·
[[
R
1
]]
+
2
·
[[
R
3
]]. Let
T
=
a.ˉ
. It is easy
1
3
to see that
A
(
T
,
R
1
)
={
2
}
and
A
(
T
,
R
3
)
={
1
}
.
Therefore,
A
(
T
,
R
2
)
={
4
}
.
So we
have
R
2
pmay
R
1
and
R
2
pmust
R
1
.
Of all the examples in this section, this is the only one for which we can show
that
pmay
both fail, i.e. both inequations that can be associated with
the axiom are unsound for
may
testing. Let
T
pmay
and
=
a.
(
ˉ
2
↕
0
)
(
b.ˉ
2
↕
c.ˉ
). It is
0,
4
,
2
,
4
}
1
not hard to check that
A
(
T
,
R
1
)
={
and
A
(
T
,
R
3
)
={
2
}
. It follows that
1
4
,
8
,
2
,
8
}
A
(
T
,
R
2
)
. Therefore, we have
R
1
pmay
R
2
.
For future reference, we also observe that
R
1
pmay
R
3
and
R
3
pmay
R
1
.
={
5.4
Must Versus May Testing
On
pCSP
there are two differences between the preorders
pmay
and
pmust
:
•
Must testing is more discriminating
•
The preorders
pmay
and
pmust
are oriented in opposite directions.
Search WWH ::
Custom Search