Re: [sv-ac] Clock rewriting rules

Hi Dmitry:

Annex F is, and has been for some time, rather delicate.

I think the whole thing should be rewritten along the lines of
suggested in Mantis 1296.  I would prefer to get rid of the 
clock rewriting rules altogether.

Regarding your particular example,

   @(c) not (Q1 and Q2), where Q1 and Q2 are clocked properties

I do not believe that this can be generated from the abstract
syntax.

J.H.


> X-Authentication-Warning: server.eda-stds.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.16,455,1175497200"; 
>    d="scan'208,217";a="242586865"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Sun, 24 Jun 2007 09:43:49 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] Clock rewriting rules
> Thread-Index: Ace2KwWTFGI6IbYKS4O1FqHIbUqcVQ==
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 24 Jun 2007 06:43:54.0952 (UTC) FILETIME=[08B8B480:01C7B62B]
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-Spam-Status: No, No
> Sender: owner-sv-ac@eda.org
> X-eda.org-MailScanner-Information: Please contact the ISP for more information
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C7B62B.06053F31
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> Hi all,
> 
> =20
> 
> Clock rewriting rules are defined in F.3.1 in the following manner:
> 
> =20
> 
> @(c) not P |-->not @(c) P.
> 
> =20
> 
> (other rules are similar),
> 
> =20
> 
> which reads: when the clocking event c is applied to 'not P', where P is
> an unclocked property, the resulting property is equivalent to not @(c)
> P.
> 
> =20
> 
> Now let's say that we have the following formula: @(c) not (Q1 and Q2),
> where Q1 and Q2 are clocked properties. Then, strictly speaking, no
> rewriting rule can be applied, since the above rewriting rule requires
> that Q1 and Q2 were unclocked.
> 
> =20
> 
> I think that a cleaner way would be to define the rewriting rules using
> a special notation for rewriting transformation as done in PSL:
> 
> =20
> 
> RW(@(c) not Q) =3D not RW(@(c) Q)
> 
> =20
> 
> Note that Q here is a clocked property.
> 
> =20
> 
> What do you think?
> 
> =20
> 
> Thanks,
> 
> Dmitry
> 
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.