Re: Group A - first draft LRM changes

Hi Erich,

I have a comment below on your

> 4. Correct the informal semantics of '@' to allow for a nested subelement that has a different clock context.
>
> - in Clause 6.1.2.5, Clocked SERE, change the informal semantics to read
> as follows: "For unclocked SERE A and Boolean CLK: A@CLK holds tightly
> on a given path iff CLK holds in the last cycle of the given path, and
> A holds tightly on the path obtained by extracting the from the given
> path exactly those cycles in which CLK holds, and any subordinate
> sequences of A hold tightly as specified by A on the corresponding
> sub-paths of the given path."
>
> - in clause 6.2.1.2, Clocked FL properties, change the informal
> semantics to read as follows: "For unclocked FL property A and Boolean
> CLK: A@CLK holds on a given path iff A holds on the path obtained by
> extracting from the given path exactly those cycles in which CLK
> holds, and any subordinate properties of A hold as specified by A at
> the corresponding cycles of the given path."
>
> [Note: I'm not happy with this yet, but this is the best I've been able
> to do so far.]
>

Note that there is not only a problem with nested clocked subproperties
here. Also nested aborts break the clock projection hypothesis. For
instance the property

((always a) abort b)@c is true in the following situation (because it is
equivalent to (always a)@c abort b.)

c:0101010...
a:0100000...
b:0010000...

whereas

((always a) abort b) is not true in

a:100...
b:000...

which is the path obtained when extracting from the given path those
cycles in which c holds.

It seems this problem with abort and clock projection is not noted
in the current informal semantics in 6.2.1.2 either.

Best Regards, Johan M.

--
------------------------------------------------------------
Johan Martensson, PhD            Office: +46 31 7451913    	
R&D                              Mobile: +46 703749681
Safelogic AB                     Fax: +46 31 7451939
Arvid Hedvalls Backe 4           johan.martensson@safelogic.se
SE-411 33 Gothenburg, SWEDEN 
PGP key ID A8857A60
www.safelogic.se
------------------------------------------------------------