[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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. 


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

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]>>

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.


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 ------------------


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 --------------------------------


, 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
/\ 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 --------------------------------


\in Nat

Clock == 1..N

\* 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]

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?.


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.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fe3028c3-5be7-4456-882c-64df8772efd9%40googlegroups.com.