[sv-ac] Clock rewriting rules

Hi all,

 

Clock rewriting rules are defined in F.3.1 in the following manner:

 

@(c) not P |-->not @(c) P.

 

(other rules are similar),

 

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.

 

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.

 

I think that a cleaner way would be to define the rewriting rules using
a special notation for rewriting transformation as done in PSL:

 

RW(@(c) not Q) = not RW(@(c) Q)

 

Note that Q here is a clocked property.

 

What do you think?

 

Thanks,

Dmitry


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