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

[mryndzionek@xxxxxxxxx]

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.