Composing multiple instances of a clock specification

[JosEdu Solsona]

Hello all,

Currently researching module composition on TLA+. 

Suppose we have a parametrized Clock specification like the one we see in Lamport's Specifying Systems:

-------------- MODULE Clock ------------------

INSTANCE TLC
INSTANCE Naturals

Init(h) == h \in 1..12
Next(h) == h' = IF h # 12 THEN h + 1 ELSE 1
Spec(h) == Init(h) /\ [][Next(h)]_h /\ WF_h(Next(h))

=============================================

Now, say i want to compose two clocks outside:

---------------------- MODULE OtherPlace --------------------------------

C == INSTANCE Clock

VARIABLES x, y

\* Composing two clocks
TwoClocks1 == C!Spec(x) /\ C!Spec(y)

\* The same as before but in "canonical form", so TLC can understand it
TwoClocks2 == /\ C!Init(x) /\ C!Init(y)
              /\ [][ \/ C!Next(x) /\ C!Next(y)
                     \/ C!Next(x) /\ y' = y
                     \/ C!Next(y) /\ x' = x
                   ]_<<x,y>>
              /\ WF_x(C!Next(x)) /\ WF_y(C!Next(y))
======================================================================

Now there are two (independent) clocks as a no-interleaving specification. 

For interleaving we can get ride of the  C!Next(x) /\ C!Next(y) action.

But suppose i want an arbitrary number of clocks. The book have an example with an array of clocks. 

I will try to reproduce something similar here:

---------------------- MODULE OtherPlace --------------------------------

C == INSTANCE Clock

CONSTANT N
ASSUME N \in Nat

Clock == 1..N

VARIABLES hr   \* supposed to be in [c \in Clock |-> 1..12]

\* Composing every clock in the array
AnyClocks1 == \A c \in Clock : C!Spec(hr[c])      

\* This should be the same as before but in "canonical form", so TLC can understand it
AnyClocks2 == /\ \A c \in Clock : C!Init(hr[c])
              /\ [][ \/ \E i,j \in Clock : i # j /\ C!Next(hr[i]) /\ C!Next(hr[j])
                     \/ \E c \in Clock : C!Next(hr[c]) /\ \A i \in Clock\{c} : hr[i]' = hr[i]
                   ]_<<hr>>
======================================================================

This fails on TLC with "hr is undefined". Even if we state it is a function on the initial predicate, 

and state hr[c]' for every c is not enough, it looks like we cant guarantee hr will be a function forever.

This is addressed in the book with a couple of suggestions. 

Currently to make this work i need to redefine the clock specification, for example with:

CNext(c) == hr' = [hr EXCEPT ![c]= IF hr[c] # 12 THEN hr[c] + 1 ELSE 1]

However, i think this will force an interleaving specification because is saying only one component will change, 

so the first action in the Next disjunction cant be taken. So i guess this can be a solution for interleaving.

I cant redefine it like

CNext(c) == hr[c]' = IF hr[c] # 12 THEN hr[c] + 1 ELSE 1

because it causes the same problem that "hr is undefined".

But... i dont really want to redefine the clock specification to make this work. I would like to use the Clock module as it is,

just like in the two clocks version. Is this possible?.

Thanks.

[Stephan Merz]

Hello,

I recall that Leslie at some point wrote a note about exactly the issue that you mention, but I don't seem to be able to find it on the TLA Web site.

In essence the problem is that writing something like

(1)  \A x \in S : f[x] = e

is weaker than writing

(2)  f = [x \in S |-> e]

because (1) doesn't tell us that the domain of f is S, or in fact that f is a function. You can strengthen (2) by writing

(3) f \in [S -> T] /\ \A x \in S : f[x] = e

for some suitable set T. Applying this line of thought to your clock specification you could write

AnyClocks1 ==

  /\ [](hr \in [Clock -> 1 .. 12])

  /\ \A c \in Clock : C!Spec(hr[c])

or, in a form suitable for TLC,

AnyClocks2 == 

  /\ \A c \in Clock : (hr \in [Clock -> 1 .. 12]) /\ C!Init(hr[c])
  /\ [][ /\ hr' \in [Clock -> 1 .. 12]

         /\ \A c \in Clock : [C!Next(hr[c])]_<<hr[c]>>

       ]_<<hr>>

and these are perfectly fine TLA+ specifications. The downside is that TLC will enumerate the set of all functions of the given shape and then filter out those that satisfy the initial and next-state conditions, so this approach will not scale for TLC. (It's not an issue when you write proofs using TLAPS.)

If I recall correctly, Leslie's conclusion was that it wasn't worth composing components in this way but better to start with a specification of an array of components in the first place.

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/837b0340-ae10-4762-afa3-0a428bdfbd7a%40googlegroups.com.

[JosEdu Solsona]

Hello Stephan,

Oh, i also tried to force  hr \in [Clock -> 1 .. 12]   inside the Next action... but now i see without the prime operator was not making any difference. I didn't notice that.

Now hr' \in [Clock -> 1 .. 12] did the trick. 

Thanks!

Hello,

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.