Re: [tlaplus] Approaching repeated assignment in PlusCal

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.

Markus

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