Subject: Re: Sugar - Complexity Question
From: Hillel Miller (hillelm@msil.sps.mot.com)
Date: Sun Jul 08 2001 - 08:45:38 PDT
Roy,
Other things that are of concern are :
How the user uses the assume/guarantee ?
How the user is taught to use assume/guarantee ?
Why is the general assertion approach better than the
restrict(Sugar)/constraint(CBV)+
DFSM approach ?
What debugging capabilities exist ?
How this works in the dynamic world ?
Regards,
Hillel
"Armoni, Roy" wrote:
> Hi Hillel,
>
> Since the issue of assume/guarantee is so important, I plan to
> write a short manuscript that will explain all the details of how
> assume/guarantee is supported in ForSpec. It will also contain
> a description of some artifact of the assume/guarantee paradigm
> that I discussed in private with the IBM people and Cindy asked me
> to explain to the committee. It will take me a few days though
> because I am leaving on a business trip tomorrow morning - hope
> to be able to complete it during the long flights :)
>
> At this point, I can answer some of the assumptions that you make
> below:
> 1) No, we do not agree that converting an assertion to an
> assumption requires determinism. Actually, if you follow the
> so called "tableau construction" of LTL, you realize that the
> assertions are those that require negation, but the assumptions
> are compiled as they are. There are more than one approach to
> tableau construction, some of them require to bring the formula
> first to negation-normal-form(NNF) and some do not. Note that at
> any rate, FTL is closed under negation, and it is possible to
> bring every FTL formula to NNF, thus allowing both approaches to
> tableau construction.
>
> 2) Having said that, we also do not agree that assuming FTL
> formulas is sometimes not practical - there is no difference
> between assuming and asserting an FTL formula. I will answer
> this issue while discussing complexity in my manuscript, but
> the short answer is that model-checking of an FTL formula (either
> assumed or asserted) is in PSPACE if time windows are not used,
> and since time windows are logarithmic notation, then with time
> windows the problem is in EXPSPACE (actually, maybe even in ESPACE,
> but I have to check this point).
>
> 3) I believe that since your assumptions about assume/guarantee
> in ForSpec are not correct, the answer to the rest of your
> questions is obvious. There is nothing special in the tools that
> identifies practical properties to be used as assumptions. I
> will repeat the mantra: every FTL property can be used as an
> assumption (and as an assertion). The answer is in the careful
> design of the language, and that makes our users happy rather than
> frustrated.
>
> Stay tuned for the full answer :)
>
> Regards, Roy
>
> -----Original Message-----
> From: Hillel Miller [mailto:hillelm@msil.sps.mot.com]
> Sent: Thursday, July 05, 2001 7:11 PM
> To: Moshe Vardi
> Cc: eisner@il.ibm.com; Edmund.Clarke@cs.cmu.edu; Sudhir_Kadkade@sifr.com;
> Vassilios.Gerousis@infineon.com; arif@synopsys.com; avner.landver@intel.com;
> axels@cadence.com; badru@athdl.com; bdeadman@sdvinc.com;
> cbrowy@avery-design.com; coelho@verplex.com; dana@wisdom.weizmann.ac.il;
> danaf@il.ibm.com; davidg@synopsys.com; dudani@synopsys.com; emc@cs.cmu.edu;
> erichm@cadence.com; fitz@co-design.com; flake@co-design.com;
> foster@rsn.hp.com; geist@il.ibm.com; gkhoory@synopsys.com;
> jbhasker@cadence.com; johne@verplex.com; kchen@verplex.com;
> limor.fix@intel.com; mac@verisity.com; matthew@verisity.com;
> michael.siegel@mchp.siemens.de; pixley@adttx.sps.mot.com;
> prakash@realintent.com; roy.armoni@intel.com; shoham@il.ibm.com;
> skshukla@ics.uci.edu; smeier@synopsys.com; swamiv@synopsys.com;
> tla@0-in.com; wolfstal@il.ibm.com; yaron@verisity.com; ychsu@novas.com;
> zhong@innologic-systems.com
> Subject: Re: Sugar - Complexity Question
>
> Moshe, Roy
>
> Could you please explain in detail the user model with Forspec as to the
> assume/gurantee
> paradigm ?
>
> I think we agree that converting an assertion to an assumption requires
> determinism.
> I think we also agree that this is sometimes not practical.
>
> What is unique about ForSpec that makes this practical ?
> Is it the fact that your tools know how to identify such assertions that
> can
> be converted ? If this is the case, then a user may spend hours writing an
>
> assertion to discover on invocation that this is not feasable for an
> environment ?
> Will this not frustrate the user ?
>
> Hillel
>
> Moshe Vardi wrote:
>
> > But you could have "(r1 && r2, r3)[*],r4", so you cannot determinize in
> > advance.
> >
> > It is known that universality of SERE is EXPSPACE-complete, so I doubt
> > that you'll be able to beat that lower bound.
> >
> > Moshe
This archive was generated by hypermail 2b28 : Sun Jul 08 2001 - 08:46:31 PDT