# Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol

Oh, never mind. I see "a step is a pair of successive states" on page 16 of the book.

On Saturday, February 13, 2021 at 7:35:33 AM UTC-8 Brian Beckman wrote:
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 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

On 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 !

On Friday, February 12, 2021 at 9:04:06 PM UTC-8 isaacd...@gmail.com wrote:
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’ = 1

Next 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,

Isaac

On 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 as

A \/ B

meaning it's an A step or a B step ... but isn't the case where
the 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' = BVar
is unchanged and B says AVar' = AVar is unchenced. So if both
A 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.