Verification Guild
A Community of Verification Professionals

 Create an AccountHome | Calendar | Downloads | FAQ | Links | Site Admin | Your Account  

Login
Nickname

Password

Security Code: Security Code
Type Security Code
BACKWARD

Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name.

Modules
· Home
· Downloads
· FAQ
· Feedback
· Recommend Us
· Web Links
· Your Account

Advertising

Who's Online
There are currently, 39 guest(s) and 0 member(s) that are online.

You are Anonymous user. You can register for free by clicking here

  
Verification Guild: Forums

 Forum FAQForum FAQ   SearchSearch   UsergroupsUsergroups   ProfileProfile  ProfileDigest    Log inLog in 

Implementing PSL

 
This forum is locked: you cannot post, reply to, or edit topics.   This topic is locked: you cannot edit posts or make replies.    Verification Guild Forum Index -> Assertions
View previous topic :: View next topic  
Author Message
tomahawkins
Senior
Senior


Joined: Mar 23, 2004
Posts: 29

PostPosted: Fri Oct 22, 2004 9:23 pm    Post subject: Implementing PSL Reply with quote

Hello,

I'm working on a verification tool that I plan to release under GPL soon. Among other languages, it will support PSL.

At this point I'm having difficulty developing the PSL parser. I started working from the grammar in the spec, but I soon realized it was meant to convey semantics rather than to be an LR(1) friendly grammar. Their are a few spots that are ambiguous to yacc.
For example:

Code:
  Property     ::= FL_Property | OBE_Property
  FL_Property  ::= Boolean     | FL_Property  AND_OP FL_Property
  OBE_Property ::= Boolean     | OBE_Property AND_OP OBE_Property


Given these rules,the expression (a && b) could reduce from FL_Property, OBE_Property, or Boolean.

Is there a reference parser available? I remember IBM open-sourced their Sugar parser a few years back, but it seems they pulled it from their website.

Any suggestions on how to structure the grammar to eliminate the ambiguities? I did consider making everything an expression (booleans, seres, properties) then resolve the types later; but still ran into yacc ambiguities.

-Tom
Back to top
View user's profile Visit poster's website
cindy
Industry Expert
Industry Expert


Joined: Aug 17, 2004
Posts: 309

PostPosted: Sun Oct 24, 2004 4:54 am    Post subject: Reply with quote

tom,

Quote:
Is there a reference parser available? I remember IBM open-sourced their Sugar parser a few years back, but it seems they pulled it from their website.


the sugar parser is still available from ibm at:

http://www.haifa.il.ibm.com/projects/verification/sugar/parser.html

while sugar and psl are not identical, it should be a good starting point.

cindy.
Back to top
View user's profile
tomahawkins
Senior
Senior


Joined: Mar 23, 2004
Posts: 29

PostPosted: Sun Oct 24, 2004 9:43 am    Post subject: Reply with quote

Quote:

the sugar parser is still available from ibm at:

http://www.haifa.il.ibm.com/projects/verification/sugar/parser.html

while sugar and psl are not identical, it should be a good starting point.


The link is still there, but it seems the parser has been moved into a restricted area. I get a promt for a username and password at https://mrtgsrv.haifa.il.ibm.com.

-Tom
Back to top
View user's profile Visit poster's website
cindy
Industry Expert
Industry Expert


Joined: Aug 17, 2004
Posts: 309

PostPosted: Sun Oct 24, 2004 9:51 am    Post subject: Reply with quote

tom,

Quote:
The link is still there, but it seems the parser has been moved into a restricted area. I get a promt for a username and password at https://mrtgsrv.haifa.il.ibm.com.


it is supposed to work. i will investigate and get back to you.

cindy.
Back to top
View user's profile
cindy
Industry Expert
Industry Expert


Joined: Aug 17, 2004
Posts: 309

PostPosted: Mon Oct 25, 2004 8:19 am    Post subject: Reply with quote

a quick update: we have identified the source of the problem, but are waiting for our web admin to fix it. i'll let you know as soon as it is done.

cindy.
Back to top
View user's profile
cindy
Industry Expert
Industry Expert


Joined: Aug 17, 2004
Posts: 309

PostPosted: Thu Oct 28, 2004 3:52 am    Post subject: Reply with quote

the problems with the download of the sugar parser from:

http://www.haifa.il.ibm.com/projects/verification/sugar/parser.html

have been fixed.

enjoy,

cindy.
Back to top
View user's profile
Display posts from previous:   
This forum is locked: you cannot post, reply to, or edit topics.   This topic is locked: you cannot edit posts or make replies.    Verification Guild Forum Index -> Assertions All times are GMT - 5 Hours
Page 1 of 1

 
Jump to:  
You can post new topics in this forum
You can reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
Verification Guild © 2006 Janick Bergeron
Web site engine's code is Copyright © 2003 by PHP-Nuke. All Rights Reserved. PHP-Nuke is Free Software released under the GNU/GPL license.
Page Generation: 0.145 Seconds