RE: [sv-ac] Annex H change for 269

 
Updated the proposal of 269, with the following:

 SV_LRM_269_with_annexH_fix.pdf (32,640 bytes) 11-29-04 10:13

Someone please delete the older file below, I can't:

***delete me*** SV_LRM_269.pdf (11,444 bytes) 11-18-04 12:15

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893
-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Monday, November 29, 2004 8:50 AM
To: sv-ac@eda.org
Subject: [sv-ac] Annex H change for 269
All:
A while ago I said that we should review how the formal semantics in Annex H
should (or should not) change in response to the clarification of what can
appear in the reset expression of a "disable iff".
In Annex H, H.3.6.1, p. 551, we say that 
   w,L_0 |= disable iff (b) P  iff  either w,L_0 |= P or
   there exists 0 <= k <= |w| such that w^k |= b[L_0] and
   w^{0,k-1}\top^\omega,L_0 |= P.  Here w^{0,-1} denotes
   the empty word.
By looking for "w^k |= b[L_0]", we are saying that the valuation of the
local variables in L_0 affects the evaluation of the reset expression b.  
I think we should change "w^k |= b[L_0]" to "w^k |= b".
According to 269, there cannot be any local variables in b.  And if there
are no local variables in b, then "w^k |= b[L_0]" is equivalent to "w^k |=
b".  Thus, technically, no change to Annex H is required.  
However, by leaving the condition as "w^k |= b[L_0]", we are confusing the
reader of Annex H, who may reasonably think that b can depend on local
variables and that the local variable values are used in evaluating b.
Best regards,
John H.