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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 13 Feb 2021 08:24:58 +0100*References*: <2f63d23e-42ba-4fe4-8f05-325515a18265n@googlegroups.com> <CAM3xQxHjgFkaCC3o7L4gjyCkfoOdZyFzWYDmE8f-GKtQNbEWHg@mail.gmail.com> <58153d24-7b76-470f-8c12-e26a3e68f6d0n@googlegroups.com>

The \/ of TLA+ is ordinary disjunction: an action A \/ B is true for two states if A is true or if B is true, including the case where both A and B are true. TLC will decompose this and check A and B separately. However, remember that given a state s, action A may be true for several pairs (s, t) of states, and TLC will compute all successor states t such that A holds of (s, t). These will in particular include all states t such that A /\ B is true for (s, t), hence there is no need to check for this case separately. In practice, it rarely happens that actions "overlap". For example consider A == x' = x+1 /\ y' = y B == y' = y+1 /\ x' = x There are no states s, t such that A /\ B is true of (s, t). 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/6E838E87-A69C-4991-8071-CD2EA4B1A2AB%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol***From:*Brian Beckman

**References**:**[tlaplus] Lecture 9, part 1, Alternating-Bit Protocol***From:*Brian Beckman

**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol***From:*Isaac DeFrain

**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol***From:*Brian Beckman

- Prev by Date:
**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol** - Next by Date:
**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol** - Previous by thread:
**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol** - Next by thread:
**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol** - Index(es):