Question

Throughout this subsection, s, s1, s2 denote sequences without clocking events; p, p1, p2 denote properties without clocking events; m, m1, m2 denote multiply-clocked sequences, q, q1, q2 denote multiply-clocked properties; and c, c1, c2 denote non-identical clocking event expressions.

Due to clock flow, juxtaposition of two clocks nullifies the first. This and the nesting of clocking events within other property building operators mean that there are subtleties in the general interpretation of the restrictions about where the clock can change in multiply-clocked properties. For example,

@(c) s |-> @(c) (p and @(c1) p1)

appears legal because the antecedent is clocked by c and the consequent begins syntactically with the clocking event @(c). However, the consequent sequence is equivalent to

(@(c) p) and (@(c1) p1)

and |-> cannot synchronize between clock c from the antecedent and clock c1 from the second conjunct of the consequent. Similarly,

@(c) s |-> @(c1) (@(c) p)

appears illegal due to the apparent clock change from c to c1 across |->. However, it is legal, although arguably misleading in style, because the consequent property is equivalent to @(c) p.

This subsection gives a more precise treatment of the restrictions on multiply-clocked use of |-> and if/if...else than the intuitive discussion in Section 17.12. The present treatment depends on the notion of the set of semantic leading clocks for a multiply-clocked sequence or property.

Some sequences and properties have no explicit leading clock event. Their initial clocking event is inherited from an outer clocking event according to the flow of clocking event scope. In this case, the semantic leading clock is said to be inherited. For example, in the property

@(c) s |=> p and @(c1) p1

the semantic leading clock of the subproperty p is inherited since the initial clock of p is the clock that flows

across |=>.

A multiply-clocked sequence has a unique semantic leading clock, defined inductively as follows.

• The semantic leading clock of s is inherited.
• The semantic leading clock of @(c) s is c.
• If inherited is the semantic leading clock of m, then the semantic leading clock of @(c) m is c. Otherwise, the semantic leading clock of @(c) m is equal to the semantic leading clock of m.
• The semantic leading clock of (m) is equal to the semantic leading clock of m.
• The semantic leading clock of m1 ## m2 is equal to the semantic leading clock of m1.

The set of semantic leading clocks of a multiply-clocked property is defined inductively as follows.

• The set of semantic leading clocks of m is {c}, where c is the unique semantic leading clock of m.
• The set of semantic leading clocks of p is {inherited}.
• If inherited is an element of the set of semantic leading clocks of q, then the set of semantic leading clocks of @(c) q is obtained from the set of semantic leading clocks of q by replacing inherited by c. Otherwise, the set of semantic leading clocks of @(c) q is equal to the set of semantic leading clocks of q.
• The set of semantic leading clocks of (q) is equal to the set of semantic leading clocks of q.
• The set of semantic leading clocks of not q is equal to the set of semantic leading clocks of q.
• The set of semantic leading clocks of q1 and q2 is the union of the set of semantic leading clocks of q1 with
• the set of semantic leading clocks of q2.
• The set of semantic leading clocks of q1 or q2 is the union of the set of semantic leading clocks of q1 with the set of semantic leading clocks of q2.
• The set of semantic leading clocks of m |-> p is equal to the set of semantic leading clocks of m.
• The set of semantic leading clocks of m |=> p is equal to the set of semantic leading clocks of m.
• The set of semantic leading clocks of if (b) q is {inherited}.
• The set of semantic leading clocks of if (b) q1 else q2 is {inherited}.
• The set of semantic leading clocks of a property instance is equal to the set of semantic leading clocks of the multiply-clocked property obtained from the body of its declaration by substituting in actual arguments.

For example, the multiply-clocked sequence

@(c1) s1 ## @(c2) s2

has c1 as its unique semantic leading clock, while the multiply-clocked property

not (p1 and (@(c2) p2)

has {inherited, c2} as its set of semantic leading clocks.

In the presence of an incoming outer clock, the inherited semantic leading clock is always understood to refer to the incoming outer clock. On the other hand, if a property has only explicit semantic leading clocks, then the incoming outer clock has no effect on the clocking of the property since the explicit clock events replace the incoming outer clock. Therefore, the clocking of a property q in the presence of incoming outer clock c is equivalent to the clocking of the property @(c) q.

The rules for using multiply-clocked overlapping implication and if/if...else in the presence of an incoming outer clock can now be stated more precisely.

1) Multiply-clocked overlapping implication.

Let c be the incoming outer clock. Then the clocking of m |-> q is equivalent to the clocking of @(c) m |-> q

In the presence of the incoming outer clock, m has a well-defined ending clock, and there is a welldefined clock that flows across |->. The multiply-clocked overlapped implication m |-> q is legal for incoming clock c if and only if the following two conditions are met:

a) Every explicit semantic leading clock of q is identical to the ending clock of m.

b) If inherited is a semantic leading clock of q, then the ending clock of m is equal to the clock that flows across |->.

For example

@(c) s |-> p1 or @(c2) p2

is not legal because the ending clock of the antecedent is c, while the consequent has c2 as an explicit semantic leading clock.

Also,

@(c) s ## (@(c1) s1) |-> p

is not legal because the set of semantic leading clocks of p is {inherited}, the ending clock of the antecedent is c1, and the clock that flows across |-> and is inherited by p is c.

On the other hand,

@(c) s |-> p1 or @(c) p2

and

@(c) s ## @(c1) s1 |-> p1 or @(c1) p2

are both legal.

2) Multiply-clocked if/if...else

Let c be the incoming outer clock. Then the clocking of if (b) q1 [ else q2 ] is equivalent to the clocking

of

@(c) if (b) q1 [ else q2 ]

The boolean condition b is clocked by c, so the multiply-clocked if/if...else if (b) q1 [ else q2 ] is legal for incoming clock c if and only if the following condition is met:

• Every explicit semantic leading clock of q1 [ or q2 ] is identical to c.

For example,

@(c) if (b) p1 else @(c) p2

is legal, but

@(c) if (b) @(c) (p1 and @(c2) p2)

is not.