[tlaplus] Modeling leases

["A. Jesse Jiryu Davis" <jesse@xxxxxxxxxxxxxxx>]

Hello! Murat Demirbas and I are designing a Raft variant that uses timed leader leases for stronger consistency. We plan to write a TLA+ spec, and it will involve clocks. We're interested in examples in addition to Lamport's "Real Time Is Really Simple" paper. Has anyone worked with time/clocks in TLA+, or could you point us to example specs?

-- 
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/CAFRUCtYYwU8mrQ_3mNqb%2BCYd5xK1ObUuFBRENv34WXMFjFrYNw%40mail.gmail.com.