Subject: RE: Similarity between ForSpec & E
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Aug 02 2001 - 01:57:00 PDT
Hi Bernard,
Please see my comments bellow.
Roy
> -----Original Message-----
> From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
> Sent: Thursday, August 02, 2001 2:18 AM
> To: vardi@cs.rice.edu
> Cc: vfv@eda.org
> Subject: Re: Similarity between ForSpec & E
>
>
> At 03:40 PM 8/1/2001 +0300, Armoni, Roy wrote:
>
> >However, I second Moshe's
> >opinion that such an end result will be more similar to E
> than to Sugar.
>
>
> At 04:05 AM 8/1/2001 -0500, Moshe Vardi wrote:
>
> > b. The EVENT construct in TemoralE has not been defined
> formally, so
> > I am not sure about its relationship to ForSpec.
>
>
> Moshe,
>
> With the greatest respect, you're clearly an intelligent man
> and much more
> of an expert in this field than me, but surely even from Verisity's
> intuitive description and examples you can't have missed the
> fact that
> "event'" and "temporal e'" are synonymous? In my
> understanding temporal
> 'e' assertions (their expect statements) are totally
> structured around the
> relationship of events so for you guys to be claiming
> possible similarity
> between ForSpec and temporal 'e' surely you *MUST* have a
> good grasp of
> this if only at an intuitive level?
>
> The point I have been trying to make for weeks is 'e' seems
> to be different
> to the other languages because (Yaron, please forgive me if I
> haven't got
> this exactly right!) one way to envisage 'e' is as a series
> of totally
> independent automata, with the 'expect' statement describing the
> relationship of the "satisfaction" of these FSM's. Or, if
> you prefer,
> their 'expect' defines the relationship of the completion
> (tail) of many
> temporal expressions rather than the 'tail' to 'head'
> relationship inherent
> in, for example, ForSpec's "triggers next" implication.
>
> At first I wondered if it was my lack of understanding that
> caused me to
> see differences that didn't exist, but from my email exchange
> with Yaron
> Kashai about mapping between 'e' and other languages I believe he's
> confirmed this opinion. [[Note: this isn't a bad thing
> because you can
> express relationships in 'e' that aren't possible in the
> other languages]]
>
> Of course it could also be that I don't understand events in
> ForSpec, but
> when I look in the 80 or so property examples I cannot find
> any use of the
> 'event' keyword and very limited use of 'change_on' so I
> wonder just how
> important events are to the language except in clocking?
> When I turn to
> the ForSpec Reference Manual on page 17 it very helpfully says that:
>
> "An event is a regular expression r, such that language of r does not
> contain the empty word".
>
> Duh! Even ignoring the probable typo, this is virtually
> useless so perhaps
> an example might have helped?
You were looking at the reference manual. We also have a user's guide that
we did not donate.
>
> Unfortunately I'm not an expert on the notation used in the semantics
> description so I'm not sure what it's trying to tell me, but
> if I rely on
> the English description (lines 4-5 of page 27), it seems to
> imply event
> satisfaction is tied to the start (head) of the event rather
> than the end
> (tail) which is consistent with everything else I've read.
> Also, if I look
> at page 18, it seems as though 'events' can only be used on
> the left side
> of SEQ and TRIGGERS which is quite different from 'e'.
Satisfaction indeed refers to the start of the event. However, for event we
have "tight satisfaction" that refers both to the beginning and the end of
the
event.
Every event is a formula. A formula can appear at the right side of SEQ and
TRIGGERS. Thus, events can appear in both sides.
>
> Forgive me for being blunt, but the heavy focus on events
> within 'e' and
> the discrepancy between 'head' and 'tail' satisfaction is why
> I am finding
> it difficult to see the connection between ForSpec and 'e'.
> And it's why I
> find it hard to imagine how, in Roy's words, "an end result
> [of changes to
> ForSpec] will be more similar to E than to Sugar".
>
> From what I can see these two languages have quite different
> foundations
> but no doubt you will correct my understanding.
Both ForSpec and e are based on linear time.
Temporal e is based on regular expressions which are very similar to the
events of ForSpec.
>
> Regards,
>
> Bernard
> PS - since we are being pedantic about definitions, I'm sure
> you're aware
> you don't define a "regular expression" anywhere in the
> Reference Manual,
> though maybe you assume it's intuitive?
This is one of our arguments. Regular expressions where defined in the 60's
so there is no point in defining them again. One can find the definitions
in
many text books. They are not intuitive - they are simply well defined.
That is
also why ForSpec is robust to changes in the set of operators of the regular
expression because it does not assign them semantics. It assigns semantics
to the languages of finite words resulting of the regular expressions.
>
> ====================================================================
> SDV Inc. 9111 Jollyville Rd, Suite 102, Austin, TX 78759 USA
> Phone: (512) 231-9806 xt 101 FAX: (512) 231-9807
> Mobile: (512)
> 431-5126
> Email: bdeadman@sdvinc.com Website: www.sdvinc.com
>
>
This archive was generated by hypermail 2b28 : Thu Aug 02 2001 - 07:57:20 PDT