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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 18 May 2020 18:16:30 +0200*References*: <e0db34df-ba74-4af3-8298-6642628e0be4@googlegroups.com>

Hello,
is what you want to write, for the reasons that you give (I'm assuming that N is a constant). Note that this formula is equivalent to \A i \in 1 .. N : []<>(pc[i] = "Done") and that, as long as processes remain at "Done" when they reach it (as in PlusCal), the latter can be further simplified to \A i \in 1 .. N : <>(pc[i] = "Done") Regards, 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/EACF9909-D913-4DD3-A3B0-5F602B3FB066%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Writing a liveness check for multiple processes***From:*tlabonte

- Prev by Date:
**[tlaplus] Writing a liveness check for multiple processes** - Next by Date:
**Re: [tlaplus] Writing a liveness check for multiple processes** - Previous by thread:
**[tlaplus] Writing a liveness check for multiple processes** - Next by thread:
**Re: [tlaplus] Writing a liveness check for multiple processes** - Index(es):