Re: [tlaplus] Re: How do you do functions of structures?

[Aaron Elligsen <aaron@xxxxxxxxxxxxxx>]

The ALIAS feature looks pretty great. I think that could ease a lot of pain related to destructuring. 

I'm not really happy with the explanations so far though. I see a lot of experienced TLA+ user chiming in that destructuring works better currently, and from experience I believe it, but I don't see an explanation of why it should be this way. It seems to me an arbitrary fact that new spec writers must learn and then code around to improve spec performance and aesthetics.

TLA+ has both the syntax for records, and it can handle multiple updates to the record using the || operator, so it's not like the spec must be written without using them. In the end it just seems like record update syntax is sort of second class and so specifications work better when omitting it. I feel like it betrays the principle that TLA+ is math, like why is one representation not as good as another?

On Monday, June 7, 2021 at 10:38:28 AM UTC-7 Markus Alexander Kuppe wrote:

On 07.06.21 06:52, Andrew Helwer wrote:
> Plus the state traces are much easier to read.


The new-ish ALIAS feature of TLC [1] addresses this problem (one less
reason to write specs that work well with the various tools).

Markus

[1] https://github.com/tlaplus/tlaplus/issues/485

-- 
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/333f8258-b3a9-478f-a50c-143c9368dfd1n%40googlegroups.com.