Subject: RE: Sugar with clocks
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Jul 19 2001 - 09:42:08 PDT
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 bring something 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 with clocks
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 : Thu Jul 19 2001 - 09:43:47 PDT