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.