Hi Ed, The definition of vacuity for "or" has not changed in 1932. Due to time constraints, I don't want to make this connection. I think that your definition will have issues under negation: not(p1 or p2) I think that in the scenario you described, the tool should report a vacuous success. It is too conservative, but I think it is better like that than having a property for which no non-vacuous success is reported, although there is no problem with it (false negative). Best regards Doron >>> >>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. >> >>But the formal semantics part is in the LTL proposal, no? The question >>is what an implementation should do. Report as I indicated? Isn't that >>counterintuitive? I wonder how to explain that to users. >> >>Question - could the |=non relation for or be defined as (w |=non P1 or >>w |=non P2) and (w |= P1 or w |=> P2) ? >> >>Similarly for and as: >> >>(w |=non P1 or w |=non P2) and (w |= P1 and w |=> P2) >> >>Or would it pose problems under negation (it seems so...)? >> >> --------------------------------------------------------------------- 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.Received on Tue Jan 29 02:49:59 2008
This archive was generated by hypermail 2.1.8 : Tue Jan 29 2008 - 02:50:09 PST