[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol
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...@xxxxxxxxx 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
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/58153d24-7b76-470f-8c12-e26a3e68f6d0n%40googlegroups.com.