RE: [sv-ac] forward progress of time

Subject: RE: [sv-ac] forward progress of time
From: Bassam Tabbara (bassam@novas.com)
Date: Mon Feb 03 2003 - 09:10:27 PST

Both Cindy's "time progression", and John's "valid prefix" discussions
get the point across, thanks. Inherently the raison d'etre for => had
always been of a "pre-condition", so nesting a precondition obviously
creates weird conclusions about validity of the statement(s) ...

* This is an issue for -both- "boolean" and "sequence" implications. (In
fact the latter is covered by the former with use of ended).

* Moving "=>" to the property layer (i.e. as top operator) seems best to
rectify this.

* It would also be nice (not required of course) to have some wording
that "implementations" are free to add a means for "ignoring" the
vacuous successes of prop cause of precondition failure, in case false
alarms are a concern to the user.

Thx.
-Bassam. 

--
Dr. Bassam Tabbara
Technical Manager, R&D
Novas Software, Inc.

http://www.novas.com
(408) 467-7893

> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of Cindy Eisner
> Sent: Monday, February 03, 2003 12:12 AM
> To: sv-ac@server.eda.org
> Subject: [sv-ac] forward progress of time
> 
> 
> all,
> 
> as i said previously, i wholeheartedly agree with john 
> havlicek on the problems of the sequence implication operator 
> as it is currently defined, and with his proposal to make it 
> a property rather than a sequence.  i would like to say a few 
> more words about the problems with the current definition, to 
> make sure that my point of thursday's meeting is clear.
> 
> john expresses the problem in terms of context sensitivity.  
> i would like to view the problem from another angle - that of 
> the forward progress of time (these are related, of course).  
> consider the following:
> 
> ((a;b;c) => (d;e;f)) ; w                                  (example 1)
> 
> that is, a sequence implication of ((a;b;c) => (d;e;f)) 
> concatenated with "w".  consider two paths:
> 
> 1.  a path where (a;b;c) occurs and is followed by (d;e;f)
> 2.  a path where (a;b;c) does not occur.  for instance, a 
> path where only
> (a;b) occurs, but "c" does not occur at the cycle following "b".
> 
> say that in both cases, the occurence of "a" is at time 0.  
> then, according to the current definition:
> 
> 1.  on path #1, "c" happens at time 2, so so does "d", and 
> thus "f" happens at time 4, and therefore we require "w" at 
> time 5. 2.  on path #2, the sequence ((a;b;c) => (d;e;f)) is 
> matched vacuously (according to page 58, last line) and 
> returns true at time 0.  therefore, we require "w" at time 1.
> 
> thus, the theoretical problems of the current definition can 
> be understood intuitively as somehow confounding the "forward 
> progress of time" in a sequence, as someone put it in 
> thursday's meeting.  that is, whatever we intuitively would 
> have expected of example 1 above, it is not a requirement 
> that "w" occur the cycle following "a".
> 
> john's proposal to move the sequence implication operator up 
> a level to a property will eliminate this very undesirable 
> characteristic of the current definition.
> 
> regards,
> 
> cindy.
> 
> Cindy Eisner
> Formal Methods Group                                 Tel: 
> +972-4-8296-266
> IBM Haifa Research Laboratory                Fax: +972-4-8296-114
> Haifa 31905, Israel                                          e-mail:
> eisner@il.ibm.com
>

This archive was generated by hypermail 2b28 : Mon Feb 03 2003 - 09:11:44 PST