Thanks Stephan, it does make more sense when I break it down in each direction and try to think of a counterexample but then realize it is covered under vacuous truth. Will chew on these some more.AndrewOn Monday, November 18, 2024 at 9:51:45 AM UTC-5 Stephan Merz wrote:Hi Andrew,you can convince yourself that both of the following are true for any actions A and B (I am dropping the subscript for simplicity):(1) If ~((ENABLED A) /\ (ENABLED B)), i.e. the actions cannot be simultaneously enabled, then WF(A \/ B) => WF(A) /\ WF(B).(2) If both (ENABLED A) /\ ~A /\ ~B => (ENABLED A)’ and (ENABLED B) /\ ~A /\ ~B => (ENABLED B’), i.e. only the occurrence of one of the actions may disable each of them, then WF(A) /\ WF(B) => WF(A \/ B).In the context of a "multiprocess program described with pseudo-code", the actions Ai of interest are those associated with each label of a fixed process p in the pseudo-code. This is basically the situation of a PlusCal algorithm, where each such action is described as a conjunction including the predicate pc[p] = i. This implies that the condition of (1) above holds true and thereforeWF(Next(p)) => \A i \in I : WF(Ai(p))For the converse implication, we have to show each subaction of process p can only be disabled by the occurrence of a step of process p. This is certainly true if the enabledness condition only depends on local variables of the process. However, if it may also depend on global variables, this will not generally be true. For example, a semaphore that synchronizes access of different processes to their critical sections could be taken by a different process, disabling process p. It is not clear to me if a sufficiently strong restriction holds for the algorithms alluded to in this part of the book, or if it is really the equivalence, and not just implication, that is required.StephanOn 17 Nov 2024, at 20:05, Andrew Helwer <andrew...@xxxxxxxxx> wrote:I am having some trouble understanding equation 4.13 on page 94; quoting:The first thing we observe is that for a multiprocess program described with pseudocode, weak fairness of a process’s next-state action is equivalent to the conjunction of weak fairness of all the actions described by the process’s statements. That is, if PNext(p) equals ∃i ∈ I :Ai(p) for a set I, where action Ai(p) describes the statement with label i, and v is the tuple of program variables, then:
(4.13) |= WFv (PNext(p)) ≡ ∀ i ∈ I : WFv (Ai (p))
I've always thought that weak fairness of a disjunct of various actions is different from a conjunct of weak fairness of those disjuncts; consider an action like:Next ==\/ A\/ B\/ CThen WF(Next) means that if one of A, B, and C are enabled continuously (they can swap off) then a Next step must eventually be taken. However, I feel that's different from WF(A) /\ WF(B) /\ WF(C), which states that if those specific actions are continuously enabled then they will eventually be taken.What might be at the root of my confusion is the assumption "for a multiprocess program described with pseudocode" since perhaps that restricts the actions we are considering; in my example with Next being the disjunction of A, B, and C, they can only swap off being enabled without themselves being taken if some other non-Next action is changing the variable state. Perhaps this hypothetical is ruled out by the assumption that we're talking about a multiprocess program described with pseudocode, and while it's true that 4.13 doesn't hold in general it does hold in this case.Andrew Helwer--
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...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4d8538b1-7c45-4660-92c0-1576b144363cn%40googlegroups.com.