Lecture 9, part 1, Alternating-Bit Protocol

[Brian Beckman]

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

[Isaac DeFrain]

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

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

--

Isaac DeFrain

[Brian Beckman]

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 !

[Stephan Merz]

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

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

[Brian Beckman]

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.

[Brian Beckman]

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

[Leslie Lamport]

If I say

  She can join the team if she is good on offense or on defense.

do you think I'm saying that she can't join the team if she is good
on both offense and defense?  In informal text, whether "or" means
"and/or" or "or ... but not both" depends on the context.  In this

context, since A \/ B is true if A /\ B is true, it means "and/or".
In a mathematical context, "or" almost always means "and/or".

Leslie 

[Isaac DeFrain]

Brian,

Stephan and Leslie certainly gave much better answers than I. The right way to think about an action is as a predicate on pairs of states. I, personally, find it helpful to think of disjunctions in action expressions as a nondeterministic choice (like that from process calculi), but this is only a heuristic. I should've been more clear about that. My apologies.

TLC uses a short-circuited semantics for boolean expressions which you can verify yourself by evaluating expressions like:

  /\ FALSE

  /\ PrintT("this will not be displayed")

and

  \/ TRUE

  \/ PrintT("this will not be displayed")

Thanks for the great questions and starting a nice discussion.

Best,

Isaac DeFrain

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

[ns]

I may not be adding much to the discussion but I understood many TLA+ constructs a lot better when I realized that they are making assertions about traces. So A \/ B will accept a trace if the step it applies to conforms to A or B. Similarly \E x. A accepts those traces for which the corresponding step has a value of x such that A holds.