Re: [tlaplus] How to determine an Action execution.

[Stephan Merz <stepha...@xxxxxxxxx>]

TLA+ actions are defined "extensionally" by formulas evaluated over pairs of states. If two action formulas A and B are equivalent, then so are WF_v(A) and WF_v(B), and any execution satisfying one of these formulas also satisfies the other one. There is no "intensional" notion of actions that would differentiate between two equivalent action formulas.

If the distinction is important, for example for identifying the server executing the action, you will have to make the distinction explicit in your specification, for example by including the server identity as a parameter of the action.

Regards,
Stephan


> On 8 Nov 2018, at 15:30, apostolis.xe...@xxxxxxxxx wrote:
> 
> Consider the case that we have two actions which are identical, they have the same conditions for triggering them and the same restrictions on the "next" step in case we don't have stuttering.
> 
> From what I understand, any fairness properties on action A will also be inherited by action B. In other words, either both actions are triggered or none.
> 
> Which means that from a meta-theoretic point of view, you can not attach a specific action to a specific entity, like a program, or a specific server etc.
> 
> -- 
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.