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

On 8 Jun 2021, at 00:43, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

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'.name = me.name
    /\ 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.

that definition indeed uniquely defines the value of me'. TLAPS has no problem with it (assuming that me \in Person). TLC can handle it provided you override the definition of Person by a finite set that TLC can enumerate, but is slow due to the explicit enumeration that TLC implements. I believe that Apalache and ProB would handle it just fine because they rely on constraint solving.

Stephan

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

--
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/0633552b-769b-425a-84da-09a8c44a2b45n%40googlegroups.com.