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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 27 May 2020 08:46:39 +0200*References*: <837b0340-ae10-4762-afa3-0a428bdfbd7a@googlegroups.com>

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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/E46A7913-D473-4058-8AC3-3158353CC898%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Composing multiple instances of a clock specification***From:*JosEdu Solsona

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

- Prev by Date:
**[tlaplus] Composing multiple instances of a clock specification** - Next by Date:
**Re: [tlaplus] Composing multiple instances of a clock specification** - Previous by thread:
**[tlaplus] Composing multiple instances of a clock specification** - Next by thread:
**Re: [tlaplus] Composing multiple instances of a clock specification** - Index(es):