I often find myself wanting to both map and filter at the same time, which requires the following somewhat cumbersome expression:
I think this would be much improved in readability if we had a language-level construct similar to:
This is similar to set comprehensions in Python, which is probably my favorite feature of that language.
EXCEPT support for nested functions
Many of the specs I write are of distributed systems, so I'll usually have one or more variables of this type:
When I want to update a single value in distributedData, I use this notation:
It would be nicer if we could write it something like this:
I recall this also as a common point of confusion among TLA+ course attendees, who intuitively tried this notation at first.
I'm not sure whether either of these suggestions violate some bedrock principle in the TLA+ construction (I could see that for the latter) but they certainly would both make my life simpler and reduce the cognitive overhead of reading/writing TLA+.
New standard module: Query
Not a fully fleshed-out idea, but it might be nice to have a new standard module that implements something like relational algebra for easy manipulation of sets of records, in addition to other common higher-level functions like fold and zip.
Anyone else have suggestions of their own?
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