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

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

 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] = eis 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] = efor some suitable set T. Applying this line of thought to your clock specification you could writeAnyClocks1 ==  /\ [](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])]_<>       ]_<
>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.StephanOn 27 May 2020, at 08:13, JosEdu Solsona 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 TLCINSTANCE NaturalsInit(h) == h \in 1..12 Next(h) == h' = IF h # 12 THEN h + 1 ELSE 1Spec(h) == Init(h) /\ [][Next(h)]_h /\ WF_h(Next(h))=============================================Now, say i want to compose two clocks outside:---------------------- MODULE OtherPlace --------------------------------C == INSTANCE ClockVARIABLES x, y \* Composing two clocks TwoClocks1 == C!Spec(x) /\ C!Spec(y)\* The same as before but in "canonical form", so TLC can understand itTwoClocks2 == /\ 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 --------------------------------C == INSTANCE ClockCONSTANT NASSUME N \in NatClock == 1..NVARIABLES hr   \* supposed to be in [c \in Clock |-> 1..12]\* Composing every clock in the arrayAnyClocks1 == \A c \in Clock : C!Spec(hr[c])       \* This should be the same as before but in "canonical form", so TLC can understand itAnyClocks2 == /\ \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 likeCNext(c) == hr[c]' = IF hr[c] # 12 THEN hr[c] + 1 ELSE 1because 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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. 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/E46A7913-D473-4058-8AC3-3158353CC898%40gmail.com.