What is the || operator?
With regard to the mathiness of it all, I'd say that's actually more like the source of this problem: the EXCEPT syntax is clunky, but necessary since you have to fully define the value of each variable in a next-state relation. Still, I guess you could do it a different way; consider:
VARIABLE me
Person == [name : STRING, age : Nat]
HaveBirthday ==
/\ me' \in Person
/\ me'.age = me.age + 1
I think that would uniquely define the value of me' right? Kind of strange to think about how that could be implemented in the tools though.
Andrew
On Monday, June 7, 2021 at 6:11:38 PM UTC-4 Aaron Elligsen wrote:
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