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

[Isaac DeFrain <isaacdefrain@xxxxxxxxx>]

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.beckman@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+unsubscribe@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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxHjgFkaCC3o7L4gjyCkfoOdZyFzWYDmE8f-GKtQNbEWHg%40mail.gmail.com.