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

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

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.