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

[tlaplus] Writing temporal formula predicated on step not being taken

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.