Subject: Re: Vacations & Clocks
From: Dana Fisman (dana@wisdom.weizmann.ac.il)
Date: Wed Aug 01 2001 - 10:17:43 PDT
Hi Roy,
Attached is the definition of Sugar clocked formulas.
Enjoy,
Dana.
On Tue, 31 Jul 2001, Yaron Wolfsthal wrote:
>
> Cindy is on vacation.. expect a response from another Sugar team member
> tomorrow or tomorrow+1.
> -Y
>
> "Armoni, Roy" <roy.armoni@intel.com> on 30/07/2001 21:56:56
>
> Please respond to "Armoni, Roy" <roy.armoni@intel.com>
>
> To: Cindy Eisner/Haifa/IBM@IBMIL
> cc: vfv@eda.org
> Subject: FW: Sugar with clocks
>
>
>
>
> Hi Cindy,
>
> Did you managed to fix the definition of clocks in Sugar?
>
> Regards, Roy
>
>
> -----Original Message-----
> From: Armoni, Roy [mailto:roy.armoni@intel.com]
> Sent: Thursday, July 19, 2001 7:42 PM
> To: Cindy Eisner
> Cc: vfv@eda.org
> Subject: RE: Sugar with clocks
>
>
> Hi Cindy,
>
> Since you have not brought a fix to Sugar clocks' semantics to Paris, could
> you please
> try to make it before the next meeting?
>
> Thanks, Roy
>
>
> -----Original Message-----
> From: Cindy Eisner [mailto:EISNER@il.ibm.com]
> Sent: Sunday, July 15, 2001 11:04 AM
> To: Tiemeyer, Andreas
> Cc: Paul Muench; ""Tiemeyer@d12relay01.de.ibm.com; Andreas"
> <andreas.tiemeyer; ""Armoni@d12relay01.de.ibm.com; Roy" <roy.armoni;
> "Bernard Deadman " <bdeadman; ""Carl. Pixley (E-mail)" <carl.pixley"; "Dvc
> "
> <dvc; ""Fix@d12relay01.de.ibm.com; Limor" <limor.fix; "Foster " <foster;
> "Hillelm " <hillelm; Shoham Ben-David; "Yaron " <yaron; dana;
> DanaFisman/Haifa/Contr/IBM@d12relay01.de.ibm.com
> Subject: RE: Sugar with clocks
>
>
> andreas,
>
> sorry, this completely slipped my mind. the fix is simple, but i do not
> want to do it in a rush and make a mistake (i leave for the airport in an
> hour). dana and i will try to bringsomething to the meeting in paris.
>
> regards,
>
> cindy.
>
> Cindy Eisner
> Formal Methods Group Tel: +972-4-8296-266
> IBM Haifa Research Laboratory Fax: +972-4-855-0070
> Haifa 31905, Israel e-mail:
> eisner@il.ibm.com
>
>
> "Tiemeyer, Andreas" <andreas.tiemeyer@intel.com> on 13/07/2001 02:56:11
>
> Please respond to "Tiemeyer, Andreas" <andreas.tiemeyer@intel.com>
>
> To: Paul Muench/San Jose/IBM@IBMUS, "Tiemeyer, Andreas"
> <andreas.tiemeyer@intel.com>
> cc: "Armoni, Roy" <roy.armoni@intel.com>, "Bernard Deadman (E-mail)"
> <bdeadman@attglobal.net>, "Carl. Pixley (E-mail)"
> <carl.pixley@mot.com>, Cindy Eisner/Haifa/IBM@IBMIL, "Dvc (E-mail)"
> <dvc@verisity.com>, "Fix, Limor" <limor.fix@intel.com>, "Foster
> (E-mail)" <foster@rsn.hp.com>, "Hillelm (E-mail)"
> <hillelm@msil.sps.mot.com>, Shoham Ben-David/Haifa/IBM@IBMIL, "Yaron
> (E-mail)" <yaron@verisity.com>
> Subject: RE: Sugar withclocks
>
>
>
>
> Hi Cindy,
>
> I'd like to follow up on this issue. You mentioned below that you are
> planning to change the semantics for clocked sugar to bring it more in line
> with the intuition for existential formulas. Would you know when we can
> expect to get the revised semantics ?
>
> Thanks,
>
> Andreas
>
> Andreas Tiemeyer
> Formal Specification Technologies Group
> Intel (UK), Pipers Way, Swindon SN1 1JW
> Tel +44 1793 404103
>
>
> > -----Original Message-----
> > From: Cindy Eisner [mailto:pmuench@us.ibm.com]
> > Sent: 13 June 2001 08:34
> > To: Tiemeyer, Andreas
> > Cc: vfv; Dana Fisman
> > Subject: Re: Sugar with clocks
> >
> >
> >
> > andreas,
> >
> > thanks for your very good questions.
> >
> > >Firstly, I did not see a definition for clocks applied to
> > the |=> and |=>!
> > >operator. That's probably because it can be rewritten in
> > terms of other
> > >operators for which clocks are defined, but I couldn't
> > figure out exactly
> > >how. Could you help?
> >
> > please see the document submitted to ovi titled "the syntax
> > and semantics
> > of sugar". (there were two documents submitted, one informal and one
> > formal. this is the formal document.) section 4.3 describes
> > |=> and |=>!.
> >
> > >Provided that I haven't made any technical mistakes I would like to
> > >understand why the current definition of clocks was chosen,
> > and not one
> > >that, as mentioned above, rewrites existential formulas into
> > existential
> > >formulas.
> >
> > you are correct that the formal definition as supplied is
> > problematical for
> > existential formulas. the answer is that this was an oversight. most
> > sugar formulas in practice are of the form "AG f", where f is either a
> > univeral or an existential formula. the use of next_event
> > was chosen to
> > work for these types of formulas. we should (and will)
> > update the formal
> > definition to make more sense for formulas whose outermost operator is
> > existential.
> >
> > regards,
> >
> > cindy.
> >
> > Cindy Eisner
> > Formal Methods Group Tel:
> > +972-4-8296-266
> > IBM Haifa Research Laboratory Fax: +972-4-855-0070
> > Haifa 31905, Israel e-mail:
> > eisner@il.ibm.com
> >
> >
>
>
>
>
>
>
>
This archive was generated by hypermail 2b28 : Wed Aug 01 2001 - 10:24:20 PDT