[sv-ac] Re: F.3.4.3.8 (p_until q) should be (p until q)

Hi, Ben.

Yes, this was brought up recently.

Stu, please fix.

Thanks,
Shalom

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Bresticker, Shalom
Sent: Tuesday, January 17, 2012 12:31 PM
To: Tapan Kapoor; Korchemny, Dmitry; 'sv-ac@eda-stds.org'
Subject: [sv-ac] RE: Draft 4 Review (resend with correction of one more numbering issue pointed by Scott)

Hi,

You're right.

It took me a little while to track this down.

This line was introduced in Mantis 1932, in file LTL_Formal.080317.pdf<http://www.eda-stds.org/mantis/file_download.php?file_id=3502&type=bug>, at the top of page 6.
It was implemented in Draft 7a of P1800-2009.
In the proposal, the line appears correctly.

As you say, there should be no underscore, but "p" should also be in italic font.

Regards,
Shalom

From: owner-sv-ac@eda.org<mailto:owner-sv-ac@eda.org> [mailto:owner-sv-ac@eda.org]<mailto:[mailto:owner-sv-ac@eda.org]> On Behalf Of Tapan Kapoor
Sent: Tuesday, January 17, 2012 9:50 AM
To: Korchemny, Dmitry; 'sv-ac@eda-stds.org'
Subject: [sv-ac] RE: Draft 4 Review (resend with correction of one more numbering issue pointed by Scott)

Dmitry, all,

I have reviewed Annex F. I could see only one issue.
In section F.3.4.3.8 (Derived unbounded temporal operators), page 1195 -it seems item #3 has a typo:

(p s_until q) $B"a(B ((p_until q) and s_eventually q).

I think $B!H(Bp_until$B!I(B should be replaced with $B!H(Bp until$B!I(B i.e. the $B!F(B_$B!G(B should be removed. This issue existed in the 2009 LRM as well.

Apart from this, rest of the text/changes seem alright to me.

Warm regards,
Tapan
---------------------------------------------------------------------
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<http://www.mailscanner.info/>, and is
believed to be clean.
---------------------------------------------------------------------
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.