Subject: Sugar subtle semantic changes
From: Armoni, Roy (roy.armoni@intel.com)
Date: Tue Nov 20 2001 - 08:13:30 PST
Hi Cindy,
For me, I am convinced now that the Sugar FL has the power to express any
omega
regular language. However, I am still pretty sure that the original
donation of Sugar to
Accellera does not have this capability.
More importantly, it seems that exactly the same operators used in the proof
for omega
regularity in Sugar FL, exist also in the original Sugar, but the proof does
not hold there!
So the "repackaging" is not only a plain separation. It involves some
subtle changes in
the semantics, let alone the additional X, U and G operators.
Regards,
Roy
-----Original Message-----
From: Cindy Eisner [mailto:EISNER@il.ibm.com]
Sent: Tuesday, November 20, 2001 3:16 PM
To: vardi@cs.rice.edu
Cc: roy.armoni@intel.com; harry@verplex.com; vfv@eda.org
Subject: RE: Accellera VFV November 14 Meeting Minutes
moshe,
>I don't see how you got:
>
>>such languages can be expressed by disjunctions of formulae of the form
>>(({true} |-> {e_1}) \ wedge ({e_1} |-> {e_2})), where both e_1 and e_2
>>are seres.
indeed, i should have used strong sere implication, so it should be:
(({true} |-> {e_1}!) \ wedge ({e_1} |-> {e_2}!))
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 : Tue Nov 20 2001 - 08:31:03 PST