Subject: Naming
From: Yaron Wolfsthal (WOLFSTAL@il.ibm.com)
Date: Tue Nov 20 2001 - 09:45:00 PST
Moshe
It is a common practice that a name of a language is coined by the
body/person who designed it.
For example, the committee referes to Intel's contribution by the names
*ForSpec 1.0* or *ForSpec 2.0*.
Similarly, please use the names *Sugar* or *Sugar Foundation Language* for
IBM's contribution. There is no need for extra creativity here.
-Yaron
Moshe Vardi <vardi@cs.rice.edu>@eda.org on 20/11/2001 18:34:42
Please respond to Moshe Vardi <vardi@cs.rice.edu>
Sent by: owner-vfv@eda.org
To: Cindy Eisner/Haifa/IBM@IBMIL, vardi@cs.rice.edu
cc: harry@verplex.com, vfv@eda.org
Subject: Re: sugar: case-by-case analysis of accellera requirements
> >attributing to [1] the claim of "no change in semantics for
> >the vast majority of properties used in practice" is a misattribution.
> >Maidl says nothing of that sort. All she does is characterize the
> >properties that are in the intersection of LTL and ACTL.
>
> as i am sure is clear to anyone who has been following this discussion, i
> never claimed that [1] discusses anything other than ltl and ctl.
Which means that it says nothing about the relationship between OldSugar
and NewSugar.
>
> >Suerly, however, you are not syaing that there is no practical
> >impact for implementors of the language.
>
> indeed there is an impact for the implementors. both ltl and ctl model
> checkers will have to implement a check whether or not a formula coded
with
> the other formalism is in the common fragment. if so, then the formula
can
> be checked in "native mode", by ignoring quantifiers or the lack of them,
> respectively. if it turns out that the formula is not in the common
> fragment, then the ltl model checker can give an error that it does not
> support the optional branching extension. the ctl model checker can use
> tableau construction, without the need to change its core algorithms.
1. We do not know how to decide if the path quantifiers of a NewSugar
formula can be deleted. Maidl's work applies only to LTL and ACTL.
2. Your earlier description of the model checking algorithm for NewSugar
said nothing about a tableau construction.
Moshe
This archive was generated by hypermail 2b28 : Tue Nov 20 2001 - 09:58:36 PST