Hi Ed, >>Regarding the leading clock in until. My point is that the rule deals with >>the case when some clock v flows in P1 until P2. But what if there is no >>clock flowing in? E.g. Assert property (P1 until P2); >>Does the leading clock of P1 have to be the same as in P2? (I hope so.) >> [[DB:]] Since the leading clock of until is inherited, there must be a clock flowing from the left into the until property; so unless there is an inferred clock, the assertion "assert property (P1 until P2);" is illegal. The rule in item c) says "- Every explicit semantic leading clock of P1 or P2 is identical to c." I think this match your intuition >>In the formal part, vacuity, in the case of P1 or P2, it seems to me that >>if P1 has vacuous success and P2 is non-vacuous failure, it would be >>declared as non-vacuous success. That looks strange. Or did I miss >>something? >> [[DB:]] I think you are right, and this is bothering. However, it is not part of 1932. We tried to give a conservative definition (no false negatives) and keep the definition indifferent to negation. I think that sometime in the future we will have to find a better definition. Thanks Doron -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Jan 28 13:13:19 2008
This archive was generated by hypermail 2.1.8 : Mon Jan 28 2008 - 13:14:03 PST