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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Mon, 30 Oct 2023 22:56:01 -0500*References*: <52e0b930-3891-4228-85cc-691e12b68eabn@googlegroups.com>*User-agent*: Mozilla Thunderbird

IIRC the following is TLC-checkable:

`~[]<><<write>>_vars => \A n, o \in Node:
state[n] = state[o]`

Where `<<A>>_v `is `A /\ ~UNCHANGED v`.

H

On 10/30/2023 5:01 PM, Andrew Helwer
wrote:

--I'm modeling a simple eventually-consistent system. In general, eventually-consistent systems will eventually converge when writes stop happening. In my system, I model this with a variable called converge that is arbitrarily set to TRUE at some point which keeps further writes from happening, so I can write a simple liveness property like:

Liveness == converge ~> \A n, o \in Node : state[n] = state[o]

This is simple and fine and works well. However, it's a bit weird to keep an entire variable around just for this purpose. Is it possible to write a temporal formula that says "if a write step is never taken, then eventually the system converges"? Something like:

Liveness == []~[write]_vars ~> \A n, o \in Node : state[n] = state[o]

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/52e0b930-3891-4228-85cc-691e12b68eabn%40googlegroups.com.

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/2c21811e-0658-44a7-a105-5da8ad0e1212%40gmail.com.

**References**:**[tlaplus] Writing temporal formula predicated on step not being taken***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Why does liveness checking take so much longer with strong fairness?** - Next by Date:
**[tlaplus] Filtering set of records** - Previous by thread:
**[tlaplus] Writing temporal formula predicated on step not being taken** - Next by thread:
**[tlaplus] Why does liveness checking take so much longer with strong fairness?** - Index(es):