Subject: [sv-ac] more on mapping SVA2PSL
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Apr 29 2003 - 22:22:50 PDT
SVA Abstract Syntax
-------------------
Note that local variables and first_match are not in the domain of the
mapping. Throughout, "SVA unclocked sequence" means "SVA unclocked sequence
without local variables or first_match". Similarly, "SVA clocked sequence"
means "SVA clocked sequence without local variables or first_match".
The abstract grammar for SVA unclocked sequences is
R ::= b
| (R)
| (R ##1 R)
| (R ##0 R)
| (R or R)
| (R intersect R)
| R[*0]
| R[*1:$]
The abstract grammar for SVA clocked sequences is
S ::= @(b) R
| (S ## S)
The abstract grammar for SVA unclocked properties is
P ::= [disable iff (b)] [not] R
| [disable iff (b)] [not] (R |-> [not] R)
Note: In this grammar, "[...]" denotes an optional component.
The abstract grammar for SVA clocked properties is
Q ::= @(b) P
| [disable iff (b)] [not] S
| [disable iff (b)] [not] (S |-> [not] S)
Note: In this grammar, "[...]" denotes an optional component.
The abstract grammar for SVA assertions is
A ::= always assert property Q
| always @(b) assert property P
| initial assert property Q
| initial @(b) assert property P
===========================================================================
MAPPING DEFINITION
===========================================================================
1. Mapping SVA unclocked sequences to PSL unclocked SEREs
---------------------------------------------------------
DEFINITION 1: Let b be a boolean expression, and let
R, R_1, R_2 be SVA unclocked sequences.
* M(b) = b
* M((R)) = {M(R)}
* M((R_1 ##1 R_2)) = {M(R_1) ; M(R_2)}
* M((R_1 ##0 R_2)) = {M(R_1) : M(R_2)}
* M((R_1 or R_2)) = {{M(R_1)} | {M(R_2)}}
* M((R_1 intersect R_2)) = {{M(R_1)} && {M(R_2)}}
* M(R[*0]) = 1[*0]
* M(R[*1:$]) = M(R)[*1:]
////
REMARK: Note that the PSL LRM, Verilog flavor is supposed to use ":"
instead of "..". This is why I have written "[*1:]" rather than
"[*1..]".
////
PROPOSITION 1.1: Let r be a SVA unclocked sequence and let w be a finite
word over 2^P. Then w |== r iff w |= M(r).
PROOF: By induction over the structure of r.
* r = b.
w |== b
iff |w| = 1 and w^0 |= b
iff |w| = 1 and w^0 |= M(b)
iff w |= M(b)
* r = (R).
w |== (R)
iff w |== R
iff [induction]
w |= M(R)
iff w |= {M(R)}
iff w |= M((R))
* r = (R_1 ##1 R_2).
w |== (R_1 ##1 R_2)
iff there exist x,y such that w = xy and x |== R_1 and y |== R_2
iff [induction]
there exist x,y such that w = xy and x |= M(R_1) and y |= M(R_2)
iff w |= M(R_1) ; M(R_2)
iff w |= {M(R_1) ; M(R_2)}
iff w |= M((R_1 ##1 R_2))
* r = (R_1 ##0 R_2).
w |== (R_1 ##0 R_2)
iff there exist x,y,z such that w = xyz and |y| = 1 and xy |== R_1 and yz |== R_2
iff [induction]
there exist x,y such that w = xyz and |y| = 1 and xy |= M(R_1) and yz |= M(R_2)
iff w |= M(R_1) : M(R_2)
iff w |= {M(R_1) : M(R_2)}
iff w |= M((R_1 ##0 R_2))
* r = (R_1 or R_2).
w |== (R_1 or R_2)
iff w |== R_1 or w |== R_2
iff [induction]
w |= M(R_1) or w |= M(R_2)
iff w |= {M(R_1)} | {M(R_2)}
iff w |= {{M(R_1)} | {M(R_2)}}
iff w |= M((R_1 or R_2))
* r = (R_1 intersect R_2).
w |== (R_1 intersect R_2)
iff w |== R_1 andr w |== R_2
iff [induction]
w |= M(R_1) and w |= M(R_2)
iff w |= {M(R_1)} && {M(R_2)}
iff w |= {{M(R_1)} && {M(R_2)}}
iff w |= M((R_1 intersect R_2))
* r = R[*0].
w |= M(R[*0])
iff w |= 1[*0]
iff w |= FALSE[*]
iff |w| = 0 or there exist w_1,...,w_j such that w = w_1...w_j and for each
i such that 1 <= i <= j, w_i |= FALSE
iff [Since w is over 2^P, w = w_1...w_j implies not(w_1 |= FALSE)]
|w| = 0
iff w |== R[*0]
* r = R[*1:$].
w |== R[*1:$]
iff there exist w_1,...,w_j, j >= 1, such that w = w_1...w_j and for each
i such that 1 <= i <= j, w_i |== R
iff [induction]
there exist w_1,...,w_j, j >= 1, such that w = w_1...w_j and for each
i such that 1 <= i <= j, w_i |= M(R)
iff there exist w_1,y such that w = w_1y and w_1 |= M(R) and either
y is empty or there exist w_2,...,w_j such that y = w_2...w_j and
for each i such that 2 <= i <= j, w_i |= M(R)
iff there exist w_1, y such that w = w_1y and w_1 |= M(R) and y |= M(R)[*]
iff w |= {M(R);M(R)[*]}
iff w |= M(R)[*1:]
iff w |= M(R[*1:$])
////
REMARK: In PSL, "TRUE" means "p || !p" and "FALSE" means "p && !p" for
some choice of atomic proposition p. In SVA, "\top" satisfies all
boolean expressions, while "\bot" satisfies no boolean expression. In
particular, \top |= FALSE. As a result, Proposition 1 does not hold
for words w over 2^P \cup {\top, \bot}. For example, if w is the
length 1 word with w^0 = \top, then
not(w |== 1[*0])
but
w |= FALSE[*], hence w |= M(1[*0])
////
===========================================================================
2. Mapping SVA clocked sequences to PSL clocked SEREs
-----------------------------------------------------
NOTATION: If S is a SVA clocked sequence, let <S> denote
the SVA unclocked sequence that results from S by applying the
SVA clock rewrite rules.
PROPOSITION 2.1: Let r be a SVA unclocked sequence, and let w be a
finite word over 2^P. Then the following are equivalent:
1. w |== <@(c) r> .
2. w |=(c) M(r) .
PROOF: By induction over the structure of r.
* r = b.
w |== <@(c) b>
iff w |== (!c[*0:$] ##1 c & b)
iff |w| >= 1 and for every i s.t. 0 <= i < |w| - 1, w^i |= !c and
w^{|w|-1} |= c & b
iff w |=(c) b
iff w |=(c) M(b)
* r = (R).
w |== <@(c) (R)>
iff w |== <@(c) R>
iff [induction]
w |=(c) M(R)
iff w |=(c) {M(R)}
iff w |=(c) M((R))
* r = (R_1 ##1 R_2).
w |== <@(c) (R_1 ##1 R_2)>
iff w |== (<@(c) R_1> ##1 <@(c) R_2>)
iff there exist x,y such that w = xy and x |== <@(c) R_1> and y |== <@(c) R_2>
iff [induction]
there exist x,y such that w = xy and x |=(c) M(R_1) and y |=(c) M(R_2)
iff w |=(c) M(R_1) ; M(R_2)
iff w |=(c) {M(R_1) ; M(R_2)}
iff w |=(c) M((R_1 ##1 R_2))
* r = (R_1 ##0 R_2).
w |== <@(c) (R_1 ##0 R_2)>
iff w |== (<@(c) R_1> ##0 <@(c) R_2>)
iff there exist x,y,z such that w = xyz and |y| = 1 and xy |== <@(c) R_1>
and yz |== <@(c) R_2>
iff [induction]
there exist x,y,z such that w = xyz and |y| = 1 and xy |=(c) M(R_1)
and yz |=(c) M(R_2)
iff w |=(c) M(R_1) : M(R_2)
iff w |=(c) {M(R_1) : M(R_2)}
iff w |=(c) M((R_1 ##0 R_2))
* r = (R_1 or R_2).
w |== <@(c) (R_1 or R_2)>
iff w |== (<@(c) R_1> or <@(c) R_2>)
iff w |== <@(c) R_1> or w |== <@(c) R_2>
iff [induction]
w |=(c) M(R_1) or w |=(c) M(R_2)
iff w |=(c) {M(R_1)} | {M(R_2)}
iff w |=(c) {{M(R_1)} | {M(R_2)}}
iff w |=(c) M((R_1 or R_2))
* r = (R_1 intersect R_2).
w |== <@(c) (R_1 intersect R_2)>
iff w |== (<@(c) R_1> intersect <@(c) R_2>)
iff w |== <@(c) R_1> and w |== <@(c) R_2>
iff [induction]
w |=(c) M(R_1) and w |=(c) M(R_2)
iff w |=(c) {M(R_1)} && {M(R_2)}
iff w |=(c) {{M(R_1)} && {M(R_2)}}
iff w |=(c) M((R_1 intersect R_2))
* r = R[*0].
w |== <@(c) R[*0]>
iff w |== (<@(c) R>)[*0]
iff |w| = 0
iff [Since w is over 2^P, w = w_1...w_j implies not(w_1 |= FALSE)]
|w| = 0 or there exist w_1,...,w_j such that w = w_1...w_j and for all
i such that 1 <= i <= j, w_i |=(c) FALSE
iff w |=(c) FALSE[*]
iff w |=(c) 1[*0]
iff w |=(c) M(R[*0])
* r = R[*1:$].
w |== <@(c) R[*1:$]>
iff w |== (<@(c) R>) [*1:$]
iff there exist w_1,...,w_j such that w = w_1...w_j and for all i such that
1 <= i <= j, w_i |== <@(c) R>
iff [induction]
there exist w_1,...,w_j such that w = w_1...w_j and for all i such that
1 <= i <= j, w_i |=(c) M(R)
iff there exist w_1,y such that w = w_1y and w_1 |=(c) M(R) and either
y is empty or there exist w_2,...,w_j such that y = w_2...w_j and
for each i such that 2 <= i <= j, w_i |=(c) M(R)
iff there exist w_1, y such that w = w_1y and w_1 |=(c) M(R) and y |=(c) M(R)[*]
iff w |=(c) {M(R);M(R)[*]}
iff w |=(c) M(R)[*1:]
iff w |=(c) M(R[*1:$])
////
LEMMA 2.1: Let w be a non-empty word over 2^P and let r be an unclocked SERE.
Then w |=(c) r iff w |=(TRUE) {r}@c.
PROOF: By induction over the structure of r. If no letter of w satisfies
c then let I = |w|. Otherwise, let I be the smallest non-negative integer
such that w^I |= c.
* r = b.
w |=(TRUE) {b}@c
iff I < |w| and w^{I..} |=(c) {b}
iff I < |w| and w^{I..} |=(c) b
iff I = |w|-1 and w^I |= c & b
iff w |=(c) b
* r = {R}.
w |=(c) {R}
iff w |=(c) R
iff [induction]
w |=(TRUE) R@c
iff I < |w| and w^{I..} |=(c) R
iff I < |w| and w^{I..} |=(c) {R}
iff I < |w| and w^{I..} |=(c) {{R}}
iff w |=(TRUE) {{R}}@c
* r = R_1 ; R_2.
w |=(c) R_1 ; R_2
iff A:
there exist x,y such that w = xy and x |=(c) R_1 and y |=(c) R_2
w |=(TRUE) {R_1 ; R_2}@c
iff I < |w| and w^{I..} |=(c) {R_1 ; R_2}
iff I < |w| and w^{I..} |=(c) R_1 ; R_2
iff B:
I < |w| and there exist x',y' such that w^{I..} = x'y' and x' |=(c) R_1
and y' |=(c) R_2
Assume A. Since w is non-empty, either x or y is non-empty.
Suppose x is non-empty. Then
[induction]
there exist x non-empty, y such that w = xy and x |=(TRUE) {R_1}@c
and y |=(c) R_2
=> there exist x non-empty, y such that w = xy and I < |x| and
x^{I..} |=(c) R_1 and y |=(c) R_2
=> [x' = x^{I..}, y' = y]
B
Suppose x is empty and y is non-empty. Then
[induction]
there exist x empty, y non-empty such that w = xy and x |=(c) R_1
and y |=(TRUE) {R_2}@(c)
=> there exist x empty, y non-empty such that w = xy and x |=(c) R_1
and I < |y| and y^{I..} |=(c) R_2
=> [x' is empty, y' = y^{I..}]
B
Now assume B. Since I < |w|, w^{I..} is non-empty, hence either x' or y'
is non-empty. Suppose x' is non-empty. Then
I < |w| and there exist x' non-empty, y' such that w^{I..} = x'y' and
x' |=(c) {R_1} and y' |=(c) R_2
=> [x' non-empty and w^{I..} = x'y' imply that x' = {w^{0,I-1}x'}^{I..}]
there exist x' non-empty, y' such that w^{I..} = x'y' and
w^{0,I-1}x' |=(TRUE) {R_1}@c and y' |=(c) R_2
=> [induction]
there exist x' non-empty, y' such that w^{I..} = x'y' and
w^{0,I-1}x' |=(c) R_1 and y' |=(c) R_2
=> [x = w^{0,I-1}x', y = y']
A
Suppose x' is empty and y' is non-empty. Then
I < |w| and there exist x' empty, y' non-empty such that w^{I..} = x'y'
and x' |=(c) R_1 and y' |=(c) {R_2}
=> [x' empty and y' non-empty and w^{I..} = x'y' imply that
y' = {w^{0,I-1}y'}^{I..}]
there exist x' empty, y' non-empty such that w^{I..} = x'y' and
x' |=(c) R_1 and w^{0,I-1}y' |=(TRUE) {R_2}@c
=> [induction]
there exist x' empty, y' non-empty such that w^{I..} = x'y' and
x' |=(c) R_1 and w^{0,I-1}y' |=(c) R_2
=> [x = empty, y = xy = w = w^{0,I-1}y']
A
* r = R_1 : R_2.
w |=(c) R_1 : R_2
iff A:
there exist x,y,z such that w = xyz and |y| = 1 and xy |=(c) R_1
and yz |=(c) R_2
w |=(TRUE) {R_1 : R_2}@c
iff I < |w| and w^{I..} |=(c) {R_1 : R_2}
iff I < |w| and w^{I..} |=(c) R_1 : R_2
iff B:
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and x'y' |=(c) R_1 and y'z' |=(c) R_2
Assume A. Then
[induction]
there exist x,y,z such that w = xyz and |y| = 1 and xy |=(TRUE) {R_1}@c
and yz |=(c) R_2
=> there exist x,y,z such that w = xyz and |y| = 1 and
I < |xy| and {xy}^{I..} |=(c) R_1 and yz |=(c) R_2
=> [I < |xy| implies {xy}^{I..} = x'y; let y' = y, z' = z]
B
Assume B. Then
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and x'y' |=(c) {R_1} and y'z' |=(c) R_2
=> [x'y' = {w^{0,I-1}x'y'}^{I..}]
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and w^{0,I-1}x'y' |=(TRUE) {R_1}@c and y'z' |=(c) R_2
=> [induction]
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and w^{0,I-1}x'y' |=(c) R_1 and y'z' |=(c) R_2
=> [x = w^{0,I-1}x', y = y', z = z']
A
* r = {R_1} | {R_2}.
w |=(c) {R_1} | {R_2}
iff w |=(c) R_1 or w |=(c) R_2
iff [induction]
w |=(TRUE) {R_1}@c or w |=(TRUE) {R_2}@c
iff I < |w| and either w^{I..} |=(c) {R_1} or w^{I..} |=(c) {R_2}
iff I < |w| and either w^{I..} |=(c) R_1 or w^{I..} |=(c) R_2
iff I < |w| and w^{I..} |=(c) {R_1} | {R_2}
iff I < |w| and w^{I..} |=(c) {{R_1} | {R_2}}
iff w |=(TRUE) {{R_1} | {R_2}}@c
* r = {R_1} && {R_2}.
w |=(c) {R_1} && {R_2}
iff w |=(c) R_1 and w |=(c) R_2
iff [induction]
w |=(TRUE) {R_1}@c and w |=(TRUE) {R_2}@c
iff I < |w| and w^{I..} |=(c) {R_1} and w^{I..} |=(c) {R_2}
iff I < |w| and w^{I..} |=(c) R_1 and w^{I..} |=(c) R_2
iff I < |w| and w^{I..} |=(c) {R_1} && {R_2}
iff I < |w| and w^{I..} |=(c) {{R_1} && {R_2}}
iff w |=(TRUE) {{R_1} && {R_2}}@c
* r = R[*].
w |=(TRUE) {R[*]}@c
iff I < |w| and w^{I..} |=(c) {R[*]}
iff I < |w| and w^{I..} |=(c) R[*]
iff [w^{I..} is non-empty]
I < |w| and there exist u_1,...,u_j non-empty such that
w^{I..} = u_1,...,u_k and for each i such that 1 <= i <= j,
u_i |=(c) R
iff I < |w| and there exist u_1,...,u_j non-empty such that
w^{I..} = u_1,...,u_j and u_1 |=(c) {R} and for each i such
that 1 < i <= j, u_i |=(c) R
iff [u_1 = {w^{0,I-1}u_1}^{I..}]
there exist u_1,...,u_j non-empty such that
w = w^{0,I-1}u_1...u_j and w^{0,I-1}u_1 |=(TRUE) {R}@c and
for each i such that 1 < i <= j, u_i |=(c) R
iff [induction]
there exist u_1,...,u_j non-empty such that
w = w^{0,I-1}u_1...u_j and w^{0,I-1}u_1 |=(c) R and
for each i such that 1 < i <= j, u_i |=(c) R
iff [w_1 = w^{0,I-1}u_1, w_i = u_i for 1 < i <= j]
there exist w_1,...,w_j non-empty such that w = w_1...w_j and
for each i such that 1 <= i <= j, w_i |=(c) R
iff [w is non-empty]
w |=(c) R[*]
////
REMARK: Lemma 1 fails if w is empty. For example, emptyword |=(c) 1[*0],
but not(emptyword |=(TRUE) {1*[0]}@c).
////
PROPOSITION 2.2: Let r be a SVA unclocked sequence and let w be a
non-empty finite word over 2^P. Then the following are equivalent:
1. w |== <@(c) r> .
2. w |=(c) M(r) .
3. w |=(TRUE) {M(r)}@c .
PROOF: 1 and 2 are equivalent by Proposition 2.1. Since w is
non-empty, Lemma 2.1 shows that 2 and 3 are equivalent.
////
DISCUSSION: The breakdown of Lemma 1, hence the equivalence of
2 and 3 in Proposition 2.2, when w is empty indicates that some care
is required in defining the mapping on SVA clocked sequences.
Naively, the definition should be
* M(@(b) R) = {M(R)} @b
* M((S_1 ## S_2)) = {M(S_1) ; M(S_2)}
but this will lead to problems if, e.g., emptyword tightly satisfies
one or both of <S_1>, <S_2>. The domain of the mapping will be
restricted to avoid these problems.
////
DEFINITION 2: Let b be a boolean expression, let R be a SVA unclocked
sequence, and let S_1, S_2 be SVA clocked sequences.
* If emptyword does not tightly satisfy R, then M(@(b) R) = {M(R)} @b.
Otherwise, @(b) R is not in the domain of M.
* If both S_1 and S_2 are in the domain of M, then
M((S_1 ## S_2)) = {M(S_1) ; M(S_2)}. Otherwise, (S_1 ## S_2) is not
in the domain of M.
////
LEMMA 2.2: If c is a boolean expression and r is a SVA unclocked
sequence, then emptyword tightly satisfies <@(c) r> iff
emptyword tightly satisfies r.
PROOF: By induction over the structure of r. Write e for emptyword.
* r = b.
e does not tightly satisfy b. <@(c) b> = (!c[*0:$];c&b), which is
also not tightly satisfied by b.
* r = (R).
e |== (R)
iff e |== R
iff [induction]
e |== <@(c) R>
iff e |== <@(c) (R)>
* r = (R_1 ##1 R_2).
e |== (R_1 ##1 R_2)
iff e |== R_1 and e |== R_2
iff [induction]
e |== <@(c) R_1> and e |== <@(c) R_2>
iff e |== (<@(c) R_1> ##1 <@(c) R_2>)
iff e |== <@(c)(R_1 ##1 R_2)>
* r = (R_1 ##0 R_2).
e does not tightly satisfy (R_1 ##0 R_2).
<@(c)(R_1 ##0 R_2)> = (<@(c) R_1> ##0 <@(c) R_2>), which is also not
tightly satisfied by e.
* r = (R_1 or R_2).
e |== (R_1 or R_2)
iff e |== R_1 or e |== R_2
iff [induction]
e |== <@(c) R_1> or e |== <@(c) R_2>
iff e |== (<@(c) R_1> or <@(c) R_2>)
iff e |== <@(c)(R_1 or R_2)>
* r = (R_1 intersect R_2).
e |== (R_1 intersect R_2)
iff e |== R_1 and e |== R_2
iff [induction]
e |== <@(c) R_1> and e |== <@(c) R_2>
iff e |== (<@(c) R_1> intersect <@(c) R_2>)
iff e |== <@(c)(R_1 intersect R_2)>
* r = R[*0].
e |== R[*0]. <@(c) R[*0]> = (<@(c) R>)[*0], which is also tightly
satisfied by e.
* r = R[*1:$].
e |== R[*1:$]
iff e |== R
iff [induction]
e |== <@(c) R>
iff e |== (<@(c) R>)[*1:$]
iff e |== <@(c) R[*1:$]>
////
LEMMA 2.3: If s is a SVA clocked sequence in the domain of M, then
emptyword does not tightly satisfy <s>.
PROOF: By induction over the structure of s.
* s = @(b) R. By definition, emptyword does not tightly satisfy R.
By Lemma 2.2, emptyword does not tightly satisfy <s>.
* s = (S_1 ## S_2). By definition, S_1 and S_2 are both in the domain
of M. By induction, emptyword tightly satisfies neither <S_1> nor
<S_2>. <s> = (<S_1> ##1 <S_2>), so it follows that emptyword does
not tightly satisfy <s>.
////
PROPOSITION 2.3: Let s be a SVA clocked sequence in the domain of M,
and let w be a non-empty finite word over 2^P. Then the following are
equivalent:
1. w |== <s> .
2. w |=(TRUE) M(s) .
PROOF: By induction over the structure of s.
* s = @(c) R. The result follows from Proposition 2.2.
* s = (S_1 ## S_2). Then both S_1, S_2 are in the domain of M.
By Lemma 3, emptyword tightly satisfies neither <S_1> nor <S_2>.
w |== <(S_1 ## S_2)>
iff w |== (<S_1> ##1 <S_2>)
iff there exist x,y such that w = xy and x |== <S_1>
and y |== <S_2>
iff [induction; x,y must be non-empty]
there exist x,y such that w = xy and x |=(TRUE) M(S_1)
and y |=(TRUE) M(S_2)
iff w |=(TRUE) {M(S_1) ; M(S_2)}
iff w |=(TRUE) M((S_1 ## S_2))
////
===========================================================================
3. Mapping SVA unclocked properties to unclocked PSL formulas
-------------------------------------------------------------
Since sequences can be properties, the letter "T" will
be used instead of "M" to denote the mapping at the level
of properties and assertions.
If phi is a SVA unclocked property and if "disable iff (b) phi"
is also a SVA unclocked property, then phi will be called a
"SVA unclocked property fragment".
DEFINITION 3: Let b be a boolean expression, let R, R_1, R_2 be
SVA unclocked sequences, and let phi be a SVA unclocked property
fragment.
* T(R) = {1} |-> {M(R)}!
* T(not R) = !({1} |-> {M(R)}!)
* T((R_1 |-> R_2)) = {M(R_1)} |-> {M(R_2)}!
* T(not(R_1 |-> R_2)) = !({M(R_1)} |-> {M(R_2)}!)
* T((R_1 |-> not R_2)) = {M(R_1)}(!({1} |-> {M(R_2)}!))
* T(not(R_1 |-> not R_2)) = !({M(R_1)}(!({1} |-> {M(R_2)}!)))
* T(disable iff (b) phi) = T(phi) abort b
////
NOTATION: For clarity, property satisfaction in SVA is
denoted "|=", while formula satisfaction in PSL is
denoted "|=.".
////
LEMMA 3.1: Let r be an unclocked SERE, and let w be a
word over 2^P. Then the following are equivalent
1. w |=. {1} |-> {r}! .
2. w is empty or there exists j such that 0 <= j < |w|
and w^{0,j} |= r .
PROOF:
w |=. {1} |-> {r}!
iff for every i such that 0 <= i < |w|, if w^{0,i} |= 1,
then there exists j such that i <= j < |w| and w^{i,j} |= r
iff [w^{0,i} |= 1 iff i = 0 and w is non-empty]
w is empty or there exists j such that 0 <= j < |w|
and w^{0,j} |= r
////
PROPOSITION 3.1: Let phi be a SVA unclocked property fragment,
and let w be an infinite word over 2^P. Then the following
are equivalent:
1. w |= phi .
2. w |=. T(phi) .
PROOF:
* phi = R.
w |= R
iff there exists j >= 0 such that w^{0,j} |== R
iff [Proposition 1.1]
there exists j >= 0 such that w^{0,j} |= M(R)
iff [Lemma 3.1; w^{0,j} is non-empty]
w |=. {1} |-> {M(R)}!
iff w |=. T(R)
* phi = not R.
w |= not R
iff [\bar w = w]
not(w |= R)
iff [proof for phi = R]
not(w |=. {1} |-> {M(R)}!)
iff w |=. !({1} |-> {M(R)}!)
iff w |=. T(not R)
* phi = (R_1 |-> R_2).
w |= (R_1 |-> R_2)
iff [\bar w = w]
for every j >= 0 such that w^{0,j} |== R_1, w^{j..} |= R_2
iff for every j >= 0 such that w^{0,j} |== R_1, there exists k >= j
such that w^{j,k} |== R_2
iff [Proposition 1.1]
for every j >= 0 such that w^{0,j} |= M(R_1), there exists k >= j
such that w^{j,k} |= M(R_2)
iff w |=. {M(R_1)} |-> {M(R_2)}!
iff w |=. T((R_1 |-> R_2))
* phi = not(R_1 |-> R_2).
w |= not(R_1 |-> R_2)
iff [\bar w = w]
not(w |= (R_1 |-> R_2))
iff [proof for phi = (R_1 |-> R_2)]
not(w |=. {M(R_1)} |-> {M(R_2)}!)
iff w |=. !({M(R_1)} |-> {M(R_2)}!)
iff w |=. T(not(R_1 |-> R_2))
* phi = (R_1 |-> not R_2).
w |= (R_1 |-> not R_2)
iff [\bar w = w]
for every j >= 0 such that w^{0,j} |== R_1, w^{j..} |= not R_2
iff [Proposition 1.1, proof for phi = not R]
for every j >= 0 such that w^{0,j} |= M(R_1),
w^{j..} |= !({1} |-> {M(R_2)}!)
iff w |=. {M(R_1)}(!({1} |-> {M(R_2)}!))
iff w |=. T((R_1 |-> not R_2))
* phi = not(R_1 |-> not R_2).
w |= not(R_1 |-> not R_2)
iff [\bar w = w]
not(w |= (R_1 |-> not R_2))
iff [proof for phi = (R_1 |-> not R_2)]
not(w |=. {M(R_1)}(!({1} |-> {M(R_2)}!)))
iff w |=. !({M(R_1)}(!({1} |-> {M(R_2)}!)))
iff w |=. T(not(R_1 |-> not R_2))
////
REMARK: The PSL semantics for abort needs to be updated before
Proposition 3.1 can be extended to general SVA unclocked properties.
Also, the semantic characterization of the mapping on finite
words requires reconciliation of the finite semantics for SVA and
PSL. Currently, SVA has no neutral semantics for finite words, while
PSL does not yet have strong and weak finite word semantics.
////
===========================================================================
This archive was generated by hypermail 2b28 : Tue Apr 29 2003 - 22:25:35 PDT