Hardware Reference
In-Depth Information
Example 22.8.
weak
(a[
*
2])
is satisfied on any trace of the form aa:::. Indeed, the
sequence
a[
*
2]
is tightly satisfied on the traces a
>
and aa where the match of the
sequence
a[
*
2]
can be witnessed.
However,
weak
(a[
*
2])
is not satisfied on the trace a
:
a:::, as the sequence
a[
*
2]
is not tightly satisfied on the trace a
:
a.
t
Consider an infinite trace and suppose that there is some time T such that any
prefix matching the sequence is of length at most T . Then there is no difference
between the weak and the strong satisfaction of the sequence on the trace. This is
the case of bounded sequences described in Sect.
6.2
.
For instance, the sequence
a[
*
2]
from Example
22.8
satisfies these conditions,
provided it is controlled by the global clock since only traces of length 2 may
match it. Therefore, there is no difference between the properties
weak
(a[
*
2])
and
strong
(a[
*
2])
when they are controlled by the global clock.
Example 22.9.
The property
weak
(##[
*
]a)
holds on any trace without any
special letter
>
or
?
. Indeed, since
>ˆ
a,
w
0;i
>j
##[
*
]a
for any
w
2
˙
!
and for any i (recall that ˙
!
is an infinite sequence of the letters from the alphabet
of the language defined by the FV model, see Sect.
21.2.2
). However, property
strong
(##[
*
]a)
is equivalent to
s_eventually
a
.
The property
weak
(##[
*
] a ##1 0)
also holds on any infinite trace without any
special letter
>
or
?
. Since
>ˆ
a and
>ˆ
false
.
D
0
/,
w
0;i
>>j
##[
*
]
a
##1 0
for any
w
2
˙
and any i . On the contrary, the property
strong
(##[
*
] a ##1 0)
is a contradiction, as
false
does not match any letter from the original unextended
alphabet.
t
22.3.4
Property Negation
In Sect.
22.1.1.2
, we gave the following definition of property negation:
w
ˆ
not
p iff
w
6ˆ
p.
This definition is only correct if
w
does not contain special letters
>
or
?
. According
to that definition, if
w
D>
!
then, for any a,
w
ˆ
a, and thus
w
6ˆ
not
a.Thisis
counterintuitive since we expect
not
a to behave the same way as
!
a when the
property is controlled by the global clock.
!
a is satisfied on
w
since
>
satisfies
every Boolean expression.
We need to modify the formal semantics of nega
ti
on to eliminate this counterin-
tuitive behavior. Given a word
w
we build the word
w
by interchanging the letters
>
and
?
in
w
and leaving all other letters unmodified. Then we can define the formal
semantics of property negation as follows:
w
ˆ
not
p iff
w
6ˆ
p.
Search WWH ::
Custom Search