Subject: RE: two remaining questions
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Dec 13 2001 - 01:31:59 PST
Hi Erich,
One more point to add is that for some reason, Sugar did not allow negation
over
"{sere}(formula)". Sugar FL allows that. This is also not a restriction,
and allowing
that is actually a key point in the proof of omega-regularity.
Roy
-----Original Message-----
From: Armoni, Roy
Sent: Thursday, December 13, 2001 11:26 AM
To: 'Erich Marschner'; vfv@eda.org
Subject: RE: two remaining questions
Hi Erich,
Please allow me to try and clarify what Moshe is saying and correct your
inaccurate
statement below.
A syntactic restriction could not possibly increase the expressive power of
Sugar!
The reason I agree that Sugar FL has an omega regular power is because of
the semantic
change between Sugar and Sugar FL. One needs to read the documents
carefully to observe
that change. If I remember correctly, Cindy agrees that there is also a
change in the
semantics; she only claims that this change cannot be observed in the
properties document.
I would also like to add that I welcome the direction that Sugar is taking.
Regards,
Roy
-----Original Message-----
From: Erich Marschner [mailto:erichm@cadence.com]
Sent: Thursday, December 13, 2001 8:10 AM
To: vardi@cs.rice.edu; owner-vfv@eda.org; vfv@eda.org
Subject: Re: two remaining questions
Moshe,
Thank you for pointing out my misunderstanding.
For the record, what I 'misunderstand' is this: a syntactic restriction to
Sugar, removing path quantifiers, which reduces the number of operators
somewhat, also aligns Sugar FL with the LTL semantics that you have argued
so convincingly are to be preferred, and has increased the power of the
language, making it omega-regular where it was not before. In particular,
I note that Roy finally agreed with Cindy that "Sugar FL has the power to
express any omega regular language".
It appears to me that this restriction of Sugar to Sugar FL gives us a
smaller yet more useful and more powerful language. To me, that sounds
like the definition of 'elegance' in language design.
Regards,
Erich
At 10:58 PM 12/12/2001, Moshe Vardi wrote:
>Erich, you misunderstood the IBM proposal. Repackaged Sugar is not a
>restriction of Sugar, is a significant extension.
>
>Moshe
>Cc: +fv
>
> > and Verisity what restrictions they plan to make. I applaud IBM's
> > restriction of Sugar via defining the Sugar Foundation Language (which,
> > especially if you factor out the 'syntactic sugar' definitions, seems
> to be
> > quite compact indeed); I'd like to see a similar commitment to
> restricting,
> > or at least limiting the growth of, the other proposed languages.
> >
> > Regards,
> >
> > Erich
> >
> >
> >
> > -------------------------------------------
> > Erich Marschner, Cadence Design Systems
> > Senior Architect, Advanced Verification
> > Phone: +1 410 750 6995 Email: erichm@cadence.com
> > Vmail: +1 410 872 4369 Email: erichm@home.com
> >
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@home.com
This archive was generated by hypermail 2b28 : Thu Dec 13 2001 - 01:33:48 PST