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

Re: [tlaplus] Approaching repeated assignment in PlusCal

On 10.12.20 09:30, Finn Hackett wrote:
I believe you can do this by passing a custom VIEW into TLC. The model checker will only consider states distinct if they have differentVIEWs. This use case is covered in pages 243-244 of /Specifying Systems./

Another angel on (view) symmetry can be found in https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-30.pdf page 38ff.


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/037ec466-721e-eb40-b240-6c26d712c216%40lemmster.de.