All, I upload the latest I have in case somebody want to review. The current status is that we still have two issues under discussion: 1. Vacuity in general and in particular for the until operator. Johan suggested an alternative definition, which we are discussing it. 2. I have some problems defining "s_eventually[m:n]" and always[m:n] without next[0]. The problem is that for "@clk1 eventually @clk2 p", suppose that clk1 and clk2 occur at the same time at the beginning of the attempt and p hold at the same time, should it count as a success? Other than that I don't think that there are substance issues that I have not fixed. The review is not over yet so I do expect more issue to be flushed. Doron --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.
This archive was generated by hypermail 2.1.8 : Tue Oct 30 2007 - 01:01:09 PDT