Re: [tlaplus] Modeling leases

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Hi Jesse,

I used Apalache to check a clock synchronization algorithm a few years
ago. You can have a look at the TLA+ specification [1] and the talk
from the TLA+ Tutorial 2021 [2].

[1] https://github.com/informalsystems/tla-apalache-workshop/blob/main/examples/clock-sync/ClockSync7.tla
[2] https://youtu.be/NXLJoUKJnDQ?t=5821

Best,
Igor

On Mon, Feb 26, 2024 at 1:18 AM A. Jesse Jiryu Davis
<jesse@xxxxxxxxxxxxxxx> wrote:
>
> 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.

-- 
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/CACooHMAmhdEOAXfnvd1y_5q-CfuG3dg%3Dc5wOm-MC5HQjorE%3D7w%40mail.gmail.com.