[sv-ac] clock rules

Hi John,

 

 I think I understand your point.

 

The solution should be another inductive function 

 

- Flow s(@(c) b) =  c.

- Flow s(@(c) (1, v = e)) = c.

- Flow s(@(c1) (@(c2) S)) =  c2.

- Flow s(@(c) (S1 ##1 S2)) =  Flow(@(Flow(@(c)S1))S2).

- Flow s(@(c) (S1 ##0 S2)) = Flow(@(Flow(@(c)S1))S2). 

- Flow s(@(c) (S1 or S2)) = if Flow(@(c)S1)=Flow(@(c)s2) then
Flow(@(c)S1) otherwise 0 .

- Flow s(@(c) (S1 intersect S2)) = if Flow(@(c)S1)=Flow(@(c)s2) then
Flow(@(c)S1) otherwise 0.

- Flow s(@(c) (first match S)) = Flow(@(c)S).

- Flow s(@(c) (S[*0])) = c.

-      Flow s(@(c) (S[*1:$])) = Flow(@(c)S).

 

Then, 

-      T p(@(c) (S |-> Q) = (T s(@(c) S) |-> T p(@(Flow(@c(S)) Q)).

 

With the restriction that Flow(@c(S)) is the only leading clock of Q
(either because of inheritance or explicitly set) 

 

Doron


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