Re: [tlaplus] Approaching repeated assignment in PlusCal

[Finn Hackett <fhackett.py@xxxxxxxxx>]

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.

-Finn

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.

H

-- 
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.