Re: [tlaplus] Modeling leases

I've now read the TLA+ spec but I haven't tried to model-check it yet. The spec uses infinite sets such as Int and Nat, it doesn't constrain these to finite sets and it doesn't use the techniques described in Lamport's "Real Time Is Really Simple" to make the state space finite. I don't think spec could be model-checked with TLC. Is this a demonstration of Apalache's advantages over TLC?

On Tue, Feb 27, 2024 at 9:23 AM A. Jesse Jiryu Davis <jesse@xxxxxxxxxxxxxxx> wrote:

Thank you!

On Tue, Feb 27, 2024 at 8:22 AM Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
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.