RE: [sv-ac] call to vote on Mantis 1932

Manisha, Lisa,

We did spend some time thinking about weak LTL operators in recursive
properties. I remember changing the derivation schema such that strong
operators are derived from weak using not; so strong operators are not
allowed. I remember discussions with John, and I am confident that the
semantics is not broken (as much as I can be confident with no written
proofs.)

Best regards

Doron

>>-----Original Message-----
>>From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
>>Sent: Monday, January 28, 2008 6:43 PM
>>To: Bustan, Doron; john.havlicek@freescale.com; sv-ac@server.eda.org
>>Subject: RE: [sv-ac] call to vote on Mantis 1932
>>
>>Hi,
>>
>>I just wanted to understand the restriction for strong property in
>>recursive properties and not weak ones. I do not think we should
>>introduce it now. I even feel that combining these new operators (like
>>until and always) in recursive properties is going to be very
confusing.
>>I was just wondering if we should restrict it for even weak
properties.
>>What do you think ? Do you think we loose anything important here by
not
>>allowing weak forms of these new operators ? Since PSL did not have a
>>concept of recursive anyway, I think no one has written these
>>combinations yet.
>>
>>Thanks.
>>Manisha
>>
>>-----Original Message-----
>>From: Bustan, Doron [mailto:doron.bustan@intel.com]
>>Sent: Monday, January 28, 2008 6:16 PM
>>To: Kulshrestha, Manisha; john.havlicek@freescale.com;
>>sv-ac@server.eda.org
>>Subject: RE: [sv-ac] call to vote on Mantis 1932
>>
>>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.