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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 12 Apr 2024 08:26:22 +0200*References*: <CA+t=SiJW9BskRavnF3Yu6=TUqJx2kBrvqEZfH6YMYko8-o-91g@mail.gmail.com> <CAL9hw25iQdZZRU7K+xAgQvemiSaJZP5dsv1VrMzy0T+Eh3x-YQ@mail.gmail.com> <EC54437A-BE72-4A65-9D78-AD9EB44C0103@gmail.com> <CA+t=SiLgdUymrXhZk-JSY3tzyk9ZQGmh5s8tg7dhqJYdUaaaDA@mail.gmail.com>

The proposed formula is equivalent to ([]<> wire_requests = << >>) => []<> TransferComplete If wire_requests is never empty (or in fact, empty only finitely often), the property holds vacuously. 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/16485DA4-558A-49AF-A33F-99F47F009DF8%40gmail.com. |

**References**:**[tlaplus] Liveness check with at least once message delivery***From:*jayaprabhakar k

**Re: [tlaplus] Liveness check with at least once message delivery***From:*divyanshu ranjan

**Re: [tlaplus] Liveness check with at least once message delivery***From:*Stephan Merz

**Re: [tlaplus] Liveness check with at least once message delivery***From:*jayaprabhakar k

- Prev by Date:
**Re: [tlaplus] Liveness check with at least once message delivery** - Next by Date:
**[tlaplus] MC file naming convention?** - Previous by thread:
**Re: [tlaplus] Liveness check with at least once message delivery** - Next by thread:
**[tlaplus] MC file naming convention?** - Index(es):