Hardware Reference
In-Depth Information
!
, then
w
D?
!
Example 22.10.
If
w
D>
6ˆ
a for any a. Therefore, according to
this modified definition,
w
ˆ
not
a.
t
Example 22.11. w
ˆ
not weak
(##[
*
]a)
iff
w
6ˆ
weak
(##[
*
]a)
.The
latter means that there exists i
0 such that
w
0;i
!
6ˆ
strong
(##[
*
]a)
.
This is impossible if
w
does not contain special letters. Therefore, we have that
not weak
(##[
*
]a)
cannot hold on a trace without special letters, which agrees
with our intuition.
w
ˆ
not strong
(##[
*
]a)
iff
w
6ˆ
strong
(##[
*
]a)
.
T
he latter means
that the sequence
##[
*
]a
does not match any finite prefix of
w
. Assuming that
w
has no special letter, this is equivalent to
w
i
>
6ˆ
a for all i , or, equivalently,
to
w
i
ˆ
!
a for all i . This, in turn, means that
always
!a
holds on
w
.Thisis
not surprising, since
strong
(##[
*
]a)
is equivalent to
s_eventually
a
, and the
negation of
s_eventually
a
is
always
!a
for Boolean
a
(Chap.
5
).
t
22.3.5
Suffix Implication
The formal semantics of suffix implication is as follows:
w
ˆ
s
|->
p iff for every i
0;
w
0;i
j
s
!
w
i::
ˆ
p
.
This definition means that for each finite prefix of trace
w
matching sequence s,
the suffix of the trace satisfies property p. The prefix and the suffix overlap at the
letter i . This definition agrees with the informal definition of the overlapping suffix
implication from Sect.
6.4
.
Note the interchange of the letters
>
and
?
in the antecedent. This is necessary
to make the formal semantics intuitive, as illustrated in the following examples.
Example 22.12.
It is natural to expect that a
|->
b behaves the same as a
implies
b
when a and b are
Bo
oleans. Assume
th
at
j
w
j
1. Then
w
ˆ
a
implies
b iff
w
ˆ
not
a
or
b iff
w
6ˆ
a or
w
ˆ
b iff
w
0;0
j
a implies
w
0::
ˆ
b.
t
Example 22.13.
Given the trace
w
D
a
^:
b
>
a
^:
b::: and the property
a[
*
3] |-> b
we can see that
b
does not b
el
ong to the first three letters of the
trace. However, the property hold
s
on
w
,as
w
D
a
^:
b
?
a
^:
b:::, and
a[
*
3]
does not match any finite prefix of
w
.
This example is important for understanding the behavior of implication under
reset discussed in Chap.
13
.
t
Is the sequence in the antecedent of a suffix implication strong or weak? The
question is malformed since weak and strong sequences are
properties
, whereas the
antecedent of a suffix implication is a
sequence
.
Search WWH ::
Custom Search