An invariant that checks if all the possible steps lead to the same final state

[mrynd...@gmail.com]

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.

[mrynd...@gmail.com]

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?