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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 6 Sep 2020 09:14:07 +0200*References*: <734edefa-87e0-4f29-8cb4-f3d0e71c5672n@googlegroups.com>

Hello, TLA+ actions describe atomic transitions, and this excludes the first option that you mention: 1. Define a refinement mapping that somehow shows that, e.g., 1 state transition of the implementation that unblocks N processes, is equivalent to N state transitions in the API spec where the transitions unblock processes one by one. The sequence of N transitions contains (visible) states that do not exist in the execution having a single transition. Therefore refinement simply does not hold. I'd recommend that your specification fully embrace the fact that several transitions may occur. In your toy example, you could do so by writing EXTENDS Integers VARIABLES s Init == s = [i \in 1..2 |-> 0] Inc(S) == s' = [i \in 1..2 |-> IF i \in S THEN s[i]+1 ELSE s[i]] Next == \E S \in SUBSET (1..2) : Inc(S) In a more realistic example, you'd replace s[i]+1 by an operator that computes the result of the operation that the action represents, based on the current state. Regards, Stephan
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/10548514-4F31-45A5-B28E-47CD6103E566%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Artificial coupling of variables***From:*Jedd Haberstro

**References**:**[tlaplus] Artificial coupling of variables***From:*Jedd Haberstro

- Prev by Date:
**[tlaplus] Artificial coupling of variables** - Next by Date:
**Re: [tlaplus] Artificial coupling of variables** - Previous by thread:
**[tlaplus] Artificial coupling of variables** - Next by thread:
**Re: [tlaplus] Artificial coupling of variables** - Index(es):