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

*From*: JosEdu Solsona <josedusolsona@xxxxxxxxx>*Date*: Wed, 27 May 2020 07:19:13 -0700 (PDT)*References*: <837b0340-ae10-4762-afa3-0a428bdfbd7a@googlegroups.com> <E46A7913-D473-4058-8AC3-3158353CC898@gmail.com>

Hello Stephan,

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

-- 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] = 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])]_<<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.StephanOn 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 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 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.

**References**:**[tlaplus] Composing multiple instances of a clock specification***From:*JosEdu Solsona

**Re: [tlaplus] Composing multiple instances of a clock specification***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Composing multiple instances of a clock specification** - Next by Date:
**[tlaplus] Specification for tic-tac-toe in PlusCal** - Previous by thread:
**Re: [tlaplus] Composing multiple instances of a clock specification** - Next by thread:
**[tlaplus] Specification for tic-tac-toe in PlusCal** - Index(es):