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

*From*: Andrew Helwer <andrew...@xxxxxxxxx>*Date*: Sat, 7 Apr 2018 10:20:28 -0700 (PDT)

TLA+ as a language is pretty much perfect, but there are a couple scenarios where I wish for additional language constructs/features:

**Combined set-builder notation**

When defining a set with set-builder notation, we have two options:

- Mapping: {f(x) : x \in S}
- Filtering: {x \in S : p(x)}

I often find myself wanting to both map and filter at the same time, which requires the following somewhat cumbersome _expression_:

- Map & Filter: {f(x) : x \in {y \in S : p(y)}}

I think this would be much improved in readability if we had a language-level construct similar to:

- Combined: {f(x) : x \in S WHERE p(x)}

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:

- distributedData \in [Node -> [Key -> Value]]

When I want to update a single value in distributedData, I use this notation:

- distributedData' = [distributedData EXCEPT ![node] = [@ EXCEPT ![key] = value]]

It would be nicer if we could write it something like this:

- distributedData' = [distributedData EXCEPT ![node][key] = value]

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?

**Follow-Ups**:**Re: Possible new language constructs for TLA+3?***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Fairness condition for messages** - Next by Date:
**Re: Possible new language constructs for TLA+3?** - Previous by thread:
**TLC model checking RealTime module: problem with variable now** - Next by thread:
**Re: Possible new language constructs for TLA+3?** - Index(es):