FW: [sv-ac] LTL 1932

 

I upload to Mantis an updated proposal

 

Thanks

 

Doron

 

________________________________

From: Bresticker, Shalom 
Sent: Sunday, October 07, 2007 9:30 AM
To: Bustan, Doron
Subject: RE: [sv-ac] LTL 1932

 

s_always

s_next

s_until

s_until_with

until_with

	 

	
________________________________


	From: Bustan, Doron 
	Sent: Sunday, October 07, 2007 9:25 AM
	To: Bresticker, Shalom
	Subject: RE: [sv-ac] LTL 1932

	I do have :

	 

	Table B1-Reserved keywords

	Note to editor: add the following keywords to Table B1

	eventually

	implies

	next

	s_eventually

	strong

	until

	weak

	 

	anything else?

	 

	
________________________________


	From: Bresticker, Shalom 
	Sent: Sunday, October 07, 2007 8:33 AM
	To: Bustan, Doron; sv-ac@server.eda-stds.org
	Subject: RE: [sv-ac] LTL 1932

	 

	Doron,

	 

	The proposal adds a bunch of new keywords that are not listed in
the changes to Annex B.

	 

	Regards,

	Shalom

		 

		
________________________________


		From: owner-sv-ac@server.eda.org
[mailto:owner-sv-ac@server.eda.org] On Behalf Of Bustan, Doron
		Sent: Sunday, October 07, 2007 8:28 AM
		To: sv-ac@server.eda-stds.org
		Subject: [sv-ac] LTL 1932

		Hi,

		 

		I 

		1.	Replaced next[range] with eventually[range] 
		2.	Add example for weak sequential property under
not. 
		3.	Change the definition for vacuity for weak
sequential properties and until. I find it hard to get a good definition
for until so I wrote a very conservative one that will not give
unnecessarily false negatives. 

		 

		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
<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.