Subject: [sv-ac] Re: flaw in Sugar clocked until semantics
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Oct 24 2002 - 12:24:04 PDT
Cindy:
> the small caveat is as follows: all semantics in weak context need to
> be prefixed with "for all i in [0..|w|) such that
> w^{0,i} |=3D {!c[*];c}". this takes care of the case that there are no
> clocks at all, which is the basic difference between strong and weak
> operators.
This seems to suggest that you want the following to hold:
a) If there does not exist i >= 0 such that w^{0,i} |= {!c[*];c}, then
w |=(c) f.
And if the strong/weak semantics are appropriately symmetric, I would
then expect:
b) If w |=(c!) f, then there exists i >= 0 such that w^{0,i} |= {!c[*];c}.
However, both a) and b) are foiled by the definitions
w |=(c!) f@c1 iff w |=(c1) f
w |=(c) f@c1! iff w |=(c1!) f
This is closely related to the problem David Van Campenhout has observed with
the semantics of &&.
Assuming that you want a) to hold, and presumably b) as well, then something
has to be changed in the definitions for weakly- and strongly-clocked f@c1
and f@c1!.
Best regards,
John H.
This archive was generated by hypermail 2b28 : Thu Oct 24 2002 - 12:25:01 PDT