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

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

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

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.