Re: [tlaplus] Composing multiple instances of a clock specification

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!

On Wednesday, May 27, 2020 at 3:46:45 AM UTC-3, Stephan Merz wrote:

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

On 27 May 2020, at 08:13, JosEdu Solsona <josedu...@xxxxxxxxx> wrote:

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.

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/837b0340-ae10-4762-afa3-0a428bdfbd7a%40googlegroups.com.