Hi Manisha, >>1. In 16.12.1, it is mentioned that 'not' operator switches the strength >>of a property. I think it will be useful to have this information in >>16.12.2 also. [[DB:]] Ed and Dmitry have the same comment so I have moved this paragraph to the negation part. >>2. Why are weak forms of these new operators allowed in recursive >>properties (and not strong ones) ? [[DB:]] We only allow weak constructs in recursive properties because alternating strong and weak in a "recursive cycle" makes it difficult to define the semantics. I guess that "strong" could be an exception because it cannot be applied on properties, and thus cannot be part of a "recursive cycle". I am a little afraid to get it in at this time in case I missing something. Do you think it is important to have it now? We can always put it latter (there are other restrictions that can be lifted as well.) >>3. In the changes for multiclocked properties, it does have 'until' as >>one of the operators which requires special care but not 'until_with'. >>Is that an oversight ? [[DB:]] I guess it is an oversight, I have add it now. Thanks 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 : Mon Jan 28 2008 - 04:51:56 PST