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

[tlaplus] Re: An invariant that checks if all the possible steps lead to the same final state

A small update. To concretize what I mean, here is an example spec I want to check: https://github.com/mryndzionek/tlaplus_specs/blob/devel/Requirements.tla
Also I had a revelation :) after reading Hillel Wayne's blog post on HYPERMODELING HYPERPROPERTIES and
I've come up with this spec: https://github.com/mryndzionek/tlaplus_specs/blob/devel/CheckRequirements.tla
Are there any improvements possible? It seems to do what I want, but maybe there is another way? 

W dniu czwartek, 16 stycznia 2020 08:47:03 UTC+1 użytkownik mrynd...@xxxxxxxxx napisał:
As in the subject. More context is that I have some requirements encoded as separate actions
and multiple actions are allowed only if they have the same final state.
I would like to check this in one invariant formula. Is this expressible in TLA+?
Any of the available action operators seems to apply to my case.

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/148ed081-28a2-45cc-920f-6b3c99e470cb%40googlegroups.com.