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

Re: [tlaplus] Approaching repeated assignment in PlusCal

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 Wed, Dec 9, 2020 at 5:45 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:

On 12/9/2020 6:12 PM, Finn Hackett wrote:
My 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 blow-up.

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.