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
/\ (hr \in [Clock -> 1 .. 12])
/\ \A c \in Clock : C!Spec(hr[c])
or, in a form suitable for TLC,
/\ \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.
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.