[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Approaching repeated assignment in PlusCal
- From: Finn Hackett <fhackett.py@xxxxxxxxx>
- Date: Thu, 10 Dec 2020 09:30:01 -0800
- References: <CAJs285kRCQAH6JRsNGk5=tSOd==hcxqWELz1czii66CNgYPNZQ@mail.gmail.com> <email@example.com>
Thanks for the note Hillel. That's interesting, as I had previously skipped that section of the TLA+ book thinking it was about something else.
Apparently I was the only one to receive your comment, so hopefully this pushes it back into the publicly visible responses.
Thanks to the others for your thoughts as well.
On 12/9/2020 6:12 PM, Finn Hackett
question, then: can anyone think of better (automatable) ways to
simulate multiple intra-action assignments to the same variable?
Would there be a TLC/toolbox feature that could help with this
kind of thing? For instance, in the dummy state variable version,
it would make a big difference if we had a way to selectively drop
some state variable from the state space, preventing space
I believe you can do this by passing a custom VIEW into
TLC. The model checker will only consider states distinct if they
have different VIEWs. This use case is covered in pages
243-244 of Specifying Systems.
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/CAJs285kBvTr9dnt1MCVHOwKqiVKg6c98N8HGcEyMxrW0boyFPA%40mail.gmail.com.