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

[mryndzionek@xxxxxxxxx]

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/0241147f-8be1-42ac-86b4-a04f45fbe612%40googlegroups.com.