Hi Andrew,
Perfection is achieved not when there is nothing more to add,
but when there is nothing left to take away.
Saint-Exupery
Except for the proof language, I'm interested in removing things from
TLA+ rather than adding them. In fact, I've stopped mentioning
constructs with free tuples such as {<<x, y>> \in S : p(x, y)},
intending to remove them from the de facto language as a prelude
to possibly removing them from the supported language. I think
{f(x) : x \in {y \in S : p(y)}}
can be expressed well enough with
LET T == {y \in S : p(y)}
IN {f(x) : x \in T}
so there's no need to add the language feature you propose.
----
The _expression_
[distributedData EXCEPT ![node][key] = value]
is already legal TLA+, as are things like
[e EXCEPT ![a].b[c]]
The ability to write such expressions is a major reason that
I prefer EXCEPT to other notations that have been proposed
for writing [e EXCEPT ![a] = b].
----
The main reason for making something a standard module is so its
operators can be implemented in Java. It's fairly easy to write your
own Java implementations of operators in a module. For any module
Foo, you just have to add a file Foo.java to the appropriate
directory. You can look up the java files corresponding to the
current standard modules to see how it's done. Anyone proposing a
standard module should try it out and see how much it speeds
execution. It might be better to modify the Toolbox and TLC to
make it easy to share such modules and their implementations
rather than to grow the set of standard modules.
Leslie