[sv-ac] 1932

Hi,

 

I made the following changes: (already uploaded in mantis)

 

Clause 16: 

 

*  I added the weak operator and specify the strength of a sequential
property

   to depend on the verification statement on which it used.

 

*  I have lifted the restriction over a strong sequence in a recursive
property.

 

In Annex F:

 

*  I add the weak operator and define the sequential property as a
derived form.

 

*  I change the definition of the LTL operators so that the operators in
the syntax are next and until (instead of s_next and s_until)

   and all other operators are derived. This way all strong operators
are derived using not. Then, I removed the change

   to the recursive properties part, because the restriction on not,
eliminates all strong operators.

 

*  I made weak(sequence) vacuous. 

 

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.