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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 10 Mar 2019 09:25:14 +0100*References*: <15ade3f5-b044-4796-95dd-4d22c10963dc@googlegroups.com> <e4e19ec7-36c4-b22d-96d7-7a9a9ac6183a@gmail.com> <CAFRUCtYr2CwMZV3F6pR9OnrYCx4RZa1dN1=U9PsjEw57r9i0LQ@mail.gmail.com> <d27a6a2e-a198-40c0-ae52-f7df432a1fa1@googlegroups.com>

Hello, as you observed, both your fairness conditions ensure that the property that you are interested in holds, but they do so for quite different reasons. The first condition, which I'll write equivalently as UnivFairSpec == /\ Spec /\ \A self \in ProcSet : SF_vars(RETRY_BEGIN(self) /\ pc'[self] = "RETRY_SUCCEED")
-- asserts that every process that infinitely may succeed (i.e., move from BEGIN to SUCCEED) will succeed eventually. The second condition, ExistFairSpec == /\ Spec /\ SF_vars(\E self \in ProcSet : RETRY_BEGIN(self) /\ pc'[self] = "RETRY_SUCCEED") asserts that if infinitely often some process may succeed, then eventually some process will. The two conditions are equivalent for your spec because processes that succeed terminate. In particular, the first process that succeeds will never move back to BEGIN. Now, the second process will continue looping and must therefore eventually succeed. (And clearly the "universal" condition implies the "existential" one.) In order to make this more concrete, consider the variant below of your algorithm, where a process restarts after having succeeded. For this variant, the expected correctness property would be that both processes succeed infinitely often: EveryProcessSucceeds == \A self \in ProcSet : []<>(succeeded[self]) You will see that this property holds with the "universal" fairness hypothesis, but not with the "existential" one, and TLC generates a counter-example where only one of the processes succeeds infinitely often. Regards, Stephan (*--algorithm retry_example variables \* Both processes have not yet succeeded. succeeded = [p \in 1..NumProcesses |-> FALSE]; define all_succeeded == \A p \in 1..NumProcesses: succeeded[p] end define; fair process retry_example \in 1..NumProcesses begin RETRY_BEGIN: either RETRY_SUCCEED: succeeded[self] := TRUE; or RETRY_ERROR: goto RETRY_BEGIN; end either; RESTART: succeeded[self] := FALSE; goto RETRY_BEGIN; end process; end algorithm *)
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

**Follow-Ups**:**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

**References**:**[tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*Hillel Wayne

**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?***From:*A. Jesse Jiryu Davis

- Prev by Date:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Next by Date:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Previous by thread:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Next by thread:
**Re: [tlaplus] How to test a process eventually succeeds after indefinite number of retries?** - Index(es):