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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 6 Jul 2021 08:34:31 +0200*Ironport-hdrordr*: A9a23:HyFfJq2v5ZcqiDUEN67rmQqjBGgkLtp133Aq2lEZdPU1SL3kqynKpp8mPHDP6Ar4JBob6LS90cW7Lk8036QFgrX5RI3SOTUO4VHYTr2KjrGP/9SfIUDDH7VmpMBdmsFFYbXN5DBB5/oSizPYLz9P+re6Ge+T9J7jJ2AEd3ANV0n6hD0JcjpyMidNNXJ77QBTLuvn2vZ6*References*: <932afbd1-f11a-4be3-a69a-ac1289ad7e11n@googlegroups.com>

Hello, requiring strong fairness for the branch1 action won't help because the non-deterministic decision of which branch to enter is taken earlier (at the "either" statement labeled "example"). This is one of the cases where the intended fairness condition has to be expressed in TLA+. You probably want to write something like /\ SF_vars(example /\ pc' = [pc EXCEPT !["test"] = "branch1"]) /\ SF_vars(example /\ pc' = [pc EXCEPT !["test"] = "branch2"]) in order to express that both branches will be taken infinitely often if execution arrives infinitely often at the "either" statement. Hope this helps, Stephan
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/12016527-CCB4-422F-965E-0D71CA237511%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Fairness and either statement***From:*Hillel Wayne

**References**:**[tlaplus] Fairness and either statement***From:*p.to...@xxxxxxxxxxxxxxxxx

- Prev by Date:
**Re: [tlaplus] Re: Is the latex source for specifying systems available? Or any other version of the published pdf file?** - Next by Date:
**Re: [tlaplus] Re: Is the latex source for specifying systems available? Or any other version of the published pdf file?** - Previous by thread:
**[tlaplus] Fairness and either statement** - Next by thread:
**Re: [tlaplus] Fairness and either statement** - Index(es):