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

[Brian Beckman <bc.beckman@xxxxxxxxx>]

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.