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

*From*: Brian Beckman <bc.beckman@xxxxxxxxx>*Date*: Sat, 13 Feb 2021 07:35:33 -0800 (PST)*References*: <2f63d23e-42ba-4fe4-8f05-325515a18265n@googlegroups.com> <CAM3xQxHjgFkaCC3o7L4gjyCkfoOdZyFzWYDmE8f-GKtQNbEWHg@mail.gmail.com> <58153d24-7b76-470f-8c12-e26a3e68f6d0n@googlegroups.com> <6E838E87-A69C-4991-8071-CD2EA4B1A2AB@gmail.com>

Thank you, Stephan.

Your answer raises a question. "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)."

I believe a "step" is officially defined as "a pair of states." So, given a behavior, a step could be a pair of adjacent or contiguous states, as in (s_i, s_{i+1}), or any pair of states, e.g. (s_i, s_{i+42}). In all examples I've seen, steps are pairs of adjacent states, as in (s_i, s_{i+1}). I think I saw in one of the videos that TLC checks successor state "graph-wise," starting from a state s_i, then constructing a ring outwards from s_i to bunch of candidate s_{i+1} states, then recursively from each candidate s_{+1} state to a bunch more of candidate s_{i+2} states, one out-edge for each action that's enabled in each iteration of that process. Does TLC also check steps from s_i to s_{i+2} etc.?

There is a way to bound this graph-building process, but I forgot where it is in the toolbox.

On Friday, February 12, 2021 at 11:25:05 PM UTC-8 Stephan Merz wrote:

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 considerA == x' = x+1 /\ y' = yB == y' = y+1 /\ x' = xThere are no states s, t such that A /\ B is true of (s, t).StephanOn 13 Feb 2021, at 06:56, Brian Beckman <bc.be...@xxxxxxxxx> wrote:Dear Isaac,Yes, this is super helpful. To be sure I understand the point:In an ordinary state predicate (with no primed variables), an _expression_ A \/ B is true if A is true, B is true, or both are true. That is the ordinary meaning of \/, disjunction, in propositional logic.In an action (function of two adjacent states -- a step -- in a behavior, with primed variables), A \/ B is true if either A is true or B is true, but we never check both. If A is true, we will for sure not check B. If B is true, we will for sure not check A. That lets us write sub-expressions in a Next action without having to negate all the variables other than the few we're concerned about in each sub-action in a disjunction. Do I have that right?If so, that's reminiscent of the short-circuit disjuctions in C, where A || B means (execute A [including side effects]; if A is true, do not execute B; if A is false, execute B [including side effects].Do I have this right? Not to belabour the point, but it seems important. When writing specs, we must know how to write actions that we want to be true or false of a step, and if disjunction means something slightly different pertaining to a single state than it does pertaining to a pair of states, I need to wake up, drink some more coffee, and be sure I know what I'm writing !Hello Brian,Disjunctions in action expressions are interpreted as a nondeterministic choice between the disjuncts. If it were possible for both disjunct actions to happen in the same step, it wouldn’t make sense to write an action _expression_ like:Next == x’ = 0 \/ x’ = 1Next actions like this are very common since, in general, we want to allow different actions that change the same variables.I hope this helps!Best,IsaacOn Fri, Feb 12, 2021 at 9:32 PM Brian Beckman <bc.be...@xxxxxxxxx> wrote:In the video, around 8:58, the Next action is defined asA \/ Bmeaning it's an A step or a B step ... but isn't the case wherethe step is BOTH an A step and a B step allowed by this_expression_?Later, A and B are defined so that A explicitly says BVar' = BVaris unchanged and B says AVar' = AVar is unchenced. So if bothA and B occur in a Next, it amounts to a stuttering step.I just want to make sure I understand----

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2f63d23e-42ba-4fe4-8f05-325515a18265n%40googlegroups.com.Isaac DeFrain--

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/58153d24-7b76-470f-8c12-e26a3e68f6d0n%40googlegroups.com.

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/96d96f7b-4f15-4330-8596-dc73c948d7f1n%40googlegroups.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

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

- 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):